Informing Haskell that `(Reverse (Reverse xs)) ~ xs`

Question

If Reverse :: [k] -> [k] is a type family then Haskell cannot tell that (Reverse (Reverse xs)) ~ xs. Is there a way to let the type system know this without any runtime cost?

I'm tempted to just use unsafeCoerce, but that seems a shame.

Answer 1

The only way that I know of to influence the behavior of ~ in GHC is to actually construct an instance of a :~: b (or similar; the important thing is to construct a term that "proves" this to the typechecker) and then pattern match on the Refl constructor, which would require evaluating the proof witness at runtime. My understanding is that the current design for dependent types in GHC is still going to require running all proofs of type equality. However, one could use GHC's rewrite rules to, after typechecking, replace the proof witness with a very low-cost function (e.g. unsafeCoerce Refl :: Reverse (Reverse a) :~: a), which would make the evaluation very low cost, but still safe (since the proof witness has already typechecked, showing that if it terminates, it will produce a correct proof).

Lots more information about the current state of dependent typing in Haskell can be found here: https://typesandkinds.wordpress.com/2016/07/24/dependent-types-in-haskell-progress-report/