new-typeable, new cast?

[Shachaf Ben-Kiki]

On Mon, Mar 4, 2013 at 4:24 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> |     λ> 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