diff --git a/Grammar.cf b/Grammar.cf
index 45021c1..a570950 100644
--- a/Grammar.cf
+++ b/Grammar.cf
@@ -1,15 +1,15 @@
 
-Program. Program ::= [Bind];
+Program. Program ::= [Bind] ;
 
-Bind. Bind ::= Ident [Ident] "=" Exp;
+Bind. Bind ::= Ident [Ident] "=" Exp ;
 
 EAnn.   Exp5 ::= Exp5 ":" Type ;
-EId.    Exp4 ::= Ident;
-EConst. Exp4 ::= Const;
-EApp.   Exp3 ::= Exp3 Exp4;
-EAdd.   Exp1 ::= Exp1 "+" Exp2;
-ELet.   Exp ::= "let" Ident "=" Exp "in" Exp; 
-EAbs.   Exp  ::= "\\" Ident "." Exp;
+EId.    Exp4 ::= Ident ;
+EConst. Exp4 ::= Const ;
+EApp.   Exp3 ::= Exp3 Exp4 ;
+EAdd.   Exp1 ::= Exp1 "+" Exp2 ;
+ELet.   Exp ::= "let" Ident "=" Exp "in" Exp ; 
+EAbs.   Exp  ::= "\\" Ident "." Exp ;
 
 CInt. Const ::= Integer ;
 CStr. Const ::= String ;
@@ -21,11 +21,11 @@ TArrow. Type ::= Type "->" Type1 ;
 token UIdent (upper (letter | digit | '_')*) ;
 token LIdent (lower (letter | digit | '_')*) ;
 
-separator Bind ";";
+separator Bind ";" ;
 separator Ident " ";
 
 coercions Type 1 ;
-coercions Exp 5;
+coercions Exp 5 ;
 
-comment "--";
-comment "{-" "-}";
+comment "--" ;
+comment "{-" "-}" ;
diff --git a/language.cabal b/language.cabal
index d254e3e..0f5aec2 100644
--- a/language.cabal
+++ b/language.cabal
@@ -17,7 +17,7 @@ extra-source-files:
 
 
 common warnings
-    ghc-options: -W
+    ghc-options: -Wdefault
 
 executable language
     import:           warnings
diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs
index 9c3ac70..36ec739 100644
--- a/src/TypeChecker/TypeChecker.hs
+++ b/src/TypeChecker/TypeChecker.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE LambdaCase, OverloadedStrings #-}
+{-# LANGUAGE LambdaCase, OverloadedStrings, OverloadedRecordDot #-}
 
 module TypeChecker.TypeChecker (typecheck) where
 
@@ -18,6 +18,8 @@ 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)
 
@@ -25,7 +27,7 @@ import TypeChecker.TypeCheckerIr
 
 data Ctx = Ctx
     { env :: [Map Ident Type]
-    , sig :: Map Ident Bind
+    , sigs :: Map Ident Type
     , typs :: Set Ident
     }
     deriving Show
@@ -35,7 +37,7 @@ type Check = ReaderT Ctx (ExceptT Error Identity)
 initEnv :: Ctx
 initEnv =
     Ctx { env = mempty
-        , sig = mempty
+        , sigs = mempty
         , typs = mempty
         }
 
@@ -54,7 +56,14 @@ inferBind (Bind _ _ e) = void $ inferExp e
 inferExp :: Old.Exp -> Check Type
 inferExp = \case
 
-    Old.EId i -> undefined
+    Old.EId i -> 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
@@ -68,8 +77,12 @@ inferExp = \case
     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 t1
+            (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
 
@@ -95,27 +108,39 @@ inferExp = \case
 
 -- Aux
 
+-- Double check this function. It's bad and maybe wrong
 subtype :: Type -> Type -> Bool
 subtype (TMono t1) (TMono t2) = t1 == t2
 subtype (TMono t1) (TPoly t2) = True
 subtype (TPoly t2) (TMono t1) = False
 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 })
+            Nothing -> lookupEnv i (Ctx { env = xs
+                                        , sigs = c.sigs
+                                        , typs = c.typs
+                                        })
             Just x -> Just x
 
-lookupSig :: Ident -> Ctx -> Maybe Bind
-lookupSig i = M.lookup i . sig
+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]}
-        (x : xs) -> Ctx{env = M.insert i t x : xs}
+        [] -> Ctx { env = [M.insert i t mempty]
+                  , sigs = c.sigs
+                  , typs = c.typs
+                  }
+
+        (x : xs) -> Ctx { env = M.insert i t x : xs
+                        , sigs = c.sigs
+                        , typs = c.typs
+                        }
 
 data Error
     = TypeMismatch
@@ -145,17 +170,19 @@ data Error
 --             ]
 --     Default mess -> mess
 
-
 -- Tests
 
 number :: Old.Exp
 number = Old.EConst (CInt 3)
 
-lambda :: Old.Exp
-lambda = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EConst (Old.CInt 3)) (Old.EConst (Old.CInt 3)))
+aToInt :: Old.Exp
+aToInt = Old.EAbs (Old.Ident "x") (Old.EAdd (Old.EConst (Old.CInt 3)) (Old.EConst (Old.CInt 3)))
+
+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 lambda (Old.EConst (Old.CInt 3))
+apply = Old.EApp aToInt (Old.EConst (Old.CInt 3))
 
 {-# WARNING todo "TODO IN CODE" #-}
 todo :: a
diff --git a/test_program b/test_program
index 14077bd..a17b924 100644
--- a/test_program
+++ b/test_program
@@ -1 +1 @@
-test y = y
+main = 3;