diff --git a/.gitignore b/.gitignore
index 5112877..193a11d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,4 +3,4 @@ dist-newstyle
 *.x
 *.bak
 src/Grammar
-/language
+language
diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs
index 36ec739..0704832 100644
--- a/src/TypeChecker/TypeChecker.hs
+++ b/src/TypeChecker/TypeChecker.hs
@@ -4,48 +4,49 @@ module TypeChecker.TypeChecker (typecheck) where
 
 import Control.Monad (when, void)
 import Control.Monad.Except (ExceptT, throwError, runExceptT)
-
 import Control.Monad.Reader (ReaderT)
 import qualified Control.Monad.Reader as R
-
 import Control.Monad.Writer (WriterT)
 import qualified Control.Monad.Writer as W
-
+import Control.Monad.State (StateT)
+import qualified Control.Monad.State as St
 import Data.Functor.Identity (Identity, runIdentity)
-
 import Data.Map (Map)
 import qualified Data.Map as M
 import Data.Set (Set)
 import qualified Data.Set as S
-
 import Data.Bool (bool)
-
 import qualified Grammar.Abs as Old
 import Grammar.ErrM (Err)
 
 import TypeChecker.TypeCheckerIr
 
-data Ctx = Ctx
-    { env :: [Map Ident Type]
-    , sigs :: Map Ident Type
-    , typs :: Set Ident
-    }
+data Ctx = Ctx { env :: Map Ident Type
+               , sigs :: Map Ident Type
+               }
     deriving Show
 
-type Check = ReaderT Ctx (ExceptT Error Identity)
+{-
+
+The type checker will assume we first rename all variables to unique name, as to not
+have to care about scoping. It significantly improves the quality of life of the
+programmer.
+
+-}
+
+type Check = StateT (Map Ident Type) (ReaderT Ctx (ExceptT Error Identity))
 
 initEnv :: Ctx
 initEnv =
     Ctx { env = mempty
         , sigs = mempty
-        , typs = mempty
         }
 
 run :: Check Type -> Either Error Type
-run = runIdentity . runExceptT . flip R.runReaderT initEnv
+run = runIdentity . runExceptT . flip R.runReaderT initEnv . flip St.evalStateT mempty
 
 typecheck :: Old.Program -> Either Error ()
-typecheck = runIdentity . runExceptT . flip R.runReaderT initEnv . inferPrg
+typecheck = todo
 
 inferPrg :: Old.Program -> Check ()
 inferPrg (Program [x]) = void $ inferBind x
@@ -56,15 +57,19 @@ inferBind (Bind _ _ e) = void $ inferExp e
 inferExp :: Old.Exp -> Check Type
 inferExp = \case
 
+    -- TODO: Fix bound variable lookup
     Old.EId i -> do
-        ctx <- R.ask
-        case lookupEnv i ctx of
+        st <- St.get 
+        case lookupBound i st of
           Just t -> return t
-          Nothing -> case lookupSigs i ctx of
-                       Just t -> return t
-                       Nothing -> throwError UnboundVar
+          Nothing -> do
+            ctx <- R.ask
+            case lookupEnv i ctx of
+              Just t -> return t
+              Nothing -> case lookupSigs i ctx of
+                           Just t -> return t
+                           Nothing -> throwError UnboundVar
         
-
     Old.EAnn e t -> do
         infT <- inferExp e
         when (t /= infT) (throwError AnnotatedMismatch)
@@ -75,17 +80,15 @@ inferExp = \case
         (Old.CStr s) -> return (TMono $ UIdent "String")
 
     Old.EAdd e1 e2 -> do
-        t1 <- inferExp e1
-        t2 <- inferExp e2
-        let int = TMono (UIdent "Int")
-        case (t1, t2) of
-            (TMono (UIdent "Int"), TMono (UIdent "Int")) -> return int
-            (_, TMono (UIdent "Int")) -> return int
-            (TMono (UIdent "Int"), _) -> return int
-            (TPoly (LIdent x), TPoly (LIdent y)) -> bool (throwError TypeMismatch) (return int) (x==y)
-            _ -> throwError NotNumber
-        return t1
+        let int = TMono "Int"
+        updateBound e1 int
+        updateBound e2 int
+        inf1 <- inferExp e1
+        inf2 <- inferExp e2
+        when (not $ isInt inf1 && isInt inf2) (throwError TypeMismatch)
+        return int
 
+    -- Incomplete and probably wrong
     Old.EApp e1 e2 -> do
         inferExp e1 >>= \case
             TArrow mono@(TMono i) t2 -> do
@@ -98,13 +101,16 @@ inferExp = \case
                 when (not $ t `subtype` t) (throwError TypeMismatch)
                 return t2
 
--- This is not entirely correct. The assumed type can change.
+    -- This is not entirely correct. The assumed type can change.
     Old.EAbs i e -> do
         let assume = (TPoly "a")
+        St.modify (M.insert i assume)
         infT <- R.local (insertEnv i assume) (inferExp e)
-        return (TArrow assume infT)
+        St.gets (M.lookup i) >>= \case
+            Nothing -> todo
+            Just x -> return (TArrow x infT)
 
-    Old.ELet i e1 e2 -> undefined
+    Old.ELet i e1 e2 -> todo
 
 -- Aux
 
@@ -117,30 +123,31 @@ subtype (TArrow t1 t2) (TArrow t3 t4) = t1 `subtype` t3 && t2 `subtype` t4
 subtype _ _                   = False
 
 lookupEnv :: Ident -> Ctx -> Maybe Type
-lookupEnv i c = case env c of
-    [] -> Nothing
-    x : xs -> case M.lookup i x of
-            Nothing -> lookupEnv i (Ctx { env = xs
-                                        , sigs = c.sigs
-                                        , typs = c.typs
-                                        })
-            Just x -> Just x
+lookupEnv i = M.lookup i . env
 
 lookupSigs :: Ident -> Ctx -> Maybe Type
 lookupSigs i = M.lookup i . sigs
 
 insertEnv :: Ident -> Type -> Ctx -> Ctx
-insertEnv i t c =
-    case env c of
-        [] -> Ctx { env = [M.insert i t mempty]
-                  , sigs = c.sigs
-                  , typs = c.typs
-                  }
+insertEnv i t c = Ctx { env = M.insert i t c.env
+                      , sigs = c.sigs
+                      }
 
-        (x : xs) -> Ctx { env = M.insert i t x : xs
-                        , sigs = c.sigs
-                        , typs = c.typs
-                        }
+updateBound :: Old.Exp -> Type -> Check ()
+updateBound (Old.EId i) t = St.modify (M.insert i t)
+updateBound _ _           = return ()
+
+isBound :: Old.Exp -> Check Bool
+isBound (Old.EId i) = (M.member i) <$> St.get
+isBound _           = return False
+
+lookupBound :: Ident -> Map Ident Type -> Maybe Type
+lookupBound = M.lookup
+
+isInt :: Type -> Bool
+isInt (TMono "Int") = True
+isInt (TPoly _)     = True
+isInt _             = False
 
 data Error
     = TypeMismatch
@@ -152,24 +159,6 @@ data Error
     | Default
     deriving Show
 
--- showErr :: Error -> String
--- showErr = \case
---     TypeMismatch expected found -> unwords ["Expected type:", show expected, "but got", show found]
---     NotNumber mess -> "Expected a number, but got: " <> mess
---     NotFunction mess func -> mess <> ": " <> func
---     FunctionTypeMismatch func expected found -> unwords ["Function:", show func, "expected:", show expected, "but got:", show found]
---     UnboundVar mess var -> mess <> ": " <> var
---     AnnotatedMismatch expression expected found ->
---         unwords
---             [ "Expression"
---             , expression
---             , "expected type"
---             , expected
---             , "but was inferred as type"
---             , found
---             ]
---     Default mess -> mess
-
 -- Tests
 
 number :: Old.Exp
@@ -181,8 +170,8 @@ aToInt = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EConst (Old.CInt 3)) (Old.ECons
 intToInt :: Old.Exp
 intToInt = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EId $ Ident "x") (Old.EConst (Old.CInt 3)))
 
-apply :: Old.Exp
-apply = Old.EApp aToInt (Old.EConst (Old.CInt 3))
+addLambda :: Old.Exp
+addLambda = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EId $ Ident "x") (Old.EId $ Ident "x"))
 
 {-# WARNING todo "TODO IN CODE" #-}
 todo :: a