diff --git a/TODO b/TODO
index 57efb6c..4cb036f 100644
--- a/TODO
+++ b/TODO
@@ -9,4 +9,8 @@ terminates by forbidding corecursion (simply done by building a reference graph
 
 3) Add Kind env and use it to have "type of types"
 
-4) Then make the SECD machine good enough to execute it :)
+4) Type annotated tree?
+
+5) Make SECD machine good enough to execute it
+
+6) Write backend for SECD machine code
diff --git a/hm.cabal b/hm.cabal
index dc39041..bce427a 100644
--- a/hm.cabal
+++ b/hm.cabal
@@ -27,6 +27,10 @@ library
                      , Hm.Lex
                      , Hm.Par
                      , Hm.Print
+                     , TC
+                     , Type
+                     , Misc
+                     , PostProcess
 
   other-modules:       Hm.ErrM
   build-tool-depends:  alex:alex >= 3.0, happy:happy >= 1.19.5
diff --git a/hm.cf b/hm.cf
index 2bc8a04..8d0234d 100644
--- a/hm.cf
+++ b/hm.cf
@@ -31,7 +31,7 @@ ExpAbs.   Exp2 ::= "λ" [Id] "." Exp3 ;
 ExpApp.   Exp3 ::= Exp4 [Exp4] ;
 ExpVar.   Exp4 ::= Id ;
 
-Assign. Assign ::= Ident "=" Exp1 ;
+Assign. Assign ::= Id "=" Exp1 ;
 separator nonempty Assign ";" ;
 
 separator nonempty Exp4 "" ;
diff --git a/src/Misc.hs b/src/Misc.hs
new file mode 100644
index 0000000..8098016
--- /dev/null
+++ b/src/Misc.hs
@@ -0,0 +1,23 @@
+module Misc where
+
+import Data.Map (Map)
+import Data.Set (Set)
+import qualified Data.Set as S
+import qualified Data.Map as M
+
+import Data.Maybe (fromMaybe)
+
+lookupDefault :: Ord k => a -> k -> Map k a -> a
+lookupDefault d k m = fromMaybe d (M.lookup k m)
+
+infixl \\
+(\\) :: Ord a => Set a -> Set a -> Set a
+(\\) = S.difference
+
+infix 5 <~>
+(<~>) :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
+(<~>) = traverse
+
+infixr 9 .:
+(.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d
+(.:) = (.) . (.)
diff --git a/src/PostProcess.hs b/src/PostProcess.hs
new file mode 100644
index 0000000..d776689
--- /dev/null
+++ b/src/PostProcess.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE TupleSections, LambdaCase, OverloadedStrings #-}
+module PostProcess where
+
+import Control.Monad.State  hiding (guard)
+import Control.Monad.Except hiding (guard)
+
+import Data.Map (Map)
+import Data.Set (Set)
+import Data.Text (Text)
+
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+import qualified Hm.Abs as H
+import Type
+import Misc
+import TC
+
+import Prelude hiding (map)
+
+-- Type env for parsing type signatures
+type Process = StateT (Set Id) Check
+
+insertType :: Id -> Process ()
+insertType i = get >>= put . S.insert i
+
+runProcess :: Process a -> Set Id -> Check a
+runProcess = (fst <$>) .: runStateT
+
+postprocess :: [H.Def] -> Process [TL]
+postprocess defs = addDef <~> defs >> defToTL <~> defs
+
+addDef :: H.Def -> Process ()
+addDef = \case
+  H.VarDef _ i t _ -> lift . addEnv i =<< typeSigToPolyT t -- the type checker will check this matches the exp
+  H.TypeDef _ t _  -> insertType =<< fst <$> typeSigToIdParams t
+
+-- 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.TypeDef p t ds) = do 
+    (i,_) <- typeSigToIdParams t
+
+    let (Id s) = i
+
+    monoT <- declTo2pl <~> ds
+    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
+
+    -- check that there are no unbound variables
+    guard (throwError (Unimplemented "Type parameters")) (free env == S.empty)
+
+    -- add recursor to env
+    tv <- lift fresh
+
+    let replace = \case {
+        TArr l r -> TArr (replace l) (replace r) ;
+        TCon i'  -> if i' == i then tv else TCon i' ;
+        TVar i'  -> TVar i' ;
+      }
+
+    recType <- lift . generalize . foldr TArr (tv `TArr` TCon i) . reverse . map (replace . snd) $ monoT
+
+    let env' = M.insert (Id ("rec[" <> s <> "]")) recType env
+
+    pure (TypeDef p i [] env')
+
+
+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, [])
+
+typeSigToPolyT :: H.TypeSig -> Process PolyT
+typeSigToPolyT t = typeSigToMonoT t >>= lift . generalize
+
+typeSigToMonoT :: H.TypeSig -> Process MonoT
+typeSigToMonoT = \case
+  H.TypeFun _ t1 t2 -> typeSigToMonoT t1 >>= (<$> typeSigToMonoT t2) . TArr
+  H.TypeApp {}      -> throwError (Unimplemented "Type parameters")
+  H.TypeVar _ i     -> get >>= \s -> pure $
+                         if S.member i s
+                            then TCon i
+                            else TVar i
+
+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.ExpVar p i     -> pure (Var p i)
+
+declTo2pl :: H.Decl -> Process (Id, MonoT)
+declTo2pl (H.Decl _ i t) = (i,) <$> typeSigToMonoT t
+
+assignTo2pl :: H.Assign -> Process (Id, Exp)
+assignTo2pl (H.Assign _ i e) = (i,) <$> expToExp e
diff --git a/src/TC.hs b/src/TC.hs
new file mode 100644
index 0000000..a7ea5a6
--- /dev/null
+++ b/src/TC.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE LambdaCase, TypeSynonymInstances, FlexibleInstances #-}
+module TC where
+
+import Control.Monad.Reader hiding (guard)
+import Control.Monad.State  hiding (guard)
+import Control.Monad.Except hiding (guard)
+
+import Data.Set (Set)
+import qualified Data.Set as S
+import qualified Data.Map as M
+
+import qualified Data.Text as T
+
+import Type
+import Misc
+
+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
+
+-- 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
+--
+-- Does it make sense to start with an empty state?
+initialState :: CheckState
+initialState = CS ([1..] >>= map (Id . T.pack) . flip replicateM ['a'..'z']) Nothing M.empty
+
+getVars :: Check [Id]
+getVars = variables <$> get
+
+setVars :: [Id] -> Check ()
+setVars ids = get >>= \s -> put (CS ids (lastPos s) (typeEnv s))
+
+getEnv :: Check TypeEnv
+getEnv = typeEnv <$> get
+
+setEnv :: TypeEnv -> Check ()
+setEnv env = get >>= \s -> put (CS (variables s) (lastPos s) env)
+
+addEnv :: Id -> PolyT -> Check ()
+addEnv i p = getEnv >>= setEnv . M.insert i p
+
+guard :: Applicative f => f () -> Bool -> f ()
+guard _ True = pure ()
+guard f False = f
+
+class Substitutable a where
+  apply :: Subst -> a -> a -- ^ apply a substitution
+  free   :: a -> Set Id    -- ^ free type variables
+
+instance Substitutable MonoT where
+  apply s = \case
+    TCon i -> TCon i
+    TVar i -> lookupDefault (TVar i) i s
+    (t1 `TArr` t2) -> apply s t1 `TArr` apply s t2
+
+  free = \case
+    TCon{} -> S.empty
+    TVar i -> S.singleton i
+    (t1 `TArr` t2) -> free t1 <> free t2
+
+instance Substitutable PolyT where
+  apply s = \case
+    Forall as t -> Forall as (apply (foldr M.delete s as) t)
+    Mono t -> Mono (apply s t)
+
+  free = \case
+    Forall as t -> free t \\ as
+    Mono t -> free t
+
+instance Substitutable TypeEnv where
+  apply s = map (apply s)
+  free    = free . M.elems
+
+instance Substitutable a => Substitutable [a] where
+  apply = map . apply
+  free  = foldMap free
+
+-- This substution, and that one
+(<&>) :: Subst -> Subst -> Subst
+(<&>) s1 s2 = map (apply s1) s2 <> s1
+
+emptySubst :: Subst
+emptySubst = M.empty
+
+unify :: MonoT -> MonoT -> Check Subst
+unify (l1 `TArr` r1) (l2 `TArr` r2) = do
+  s1 <- unify l1 l2
+  s2 <- unify (apply s1 r1) (apply s1 r2)
+  pure (s1 <&> s2)
+
+unify (TVar i) t = bind i t
+unify t (TVar i) = bind i t
+
+unify (TCon i1) (TCon i2) | i1 == i2 = pure emptySubst
+
+unify t1 t2 = throwError (UnificationFailure t1 t2)
+
+bind :: Id -> MonoT -> Check Subst
+bind i1 (TVar i2) | i1 == i2            = pure emptySubst
+bind i t          | S.member i (free t) = throwError (InfiniteType i t)
+                  | otherwise           = pure (M.singleton i t)
+
+fresh :: Check MonoT
+fresh = do
+  (var:vars) <- getVars
+  setVars vars
+  pure (TVar var)
+
+-- replace polymorphic type variables with monomorphic ones
+instantiate :: PolyT -> Check MonoT
+instantiate (Mono t) = pure t
+instantiate (Forall is t) = foldM freshInsert emptySubst is >>= pure . (flip apply) t
+  where
+    freshInsert :: Subst -> Id -> Check Subst
+    freshInsert s k = (\a -> M.insert k a s) <$> fresh
+
+generalize :: MonoT -> Check PolyT
+generalize t = getEnv >>= \env -> pure (Forall (free t \\ free env) t)
+
+lookupType :: Id -> Check MonoT
+lookupType i = getEnv >>= \env ->
+  case M.lookup i env of
+    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
diff --git a/src/Type.hs b/src/Type.hs
new file mode 100644
index 0000000..2d65676
--- /dev/null
+++ b/src/Type.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+module Type 
+  ( module Type
+  , Id(..)
+  ) where
+
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.Monad.Except
+
+import Data.Map (Map)
+import Data.Set (Set)
+import Data.Text (Text)
+
+import Hm.Abs (Id(..))
+
+data PolyT
+  = Forall (Set Id) MonoT -- ^ ∀ σ₁ σ₂ … σₙ. τ
+  | Mono MonoT        -- ^ τ
+  deriving Show
+
+infixr `TArr`
+data MonoT
+  = TArr MonoT MonoT -- ^ function
+  | TVar Id          -- ^ variable
+  | TCon Id          -- ^ constant
+  deriving Show
+
+type Pos = Maybe (Int, Int)
+
+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
+
+type Exp = Exp' Pos
+data Exp' a
+  = Typed a Exp MonoT
+  | Let a [(Id, Exp)] Exp
+  | Abs a [Id] Exp
+  | App a Exp [Exp]
+  | Var a Id
+
+data TypeError
+  = Oop -- ^ compiler error (oops)
+  | UnificationFailure MonoT MonoT
+  | InfiniteType Id MonoT
+  | UnboundVariable Id
+  | Unimplemented Text
+  | InvalidTypeDecl Pos
+  | InvalidConstructor Pos
+  deriving Show
+
+type TypeEnv = Map Id PolyT
+
+type Subst = Map Id MonoT
+
+data CheckState = CS { variables :: [Id] 
+                     , lastPos :: Pos
+                     , typeEnv :: TypeEnv
+                     } deriving Show
+
+newtype Check a = Check { getCheck :: ExceptT TypeError (State CheckState) a }
+  deriving (Functor, Applicative, Monad, MonadError TypeError, MonadState CheckState)
+
+instance MonadFail Check where
+  fail _ = throwError Oop