[Haskell-cafe] Is it possible to prove type *non*-equality in Haskell?

[Ryan Ingram]

Short version: How can I get from (Z ~ S n) to a useful contradiction?

Type equality coercions[1] let us write proofs in Haskell that two
types are equal:

> {-# LANGUAGE GADTs, RankNTypes, TypeFamilies #-}
> {-# OPTIONS_GHC -Wall #-}
> module TEq where

> data TEq a b = (a ~ b) => TEq

This provides all the expected properties for equality:

> refl :: TEq a a
> refl = TEq
> symm :: TEq a b -> TEq b a
> symm TEq = TEq
> trans :: TEq a b -> TEq b c -> TEq a c
> trans TEq TEq = TEq

Here's an example use:

> data Z = Z
> newtype S n = S n

> data Nat a where
>     Nz :: Nat Z
>     Ns :: Nat x -> Nat (S x)

> proveEq :: Nat a -> Nat b -> Maybe (TEq a b)
> proveEq Nz Nz = return TEq
> proveEq (Ns a) (Ns b) = do
>     TEq <- proveEq a b
>     return TEq
> proveEq _ _ = Nothing

But if you get "Nothing" back, there's no proof that the two types are
in fact non-equal.

You can use "_|_ as negation":

> newtype Not p = Contr { contradiction :: forall a. p -> a }
>
> nsymm :: Not (TEq a b) -> Not (TEq b a)
> nsymm pf = Contr (contradiction pf . symm)

We know by parametricity that "contradiction n p" isn't inhabited as
its type is (forall a. a)

But I can't figure out a way to write this without "error":

> notZeqS :: forall n. Not (TEq Z (S n))
> notZeqS = Contr (\x -> x `seq` error "impossible")

As a first step, I'd like to write this:

> -- notZeqS = Contr (\TEq -> error "impossible")

but the compiler complains immediately about the pattern match being unsound:
TEq.lhs:39:20:
    Couldn't match expected type `S n' against inferred type `Z'
    In the pattern: TEq
    In the first argument of `Contr', namely
        `(\ TEq -> error "impossible")'
    In the expression: Contr (\ TEq -> error "impossible")

Is there any way to use the obvious unsoundness we get from (Z ~ S n) to
generate a contradiction?

Ideally I'd like to be able to implement
] natEqDec :: Nat a -> Nat b -> Either (TEq a b) (Not (TEq a b))
as follows:

> predEq :: TEq (f a) (f b) -> TEq a b
> predEq TEq = TEq

> natEqDec :: Nat a -> Nat b -> Either (TEq a b) (Not (TEq a b))
> natEqDec Nz     Nz     = Left TEq
> natEqDec (Ns a) (Ns b) = case natEqDec a b of
>     Left TEq -> Left TEq
>     Right pf -> Right $ Contr $ \eq -> contradiction pf (predEq eq)
> natEqDec Nz     (Ns _) = Right notZeqS
> natEqDec (Ns _) Nz     = Right (nsymm notZeqS)

Which compiles successfully, but the "error" call in "notZeqS" is a
big wart.  Is there a better implementation of "Not" that allows us to
avoid this wart?

  -- ryan

[1] http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/