new-typeable, new cast?

[Shachaf Ben-Kiki]

This came up in #haskell -- rather than just provide coerce, cast (or
a primitive that cast can be built on, as well as other things) can
give a type equality witness of some kind. Some possible signatures
are:

    cast :: (Typeable a, Typeable b) => Maybe (p a -> p b) --
Leibniz-style equality
    cast :: (Typeable a, Typeable b) => p a -> Maybe (p b) -- another form
    cast :: (Typeable a, Typeable b) => Maybe (Is a b) -- GADT-style equality
    cast :: (Typeable a, Typeable b) => MightBe a b -- another form
    -- With
    data Is a b where { Refl :: Is a a } -- standard equality GADT
    data MightBe a b where -- version with built-in Maybe, for more
convenient types
      Is :: MightBe a a
      Isn't :: MightBe a b

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.

The GADT form can let you write code like

    foo :: forall a. Typeable a => a -> ...
    foo x
      | Is <- cast :: MightBe a Int = ...x...
      | Is <- cast :: MightBe a Char = ...x...
      | otherwise = ...

Without coming up with a new name for x. It's possible to provide
other functions on top of this primitive, like

    cast :: (Typeable a, Typeable b) => proxy a -> qroxy b -> ... --
to save some type annotations
    cast :: (Typeable a, Typeable b) => (a ~ b => r) -> Maybe r -- to
use an expression directly
    cast :: (Typeable a, Typeable b) => a -> Maybe b -- the original

Of the primitives I mentioned, the first two are H2010. The last two
are nice to use directly, but use extensions (this probably doesn't
matter so much for new-typeable). The Maybe form lets you say things
like `fmap (\Is -> ...) (cast :: ...)` -- unfortunately, there's no
"proper" Is type in base right now. The fourth version might save some
typing, and might be slightly better performance-wise, since it saves
a ⊥ (it's just represented like Bool at runtime)? Probably it all gets
inlined so that doesn't matter anyway.

Regardless of which particular primitive is used, it would be great
for new-typeable to provide something stronger than cast.

    Shachaf