Trying to prove (a > b) || (a < b) || (a == b)

ipl.hs

{-# LANGUAGE TypeOperators, GADTs, StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall #-}

import Prelude hiding(True, False, Bool, Eq)

data Z = Z
data S n = S n

data Nat n where
   Zero :: Nat Z
   Succ :: Nat n -> Nat (S n)
deriving instance Show (Nat n)

data a :=: b where
   EQZ :: Nat Z :=: Nat Z
   EQS :: Nat a :=: Nat b -> Nat (S a) :=: Nat (S b)
deriving instance Show (a :=: b)

-- less than
data a :<: b where
   LT1 :: Nat Z :<: Nat (S n)
   LT2 :: Nat n :<: Nat m -> Nat (S n) :<: Nat (S m)
deriving instance Show (a :<: b)

-- Greater than
data a :>: b where
   GT1 :: Nat (S n) :>: Nat Z
   GT2 :: Nat n :>: Nat m -> Nat (S n) :>: Nat (S m)
deriving instance Show (a :>: b)

data a :+: b = Inl a | Inr b
     deriving Show

data a :*: b = a :*: b
     deriving Show

dist_or_and :: c :+: (a :*: b) -> (c :+: a) :*: (c :+: b)
dist_or_and (Inl c) = (Inl c) :*: (Inl c)
dist_or_and (Inr (a :*: b)) = (Inr a) :*: (Inr b)

dist_and_or :: a :*: (b :+: c) -> (a :*: b) :+: (a :*: c)
dist_and_or (a :*: (Inl b)) = Inl (a :*: b)
dist_and_or (a :*: (Inr c)) = Inr (a :*: c)

commute_or :: a :+: b -> b :+: a
commute_or (Inl a) = Inr a
commute_or (Inr b) = Inl b

gt_lt_or_eq :: Nat n -> Nat m -> ((Nat n :>: Nat m) :+: (Nat n :<: Nat m)) :+: (Nat n :=: Nat m)
gt_lt_or_eq Zero Zero = Inr EQZ
gt_lt_or_eq (Succ _) Zero = Inl (Inl (GT1))
gt_lt_or_eq Zero (Succ _) = Inl (Inr (LT1))
gt_lt_or_eq (Succ n) (Succ m) = gt_lt_or_eq n m

ipl.hs:57:45:
    Could not deduce (n1 ~ S n1)
    from the context (n ~ S n1)
      bound by a pattern with constructor
                 Succ :: forall n. Nat n -> Nat (S n),
               in an equation for `gt_lt_or_eq'
      at ipl.hs:57:14-19
    or from (m ~ S n2)
      bound by a pattern with constructor
                 Succ :: forall n. Nat n -> Nat (S n),
               in an equation for `gt_lt_or_eq'
      at ipl.hs:57:23-28
      `n1' is a rigid type variable bound by
           a pattern with constructor
             Succ :: forall n. Nat n -> Nat (S n),
           in an equation for `gt_lt_or_eq'
           at ipl.hs:57:14
    Expected type: Nat n
      Actual type: Nat n1
    In the first argument of `gt_lt_or_eq', namely `n'
    In the expression: gt_lt_or_eq n m
    In an equation for `gt_lt_or_eq':
        gt_lt_or_eq (Succ n) (Succ m) = gt_lt_or_eq n m

{- Results in the error:
ipl.hs:57:47:
    Could not deduce (n2 ~ S n2)
    from the context (n ~ S n1)
      bound by a pattern with constructor
                 Succ :: forall n. Nat n -> Nat (S n),
               in an equation for `gt_lt_or_eq'
      at ipl.hs:57:14-19
    or from (m ~ S n2)
      bound by a pattern with constructor
                 Succ :: forall n. Nat n -> Nat (S n),
               in an equation for `gt_lt_or_eq'
      at ipl.hs:57:23-28
      `n2' is a rigid type variable bound by
           a pattern with constructor
             Succ :: forall n. Nat n -> Nat (S n),
           in an equation for `gt_lt_or_eq'
           at ipl.hs:57:23
    Expected type: Nat m
      Actual type: Nat n2
    In the second argument of `gt_lt_or_eq', namely `m'
    In the expression: gt_lt_or_eq n m
    In an equation for `gt_lt_or_eq':
        gt_lt_or_eq (Succ n) (Succ m) = gt_lt_or_eq n m
-}


main :: IO ()
main = return ()