# Pastebin 8ne3txlx
wand :: [Constraint] -> [Goal] -> State Int [Constraint]
wand c [] = pure c
wand cs ((Goal ctx expr ty) : gs) = do
    n <- get
    modify (+1) -- Instead of here...
    let (cs', gs') = case expr of
            Tru -> ([IsEq ty Bool], [])
            Fal -> ([IsEq ty Bool], [])
            (Lam x m) -> do
                -- ...I want to do it here.
                let nytvar = TyVar("t" ++ show n)
                let x = ([IsEq nytvar Bool], [])
                x
    wand (cs' ++ cs) (gs' ++ gs)