Data.Type.Equality and coercions

[Richard Eisenberg]

I've noticed two infelicities with the Data.Type.Equality module that I added this summer (according to this proposal: http://ghc.haskell.org/trac/ghc/wiki/TypeLevelReasoning)  For those of you unfamiliar, the key definition is this:

> data a :=: b where
>   Refl :: a :=: a

This is essentially just like (~), but in * instead of Constraint.

1. There is a function
> coerce :: (a :=: b) -> a -> b

This function conflicts with the new function of the same name in the Coercible class (defined in GHC.Prim), with the type
> coerce :: Coercible a b => a -> b

So, these functions are very similar. The first uses explicit nominal equality, while the second uses implicit representational equality. Neither quite subsumes the other.

(Disclaimer: I may or may not have named both of these myself, albeit separated by several months. If I did, sorry for creating this problem.)

My slight inclination: rename the Coercible version to `coerceRep`, as it really is doing a runtime coercion, as opposed to `coerce`. But, I'm quite happy for someone else to have a better idea.


2. There is a useful function that should be added to Data.Type.Equality:

> gcoerce :: (a :=: b) -> ((a ~ b) => r) -> r
> gcoerce Refl x = x

For an example of this in action, see https://gist.github.com/goldfirere/6902431, which is related to #8423 but can be read standalone.

I don't think that gcoerce can subsume coerce because they have different type inference implications. In particular, the types of the coercion in `coerce` can improve the type of the equality witness, whereas this is not possible in `gcoerce`. 

Discussion time: 1 week.

Thanks!
Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131009/0bbf2622/attachment.html>