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