new-typeable, new cast?

Shachaf Ben-Kiki shachaf at
Mon Mar 4 08:49:20 CET 2013

On Sun, Mar 3, 2013 at 11:43 PM, Shachaf Ben-Kiki <shachaf at> 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.


More information about the Libraries mailing list