alternative beta-eta equality test

import Prelude hiding (lookup,($))
import Control.Monad

type Ref = Integer

data V
 = Neutral N
 | Lam (V -> V)
 | Pi V (V -> V)
 | Set
 | Type

data N
 = App N V
 | Var Ref

Neutral n $ x = Neutral (App n x)
Lam f $ x = f x

lookup ((i, tau) : gamma) j
 | i == j = Just tau
 | otherwise = lookup gamma j
lookup [] _ = Nothing

eq gamma i f g (Pi tau sigmaF) = eq ((i, tau) : gamma) (i+1) (f $ x) (g $ x) (sigmaF x) where x = Neutral (Var i)
eq gamma i (Neutral n) (Neutral m) Set = maybe False (const True) (eqN gamma i n m)
eq gamma i s t Type = eqT gamma i s t

eqT gamma i (Pi s tF) (Pi u vF) = eqT gamma i s u && eqT ((i, s) : gamma) (i+1) (tF x) (vF x) where x = Neutral (Var i)
eqT gamma i Set Set = True

eqN gamma i (App n x) (App m y) = do
 Pi tau sigmaF <- eqN gamma i n m
 guard (eq gamma i x y tau)
 return (sigmaF x)
eqN gamma _ (Var i) (Var j)
 | i == j = lookup gamma i
 | otherwise = Nothing

-- test = eq [] 0
--   (Lam (\x -> x))
--   (Lam (\f -> Lam (\x -> f $ x)))
--   (Pi (Pi Set (\_ -> Set)) (\_ -> (Pi Set (\_ -> Set))))

-- > test
-- True