Proxy, new Typeable, and type-level equality

[Richard Eisenberg]

Hi all,

Combining ideas from a number of people/threads ("Proxy and new-typeable" [on libraries] and "RFC: Singleton equality witnesses" [on ghc-devs]), I propose this:

> module GHC.TypeReasoning where
> 
> data a :~: b where
>   Refl :: a :~: a
>
> -- with credit to Conal Elliott for 'ty' and Erik Hesselink & Martijn van Steenbergen for 'type-equality'
> sym :: (a :~: b) -> (b :~: a)
> trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
> coerce :: (a :~: b) -> a -> b
> liftEq :: (a :~: b) -> (f a :~: f b)
> liftEq2 :: (a :~: a') -> (b :~: b') -> (f a b :~: f a' b')
> liftEq3 :: ...
> liftEq4 :: ...
>
> instance Eq (a :~: b) where ...
> instance Show (a :~: b) where ...
> instance Read (a :~: a) where ...
> instance Ord (a :~: b) where ...
> -- what other instances?
>
> data Void
> -- instances as in Edward Kmett's 'void' package
> 
> absurd :: Void -> a
>
> type Refuted a = a -> Void
> type Decision a = Proved a
>                 | Disproved (Refuted a)
>
> class EqT f where
>   eqT :: f a -> f b -> Maybe (a :~: b)
>
> class EqT f => DecideEqT f where
>   decideEqT :: f a -> f b -> Decision (a :~: b)
>
> defaultEqT :: DecideEqT f => f a -> f b -> Maybe (a :~: b) -- for easy writing of EqT instances
>
> instance EqT ((:~:) a) where ...
> instance DecideEqT ((:~:) a) where ...


> module Data.Proxy where
> -- as in Ben Gamari's version


> module Data.Typeable ( … , Proxy(..), (:~:)(..) ) where
> 
> ...
> import GHC.TypeReasoning
> import {-# SOURCE #-} Data.Proxy
> 
> ...
> eqTypeable :: (Typeable a, Typeable b) => Maybe (a :~: b)
> decideEqTypeable :: (Typeable a, Typeable b) => Decision (a :~: b)
> -- can't use EqT and DecideEqT because Typeable is in Constraint, not *
>
> gcast :: (Typeable a, Typeable b) => c a -> Maybe (c b) -- it is now polykinded
>
> {-# DEPRECATED gcast1 ... #-}
> {-# DEPRECATED gcast2 ... #-}
> ...

On top of features others have proposed/written in packages, I have added DecideEqT and related definitions. I would indeed have use for this definition, and I imagine others will, too, once it's out there. We could theoretically hold off on that one, but it seems easy enough just to put it in now, while we're all thinking about it. I've tested the definition by writing instances of singletons, and it works as desired.

If this proposal is accepted, we can then look at changing some of the definitions around TypeLits as well, linking in much of the ghc-devs thread "RFC: Singleton equality witnesses". I don't see any dependencies from the code above on the TypeLits/singleton stuff, so I think we can take those changes in a second round.

One question in the above code: What other instances should there be for (:~:)?

Comments? Thoughts?

Thanks,
Richard