diff --git a/Grammar.cf b/Grammar.cf
index 410d11d..b58dbea 100644
--- a/Grammar.cf
+++ b/Grammar.cf
@@ -1,20 +1,28 @@
 
-
 Program. Program ::= [Bind];
 
-EId.  Exp3 ::= Ident;
-EInt. Exp3 ::= Integer;
-ELet. Exp3 ::= "let" [Bind] "in" Exp; 
-EApp. Exp2 ::= Exp2 Exp3;
-EAdd. Exp1 ::= Exp1 "+" Exp2;
-EAbs. Exp  ::= "\\" Ident "." Exp;
-
 Bind. Bind ::= Ident [Ident] "=" Exp;
+
+EAnn.   Exp5 ::= Exp5 ":" Type ;
+EId.    Exp4 ::= Ident;
+EConst. Exp4 ::= Const;
+EApp.   Exp3 ::= Exp3 Exp4;
+ELet.   Exp2 ::= "let" Bind "in" Exp; 
+EAdd.   Exp1 ::= Exp1 "+" Exp2;
+EAbs.   Exp  ::= "\\" Ident "." Exp;
+
+CInt. Const ::= Integer ;
+CStr. Const ::= String ;
+
+TMono. Type1 ::= Ident ;
+TPoly. Type1 ::= Ident ;
+TFun. Type  ::= Type1 "->" Type ;
+
 separator Bind ";";
 separator Ident " ";
 
-coercions Exp 3;
+coercions Type 1 ;
+coercions Exp 5;
 
 comment "--";
 comment "{-" "-}";
-
diff --git a/Makefile b/Makefile
index 6e8a54d..ad830b5 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
 .PHONY : sdist clean
 
 language : src/Grammar/Test
-	cabal install --installdir=.
+	cabal install --installdir=. --overwrite-policy=always
 
 src/Grammar/Test.hs src/Grammar/Lex.x src/Grammar/Par.y : Grammar.cf
 	bnfc -o src -d $<
diff --git a/language.cabal b/language.cabal
index 3f4860c..d254e3e 100644
--- a/language.cabal
+++ b/language.cabal
@@ -17,7 +17,7 @@ extra-source-files:
 
 
 common warnings
-    ghc-options: -Wall
+    ghc-options: -W
 
 executable language
     import:           warnings
@@ -30,7 +30,12 @@ executable language
       Grammar.Par
       Grammar.Print
       Grammar.Skel
-      LambdaLifter
+      Grammar.ErrM
+      -- LambdaLifter
+      TypeChecker.TypeChecker
+      TypeChecker.TypeCheckerIr
+      -- Renamer.Renamer
+      -- Renamer.RenamerIr
       -- Interpreter
 
     hs-source-dirs:   src
@@ -40,7 +45,7 @@ executable language
       , mtl
       , containers
       , either
-      , array
       , extra
+      , array
 
     default-language: GHC2021
diff --git a/src/Abs.hs b/src/Abs.hs
deleted file mode 100644
index 7cc3064..0000000
--- a/src/Abs.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-{-# LANGUAGE TypeFamilies, PatternSynonyms, StandaloneDeriving #-}
-
-module Abs where
-
-import Data.String
-
-data Program a = Program [Bind a]
-
-data Bind a = Bind Ident [Ident] (Exp a)
-
-newtype Ident = Ident String
-    deriving (Eq, Ord, Show, Data.String.IsString)
-
-data Exp a = EId  (IdFamily  a)  Ident
-           | EInt (IntFamily a) Integer
-           | EAdd (AddFamily a) (Exp a) (Exp a)
-           | EApp (AppFamily a) (Exp a) (Exp a)
-           | EAbs (AbsFamily a) Ident (Exp a)
-           | ELet (LetFamily a) [Bind a] (Exp a)
-           | EExp (ExpFamily a) (Exp a)
-
-type family IdFamily  a
-type family IntFamily a
-type family AddFamily a
-type family AppFamily a
-type family AbsFamily a
-type family LetFamily a
-type family ExpFamily a
diff --git a/src/LambdaLifter.hs b/src/LambdaLifter.hs
deleted file mode 100644
index 79d5b8a..0000000
--- a/src/LambdaLifter.hs
+++ /dev/null
@@ -1,253 +0,0 @@
-{-# LANGUAGE LambdaCase, OverloadedStrings, TypeFamilies, PatternSynonyms #-}
-
-
-module LambdaLifter (lambdaLift, freeVars, abstract, rename, collectScs) where
-
-import           Data.List        (mapAccumL)
-import           Data.Map         (Map)
-import qualified Data.Map         as Map
-import           Data.Maybe       (fromMaybe)
-import           Data.Set         (Set, (\\))
-import qualified Data.Set         as Set
-import           Data.Tuple.Extra (uncurry3)
-import           Grammar.Abs
-import           Prelude          hiding (exp)
-import qualified Abs              as A
-import           Data.Void
-
-
-
--- | Lift lambdas and let expression into supercombinators.
-lambdaLift :: Program -> Program
-lambdaLift = collectScs . rename . abstract . freeVars
-
-
--- | Annotate free variables
-freeVars :: Program -> AnnProgram
-freeVars (Program ds) = [ (n, xs, freeVarsExp (Set.fromList xs) e)
-                        | Bind n xs e <- ds
-                        ]
-
-freeVarsExp :: Set Ident -> Exp -> AnnExp
-freeVarsExp lv = \case
-
-  EId n | Set.member n lv -> (Set.singleton n, AId n)
-        | otherwise       -> (mempty, AId n)
-
-  EInt i     -> (mempty, AInt i)
-
-  EApp e1 e2 -> (Set.union (freeVarsOf e1') (freeVarsOf e2'), AApp e1' e2')
-    where e1' = freeVarsExp lv e1
-          e2' = freeVarsExp lv e2
-
-  EAdd e1 e2 -> (Set.union (freeVarsOf e1') (freeVarsOf e2'), AAdd e1' e2')
-    where e1' = freeVarsExp lv e1
-          e2' = freeVarsExp lv e2
-
-  EAbs n  e  -> (Set.delete n $ freeVarsOf e', AAbs n e')
-    where e'  = freeVarsExp (Set.insert n lv) e
-
-  ELet bs e  -> (Set.union bsFree eFree, ALet bs' e')
-    where
-      bsFree       = freeInValues \\ nsSet
-      eFree        = freeVarsOf e' \\ nsSet
-      bs'          = zipWith3 ABind ns xs es'
-      e'           = freeVarsExp e_lv e
-      (ns, xs, es) = fromBinders bs
-      nsSet        = Set.fromList ns
-      e_lv         = Set.union lv nsSet
-      es'          = map (freeVarsExp e_lv) es
-      freeInValues = foldr1 Set.union (map freeVarsOf es')
-
-
-freeVarsOf :: AnnExp -> Set Ident
-freeVarsOf = fst
-
-fromBinders :: [Bind] -> ([Ident], [[Ident]], [Exp])
-fromBinders bs = unzip3 [ (n, xs, e) | Bind n xs e <- bs ]
-
--- AST annotated with free variables
-type AnnProgram = [(Ident, [Ident], AnnExp)]
-
-type AnnExp = (Set Ident, AnnExp')
-
-data ABind = ABind Ident [Ident] AnnExp deriving Show
-
-data AnnExp' = AId Ident
-             | AInt Integer
-             | AApp (Set Ident, AnnExp') (Set Ident, AnnExp')
-             | AAdd (Set Ident, AnnExp') (Set Ident, AnnExp') 
-             | AAbs Ident   (Set Ident, AnnExp') 
-             | ALet [ABind] (Set Ident, AnnExp') 
-             deriving Show
-
--- | Lift lambdas to let expression of the form @let sc = \x -> rhs@
-abstract :: AnnProgram -> Program
-abstract prog = Program $ map f prog
-  where
-  f :: (Ident, [Ident], AnnExp) -> Bind
-  f (name, pars, rhs@(_, e)) =
-    case e of
-      AAbs par body -> Bind name (snoc par pars) $ abstractExp body
-      _             -> Bind name pars            $ abstractExp rhs
-
-abstractExp :: AnnExp -> Exp
-abstractExp (free, exp) = case exp of
-  AId  n     -> EId n
-  AInt i     -> EInt i
-  AApp e1 e2 -> EApp (abstractExp e1) (abstractExp e2)
-  AAdd e1 e2 -> EAdd (abstractExp e1) (abstractExp e2)
-  ALet bs e  -> ELet [Bind n xs (abstractExp e1) | ABind n xs e1 <- bs ] $ abstractExp e
-  AAbs n  e  -> foldl EApp sc (map EId fvList)
-    where
-      fvList = Set.toList free
-      bind = Bind "sc" [] e'
-      e' = foldr EAbs (abstractExp e) (fvList ++ [n])
-      sc = ELet [bind] (EId (Ident "sc"))
-
-
-snoc :: a -> [a] -> [a]
-snoc x xs = xs ++ [x]
-
--- | Rename all supercombinators and variables
-rename :: Program -> Program
-rename (Program ds) = Program $ map (uncurry3 Bind) tuples
-  where
-    tuples = snd (mapAccumL renameSc 0 ds)
-    renameSc i (Bind n xs e) = (i2, (n, xs', e'))
-      where
-        (i1, xs', env) = newNames i xs
-        (i2, e')       = renameExp env i1 e
-
-renameExp :: Map Ident Ident -> Int -> Exp -> (Int, Exp)
-renameExp env i = \case
-
-  EId  n     -> (i, EId . fromMaybe n $ Map.lookup n env)
-
-  EInt i1    -> (i, EInt i1)
-
-  EApp e1 e2 -> (i2, EApp e1' e2')
-    where
-      (i1, e1') = renameExp env i e1
-      (i2, e2') = renameExp env i1 e2
-
-  EAdd e1 e2 -> (i2, EAdd e1' e2')
-    where
-      (i1, e1') = renameExp env i e1
-      (i2, e2') = renameExp env i1 e2
-
-  ELet bs e  -> (i3, ELet (zipWith3 Bind ns' xs es') e')
-    where
-      (i1, e')        = renameExp e_env i e
-      (ns, xs, es)    = fromBinders bs
-      (i2, ns', env') = newNames i1 ns
-      e_env           = Map.union env' env
-      (i3, es')       = mapAccumL (renameExp e_env) i2 es
-
-
-  EAbs n  e  -> (i2, EAbs (head ns) e')
-    where
-      (i1, ns, env') = newNames i [n]
-      (i2, e')       = renameExp (Map.union env' env ) i1 e
-
-
-newNames :: Int -> [Ident] -> (Int, [Ident], Map Ident Ident)
-newNames i old_names = (i', new_names, env)
-  where
-    (i', new_names) = getNames i old_names
-    env = Map.fromList $ zip old_names new_names
-
-
-getName :: Int -> Ident -> (Int, Ident)
-getName i (Ident s) = (i + 1, makeName s i)
-
-getNames :: Int -> [Ident] -> (Int, [Ident])
-getNames i ns = (i + length ss, zipWith makeName ss [i..])
-  where
-    ss = map (\(Ident s) -> s) ns
-
-makeName :: String -> Int -> Ident
-makeName prefix i = Ident (prefix ++ "_" ++ show i)
-
-
--- | Collects supercombinators by lifting appropriate let expressions
-collectScs :: Program -> Program
-collectScs (Program ds) = Program $ concatMap collectOneSc ds
-  where
-    collectOneSc (Bind name args rhs) = Bind name args rhs' : scs
-      where (scs, rhs') = collectScsExp rhs
-
-collectScsExp :: Exp -> ([Bind], Exp)
-collectScsExp = \case
-
-  EId  n     -> ([], EId n)
-
-  EInt i     -> ([], EInt i)
-
-  EApp e1 e2 -> (scs1 ++ scs2, EApp e1' e2')
-    where
-      (scs1, e1') = collectScsExp e1
-      (scs2, e2') = collectScsExp e2
-
-  EAdd e1 e2 -> (scs1 ++ scs2, EAdd e1' e2')
-    where
-      (scs1, e1') = collectScsExp e1
-      (scs2, e2') = collectScsExp e2
-
-  EAbs x  e  -> (scs, EAbs x e')
-    where
-      (scs, e') = collectScsExp e
-
-  ELet bs e  -> (rhss_scs ++ e_scs ++ local_scs, mkEAbs non_scs' e')
-    where
-      (rhss_scs, bs') = mapAccumL collectScs_d [] bs
-      scs'            = [ Bind n xs rhs | Bind n xs rhs <- bs', isEAbs rhs]
-      non_scs'        = [ Bind n xs rhs | Bind n xs rhs <- bs', not $ isEAbs rhs]
-      local_scs       = [ Bind n (xs ++ [x]) e1 | Bind n xs (EAbs x e1) <- scs']
-      (e_scs, e')     = collectScsExp e
-
-      collectScs_d scs (Bind n xs rhs) = (scs ++ rhs_scs1, Bind n xs rhs')
-        where
-          (rhs_scs1, rhs') = collectScsExp rhs
-
-isEAbs :: Exp -> Bool
-isEAbs = \case
-  EAbs {} -> True
-  _       -> False
-
-mkEAbs :: [Bind] -> Exp -> Exp
-mkEAbs [] e = e
-mkEAbs bs e = ELet bs e
-
-
-{----------- BOILERPLATE -----------}
-
-data LL 
-
-type instance A.IdFamily  LL = ()
-type instance A.IntFamily LL = ()
-type instance A.AddFamily LL = (Set Ident, Set Ident)
-type instance A.AppFamily LL = (Set Ident, Set Ident)
-type instance A.AbsFamily LL = Set Ident
-type instance A.LetFamily LL = Set Ident
-type instance A.ExpFamily LL = Void
-
-pattern LLId ident = A.EId () ident
-pattern LLInt int = A.EInt () int
-pattern LLAdd s1 s2 e1 e2 = A.EAdd (s1,s2) e1 e2
-pattern LLApp s1 s2 e1 e2 = A.EApp (s1,s2) e1 e2
-pattern LLAbs s i e = A.EAbs s i e
-pattern LLLet s binds e = A.ELet s binds e
-pattern LLExp v e = A.EExp v e
-
-{-
-
-data AnnExp' = AId Ident
-             | AInt Integer
-             | AApp (Set Ident, AnnExp') (Set Ident, AnnExp')
-             | AAdd (Set Ident, AnnExp') (Set Ident, AnnExp') 
-             | AAbs Ident   (Set Ident, AnnExp') 
-             | ALet [ABind] (Set Ident, AnnExp') 
-             deriving Show
-
--}
diff --git a/src/Main.hs b/src/Main.hs
index d367bc1..e55afe9 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -3,7 +3,6 @@ module Main where
 
 import           Grammar.Par        (myLexer, pProgram)
 import           Grammar.Print      (printTree)
-import           LambdaLifter       (lambdaLift)
 import           System.Environment (getArgs)
 import           System.Exit        (exitFailure, exitSuccess)
 
@@ -17,17 +16,4 @@ main = getArgs >>= \case
        putStrLn "SYNTAX ERROR"
        putStrLn err
        exitFailure
-      Right prg -> do
-        putStrLn "-- Parse"
-        putStrLn $ printTree prg
-        -- putStrLn "\n-- Abstract"
-        -- putStrLn . printTree $ (abstract . freeVars) prg
-        -- putStrLn "\n-- Rename"
-        -- putStrLn . printTree $ (rename . abstract . freeVars) prg
-        putStrLn "\n-- Lamda lifter"
-        putStrLn . printTree $ lambdaLift prg
-        putStrLn ""
-        exitSuccess
-
-
-
+      Right prg -> putStrLn "NO SYNTAX ERROR"
diff --git a/src/Renamer/Renamer.hs b/src/Renamer/Renamer.hs
new file mode 100644
index 0000000..8d3fa1c
--- /dev/null
+++ b/src/Renamer/Renamer.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+
+module Renamer.Renamer (rename) where
+
+import           Control.Applicative  (Applicative (liftA2))
+import           Control.Monad.Except (MonadError (throwError))
+import           Control.Monad.RWS    (MonadState, gets, modify)
+import           Control.Monad.State  (StateT, evalStateT)
+import           Data.Set             (Set)
+import qualified Data.Set             as Set
+import           Grammar.Abs
+import           Grammar.ErrM         (Err)
+import           Grammar.Print        (printTree)
+import qualified Renamer.RenamerIr            as R
+
+
+data Cxt = Cxt
+  { uniques    :: [(Ident, R.Unique)]
+  , nextUnique :: R.Unique
+  , sig        :: Set Ident
+  }
+
+initCxt :: Cxt
+initCxt = Cxt
+  { uniques    = []
+  , nextUnique = R.Unique 0
+  , sig        = mempty
+  }
+
+newtype Rn a = Rn { runRn :: StateT Cxt Err a }
+  deriving (Functor, Applicative, Monad, MonadState Cxt, MonadError String)
+
+rename :: Program -> Err R.Program
+rename p = evalStateT (runRn $ renameProgram p) initCxt
+
+renameProgram :: Program -> Rn R.Program
+renameProgram (Program ds (Main e)) = do
+  ds' <- mapM renameDef ds
+  e'  <- renameExp e
+  pure $ R.Program ds' (R.Main e')
+
+renameDef :: Def -> Rn R.Def
+renameDef = \case
+  DExp x t _ xs e -> do
+    newSig x
+    xs' <- mapM newUnique xs
+    e'  <- renameExp e
+    let e'' = foldr ($) e' . zipWith R.EAbs xs' $ fromTree t
+    pure . R.DBind $ R.Bind x t e''
+
+renameExp :: Exp -> Rn R.Exp
+renameExp = \case
+  EId x      -> R.EId <$> findBind x
+  EInt i     -> pure $ R.EInt i
+  EApp e e1  -> liftA2 R.EApp (renameExp e) $ renameExp e1
+  EAdd e e1  -> liftA2 R.EAdd (renameExp e) $ renameExp e1
+  EAbs x t e -> do
+    x' <- newUnique x
+    e' <- renameExp e
+    pure $ R.EAbs x' t e'
+
+findBind :: Ident -> Rn R.Name
+findBind x = lookupUnique x >>= \case
+    Just u  -> pure $ R.Nu u
+    Nothing -> gets (Set.member x . sig) >>= \case
+      False -> throwError ("Unbound variable " ++ printTree x)
+      True  -> pure $ R.Ni x
+
+newUnique :: Ident -> Rn R.Unique
+newUnique x = do
+  u <- gets nextUnique
+  modify $ \env -> env { nextUnique = succ u
+                       , uniques = (x, u) : env.uniques
+                       }
+  pure u
+
+newSig :: Ident -> Rn ()
+newSig x = modify $ \cxt -> cxt { sig = Set.insert x cxt.sig}
+
+lookupUnique :: Ident -> Rn (Maybe R.Unique)
+lookupUnique x = lookup x <$> gets uniques
+
+fromTree :: Type -> [Type]
+fromTree = fromTree' []
+
+fromTree' :: [Type] -> Type -> [Type]
+fromTree' acc = \case
+  TFun t t1 -> acc ++ [t] ++ fromTree t1
+  other     -> other : acc
diff --git a/src/Renamer/RenamerIr.hs b/src/Renamer/RenamerIr.hs
new file mode 100644
index 0000000..e3c4cce
--- /dev/null
+++ b/src/Renamer/RenamerIr.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase                 #-}
+
+module Renamer.RenamerIr where
+
+import           Grammar.Abs   (Ident, Type (..))
+import           Grammar.Print
+
+
+data Program = Program [Def] Main
+  deriving (Eq, Ord, Show, Read)
+
+newtype Main = Main Exp
+  deriving (Eq, Ord, Show, Read)
+
+
+newtype Def = DBind Bind
+  deriving (Eq, Ord, Show, Read)
+
+data Name = Nu Unique | Ni Ident deriving (Ord, Show, Eq, Read)
+
+newtype Unique = Unique Int deriving (Enum, Eq, Read, Ord)
+instance Show Unique where show (Unique i) = "x" ++ show i
+
+data Exp
+    = EId  Name
+    | EInt Integer
+    | EApp Exp Exp
+    | EAdd Exp Exp
+    | EAbs Unique Type Exp
+  deriving (Eq, Ord, Show, Read)
+
+
+data Bind = Bind Ident Type Exp
+  deriving (Eq, Ord, Show, Read)
+
+
+instance Print Program where
+  prt i = \case
+    Program defs main -> prPrec i 0 (concatD [prt 0 defs, prt 0 main])
+
+
+instance Print Def where
+  prt i (DBind b) = prPrec i 0 $ concatD [prt 0 b, doc (showString ";")]
+
+instance Print Bind where
+  prt i = \case
+    Bind x t e -> prPrec i 0 $ concatD
+      [ prt 0 x
+      , doc (showString ":")
+      , prt 0 t
+      , doc (showString "=")
+      , prt 0 e]
+
+instance Print [Def] where
+  prt _ []     = concatD []
+  prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
+
+
+instance Print Main where
+  prt i = \case
+    Main exp -> prPrec i 0 $ concatD
+     [ doc (showString "main")
+     , doc (showString "=")
+     , prt 0 exp
+     , doc (showString ";")
+     ]
+
+instance Print Exp where
+  prt i = \case
+    EId u -> prPrec i 3 (concatD [prt 0 u])
+    EInt n -> prPrec i 3 (concatD [prt 0 n])
+    EApp e e1 -> prPrec i 2 (concatD [prt 2 e, prt 3 e1])
+    EAdd e e1 -> prPrec i 1 (concatD [prt 1 e, doc (showString "+"), prt 2 e1])
+    EAbs u t e -> prPrec i 0 (concatD [doc (showString "\\"), prt 0 u, doc (showString ":"), prt 0 t, doc (showString "."), prt 0 e])
+
+
+instance Print Name where
+  prt _ = \case
+    Ni i -> prt 0 i
+    Nu u -> prt 0 u
+
+instance Print Unique where
+  prt _ = doc . showString . show
diff --git a/src/TypeChecker.hs b/src/TypeChecker.hs
deleted file mode 100644
index e69de29..0000000
diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs
new file mode 100644
index 0000000..c98ad66
--- /dev/null
+++ b/src/TypeChecker/TypeChecker.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE LambdaCase #-}
+
+module TypeChecker.TypeChecker where
+
+import Control.Monad (when)
+import Control.Monad.Except (throwError)
+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 Data.Map (Map)
+import qualified Data.Map as M
+import Data.Set (Set)
+import qualified Data.Set as S
+
+import qualified Grammar.Abs as Old
+import Grammar.ErrM (Err)
+
+import TypeChecker.TypeCheckerIr
+
+data Ctx = Ctx
+    { env :: [Map Ident Type]
+    , sig :: Map Ident Bind
+    , typs :: Set Ident
+    }
+
+type Check a = WriterT String (ReaderT Ctx Err) a
+
+inferExp :: Old.Exp -> Check Type
+inferExp = \case
+    Old.EAnn e t -> do
+        infT <- inferExp e
+        when (t /= infT) (throwError $ show (AnnotatedMismatch (show e) (show t) (show infT)))
+        return infT
+    Old.EConst c -> case c of
+        (CInt i) -> return (TMono $ Old.Ident "Int")
+        (CStr s) -> return (TMono $ Old.Ident "String")
+    Old.EId i -> lookupEnv i
+    Old.EAdd e1 e2 -> do
+        t1 <- inferExp e1
+        t2 <- inferExp e2
+        case (t1, t2) of
+            (TMono (Old.Ident "Int"), TMono (Old.Ident "Int")) -> return t1
+            _ -> throwError $ show (NotNumber (show t1))
+        return t1
+
+    -- This is wrong currently. (a -> b) should be able to take String
+    Old.EApp e1 e2 -> do
+        inferExp e1 >>= \case
+            TFun mono@(TMono i) t2 -> do
+                t <- inferExp e2
+                when (t /= mono) (throwError $ show $ TypeMismatch (show t) (show mono))
+                return t
+
+            -- Not entirely correct. Should sometimes be able to provide mono types where poly expected.
+            -- i.e id : a -> a; id "string"
+            TFun poly@(TPoly f) t2 -> do
+                t <- inferExp e2
+                when (t /= poly) (throwError $ show (TypeMismatch (show t) (show poly)))
+                return t
+            t -> throwError $ show (NotFunction "Expected a function, but got:" (show t))
+
+    Old.EAbs i e -> undefined
+
+    Old.ELet b e -> undefined
+
+-- Aux
+
+lookupEnv :: Ident -> Check Type
+lookupEnv i =
+    R.asks env >>= \case
+        [] -> throwError $ show (UnboundVar "Variable not found" (show i))
+        xs -> lookupEnv' i xs
+  where
+    lookupEnv' :: Ident -> [Map Ident Type] -> Check Type
+    lookupEnv' i [] = throwError $ show (UnboundVar "Variable not found" (show i))
+    lookupEnv' i (x : xs) = case M.lookup i x of
+        Just t -> return t
+        Nothing -> lookupEnv' i xs
+
+lookupSig :: Ident -> Check Bind
+lookupSig b =
+    R.asks sig >>= \m -> case M.lookup b m of
+        Nothing -> undefined
+        Just b -> return b
+
+insertEnv :: Ident -> Type -> Ctx -> Ctx
+insertEnv i t c =
+    case env c of
+        [] -> Ctx{env = [M.insert i t mempty]}
+        (x : xs) -> Ctx{env = M.insert i t x : xs}
+
+data Error
+    = TypeMismatch String String
+    | NotNumber String
+    | FunctionTypeMismatch String String String
+    | NotFunction String String
+    | UnboundVar String String
+    | AnnotatedMismatch String String String
+    | Default String
+
+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
+
+instance Show Error where
+    show = showErr
diff --git a/src/TypeChecker/TypeCheckerIr.hs b/src/TypeChecker/TypeCheckerIr.hs
new file mode 100644
index 0000000..3bca405
--- /dev/null
+++ b/src/TypeChecker/TypeCheckerIr.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE LambdaCase #-}
+
+module TypeChecker.TypeCheckerIr
+    ( Program(..)
+    , Bind(..)
+    , Ident
+    , Type(..)
+    , Const(..)
+    , Exp(..)
+    )
+        where
+
+import Grammar.Abs (Program(..), Bind(..), Ident, Type(..), Const(..))
+
+data Exp
+    = EAnn Exp Type
+    | EId Ident Type
+    | EConst Const Type
+    | EApp Exp Exp Type
+    | EAdd Exp Exp Type
+    | EAbs Ident Exp Type
+  deriving (Eq, Ord, Show, Read)
diff --git a/test_program b/test_program
new file mode 100644
index 0000000..4a7b634
--- /dev/null
+++ b/test_program
@@ -0,0 +1 @@
+main = \x. x + (3 : Int)