Fun with Functional Dependencies in Purescript

Main.purs

module Main where

data Proxy a = Proxy

data Zero
data Su n

type Three = Su (Su (Su Zero))

class Even n where
  even :: Proxy n
class Odd n where
  odd :: Proxy n
  
instance evenZero :: Even Zero where
  even = Proxy
  
instance oddNumber :: (Even n) => Odd (Su n) where
  odd = Proxy
  
instance evenNumber :: (Odd n) => Even (Su n) where
  even = Proxy

-- | This is not even should fail
x :: Proxy (Su (Su (Su Zero)))
x = even