TypeLeve.purs

data Zero
data Succ n

type Two = Succ (Succ Zero)
type Three = Succ (Succ (Succ Zero))

data True
data False

class IsEven n b
class IsOdd n b

instance isEvenZero :: IsEven Zero True
instance isEvenSucc :: IsOdd n b ⇒ IsEven (Succ n) b
instance isOddZero  :: IsOdd Zero False
instance isOddSucc  :: IsEven n b ⇒ IsOdd (Succ n) b

undefined :: ∀ a. a
undefined = unsafeCoerce unit

test1 :: True
test1 = (undefined :: ∀ b. IsEven Two b => b)

-- Can't get compiled
-- test2 :: True
-- test2 = (undefined :: ∀ b. IsEven Three b => b)