Haskell type-level literal test (ghc 7.8.2)

typelittest.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ExplicitForAll #-}

import GHC.TypeLits


data Proxy (a :: Nat) = Proxy 

data TLT
data TEQ
data TGT

data Compare (a :: Nat) (b :: Nat) r where
  LessThan    :: forall (a :: Nat) (b :: Nat) (x :: Nat). (a+x) ~ b => Proxy a -> Proxy b -> Compare a b TLT
  Equal       :: forall (a :: Nat) (b :: Nat). a ~ (b + 0)          => Proxy a -> Proxy b -> Compare a b TEQ
  GreaterThan :: forall (a :: Nat) (b :: Nat) (x :: Nat). a ~ (b+x) => Proxy a -> Proxy b -> Compare a b TGT

test :: Compare a b r -> String 
test (LessThan _ _)     = "LessThan"
test (Equal _ _)        = "Equal"
test (GreaterThan _ _)  = "GreaterThan"


main = do 
  print "hello"
  print (test (LessThan (Proxy :: Proxy 1) (Proxy :: Proxy 3)))
  print (test (Equal (Proxy :: Proxy 1) (Proxy :: Proxy 1)))