diff --git a/Grammar.cf b/Grammar.cf
index 356646d..27dfd05 100644
--- a/Grammar.cf
+++ b/Grammar.cf
@@ -1,12 +1,13 @@
---------------------------------------------------------------------------------
+
+-------------------------------------------------------------------------------
 -- * PROGRAM
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 
 Program. Program ::= [Def] ;
 
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- * TOP-LEVEL
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 
 DBind. Def ::= Bind ;
 DSig.  Def ::= Sig ;
@@ -16,9 +17,9 @@ Sig. Sig ::= LIdent ":" Type ;
 
 Bind. Bind ::= LIdent [LIdent] "=" Exp ;
 
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- * TYPES
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 
          TLit.     Type2 ::= UIdent ;
          TVar.     Type2 ::= TVar ;
@@ -30,9 +31,9 @@ internal TEVar.    Type1 ::= TEVar ;
          MkTVar.  TVar  ::= LIdent ;
 internal MkTEVar. TEVar ::= LIdent ;
 
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- * DATA TYPES
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 
 Constructor. Constructor ::= UIdent ":" Type ;
 
@@ -40,12 +41,12 @@ Indexed. Indexed ::= UIdent "(" [Type] ")" ;
 
 Data. Data ::= "data" Indexed "where" "{" [Constructor] "}" ;
 
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- * EXPRESSIONS
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 
 EAnn.   Exp5 ::= "(" Exp ":" Type ")" ;
-EId.    Exp4 ::= LIdent ;
+EId.    Exp4 ::= Ident ;
 ELit.   Exp4 ::= Lit ;
 EApp.   Exp3 ::= Exp3 Exp4 ;
 EAdd.   Exp1 ::= Exp1 "+" Exp2 ;
@@ -53,16 +54,16 @@ ELet.   Exp  ::= "let" LIdent "=" Exp "in" Exp ;
 EAbs.   Exp  ::= "\\" LIdent "." Exp ;
 ECase.  Exp  ::= "case" Exp "of" "{" [Inj] "}";
 
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- * LITERALS
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 
 LInt. Lit ::= Integer ;
 LChar. Lit ::= Char ;
 
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- * CASE
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 
 Inj. Inj ::= Init "=>" Exp ;
 
@@ -70,9 +71,9 @@ InitLit. Init         ::= Lit ;
 InitConstructor. Init ::= UIdent [LIdent] ;
 InitCatch. Init       ::= "_" ;
 
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- * AUX
---------------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 
 separator Def ";" ;
 separator nonempty Constructor "" ;
@@ -80,6 +81,7 @@ separator Type " " ;
 separator nonempty Inj ";" ;
 separator Ident " ";
 separator LIdent " ";
+separator TVar " " ;
 
 coercions Exp 5 ;
 coercions Type 2 ;
diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs
index 4e072d2..4b9269d 100644
--- a/src/TypeChecker/TypeChecker.hs
+++ b/src/TypeChecker/TypeChecker.hs
@@ -4,543 +4,518 @@
 -- | A module for type checking and inference using algorithm W, Hindley-Milner
 module TypeChecker.TypeChecker where
 
--- import Control.Monad.Except
--- import Control.Monad.Reader
--- import Control.Monad.State
--- import Data.Bifunctor (second)
--- import Data.Foldable (traverse_)
--- import Data.Functor.Identity (runIdentity)
--- import Data.List (foldl')
--- import Data.List.Extra (unsnoc)
--- import Data.Map (Map)
--- import Data.Map qualified as M
--- import Data.Maybe (fromMaybe)
--- import Data.Set (Set)
--- import Data.Set qualified as S
--- import Debug.Trace (trace)
--- import Grammar.Abs
--- import Grammar.Print (printTree)
--- import TypeChecker.TypeCheckerIr (
---     Ctx (..),
---     Env (..),
---     Error,
---     Infer,
---     Poly (..),
---     Subst,
---  )
--- import TypeChecker.TypeCheckerIr qualified as T
+import Control.Monad.Except
+import Control.Monad.Reader
+import Control.Monad.State
+import Data.Bifunctor (second)
+import Data.Coerce (coerce)
+import Data.Foldable (traverse_)
+import Data.Functor.Identity (runIdentity)
+import Data.List (foldl')
+import Data.List.Extra (unsnoc)
+import Data.Map (Map)
+import Data.Map qualified as M
+import Data.Maybe (fromMaybe)
+import Data.Set (Set)
+import Data.Set qualified as S
+import Debug.Trace (trace)
+import Grammar.Abs
+import Grammar.Print (printTree)
+import TypeChecker.TypeCheckerIr (
+    Ctx (..),
+    Env (..),
+    Error,
+    Infer,
+    Poly (..),
+    Subst,
+ )
+import TypeChecker.TypeCheckerIr qualified as T
 
--- initCtx = Ctx mempty
+initCtx = Ctx mempty
 
--- initEnv = Env 0 mempty mempty
+initEnv = Env 0 mempty mempty
 
--- runPretty :: Exp -> Either Error String
--- runPretty = fmap (printTree . fst) . run . inferExp
+runPretty :: Exp -> Either Error String
+runPretty = fmap (printTree . fst) . run . inferExp
 
--- run :: Infer a -> Either Error a
--- run = runC initEnv initCtx
+run :: Infer a -> Either Error a
+run = runC initEnv initCtx
 
--- runC :: Env -> Ctx -> Infer a -> Either Error a
--- runC e c = runIdentity . runExceptT . flip runReaderT c . flip evalStateT e
+runC :: Env -> Ctx -> Infer a -> Either Error a
+runC e c = runIdentity . runExceptT . flip runReaderT c . flip evalStateT e
 
--- typecheck :: Program -> Either Error T.Program
--- typecheck = run . checkPrg
+typecheck :: Program -> Either Error T.Program
+typecheck = run . checkPrg
 
--- {- | Start by freshening the type variable of data types to avoid clash with
--- other user defined polymorphic types
--- -}
--- freshenData :: Data -> Infer Data
--- freshenData (Data (Constr name ts) constrs) = do
---     let xs = (S.toList . free) =<< ts
---     frs <- traverse (const fresh) xs
---     let m = M.fromList $ zip xs frs
---     return $
---         Data
---             (Constr name (map (freshenType m) ts))
---             ( map
---                 ( \(Constructor ident t) ->
---                     Constructor ident (freshenType m t)
---                 )
---                 constrs
---             )
+checkData :: Data -> Infer ()
+checkData d = do
+    case d of
+        (Data typ@(Indexed name ts) constrs) -> do
+            unless
+                (all isPoly ts)
+                (throwError $ unwords ["Data type incorrectly declared"])
+            traverse_
+                ( \(Constructor name' t') ->
+                    if TIndexed typ == retType t'
+                        then insertConstr name' t'
+                        else
+                            throwError $
+                                unwords
+                                    [ "return type of constructor:"
+                                    , printTree name
+                                    , "with type:"
+                                    , printTree (retType t')
+                                    , "does not match data: "
+                                    , printTree typ
+                                    ]
+                )
+                constrs
 
--- {- | Freshen all polymorphic variables, regardless of name
+retType :: Type -> Type
+retType (TFun _ t2) = retType t2
+retType a = a
 
-{- | freshenType "d" (a -> b -> c) becomes (d -> d -> d)
--\}
-freshenType :: Map Ident Type -> Type -> Type
-freshenType m t = case t of
-    TPol poly -> fromMaybe (error "bug in \'free\'") (M.lookup poly m)
-    TMono mono -> TMono mono
-    TArr t1 t2 -> TArr (freshenType m t1) (freshenType m t2)
-    TConstr (Constr ident ts) -> TConstr (Constr ident (map (freshenType m) ts))
+checkPrg :: Program -> Infer T.Program
+checkPrg (Program bs) = do
+    preRun bs
+    bs' <- checkDef bs
+    return $ T.Program bs'
+  where
+    preRun :: [Def] -> Infer ()
+    preRun [] = return ()
+    preRun (x : xs) = case x of
+        -- TODO: Check for no overlapping signature definitions
+        DSig (Sig n t) -> insertSig n t >> preRun xs
+        DBind (Bind{}) -> preRun xs
+        DData d@(Data _ _) -> checkData d >> preRun xs
+
+    checkDef :: [Def] -> Infer [T.Def]
+    checkDef [] = return []
+    checkDef (x : xs) = case x of
+        (DBind b) -> do
+            b' <- checkBind b
+            fmap (T.DBind b' :) (checkDef xs)
+        (DData d) -> fmap (T.DData d :) (checkDef xs)
+        (DSig _) -> checkDef xs
+
+checkBind :: Bind -> Infer T.Bind
+checkBind (Bind name args e) = do
+    let lambda = makeLambda e (reverse args)
+    e@(_, t') <- inferExp lambda
+    -- TODO: Check for match against existing signatures
+    return $ T.Bind (coerce name, t') [] e -- (apply s e)
+  where
+    makeLambda :: Exp -> [LIdent] -> Exp
+    makeLambda = foldl (flip EAbs)
+
+{- | Check if two types are considered equal
+  For the purpose of the algorithm two polymorphic types are always considered
+  equal
 -}
+typeEq :: Type -> Type -> Bool
+typeEq (TFun l r) (TFun l' r') = typeEq l l' && typeEq r r'
+typeEq (TLit a) (TLit b) = a == b
+typeEq (TIndexed (Indexed name a)) (TIndexed (Indexed name' b)) =
+    length a == length b
+        && name == name'
+        && and (zipWith typeEq a b)
+typeEq (TAll n1 t1) (TAll n2 t2) = t1 `typeEq` t2
+typeEq _ _ = False
 
--- checkData :: Data -> Infer ()
--- checkData d = do
---     d' <- freshenData d
---     case d' of
---         (Data typ@(Constr name ts) constrs) -> do
---             unless
---                 (all isPoly ts)
---                 (throwError $ unwords ["Data type incorrectly declared"])
---             traverse_
---                 ( \(Constructor name' t') ->
---                     if TConstr typ == retType t'
---                         then insertConstr name' t'
---                         else
---                             throwError $
---                                 unwords
---                                     [ "return type of constructor:"
---                                     , printTree name
---                                     , "with type:"
---                                     , printTree (retType t')
---                                     , "does not match data: "
---                                     , printTree typ
---                                     ]
---                 )
---                 constrs
+isMoreSpecificOrEq :: T.Type -> T.Type -> Bool
+isMoreSpecificOrEq _ (T.TAll _ _) = True
+isMoreSpecificOrEq (T.TFun a b) (T.TFun c d) =
+    isMoreSpecificOrEq a c && isMoreSpecificOrEq b d
+isMoreSpecificOrEq (T.TIndexed (T.Indexed n1 ts1)) (T.TIndexed (T.Indexed n2 ts2)) =
+    n1 == n2
+        && length ts1 == length ts2
+        && and (zipWith isMoreSpecificOrEq ts1 ts2)
+isMoreSpecificOrEq a b = a == b
 
--- retType :: Type -> Type
--- retType (TArr _ t2) = retType t2
--- retType a = a
+isPoly :: Type -> Bool
+isPoly (TAll _ _) = True
+isPoly _ = False
 
--- checkPrg :: Program -> Infer T.Program
--- checkPrg (Program bs) = do
---     preRun bs
---     bs' <- checkDef bs
---     return $ T.Program bs'
---   where
---     preRun :: [Def] -> Infer ()
---     preRun [] = return ()
---     preRun (x : xs) = case x of
---         DBind (Bind n t _ _ _) -> insertSig n t >> preRun xs
---         DData d@(Data _ _) -> checkData d >> preRun xs
+inferExp :: Exp -> Infer T.ExpT
+inferExp e = do
+    (s, t, e') <- algoW e
+    let subbed = apply s t
+    return $ replace subbed (e', t)
 
---     checkDef :: [Def] -> Infer [T.Def]
---     checkDef [] = return []
---     checkDef (x : xs) = case x of
---         (DBind b) -> do
---             b' <- checkBind b
---             fmap (T.DBind b' :) (checkDef xs)
---         (DData d) -> do
---             d' <- freshenData d
---             fmap (T.DData d' :) (checkDef xs)
+replace :: T.Type -> T.ExpT -> T.ExpT
+replace t = second (const t)
 
--- checkBind :: Bind -> Infer T.Bind
--- checkBind (Bind n t _ args e) = do
---     let lambda = makeLambda e (reverse args)
---     (t', e) <- inferExp lambda
---     s <- unify t' t
---     let t'' = apply s t
---     unless
---         (t `typeEq` t'')
---         ( throwError $
---             unwords
---                 [ "Top level signature"
---                 , printTree t
---                 , "does not match body with inferred type:"
---                 , printTree t''
---                 ]
---         )
---     return $ T.Bind (n, t) (apply s e)
---   where
---     makeLambda :: Exp -> [Ident] -> Exp
---     makeLambda = foldl (flip EAbs)
+class NewType a b where
+    toNew :: a -> b
 
--- {- | Check if two types are considered equal
---   For the purpose of the algorithm two polymorphic types are always considered
---   equal
--- -}
--- typeEq :: Type -> Type -> Bool
--- typeEq (TArr l r) (TArr l' r') = typeEq l l' && typeEq r r'
--- typeEq (TMono a) (TMono b) = a == b
--- typeEq (TConstr (Constr name a)) (TConstr (Constr name' b)) =
---     length a == length b
---         && name == name'
---         && and (zipWith typeEq a b)
--- typeEq (TPol _) (TPol _) = True
--- typeEq _ _ = False
+instance NewType Type T.Type where
+    toNew = \case
+        TLit i -> T.TLit $ coerce i
+        TVar v -> T.TVar v
+        TFun t1 t2 -> T.TFun (toNew t1) (toNew t2)
+        TAll b t -> T.TAll b (toNew t)
+        TIndexed i -> T.TIndexed (toNew i)
+        TEVar _ -> error "Should not exist after typechecker"
 
--- isMoreSpecificOrEq :: Type -> Type -> Bool
--- isMoreSpecificOrEq _ (TPol _) = True
--- isMoreSpecificOrEq (TArr a b) (TArr c d) =
---     isMoreSpecificOrEq a c && isMoreSpecificOrEq b d
--- isMoreSpecificOrEq (TConstr (Constr n1 ts1)) (TConstr (Constr n2 ts2)) =
---     n1 == n2
---         && length ts1 == length ts2
---         && and (zipWith isMoreSpecificOrEq ts1 ts2)
--- isMoreSpecificOrEq a b = a == b
+instance NewType Indexed T.Indexed where
+    toNew (Indexed name vars) = T.Indexed (coerce name) (map toNew vars)
 
--- isPoly :: Type -> Bool
--- isPoly (TPol _) = True
--- isPoly _ = False
+algoW :: Exp -> Infer (Subst, T.ExpT)
+algoW = \case
+    -- \| TODO: More testing need to be done. Unsure of the correctness of this
+    EAnn e t -> do
+        (s1, (e', t')) <- algoW e
+        unless
+            (toNew t `isMoreSpecificOrEq` t')
+            ( throwError $
+                unwords
+                    [ "Annotated type:"
+                    , printTree t
+                    , "does not match inferred type:"
+                    , printTree t'
+                    ]
+            )
+        applySt s1 $ do
+            s2 <- unify (toNew t) t'
+            let comp = s2 `compose` s1
+            return (comp, (apply comp e', toNew t))
 
--- inferExp :: Exp -> Infer (Type, T.Exp)
--- inferExp e = do
---     (s, t, e') <- algoW e
---     let subbed = apply s t
---     return (subbed, replace subbed e')
+    -- \| ------------------
+    -- \|   Γ ⊢ i : Int, ∅
 
--- replace :: Type -> T.Exp -> T.Exp
--- replace t = \case
---     T.ELit _ e -> T.ELit t e
---     T.EId (n, _) -> T.EId (n, t)
---     T.EAbs _ name e -> T.EAbs t name e
---     T.EApp _ e1 e2 -> T.EApp t e1 e2
---     T.EAdd _ e1 e2 -> T.EAdd t e1 e2
---     T.ELet (T.Bind (n, _) e1) e2 -> T.ELet (T.Bind (n, t) e1) e2
---     T.ECase _ expr injs -> T.ECase t expr injs
+    ELit lit ->
+        let lt = toNew $ litType lit
+         in return (nullSubst, (T.ELit lt lit, lt))
+    -- \| x : σ ∈ Γ   τ = inst(σ)
+    -- \| ----------------------
+    -- \|     Γ ⊢ x : τ, ∅
 
--- algoW :: Exp -> Infer (Subst, Type, T.Exp)
--- algoW = \case
---     -- \| TODO: More testing need to be done. Unsure of the correctness of this
---     EAnn e t -> do
---         (s1, t', e') <- algoW e
---         unless
---             (t `isMoreSpecificOrEq` t')
---             ( throwError $
---                 unwords
---                     [ "Annotated type:"
---                     , printTree t
---                     , "does not match inferred type:"
---                     , printTree t'
---                     ]
---             )
---         applySt s1 $ do
---             s2 <- unify t t'
---             let comp = s2 `compose` s1
---             return (comp, t, apply comp e')
+    EId i -> do
+        var <- asks vars
+        case M.lookup i var of
+            Just t -> inst (toNew t) >>= \x -> return (nullSubst, x, T.EId (i, x))
+            Nothing -> do
+                sig <- gets sigs
+                case M.lookup i sig of
+                    Just t -> return (nullSubst, toNew t, T.EId (i, toNew t))
+                    Nothing -> do
+                        constr <- gets constructors
+                        case M.lookup i constr of
+                            Just t -> return (nullSubst, toNew t, T.EId (i, toNew t))
+                            Nothing ->
+                                throwError $
+                                    "Unbound variable: " ++ show i
 
---     -- \| ------------------
---     -- \|   Γ ⊢ i : Int, ∅
+    -- \| τ = newvar   Γ, x : τ ⊢ e : τ', S
+    -- \| ---------------------------------
+    -- \|     Γ ⊢ w λx. e : Sτ → τ', S
 
---     ELit lit ->
---         let lt = litType lit
---          in return (nullSubst, lt, T.ELit lt lit)
---     -- \| x : σ ∈ Γ   τ = inst(σ)
---     -- \| ----------------------
---     -- \|     Γ ⊢ x : τ, ∅
+    EAbs name e -> do
+        fr <- fresh
+        withBinding (coerce name) (Forall [] (toNew fr)) $ do
+            (s1, t', e') <- algoW e
+            let varType = toNew $ apply s1 fr
+            let newArr = T.TFun varType (toNew t')
+            return (s1, newArr, apply s1 $ T.EAbs newArr (coerce name, varType) (e', newArr))
 
---     EId i -> do
---         var <- asks vars
---         case M.lookup i var of
---             Just t -> inst t >>= \x -> return (nullSubst, x, T.EId (i, x))
---             Nothing -> do
---                 sig <- gets sigs
---                 case M.lookup i sig of
---                     Just t -> return (nullSubst, t, T.EId (i, t))
---                     Nothing -> do
---                         constr <- gets constructors
---                         case M.lookup i constr of
---                             Just t -> return (nullSubst, t, T.EId (i, t))
---                             Nothing ->
---                                 throwError $
---                                     "Unbound variable: " ++ show i
+    -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S₁
+    -- \| s₂ = mgu(s₁τ₀, Int)    s₃ = mgu(s₂τ₁, Int)
+    -- \| ------------------------------------------
+    -- \|        Γ ⊢ e₀ + e₁ : Int, S₃S₂S₁S₀
+    -- This might be wrong
 
---     -- \| τ = newvar   Γ, x : τ ⊢ e : τ', S
---     -- \| ---------------------------------
---     -- \|     Γ ⊢ w λx. e : Sτ → τ', S
+    EAdd e0 e1 -> do
+        (s1, t0, e0') <- algoW e0
+        applySt s1 $ do
+            (s2, t1, e1') <- algoW e1
+            -- applySt s2 $ do
+            s3 <- unify (apply s2 t0) (T.TLit "Int")
+            s4 <- unify (apply s3 t1) (T.TLit "Int")
+            let comp = s4 `compose` s3 `compose` s2 `compose` s1
+            return
+                ( comp
+                , T.TLit "Int"
+                , apply comp $ T.EAdd (T.TLit "Int") (e0', t0) (e1', t1)
+                )
 
---     EAbs name e -> do
---         fr <- fresh
---         withBinding name (Forall [] fr) $ do
---             (s1, t', e') <- algoW e
---             let varType = apply s1 fr
---             let newArr = TArr varType t'
---             return (s1, newArr, apply s1 $ T.EAbs newArr (name, varType) e')
+    -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S1
+    -- \| τ' = newvar    S₂ = mgu(S₁τ₀, τ₁ → τ')
+    -- \| --------------------------------------
+    -- \|       Γ ⊢ e₀ e₁ : S₂τ', S₂S₁S₀
 
---     -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S₁
---     -- \| s₂ = mgu(s₁τ₀, Int)    s₃ = mgu(s₂τ₁, Int)
---     -- \| ------------------------------------------
---     -- \|        Γ ⊢ e₀ + e₁ : Int, S₃S₂S₁S₀
---     -- This might be wrong
+    EApp e0 e1 -> do
+        fr <- toNew <$> fresh
+        (s0, t0, e0') <- algoW e0
+        applySt s0 $ do
+            (s1, t1, e1') <- algoW e1
+            -- applySt s1 $ do
+            s2 <- unify (apply s1 t0) (T.TFun (toNew t1) fr)
+            let t = apply s2 fr
+            let comp = s2 `compose` s1 `compose` s0
+            return (comp, t, apply comp $ T.EApp t (e0', t0) (e1', t1))
 
---     EAdd e0 e1 -> do
---         (s1, t0, e0') <- algoW e0
---         applySt s1 $ do
---             (s2, t1, e1') <- algoW e1
---             -- applySt s2 $ do
---             s3 <- unify (apply s2 t0) (TMono "Int")
---             s4 <- unify (apply s3 t1) (TMono "Int")
---             let comp = s4 `compose` s3 `compose` s2 `compose` s1
---             return
---                 ( comp
---                 , TMono "Int"
---                 , apply comp $ T.EAdd (TMono "Int") e0' e1'
---                 )
+    -- \| Γ ⊢ e₀ : τ, S₀     S₀Γ, x : S̅₀Γ̅(τ) ⊢ e₁ : τ', S₁
+    -- \| ----------------------------------------------
+    -- \|        Γ ⊢ let x = e₀ in e₁ : τ', S₁S₀
 
---     -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S1
---     -- \| τ' = newvar    S₂ = mgu(S₁τ₀, τ₁ → τ')
---     -- \| --------------------------------------
---     -- \|       Γ ⊢ e₀ e₁ : S₂τ', S₂S₁S₀
+    -- The bar over S₀ and Γ means "generalize"
 
---     EApp e0 e1 -> do
---         fr <- fresh
---         (s0, t0, e0') <- algoW e0
---         applySt s0 $ do
---             (s1, t1, e1') <- algoW e1
---             -- applySt s1 $ do
---             s2 <- unify (apply s1 t0) (TArr t1 fr)
---             let t = apply s2 fr
---             let comp = s2 `compose` s1 `compose` s0
---             return (comp, t, apply comp $ T.EApp t e0' e1')
+    ELet name e0 e1 -> do
+        (s1, t1, e0') <- algoW e0
+        env <- asks vars
+        let t' = generalize (apply s1 env) t1
+        withBinding name t' $ do
+            (s2, t2, e1') <- algoW e1
+            let comp = s2 `compose` s1
+            return (comp, t2, apply comp $ T.ELet (T.Bind (name, t2) e0') e1')
+    ECase caseExpr injs -> do
+        (sub, t, e') <- algoW caseExpr
+        (subst, injs, ret_t) <- checkCase t injs
+        let comp = subst `compose` sub
+        let t' = apply comp ret_t
+        return (comp, t', T.ECase t' e' injs)
 
---     -- \| Γ ⊢ e₀ : τ, S₀     S₀Γ, x : S̅₀Γ̅(τ) ⊢ e₁ : τ', S₁
---     -- \| ----------------------------------------------
---     -- \|        Γ ⊢ let x = e₀ in e₁ : τ', S₁S₀
+-- | Unify two types producing a new substitution
+unify :: T.Type -> T.Type -> Infer Subst
+unify t0 t1 = do
+    case (t0, t1) of
+        (T.TFun a b, T.TFun c d) -> do
+            s1 <- unify a c
+            s2 <- unify (apply s1 b) (apply s1 d)
+            return $ s1 `compose` s2
+        (T.TVar t, b) -> occurs b t
+        (a, T.TVar t) -> occurs a t
+        (T.TAll _ t, b) -> unify t b
+        (a, T.TAll _ t) -> unify a t
+        (T.TLit a, T.TLit b) ->
+            if a == b then return M.empty else throwError "Types do not unify"
+        (T.TIndexed (T.Indexed name t), T.TIndexed (T.Indexed name' t')) ->
+            if name == name' && length t == length t'
+                then do
+                    xs <- zipWithM unify t t'
+                    return $ foldr compose nullSubst xs
+                else
+                    throwError $
+                        unwords
+                            [ "T.Type constructor:"
+                            , printT . Tree name
+                            , "(" ++ printT . Tree t ++ ")"
+                            , "does not match with:"
+                            , printT . Tree name'
+                            , "(" ++ printT . Tree t' ++ ")"
+                            ]
+        (a, b) -> do
+            ctx <- ask
+            env <- get
+            throwError . unwords $
+                [ "T.Type:"
+                , printT . Tree a
+                , "can't be unified with:"
+                , printT . Tree b
+                , "\nCtx:"
+                , show ctx
+                , "\nEnv:"
+                , show env
+                ]
 
---     -- The bar over S₀ and Γ means "generalize"
+{- | Check if a type is contained in another type.
+I.E. { a = a -> b } is an unsolvable constraint since there is no substitution
+where these are equal
+-}
+occurs :: LIdent -> T.Type -> Infer Subst
+occurs i t@(T.TVar _) = return (M.singleton i t)
+occurs i t =
+    if S.member i (free t)
+        then
+            throwError $
+                unwords
+                    [ "Occurs check failed, can't unify"
+                    , printTree (TVar $ MkTVar i)
+                    , "with"
+                    , printTree t
+                    ]
+        else return $ M.singleton i t
 
---     ELet name e0 e1 -> do
---         (s1, t1, e0') <- algoW e0
---         env <- asks vars
---         let t' = generalize (apply s1 env) t1
---         withBinding name t' $ do
---             (s2, t2, e1') <- algoW e1
---             let comp = s2 `compose` s1
---             return (comp, t2, apply comp $ T.ELet (T.Bind (name, t2) e0') e1')
---     ECase caseExpr injs -> do
---         (sub, t, e') <- algoW caseExpr
---         (subst, injs, ret_t) <- checkCase t injs
---         let comp = subst `compose` sub
---         let t' = apply comp ret_t
---         return (comp, t', T.ECase t' e' injs)
+-- | Generalize a type over all free variables in the substitution set
+generalize :: Map Ident Poly -> Type -> Poly
+generalize env t = Forall (S.toList $ free t S.\\ free env) t
 
--- -- | Unify two types producing a new substitution
--- unify :: Type -> Type -> Infer Subst
--- unify t0 t1 = do
---     case (t0, t1) of
---         (TArr a b, TArr c d) -> do
---             s1 <- unify a c
---             s2 <- unify (apply s1 b) (apply s1 d)
---             return $ s1 `compose` s2
---         (TPol a, b) -> occurs a b
---         (a, TPol b) -> occurs b a
---         (TMono a, TMono b) ->
---             if a == b then return M.empty else throwError "Types do not unify"
---         (TConstr (Constr name t), TConstr (Constr name' t')) ->
---             if name == name' && length t == length t'
---                 then do
---                     xs <- zipWithM unify t t'
---                     return $ foldr compose nullSubst xs
---                 else
---                     throwError $
---                         unwords
---                             [ "Type constructor:"
---                             , printTree name
---                             , "(" ++ printTree t ++ ")"
---                             , "does not match with:"
---                             , printTree name'
---                             , "(" ++ printTree t' ++ ")"
---                             ]
---         (a, b) -> do
---             ctx <- ask
---             env <- get
---             throwError . unwords $
---                 [ "Type:"
---                 , printTree a
---                 , "can't be unified with:"
---                 , printTree b
---                 , "\nCtx:"
---                 , show ctx
---                 , "\nEnv:"
---                 , show env
---                 ]
+{- | Instantiate a polymorphic type. The free type variables are substituted
+with fresh ones.
+-}
+inst :: T.Type -> Infer T.Type
+inst = \case
+    T.TAll bound t -> do
+        fr <- fresh
+        let s = M.singleton fr bound
+        apply s <$> inst t
+    _ -> undefined
 
--- {- | Check if a type is contained in another type.
--- I.E. { a = a -> b } is an unsolvable constraint since there is no substitution
--- where these are equal
--- -}
--- occurs :: Ident -> Type -> Infer Subst
--- occurs i t@(TPol _) = return (M.singleton i t)
--- occurs i t =
---     if S.member i (free t)
---         then
---             throwError $
---                 unwords
---                     [ "Occurs check failed, can't unify"
---                     , printTree (TPol i)
---                     , "with"
---                     , printTree t
---                     ]
---         else return $ M.singleton i t
+-- | Compose two substitution sets
+compose :: Subst -> Subst -> Subst
+compose m1 m2 = M.map (apply m1) m2 `M.union` m1
 
--- -- | Generalize a type over all free variables in the substitution set
--- generalize :: Map Ident Poly -> Type -> Poly
--- generalize env t = Forall (S.toList $ free t S.\\ free env) t
+-- TODO: Split this class into two separate classes, one for free variables
+--       and one for applying substitutions
 
--- {- | Instantiate a polymorphic type. The free type variables are substituted
--- with fresh ones.
--- -}
--- inst :: Poly -> Infer Type
--- inst (Forall xs t) = do
---     xs' <- mapM (const fresh) xs
---     let s = M.fromList $ zip xs xs'
---     return $ apply s t
+-- | A class representing free variables functions
+class FreeVars t where
+    -- | Get all free variables from t
+    free :: t -> Set LIdent
 
--- -- | Compose two substitution sets
--- compose :: Subst -> Subst -> Subst
--- compose m1 m2 = M.map (apply m1) m2 `M.union` m1
+    -- | Apply a substitution to t
+    apply :: Subst -> t -> t
 
--- -- TODO: Split this class into two separate classes, one for free variables
--- --       and one for applying substitutions
+instance FreeVars T.Type where
+    free :: T.Type -> Set LIdent
+    free (T.TVar (MkTVar a)) = S.singleton a
+    free (T.TAll (MkTVar bound) t) = (S.singleton bound) `S.intersection` free t
+    free (T.TLit _) = mempty
+    free (T.TFun a b) = free a `S.union` free b
+    -- \| Not guaranteed to be correct
+    free (T.TIndexed (T.Indexed _ a)) =
+        foldl' (\acc x -> free x `S.union` acc) S.empty a
 
--- -- | A class representing free variables functions
--- class FreeVars t where
---     -- | Get all free variables from t
---     free :: t -> Set Ident
+    apply :: Subst -> T.Type -> T.Type
+    apply sub t = do
+        case t of
+            T.TLit a -> T.TLit a
+            T.TVar (MkTVar a) -> case M.lookup a sub of
+                Nothing -> T.TVar (MkTVar a)
+                Just t -> t
+            T.TAll bound t -> undefined
+            T.TFun a b -> T.TFun (apply sub a) (apply sub b)
+            T.TIndexed (T.Indexed name a) -> T.TIndexed (T.Indexed name (map (apply sub) a))
 
---     -- | Apply a substitution to t
---     apply :: Subst -> t -> t
+instance FreeVars Poly where
+    free :: Poly -> Set LIdent
+    free (Forall xs t) = free t S.\\ S.fromList xs
+    apply :: Subst -> Poly -> Poly
+    apply s (Forall xs t) = Forall xs (apply (foldr M.delete s xs) t)
 
--- instance FreeVars Type where
---     free :: Type -> Set Ident
---     free (TPol a) = S.singleton a
---     free (TMono _) = mempty
---     free (TArr a b) = free a `S.union` free b
---     -- \| Not guaranteed to be correct
---     free (TConstr (Constr _ a)) =
---         foldl' (\acc x -> free x `S.union` acc) S.empty a
+instance FreeVars (Map LIdent Poly) where
+    free :: Map LIdent Poly -> Set LIdent
+    free m = foldl' S.union S.empty (map free $ M.elems m)
+    apply :: Subst -> Map LIdent Poly -> Map LIdent Poly
+    apply s = M.map (apply s)
 
---     apply :: Subst -> Type -> Type
---     apply sub t = do
---         case t of
---             TMono a -> TMono a
---             TPol a -> case M.lookup a sub of
---                 Nothing -> TPol a
---                 Just t -> t
---             TArr a b -> TArr (apply sub a) (apply sub b)
---             TConstr (Constr name a) -> TConstr (Constr name (map (apply sub) a))
+instance FreeVars T.Exp where
+    free :: T.Exp -> Set LIdent
+    free = error "free not implemented for T.Exp"
+    apply :: Subst -> T.Exp -> T.Exp
+    apply s = \case
+        T.EId (ident, t) ->
+            T.EId (ident, apply s t)
+        T.ELit t lit ->
+            T.ELit (apply s t) lit
+        T.ELet (T.Bind (ident, t) args e1) e2 ->
+            T.ELet (T.Bind (ident, apply s t) args (apply s e1)) (apply s e2)
+        T.EApp t e1 e2 ->
+            T.EApp (apply s t) (apply s e1) (apply s e2)
+        T.EAdd t e1 e2 ->
+            T.EAdd (apply s t) (apply s e1) (apply s e2)
+        T.EAbs t1 (ident, t2) e ->
+            T.EAbs (apply s t1) (ident, apply s t2) (apply s e)
+        T.ECase t e injs ->
+            T.ECase (apply s t) (apply s e) (apply s injs)
 
--- instance FreeVars Poly where
---     free :: Poly -> Set Ident
---     free (Forall xs t) = free t S.\\ S.fromList xs
---     apply :: Subst -> Poly -> Poly
---     apply s (Forall xs t) = Forall xs (apply (foldr M.delete s xs) t)
+instance FreeVars T.Inj where
+    free :: T.Inj -> Set LIdent
+    free = undefined
+    apply :: Subst -> T.Inj -> T.Inj
+    apply s (T.Inj (i, t) e) = T.Inj (i, apply s t) (apply s e)
 
--- instance FreeVars (Map Ident Poly) where
---     free :: Map Ident Poly -> Set Ident
---     free m = foldl' S.union S.empty (map free $ M.elems m)
---     apply :: Subst -> Map Ident Poly -> Map Ident Poly
---     apply s = M.map (apply s)
+instance FreeVars [T.Inj] where
+    free :: [T.Inj] -> Set LIdent
+    free = foldl' (\acc x -> free x `S.union` acc) mempty
+    apply s = map (apply s)
 
--- instance FreeVars T.Exp where
---     free :: T.Exp -> Set Ident
---     free = error "free not implemented for T.Exp"
---     apply :: Subst -> T.Exp -> T.Exp
---     apply s = \case
---         T.EId (ident, t) ->
---             T.EId (ident, apply s t)
---         T.ELit t lit ->
---             T.ELit (apply s t) lit
---         T.ELet (T.Bind (ident, t) e1) e2 ->
---             T.ELet (T.Bind (ident, apply s t) (apply s e1)) (apply s e2)
---         T.EApp t e1 e2 ->
---             T.EApp (apply s t) (apply s e1) (apply s e2)
---         T.EAdd t e1 e2 ->
---             T.EAdd (apply s t) (apply s e1) (apply s e2)
---         T.EAbs t1 (ident, t2) e ->
---             T.EAbs (apply s t1) (ident, apply s t2) (apply s e)
---         T.ECase t e injs ->
---             T.ECase (apply s t) (apply s e) (apply s injs)
+-- | Apply substitutions to the environment.
+applySt :: Subst -> Infer a -> Infer a
+applySt s = local (\st -> st{vars = apply s (vars st)})
 
--- instance FreeVars T.Inj where
---     free :: T.Inj -> Set Ident
---     free = undefined
---     apply :: Subst -> T.Inj -> T.Inj
---     apply s (T.Inj (i, t) e) = T.Inj (i, apply s t) (apply s e)
+-- | Represents the empty substition set
+nullSubst :: Subst
+nullSubst = M.empty
 
--- instance FreeVars [T.Inj] where
---     free :: [T.Inj] -> Set Ident
---     free = foldl' (\acc x -> free x `S.union` acc) mempty
---     apply s = map (apply s)
+-- | Generate a new fresh variable and increment the state counter
+fresh :: Infer Type
+fresh = do
+    n <- gets count
+    modify (\st -> st{count = n + 1})
+    return . TVar . MkTVar . LIdent $ show n
 
--- -- | Apply substitutions to the environment.
--- applySt :: Subst -> Infer a -> Infer a
--- applySt s = local (\st -> st{vars = apply s (vars st)})
+-- | Run the monadic action with an additional binding
+withBinding :: (Monad m, MonadReader Ctx m) => Ident -> Poly -> m a -> m a
+withBinding i p = local (\st -> st{vars = M.insert i p (vars st)})
 
--- -- | Represents the empty substition set
--- nullSubst :: Subst
--- nullSubst = M.empty
+-- | Run the monadic action with several additional bindings
+withBindings :: (Monad m, MonadReader Ctx m) => [(Ident, Poly)] -> m a -> m a
+withBindings xs =
+    local (\st -> st{vars = foldl' (flip (uncurry M.insert)) (vars st) xs})
 
--- -- | Generate a new fresh variable and increment the state counter
--- fresh :: Infer Type
--- fresh = do
---     n <- gets count
---     modify (\st -> st{count = n + 1})
---     return . TPol . Ident $ show n
+-- | Insert a function signature into the environment
+insertSig :: LIdent -> Type -> Infer ()
+insertSig i t = modify (\st -> st{sigs = M.insert i t (sigs st)})
 
--- -- | Run the monadic action with an additional binding
--- withBinding :: (Monad m, MonadReader Ctx m) => Ident -> Poly -> m a -> m a
--- withBinding i p = local (\st -> st{vars = M.insert i p (vars st)})
+-- | Insert a constructor with its data type
+insertConstr :: UIdent -> Type -> Infer ()
+insertConstr i t =
+    modify (\st -> st{constructors = M.insert i t (constructors st)})
 
--- -- | Run the monadic action with several additional bindings
--- withBindings :: (Monad m, MonadReader Ctx m) => [(Ident, Poly)] -> m a -> m a
--- withBindings xs =
---     local (\st -> st{vars = foldl' (flip (uncurry M.insert)) (vars st) xs})
+-------- PATTERN MATCHING ---------
 
--- -- | Insert a function signature into the environment
--- insertSig :: Ident -> Type -> Infer ()
--- insertSig i t = modify (\st -> st{sigs = M.insert i t (sigs st)})
+checkCase :: Type -> [Inj] -> Infer (Subst, [T.Inj], Type)
+checkCase expT injs = do
+    (injTs, injs, returns) <- unzip3 <$> mapM checkInj injs
+    (sub1, _) <-
+        foldM
+            ( \(sub, acc) x ->
+                (\a -> (a `compose` sub, a `apply` acc)) <$> unify x acc
+            )
+            (nullSubst, expT)
+            injTs
+    (sub2, returns_type) <-
+        foldM
+            ( \(sub, acc) x ->
+                (\a -> (a `compose` sub, a `apply` acc)) <$> unify x acc
+            )
+            (nullSubst, head returns)
+            (tail returns)
+    return (sub2 `compose` sub1, injs, returns_type)
 
--- -- | Insert a constructor with its data type
--- insertConstr :: Ident -> Type -> Infer ()
--- insertConstr i t =
---     modify (\st -> st{constructors = M.insert i t (constructors st)})
+{- | fst = type of init
+   | snd = type of expr
+-}
+checkInj :: Inj -> Infer (Type, T.Inj, Type)
+checkInj (Inj it expr) = do
+    (initT, vars) <- inferInit it
+    let converted = map (second (Forall [])) vars
+    (exprT, e) <- withBindings converted (inferExp expr)
+    return (initT, T.Inj (it, initT) e, exprT)
 
--- -------- PATTERN MATCHING ---------
+inferInit :: Init -> Infer (Type, [T.Id])
+inferInit = \case
+    InitLit lit -> return (litType lit, mempty)
+    InitConstructor fn vars -> do
+        gets (M.lookup fn . constructors) >>= \case
+            Nothing ->
+                throwError $
+                    "Constructor: " ++ printTree fn ++ " does not exist"
+            Just a -> do
+                case unsnoc $ flattenType a of
+                    Nothing -> throwError "Partial pattern match not allowed"
+                    Just (vs, ret) ->
+                        case length vars `compare` length vs of
+                            EQ -> do
+                                return (ret, zip vars vs)
+                            _ -> throwError "Partial pattern match not allowed"
+    InitCatch -> (,mempty) <$> fresh
 
--- checkCase :: Type -> [Inj] -> Infer (Subst, [T.Inj], Type)
--- checkCase expT injs = do
---     (injTs, injs, returns) <- unzip3 <$> mapM checkInj injs
---     (sub1, _) <-
---         foldM
---             ( \(sub, acc) x ->
---                 (\a -> (a `compose` sub, a `apply` acc)) <$> unify x acc
---             )
---             (nullSubst, expT)
---             injTs
---     (sub2, returns_type) <-
---         foldM
---             ( \(sub, acc) x ->
---                 (\a -> (a `compose` sub, a `apply` acc)) <$> unify x acc
---             )
---             (nullSubst, head returns)
---             (tail returns)
---     return (sub2 `compose` sub1, injs, returns_type)
+flattenType :: Type -> [Type]
+flattenType (TFun a b) = flattenType a ++ flattenType b
+flattenType a = [a]
 
--- {- | fst = type of init
---    | snd = type of expr
--- -}
--- checkInj :: Inj -> Infer (Type, T.Inj, Type)
--- checkInj (Inj it expr) = do
---     (initT, vars) <- inferInit it
---     let converted = map (second (Forall [])) vars
---     (exprT, e) <- withBindings converted (inferExp expr)
---     return (initT, T.Inj (it, initT) e, exprT)
-
--- inferInit :: Init -> Infer (Type, [T.Id])
--- inferInit = \case
---     InitLit lit -> return (litType lit, mempty)
---     InitConstr fn vars -> do
---         gets (M.lookup fn . constructors) >>= \case
---             Nothing ->
---                 throwError $
---                     "Constructor: " ++ printTree fn ++ " does not exist"
---             Just a -> do
---                 case unsnoc $ flattenType a of
---                     Nothing -> throwError "Partial pattern match not allowed"
---                     Just (vs, ret) ->
---                         case length vars `compare` length vs of
---                             EQ -> do
---                                 return (ret, zip vars vs)
---                             _ -> throwError "Partial pattern match not allowed"
---     InitCatch -> (,mempty) <$> fresh
-
--- flattenType :: Type -> [Type]
--- flattenType (TArr a b) = flattenType a ++ flattenType b
--- flattenType a = [a]
-
--- litType :: Literal -> Type
--- litType (LInt _) = TMono "Int"
+litType :: Lit -> Type
+litType (LInt _) = TLit "Int"
+litType (LChar _) = TLit "Char"
diff --git a/src/TypeChecker/TypeCheckerIr.hs b/src/TypeChecker/TypeCheckerIr.hs
index 2b3c702..bfc8a6a 100644
--- a/src/TypeChecker/TypeCheckerIr.hs
+++ b/src/TypeChecker/TypeCheckerIr.hs
@@ -2,178 +2,207 @@
 
 module TypeChecker.TypeCheckerIr where
 
--- import Control.Monad.Except
--- import Control.Monad.Reader
--- import Control.Monad.State
--- import Data.Functor.Identity (Identity)
--- import Data.Map (Map)
--- import Grammar.Abs (
---     Data (..),
---     Ident (..),
---     Init (..),
---     Literal (..),
---     Type (..),
---  )
--- import Grammar.Print
--- import Prelude
--- import Prelude qualified as C (Eq, Ord, Read, Show)
+import Control.Monad.Except
+import Control.Monad.Reader
+import Control.Monad.State
+import Data.Functor.Identity (Identity)
+import Data.Map (Map)
+import Grammar.Abs (
+    Data (..),
+    Ident (..),
+    Init (..),
+    Lit (..),
+    TVar (..),
+ )
+import Grammar.Abs qualified as GA (Type (..))
+import Grammar.Print
+import Prelude
+import Prelude qualified as C (Eq, Ord, Read, Show)
 
--- -- | A data type representing type variables
--- data Poly = Forall [Ident] Type
---     deriving (Show)
+-- | A data type representing type variables
+data Poly = Forall [Ident] Type
+    deriving (Show)
 
--- newtype Ctx = Ctx {vars :: Map Ident Poly}
---     deriving Show
+newtype Ctx = Ctx {vars :: Map Ident Poly}
+    deriving (Show)
 
--- data Env = Env
---     { count :: Int
---     , sigs :: Map Ident Type
---     , constructors :: Map Ident Type
---     } deriving Show
+data Env = Env
+    { count :: Int
+    , sigs :: Map Ident GA.Type
+    , constructors :: Map Ident GA.Type
+    }
+    deriving (Show)
 
--- type Error = String
--- type Subst = Map Ident Type
+type Error = String
+type Subst = Map Ident Type
 
--- type Infer = StateT Env (ReaderT Ctx (ExceptT Error Identity))
+type Infer = StateT Env (ReaderT Ctx (ExceptT Error Identity))
 
--- newtype Program = Program [Def]
---     deriving (C.Eq, C.Ord, C.Show, C.Read)
+newtype Program = Program [Def]
+    deriving (C.Eq, C.Ord, C.Show, C.Read)
 
--- data Exp
---     = EId Id
---     | ELit Type Literal
---     | ELet Bind Exp
---     | EApp Type Exp Exp
---     | EAdd Type Exp Exp
---     | EAbs Type Id Exp
---     | ECase Type Exp [Inj]
---     deriving (C.Eq, C.Ord, C.Read, C.Show)
+data Type
+    = TLit Ident
+    | TVar TVar
+    | TFun Type Type
+    | TAll TVar Type
+    | TIndexed Indexed
+    deriving (Show, Eq, Ord, Read)
 
--- data Inj = Inj (Init, Type) Exp
---     deriving (C.Eq, C.Ord, C.Read, C.Show)
+data Exp
+    = EId Id
+    | ELit Lit
+    | ELet Bind ExpT
+    | EApp ExpT ExpT
+    | EAdd ExpT ExpT
+    | EAbs Id ExpT
+    | ECase ExpT [Inj]
+    deriving (C.Eq, C.Ord, C.Read, C.Show)
 
--- data Def = DBind Bind | DData Data
---     deriving (C.Eq, C.Ord, C.Read, C.Show)
+type ExpT = (Exp, Type)
 
--- type Id = (Ident, Type)
+data Indexed = Indexed Ident [Type]
+    deriving (Show, Read, Ord, Eq)
 
--- data Bind = Bind Id Exp
---     deriving (C.Eq, C.Ord, C.Show, C.Read)
+data Inj = Inj (Init, Type) ExpT
+    deriving (C.Eq, C.Ord, C.Read, C.Show)
 
--- instance Print [Def] where
---     prt _ [] = concatD []
---     prt _ (x : xs) = concatD [prt 0 x, doc (showString "\n"), prt 0 xs]
+data Def = DBind Bind | DData Data
+    deriving (C.Eq, C.Ord, C.Read, C.Show)
 
--- instance Print Def where
---     prt i (DBind bind) = prt i bind
---     prt i (DData d) = prt i d
+type Id = (Ident, Type)
 
--- instance Print Program where
---     prt i (Program sc) = prPrec i 0 $ prt 0 sc
+data Bind = Bind Id [Id] ExpT
+    deriving (C.Eq, C.Ord, C.Show, C.Read)
 
--- instance Print Bind where
---     prt i (Bind (t, name) rhs) =
---         prPrec i 0 $
---             concatD
---                 [ prt 0 name
---                 , doc $ showString ":"
---                 , prt 0 t
---                 , doc $ showString "\n"
---                 , prt 0 name
---                 , doc $ showString "="
---                 , prt 0 rhs
---                 ]
+instance Print [Def] where
+    prt _ [] = concatD []
+    prt _ (x : xs) = concatD [prt 0 x, doc (showString "\n"), prt 0 xs]
 
--- instance Print [Bind] where
---     prt _ [] = concatD []
---     prt _ [x] = concatD [prt 0 x]
---     prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), doc (showString "\n"), prt 0 xs]
+instance Print Def where
+    prt i (DBind bind) = prt i bind
+    prt i (DData d) = prt i d
 
--- prtIdPs :: Int -> [Id] -> Doc
--- prtIdPs i = prPrec i 0 . concatD . map (prtIdP i)
+instance Print Program where
+    prt i (Program sc) = prPrec i 0 $ prt 0 sc
 
--- prtId :: Int -> Id -> Doc
--- prtId i (name, t) =
---     prPrec i 0 $
---         concatD
---             [ prt 0 name
---             , doc $ showString ":"
---             , prt 0 t
---             ]
+instance Print Bind where
+    prt i (Bind (t, name) args rhs) =
+        prPrec i 0 $
+            concatD
+                [ prt 0 name
+                , doc $ showString ":"
+                , prt 0 t
+                , doc $ showString "\n"
+                , prt 0 name
+                , doc $ showString "="
+                , prt 0 rhs
+                ]
 
--- prtIdP :: Int -> Id -> Doc
--- prtIdP i (name, t) =
---     prPrec i 0 $
---         concatD
---             [ doc $ showString "("
---             , prt 0 name
---             , doc $ showString ":"
---             , prt 0 t
---             , doc $ showString ")"
---             ]
+instance Print [Bind] where
+    prt _ [] = concatD []
+    prt _ [x] = concatD [prt 0 x]
+    prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), doc (showString "\n"), prt 0 xs]
 
--- instance Print Exp where
---     prt i = \case
---         EId n -> prPrec i 3 $ concatD [prtId 0 n, doc $ showString "\n"]
---         ELit _ (LInt i1) -> prPrec i 3 $ concatD [prt 0 i1, doc $ showString "\n"]
---         ELet bs e ->
---             prPrec i 3 $
---                 concatD
---                     [ doc $ showString "let"
---                     , prt 0 bs
---                     , doc $ showString "in"
---                     , prt 0 e
---                     , doc $ showString "\n"
---                     ]
---         EApp _ e1 e2 ->
---             prPrec i 2 $
---                 concatD
---                     [ prt 2 e1
---                     , prt 3 e2
---                     ]
---         EAdd t e1 e2 ->
---             prPrec i 1 $
---                 concatD
---                     [ doc $ showString "@"
---                     , prt 0 t
---                     , prt 1 e1
---                     , doc $ showString "+"
---                     , prt 2 e2
---                     , doc $ showString "\n"
---                     ]
---         EAbs t n e ->
---             prPrec i 0 $
---                 concatD
---                     [ doc $ showString "@"
---                     , prt 0 t
---                     , doc $ showString "\\"
---                     , prtId 0 n
---                     , doc $ showString "."
---                     , prt 0 e
---                     , doc $ showString "\n"
---                     ]
---         ECase t exp injs ->
---             prPrec
---                 i
---                 0
---                 ( concatD
---                     [ doc (showString "case")
---                     , prt 0 exp
---                     , doc (showString "of")
---                     , doc (showString "{")
---                     , prt 0 injs
---                     , doc (showString "}")
---                     , doc (showString ":")
---                     , prt 0 t
---                     , doc $ showString "\n"
---                     ]
---                 )
+prtIdPs :: Int -> [Id] -> Doc
+prtIdPs i = prPrec i 0 . concatD . map (prtIdP i)
 
--- instance Print Inj where
---     prt i = \case
---         Inj (init, t) exp -> prPrec i 0 (concatD [prt 0 init, doc (showString ":"), prt 0 t, doc (showString "=>"), prt 0 exp])
+prtId :: Int -> Id -> Doc
+prtId i (name, t) =
+    prPrec i 0 $
+        concatD
+            [ prt 0 name
+            , doc $ showString ":"
+            , prt 0 t
+            ]
 
--- instance Print [Inj] where
---     prt _ [] = concatD []
---     prt _ [x] = concatD [prt 0 x]
---     prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
+prtIdP :: Int -> Id -> Doc
+prtIdP i (name, t) =
+    prPrec i 0 $
+        concatD
+            [ doc $ showString "("
+            , prt 0 name
+            , doc $ showString ":"
+            , prt 0 t
+            , doc $ showString ")"
+            ]
+
+instance Print Exp where
+    prt i = \case
+        EId n -> prPrec i 3 $ concatD [prtId 0 n, doc $ showString "\n"]
+        ELit _ lit -> prPrec i 3 $ concatD [prt 0 lit, doc $ showString "\n"]
+        ELet bs e ->
+            prPrec i 3 $
+                concatD
+                    [ doc $ showString "let"
+                    , prt 0 bs
+                    , doc $ showString "in"
+                    , prt 0 e
+                    , doc $ showString "\n"
+                    ]
+        EApp _ e1 e2 ->
+            prPrec i 2 $
+                concatD
+                    [ prt 2 e1
+                    , prt 3 e2
+                    ]
+        EAdd t e1 e2 ->
+            prPrec i 1 $
+                concatD
+                    [ doc $ showString "@"
+                    , prt 0 t
+                    , prt 1 e1
+                    , doc $ showString "+"
+                    , prt 2 e2
+                    , doc $ showString "\n"
+                    ]
+        EAbs t n e ->
+            prPrec i 0 $
+                concatD
+                    [ doc $ showString "@"
+                    , prt 0 t
+                    , doc $ showString "\\"
+                    , prtId 0 n
+                    , doc $ showString "."
+                    , prt 0 e
+                    , doc $ showString "\n"
+                    ]
+        ECase t exp injs ->
+            prPrec
+                i
+                0
+                ( concatD
+                    [ doc (showString "case")
+                    , prt 0 exp
+                    , doc (showString "of")
+                    , doc (showString "{")
+                    , prt 0 injs
+                    , doc (showString "}")
+                    , doc (showString ":")
+                    , prt 0 t
+                    , doc $ showString "\n"
+                    ]
+                )
+
+instance Print ExpT where
+    prt i (e, t) = concatD [prt i e, doc (showString ":"), prt i t]
+
+instance Print Inj where
+    prt i = \case
+        Inj (init, t) exp -> prPrec i 0 (concatD [prt 0 init, doc (showString ":"), prt 0 t, doc (showString "=>"), prt 0 exp])
+
+instance Print [Inj] where
+    prt _ [] = concatD []
+    prt _ [x] = concatD [prt 0 x]
+    prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
+
+instance Print Type where
+    prt i = \case
+        TLit uident -> prPrec i 2 (concatD [prt 0 uident])
+        TVar tvar -> prPrec i 2 (concatD [prt 0 tvar])
+        TAll tvar type_ -> prPrec i 1 (concatD [doc (showString "forall"), prt 0 tvar, doc (showString "."), prt 0 type_])
+        TIndexed indexed -> prPrec i 1 (concatD [prt 0 indexed])
+        TFun type_1 type_2 -> prPrec i 0 (concatD [prt 1 type_1, doc (showString "->"), prt 0 type_2])
+
+instance Print Indexed where
+    prt i (Indexed u ts) = concatD [prt i u, prt i ts]