(This lesson requires GHC 9.0 or newer.)
In this video about implementing reverse for dependently-typed vectors it is mentioned that type equality proofs involving singletons are executed at runtime, and in fact can be costly to compute.
The solution proposed in the video is employing a combination of RULES and NOINLINE to "coerce" the proofs to Refl instead of running them.
This lesson proposes an alternative solution: create a module signature for the proofs, and then provide two implementations: one with actual proofs (used during tests), and another with "coerced proofs" (used in the executable).
The Vec datatype is defined in module Lesson10 of the main library, and it depends on the Lesson10.Proofs module signature. Therefore the main library is indefinite. Both the executable and the test suite depend on the library, and the they also depend, respectively, on the sub-libraries proofs-coerced and proofs.
One potential disadvantage of this solution is that we might actually forget to compile the version with the non-coerced proofs!
Run the executable with:
cabal run lesson10-coercing-proofs:exe:lesson10
Run the tests with:
cabal test lesson10-coercing-proofs:test:tests
This comment on Reddit.