diff --git a/src/Renamer/Renamer.hs b/src/Renamer/Renamer.hs
index 66c8fb2..3fa1afc 100644
--- a/src/Renamer/Renamer.hs
+++ b/src/Renamer/Renamer.hs
@@ -7,7 +7,7 @@ module Renamer.Renamer (rename) where
 
 import Auxiliary (mapAccumM)
 import Control.Applicative (Applicative (liftA2))
-import Control.Monad.Except (ExceptT, runExceptT)
+import Control.Monad.Except (ExceptT, MonadError, runExceptT, throwError)
 import Control.Monad.Identity (Identity, runIdentity)
 import Control.Monad.State (
     MonadState,
@@ -41,19 +41,21 @@ renameDefs defs = runIdentity $ runExceptT $ evalStateT (runRn $ mapM renameDef
             rhs' <- snd <$> renameExp new_names rhs
             pure . DBind $ Bind name (coerce vars') rhs'
         DData (Data (Indexed cname types) constrs) -> do
-            tvars' <- mapM nextNameTVar tvars
-            let tvars_lt = zip tvars tvars'
+            tvars_ <- tvars
+            tvars' <- mapM nextNameTVar tvars_
+            let tvars_lt = zip tvars_ tvars'
                 typ' = map (substituteTVar tvars_lt) types
                 constrs' = map (renameConstr tvars_lt) constrs
             pure . DData $ Data (Indexed cname typ') constrs'
           where
-            tvars = concatMap (collectTVars []) types
+            tvars = concat <$> mapM (collectTVars []) types
+            collectTVars :: [TVar] -> Type -> Rn [TVar]
             collectTVars tvars = \case
                 TAll tvar t -> collectTVars (tvar : tvars) t
-                TIndexed _ -> tvars
+                TIndexed _ -> return tvars
                 -- Should be monad error
-                TVar v -> [v]
-                _ -> error ("Bad data type definition: " ++ show types)
+                TVar v -> return [v]
+                _ -> throwError ("Bad data type definition: " ++ show types)
 
     renameConstr :: [(TVar, TVar)] -> Constructor -> Constructor
     renameConstr new_types (Constructor name typ) =
@@ -88,7 +90,7 @@ data Cxt = Cxt
 
 -- | Rename monad. State holds the number of renamed names.
 newtype Rn a = Rn {runRn :: StateT Cxt (ExceptT String Identity) a}
-    deriving (Functor, Applicative, Monad, MonadState Cxt)
+    deriving (Functor, Applicative, Monad, MonadState Cxt, MonadError String)
 
 -- | Maps old to new name
 type Names = Map LIdent LIdent
diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs
index 7da23a6..2bab6c8 100644
--- a/src/TypeChecker/TypeChecker.hs
+++ b/src/TypeChecker/TypeChecker.hs
@@ -77,7 +77,9 @@ checkPrg :: Program -> Infer T.Program
 checkPrg (Program bs) = do
     preRun bs
     -- Type check the program twice to produce all top-level types in the first pass through
-    _ <- checkDef bs
+    bs' <- checkDef bs
+    trace "\nFIRST ITERATION" return ()
+    trace (printTree bs' ++ "\nSECOND ITERATION\n") return ()
     bs'' <- checkDef bs
     return $ T.Program bs''
   where
@@ -107,8 +109,6 @@ checkBind (Bind name args e) = do
     let lambda = makeLambda e (reverse $ coerce args)
     e@(_, t') <- inferExp lambda
     s <- gets sigs
-    -- let fs = map (second Just) $ getFunctionTypes s e
-    -- mapM_ (uncurry insertSig) fs
     case M.lookup (coerce name) s of
         Just (Just t) -> do
             sub <- unify t t'
@@ -122,18 +122,6 @@ checkBind (Bind name args e) = do
     makeLambda :: Exp -> [Ident] -> Exp
     makeLambda = foldl (flip (EAbs . coerce))
 
-    -- getFunctionTypes :: Map Ident (Maybe T.Type) -> T.ExpT -> [(Ident, T.Type)]
-    -- getFunctionTypes s = \case
-    --     (T.EId b, t) -> case M.lookup b s of
-    --         Just Nothing -> return (b, t)
-    --         _ -> []
-    --     (T.ELit _, _) -> []
-    --     (T.ELet (T.Bind _ _ e1) e2, _) -> getFunctionTypes s e1 ++ getFunctionTypes s e2
-    --     (T.EApp e1 e2, _) -> getFunctionTypes s e1 ++ getFunctionTypes s e2
-    --     (T.EAdd e1 e2, _) -> getFunctionTypes s e1 ++ getFunctionTypes s e2
-    --     (T.EAbs _ e, _) -> getFunctionTypes s e
-    --     (T.ECase e injs, _) -> getFunctionTypes s e ++ concatMap (getFunctionTypes s . \(T.Inj _ e) -> e) injs
-
 isMoreSpecificOrEq :: T.Type -> T.Type -> Bool
 isMoreSpecificOrEq _ (T.TAll _ _) = True
 isMoreSpecificOrEq (T.TFun a b) (T.TFun c d) =
@@ -231,7 +219,7 @@ algoW = \case
             (s1, (e', t')) <- algoW e
             let varType = apply s1 fr
             let newArr = T.TFun varType t'
-            return (s1, apply s1 (T.EAbs (coerce name, varType) (e', t'), newArr))
+            return (s1, apply s1 (T.EAbs (coerce name) (e', t'), newArr))
 
     -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S₁
     -- \| s₂ = mgu(s₁τ₀, Int)    s₃ = mgu(s₂τ₁, Int)
@@ -424,7 +412,7 @@ instance FreeVars T.ExpT where
         (T.ELet (T.Bind (ident, t1) args e1) e2, t2) -> (T.ELet (T.Bind (ident, apply s t1) args (apply s e1)) (apply s e2), apply s t2)
         (T.EApp e1 e2, t) -> (T.EApp (apply s e1) (apply s e2), apply s t)
         (T.EAdd e1 e2, t) -> (T.EAdd (apply s e1) (apply s e2), apply s t)
-        (T.EAbs (ident, t2) e, t1) -> (T.EAbs (ident, apply s t2) (apply s e), apply s t1)
+        (T.EAbs ident e, t1) -> (T.EAbs ident (apply s e), apply s t1)
         (T.ECase e injs, t) -> (T.ECase (apply s e) (apply s injs), apply s t)
 
 instance FreeVars T.Inj where
diff --git a/src/TypeChecker/TypeCheckerIr.hs b/src/TypeChecker/TypeCheckerIr.hs
index 7c24ab3..03a2065 100644
--- a/src/TypeChecker/TypeCheckerIr.hs
+++ b/src/TypeChecker/TypeCheckerIr.hs
@@ -52,7 +52,7 @@ data Exp
     | ELet Bind ExpT
     | EApp ExpT ExpT
     | EAdd ExpT ExpT
-    | EAbs Id ExpT
+    | EAbs Ident ExpT
     | ECase ExpT [Inj]
     deriving (C.Eq, C.Ord, C.Read, C.Show)
 
@@ -156,7 +156,7 @@ instance Print Exp where
             prPrec i 0 $
                 concatD
                     [ doc $ showString "λ"
-                    , prtId 0 n
+                    , prt 0 n
                     , doc $ showString "."
                     , prt 0 e
                     ]