Further support for my proposal: we already have the analogous partial version
Data.Typeable.gcast :: forall a b c. (Typeable a, Typeable b) => c a
-> Maybe (c b)
On Mon, Nov 14, 2016 at 3:21 PM, David Feuer
Most of Data.Type.Equality can be supported by any Haskell implementation with Rank2Types and TypeOperators, using, for example, the well-known definition
newtype a :~: b = Equality { subst :: forall f . f a -> f b }
(The parts that can't be supported so are the gcastWith function, the ~~ constraint, and the == type family.)
What's most prominently missing is the ability to *use* equality for anything beyond castWith without leaning on GHC's equality constraints.
I propose that we add the eliminator subst as a function:
subst :: a :~: b -> f a -> f b subst Refl x = x
Note that we already have an introduction rule
Control.Category.id :: a :~: a
David Feuer