On Mon, Mar 4, 2013 at 4:24 AM, Simon Peyton-Jones
| λ> data a :~: b where Refl :: a :~: a | λ> :t gcast Refl | gcast Refl :: forall a b. (Typeable a, Typeable b) => Maybe ((:~:) * | a b)
That is a ferociously-unintuitive use of 'gcast'! It too me dome while to convince myself that it was right. Though it does indeed work. I'd see (gcast Refl) as the primitive, with 'gcast' itself as a simple derived function.
I'm not sure what name to give the new cast function ?? :: Typeable a, Typeable b) => Maybe (a :~: b)
Do we need gcast1 and gcast2 any more, in our new polykinded world? Can they be depreceated?
Simon
A couple of people have suggested "same". (I wonder if this would also subsume eqSingNat/eqSingSym?). By the way -- since (:~:) seems to be in HEAD now, but not yet released, is there a chance of renaming it? ":~:" is pretty awkward to type, given all the new TypeOperators options these days; how about "=="? Shachaf