[Haskell-cafe] in-equality type constraint?

[Ryan Ingram]

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 <ninegua at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>