diff --git a/TODO b/TODO
index 4cb036f..7eea998 100644
--- a/TODO
+++ b/TODO
@@ -1,16 +1,20 @@
-1) Write a Hindley Milner type checker for that injective datatype recursor language
+*) Fix user defined type stuff
 
-https://wikimedia.org/api/rest_v1/media/math/render/svg/431b94815103ac9dc77d0e92739456c3c2c90803
-https://github.com/sdiehl/write-you-a-haskell/blob/master/chapter7/poly_constraints/src/Infer.hs
-https://github.com/sdiehl/write-you-a-haskell/blob/master/chapter7/poly/src/Infer.hs
+*) Implement top level stuff
 
-2) Extend it to allow for referencing declerations "further down" in file, but make sure it
+*) Rewrite type checker to collect and then solve constraints
+
+*) Extend it to allow for referencing declarations "further down" in file, but make sure it
 terminates by forbidding corecursion (simply done by building a reference graph and then looking at it)
 
-3) Add Kind env and use it to have "type of types"
+*) Add Kind env and type parameters
 
-4) Type annotated tree?
+*) Type annotated tree?
 
-5) Make SECD machine good enough to execute it
+*) Make SECD machine good enough to execute it
 
-6) Write backend for SECD machine code
+*) Write backend for SECD machine code
+
+*) Pattern matching to recursor syntactic sugar
+
+*) Record types
diff --git a/app/Main.hs b/app/Main.hs
index d582e1e..1926cab 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,2 +1,40 @@
+import System.Exit
+
+import Hm.Layout ( resolveLayout )
+import Hm.Lex    ( Token, mkPosToken )
+import Hm.Par    ( pExp, myLexer )
+import Hm.Print  ( Print, printTree )
+
+import Data.Text (Text)
+import qualified Data.Text.IO as T
+
+import qualified Data.Set as S
+
+import TC (initialState, runCheck, infer, generalize)
+import PostProcess (expToExp, runProcess)
+import Pretty
+
+inferType :: Text -> IO ()
+inferType s = case pExp ts of
+    Left err -> do
+      putStrLn "\nParse              Failed...\n"
+      putStrLn  "Tokens:"
+      mapM_ (putStrLn . showPosToken . mkPosToken) ts
+      putStrLn err
+      exitFailure
+    Right tree -> do
+      putStrLn "\nParse Successful!"
+      putStrLn (printTree tree)
+
+      let action = runProcess (expToExp tree) S.empty >>= infer >>= generalize . snd
+      let result = fst (runCheck initialState action)
+
+      case result of
+        Left  err -> print err
+        Right res -> T.putStrLn (pretty res)
+  where
+    ts = init (resolveLayout True (myLexer s))
+    showPosToken ((l,c),t) = concat [ show l, ":", show c, "\t", show t ]
+
 main :: IO ()
-main = pure ()
+main = T.getContents >>= inferType
diff --git a/hm.cabal b/hm.cabal
index bce427a..3a24acd 100644
--- a/hm.cabal
+++ b/hm.cabal
@@ -31,6 +31,7 @@ library
                      , Type
                      , Misc
                      , PostProcess
+                     , Pretty
 
   other-modules:       Hm.ErrM
   build-tool-depends:  alex:alex >= 3.0, happy:happy >= 1.19.5
@@ -45,6 +46,6 @@ library
 
 executable sexprml
   main-is:             Main.hs
-  build-depends:       base >=4, hm
+  build-depends:       base >=4, hm, text, containers
   hs-source-dirs:      app
   default-language:    Haskell2010
diff --git a/hm.cf b/hm.cf
index 8d0234d..83e95da 100644
--- a/hm.cf
+++ b/hm.cf
@@ -25,16 +25,15 @@ coercions TypeSig 2;
 
 separator nonempty TypeSig2 "" ;
 
-ExpLet.   Exp  ::= "let" "{" [Assign] "}" "in" Exp2 ;
-ExpTyped. Exp1 ::= Exp2 ":" TypeSig ;
-ExpAbs.   Exp2 ::= "λ" [Id] "." Exp3 ;
-ExpApp.   Exp3 ::= Exp4 [Exp4] ;
-ExpVar.   Exp4 ::= Id ;
+ExpLet.   Exp  ::= "let" "{" [Assign] "}" "in" Exp1 ;
+ExpAbs.   Exp1 ::= "λ" [Id] "." Exp1 ;
+ExpApp.   Exp1 ::= Exp2 [Exp2] ;
+ExpVar.   Exp2 ::= Id ;
 
-Assign. Assign ::= Id "=" Exp1 ;
+Assign. Assign ::= Id ":=" Exp ;
 separator nonempty Assign ";" ;
 
-separator nonempty Exp4 "" ;
-coercions Exp 4 ;
+separator nonempty Exp2 "" ;
+coercions Exp 2 ;
 
 separator nonempty Id "" ;
diff --git a/src/PostProcess.hs b/src/PostProcess.hs
index d776689..f2afb14 100644
--- a/src/PostProcess.hs
+++ b/src/PostProcess.hs
@@ -37,8 +37,10 @@ addDef = \case
 
 -- add type before typesig to id params
 defToTL :: H.Def -> Process TL
-defToTL (H.VarDef p i t e) = VarDef p i <$> typeSigToPolyT t <*> expToExp e
+defToTL (H.VarDef p i t e) = VarDef <$> lift (setPos p) <*> pure i <*> typeSigToPolyT t <*> expToExp e
 defToTL (H.TypeDef p t ds) = do 
+    _ <- lift (setPos p)
+
     (i,_) <- typeSigToIdParams t
 
     let (Id s) = i
@@ -47,7 +49,7 @@ defToTL (H.TypeDef p t ds) = do
     let env = M.fromList (map (\(i,m) -> (i, Mono m)) monoT)
 
     -- check that all constructors construct correct type
-    mapM_ (guard (throwError (InvalidConstructor p)) . constructs i . snd) monoT
+    mapM_ (guard (throwError (InvalidConstructor)) . constructs i . snd) monoT
 
     -- check that there are no unbound variables
     guard (throwError (Unimplemented "Type parameters")) (free env == S.empty)
@@ -69,10 +71,10 @@ defToTL (H.TypeDef p t ds) = do
 
 
 typeSigToIdParams :: H.TypeSig -> Process (Id, [Id])
-typeSigToIdParams = \case
-  H.TypeFun p _ _ -> throwError (InvalidTypeDecl p)
-  H.TypeApp {}    -> throwError (Unimplemented "Type parameters")
-  H.TypeVar _ i   -> pure (i, [])
+typeSigToIdParams = lift . setPos >=> \case
+  H.TypeFun{}   -> throwError InvalidTypeDecl
+  H.TypeApp{}   -> throwError (Unimplemented "Type parameters")
+  H.TypeVar _ i -> pure (i, [])
 
 typeSigToPolyT :: H.TypeSig -> Process PolyT
 typeSigToPolyT t = typeSigToMonoT t >>= lift . generalize
@@ -89,9 +91,13 @@ typeSigToMonoT = \case
 expToExp :: H.Exp -> Process Exp
 expToExp = \case
   H.ExpLet p as e  -> Let p <$> assignTo2pl <~> as <*> expToExp e
-  H.ExpTyped p e t -> Typed p <$> expToExp e <*> typeSigToMonoT t
   H.ExpAbs p is e  -> Abs p is <$> expToExp e
-  H.ExpApp p e es  -> App p <$> expToExp e <*> expToExp <~> es
+  H.ExpApp p e1 (e2:es)  -> do
+    e1' <- expToExp e1
+    e2' <- expToExp e2
+    es' <- traverse expToExp es
+    pure (foldl (App p) (App p e1' e2') es')
+  H.ExpApp p e []  -> throwError Oop
   H.ExpVar p i     -> pure (Var p i)
 
 declTo2pl :: H.Decl -> Process (Id, MonoT)
diff --git a/src/Pretty.hs b/src/Pretty.hs
new file mode 100644
index 0000000..a92e083
--- /dev/null
+++ b/src/Pretty.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE OverloadedStrings, LambdaCase #-}
+module Pretty (Pretty(..)) where
+
+import Data.Text (Text)
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+
+import Type
+import Data.List (sort)
+import TC (initialState, apply, free)
+
+class Pretty a where
+  pretty :: a -> Text
+
+instance Pretty PolyT where
+  pretty t = case normalize t of
+    Forall s t -> "∀" <> foldMap (\(Id v) -> " " <> v) s <> ": " <> pretty t
+    Mono t     -> pretty t
+
+instance Pretty MonoT where
+  pretty = go . normalize
+    where
+      go = \case
+        TArr tl@TArr{} tr -> "(" <> go tl <> ") → " <> go tr
+        TArr tl tr        ->        go tl <>  " → " <> go tr
+        TVar (Id i)       -> i
+        TCon (Id i)       -> i
+
+class Normalize a where
+  normalize :: a -> a
+
+instance Normalize PolyT where
+  normalize = \case
+      Forall i t -> Forall (S.fromList (snd <$> go t)) (normalize t)
+      t@Mono{}   -> normalize t
+
+instance Normalize MonoT where
+  normalize t = apply (goS t) t
+
+go :: MonoT -> [(Id, Id)]
+go t = zip (sort (S.toList (free t))) (variables initialState)
+
+goS :: MonoT -> Subst
+goS = M.fromList . map (\(x,y) -> (x, TVar y)) . go
diff --git a/src/TC.hs b/src/TC.hs
index a7ea5a6..e96e408 100644
--- a/src/TC.hs
+++ b/src/TC.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE LambdaCase, TypeSynonymInstances, FlexibleInstances #-}
+{-# LANGUAGE LambdaCase, TypeSynonymInstances #-}
+{-# LANGUAGE TupleSections, FlexibleInstances #-}
 module TC where
 
 import Control.Monad.Reader hiding (guard)
@@ -19,8 +20,8 @@ import Prelude hiding (map)
 map :: Functor f => (a -> b) -> f a -> f b
 map = fmap
 
-runCheck :: CheckState -> Check a -> Either TypeError a
-runCheck s = fst . (flip runState) s . runExceptT . getCheck
+runCheck :: CheckState -> Check a -> (Either TypeError a, CheckState)
+runCheck s = (flip runState) s . runExceptT . getCheck
 
 -- I'm still not quite sure how replicateM works, but in this instance it is
 -- used to generate a list of strings "a", "b" ... "z", "aa", "ab" ... so on
@@ -44,6 +45,16 @@ setEnv env = get >>= \s -> put (CS (variables s) (lastPos s) env)
 addEnv :: Id -> PolyT -> Check ()
 addEnv i p = getEnv >>= setEnv . M.insert i p
 
+localEnv :: TypeEnv -> Check a -> Check a
+localEnv e m = getEnv >>= \o -> setEnv e >> m >>= \r -> setEnv o >> pure r
+
+localEnv' :: Check a -> Check a
+localEnv' m = getEnv >>= \o -> m >>= \r -> setEnv o >> pure r
+
+-- returns p again to allow chaining into lambdacase
+setPos :: Positioned p => p -> Check p
+setPos p = get >>= \s -> put (CS (variables s) (pos p) (typeEnv s)) >> pure p
+
 guard :: Applicative f => f () -> Bool -> f ()
 guard _ True = pure ()
 guard f False = f
@@ -80,6 +91,9 @@ instance Substitutable a => Substitutable [a] where
   apply = map . apply
   free  = foldMap free
 
+applyEnv :: Subst -> Check ()
+applyEnv s = getEnv >>=  setEnv . apply s
+
 -- This substution, and that one
 (<&>) :: Subst -> Subst -> Subst
 (<&>) s1 s2 = map (apply s1) s2 <> s1
@@ -128,10 +142,36 @@ lookupType i = getEnv >>= \env ->
     Nothing -> throwError (UnboundVariable i)
     Just t  -> instantiate t
 
-infer :: Exp -> Check MonoT
-infer = undefined
-
 constructs :: Id -> MonoT -> Bool
 constructs i (TArr _ t) = constructs i t
 constructs i1 (TCon i2) = i1 == i2
 constructs _ _          = False
+
+infer :: Exp -> Check (Subst, MonoT)
+infer = setPos >=> \case
+  Let   _ [] e            -> infer e
+  Let   p ((i,e1):ies) e2 -> do
+    (s1, t1) <- infer e1
+    apply s1 <$> getEnv >>= \e -> localEnv e $ do
+      t1g <- generalize t1
+      addEnv i t1g
+      (s2, t2) <- infer (Let p ies e2)
+      pure (s2 <&> s1, t2)
+
+  Abs   _ [] e     -> infer e
+  Abs   p (i:is) e -> localEnv' $ do
+    tv <- fresh
+    addEnv i (Forall S.empty tv)
+    (s, t) <- infer (Abs p is e)
+    pure (s, apply s tv `TArr` t)
+
+  App   p e1 e2 -> localEnv' $ do
+    tv <- fresh
+    (s1, t1) <- infer e1
+    applyEnv s1
+    (s2, t2) <- infer e2
+    s3       <- unify (apply s2 t1) (TArr t2 tv)
+    return (s3 <&> s2 <&> s1, apply s3 tv)
+  App   _ _ _ -> throwError Oop
+
+  Var   _ i   -> (emptySubst,) <$> lookupType i
diff --git a/src/Type.hs b/src/Type.hs
index 2d65676..c9d141b 100644
--- a/src/Type.hs
+++ b/src/Type.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, LambdaCase #-}
+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 module Type 
   ( module Type
   , Id(..)
@@ -14,6 +15,8 @@ import Data.Text (Text)
 
 import Hm.Abs (Id(..))
 
+import qualified Hm.Abs as H (TypeSig'(..), TypeSig(..))
+
 data PolyT
   = Forall (Set Id) MonoT -- ^ ∀ σ₁ σ₂ … σₙ. τ
   | Mono MonoT        -- ^ τ
@@ -32,14 +35,39 @@ type TL = TL' Pos
 data TL' a
   = TypeDef a Id [Id]  TypeEnv -- ^ name, parameters, constructors and recursor
   | VarDef  a Id PolyT Exp     -- ^ name, declared type, expression
+  deriving Show
 
 type Exp = Exp' Pos
 data Exp' a
-  = Typed a Exp MonoT
-  | Let a [(Id, Exp)] Exp
+  = Let a [(Id,Exp)] Exp
   | Abs a [Id] Exp
-  | App a Exp [Exp]
+  | App a Exp Exp
   | Var a Id
+  deriving Show
+
+class Positioned p where
+  pos :: p -> Pos
+
+instance Positioned TL where
+  pos = \case
+    TypeDef p _ _ _ -> p
+    VarDef  p _ _ _ -> p
+
+instance Positioned Exp where
+  pos = \case
+    Let   p _ _ -> p
+    Abs   p _ _ -> p
+    App   p _ _ -> p
+    Var   p _   -> p
+
+instance Positioned Pos where
+  pos = id
+
+instance Positioned H.TypeSig where
+  pos = \case
+    H.TypeFun p _ _ -> p
+    H.TypeApp p _ _ -> p
+    H.TypeVar p _   -> p
 
 data TypeError
   = Oop -- ^ compiler error (oops)
@@ -47,8 +75,9 @@ data TypeError
   | InfiniteType Id MonoT
   | UnboundVariable Id
   | Unimplemented Text
-  | InvalidTypeDecl Pos
-  | InvalidConstructor Pos
+  | InvalidTypeDecl
+  | InvalidConstructor
+  | ArityMismatch
   deriving Show
 
 type TypeEnv = Map Id PolyT