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