Re: [Haskell-cafe] Use distributivity proof in a simple example

Adam Gundry writes:

-- Now it's easy to define wrap wrap :: DF xs -> DF (Map [] xs) wrap Empty = Empty wrap (Single a) = Single [ a ] wrap (Cons x y) = case mapDist (toSingleton x) y of Refl -> Cons (wrap x) (wrap y)

Am I right in thinking that you can also use case unsafeCoerce Refl `asTypeOf` mapDist (toSingleton x) of .. to get the same proof, but without any runtime cost? It seems like this might be a nice middle ground. Of course there is a risk that the proof is just wrong, in which case things could awry. Maybe another option is to switch that line with -XCPP macros depending on whether or not you're in "production" mode. - Ollie