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

[Oliver Charles]

Adam Gundry <adam at well-typed.com> 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