I was wondering this. I was recently able to write some code for negation of type equality, using the encoding "Not p" == "p -> forall a. a"
But it doesn't generalize; you need to create a witness of inequality for every pair of types you care about. {-# LANGUAGE RankNTypes, TypeFamillies, ExistentialQuantification #-} module NotEq where data TypeEqual a b = (a ~ b) => Refl newtype Void = Void { voidElim :: forall a. a } type Not p = (p -> Void) data family IntVsBool a newtype instance IntVsBool Int = OK () newtype instance IntVsBool Bool = NotOK Void liftEq :: TypeEqual a b -> TypeEqual (f a) (f b) liftEq Refl = Refl cast :: TypeEqual a b -> a -> b cast Refl = id int_neq_bool :: Not (TypeEqual Int Bool) int_neq_bool = \int_eq_bool -> case (cast (liftEq int_eq_bool) (OK ())) of (NotOK v) -> v On Fri, Jul 16, 2010 at 4:08 PM, Paul L <nine...@gmail.com> wrote: > Does anybody know why the type families only supports equality test > like a ~ b, but not its negation? > > -- > Regards, > Paul Liu > > Yale Haskell Group > http://www.haskell.org/yale > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe