new-typeable, new cast?

[Shachaf Ben-Kiki]

On Sun, Mar 3, 2013 at 11:43 PM, Shachaf Ben-Kiki <shachaf at gmail.com> wrote
> Any of these lets you write any of the other ones, of course. But
> "cast" doesn't let you write any of them, because it only goes in one
> direction.

Note: It turns out this isn't actually true, since Is can derive Typeable:

λ> data Is :: * -> * -> * where Refl :: Is a a deriving Typeable
λ> let cast' :: forall a b. (Typeable a, Typeable b) => Maybe (Is a
b); cast' = cast (Refl :: Is a a)

It probably still makes sense to provide an equality witness in a less
roundabout way, though.

    Shachaf