diff --git a/Grammar.cf b/Grammar.cf
index 37305e2..356646d 100644
--- a/Grammar.cf
+++ b/Grammar.cf
@@ -1,50 +1,91 @@
+--------------------------------------------------------------------------------
+-- * PROGRAM
+--------------------------------------------------------------------------------
 
 Program. Program ::= [Def] ;
 
+--------------------------------------------------------------------------------
+-- * TOP-LEVEL
+--------------------------------------------------------------------------------
+
 DBind. Def ::= Bind ;
+DSig.  Def ::= Sig ;
 DData. Def ::= Data ;
-separator Def ";" ;
 
-Bind. Bind ::= Ident ":" Type ";"
-               Ident [Ident] "=" Exp ;
+Sig. Sig ::= LIdent ":" Type ;
 
-Data. Data ::= "data" Constr "where" "{" [Constructor] "}" ;
+Bind. Bind ::= LIdent [LIdent] "=" Exp ;
 
-Constructor. Constructor ::= Ident ":" Type ;
-separator nonempty Constructor "" ;
+--------------------------------------------------------------------------------
+-- * TYPES
+--------------------------------------------------------------------------------
 
-TMono.   Type1 ::= "_" Ident ;
-TPol.    Type1 ::= "'" Ident ;
-TConstr. Type1 ::= Constr ;
-TArr.    Type  ::= Type1 "->" Type ;
+         TLit.     Type2 ::= UIdent ;
+         TVar.     Type2 ::= TVar ;
+         TAll.     Type1 ::= "forall" TVar "." Type ;
+         TIndexed. Type1 ::= Indexed ;
+internal TEVar.    Type1 ::= TEVar ;
+         TFun.     Type  ::= Type1 "->" Type ;
 
-Constr.  Constr ::= Ident "(" [Type] ")" ;
+         MkTVar.  TVar  ::= LIdent ;
+internal MkTEVar. TEVar ::= LIdent ;
+
+--------------------------------------------------------------------------------
+-- * DATA TYPES
+--------------------------------------------------------------------------------
+
+Constructor. Constructor ::= UIdent ":" Type ;
+
+Indexed. Indexed ::= UIdent "(" [Type] ")" ;
+
+Data. Data ::= "data" Indexed "where" "{" [Constructor] "}" ;
+
+--------------------------------------------------------------------------------
+-- * EXPRESSIONS
+--------------------------------------------------------------------------------
 
--- TODO: Move literal to its own thing since it's reused in Init as well.
 EAnn.   Exp5 ::= "(" Exp ":" Type ")" ;
-EId.    Exp4 ::= Ident ;
-ELit.   Exp4 ::= Literal ;
+EId.    Exp4 ::= LIdent ;
+ELit.   Exp4 ::= Lit ;
 EApp.   Exp3 ::= Exp3 Exp4 ;
 EAdd.   Exp1 ::= Exp1 "+" Exp2 ;
-ELet.   Exp  ::= "let" Ident "=" Exp "in" Exp ; 
-EAbs.   Exp  ::= "\\" Ident "." Exp ;
+ELet.   Exp  ::= "let" LIdent "=" Exp "in" Exp ; 
+EAbs.   Exp  ::= "\\" LIdent "." Exp ;
 ECase.  Exp  ::= "case" Exp "of" "{" [Inj] "}";
 
-LInt. Literal ::= Integer ;
+--------------------------------------------------------------------------------
+-- * LITERALS
+--------------------------------------------------------------------------------
+
+LInt. Lit ::= Integer ;
+LChar. Lit ::= Char ;
+
+--------------------------------------------------------------------------------
+-- * CASE
+--------------------------------------------------------------------------------
 
 Inj. Inj ::= Init "=>" Exp ;
-separator nonempty Inj ";" ;
 
-InitLit. Init    ::= Literal ;
-InitConstr. Init ::= Ident [Ident] ;
-InitCatch. Init  ::= "_" ;
+InitLit. Init         ::= Lit ;
+InitConstructor. Init ::= UIdent [LIdent] ;
+InitCatch. Init       ::= "_" ;
 
+--------------------------------------------------------------------------------
+-- * AUX
+--------------------------------------------------------------------------------
+
+separator Def ";" ;
+separator nonempty Constructor "" ;
 separator Type " " ;
-coercions Type 2 ;
-
+separator nonempty Inj ";" ;
 separator Ident " ";
+separator LIdent " ";
 
 coercions Exp 5 ;
+coercions Type 2 ;
+
+token UIdent (upper (letter | digit | '_')*) ;
+token LIdent (lower (letter | digit | '_')*) ;
 
 comment "--" ;
 comment "{-" "-}" ;
diff --git a/sample-programs/basic-1 b/sample-programs/basic-1
index 5cb2b2a..d52aac2 100644
--- a/sample-programs/basic-1
+++ b/sample-programs/basic-1
@@ -1,2 +1,2 @@
-f : _Int -> _Int ;
+f : Int -> Int ;
 f = \x. x+1 ;
diff --git a/sample-programs/basic-2 b/sample-programs/basic-2
index 2f0448c..2db6128 100644
--- a/sample-programs/basic-2
+++ b/sample-programs/basic-2
@@ -1,5 +1,5 @@
-add : _Int -> _Int -> _Int ;
+add : Int -> Int -> Int ;
 add x = \y. x+y;
 
-main : _Int ;
+main : Int ;
 main = (\z. z+z) ((add 4) 6) ;
diff --git a/sample-programs/basic-3 b/sample-programs/basic-3
index 7ba4971..98c03b9 100644
--- a/sample-programs/basic-3
+++ b/sample-programs/basic-3
@@ -1,2 +1,2 @@
-main : _Int ;
+main : Int ;
 main = (\x. x+x+3) ((\x. x) 2) ;
diff --git a/sample-programs/basic-4 b/sample-programs/basic-4
index 365e4cb..55ac9eb 100644
--- a/sample-programs/basic-4
+++ b/sample-programs/basic-4
@@ -1,2 +1,2 @@
-f : _Int -> _Int ;
+f : Int -> Int ;
 f x = let g = (\y. y+1) in g (g x)
diff --git a/sample-programs/basic-5 b/sample-programs/basic-5
index 319b9b0..a6414f2 100644
--- a/sample-programs/basic-5
+++ b/sample-programs/basic-5
@@ -1,8 +1,8 @@
-double : _Int -> _Int ;
+double : Int -> Int ;
 double n = n + n;
 
-id : 'a -> 'a ;
+id : forall a. a -> a ;
 id x = x ;
 
-main : _Int ;
+main : Int ;
 main = id double 5;
diff --git a/sample-programs/basic-6 b/sample-programs/basic-6
index 467d263..3ed64a0 100644
--- a/sample-programs/basic-6
+++ b/sample-programs/basic-6
@@ -3,7 +3,7 @@ data Bool () where {
     False : Bool ()
 };
 
-main : Bool () -> _Int ;
+main : Bool () -> Int ;
 main b = case b of {
     False => 0;
     True => 0
diff --git a/sample-programs/basic-7 b/sample-programs/basic-7
index 3ddf98b..9ae2bdf 100644
--- a/sample-programs/basic-7
+++ b/sample-programs/basic-7
@@ -3,7 +3,7 @@ data Bool () where {
     False : Bool ()
 };
 
-ifThenElse : Bool () -> 'a -> 'a -> 'a;
+ifThenElse : forall a. Bool () -> a -> a -> a;
 ifThenElse b if else = case b of {
         True => if;
         False => else
diff --git a/sample-programs/basic-8 b/sample-programs/basic-8
index d916d03..c2c4042 100644
--- a/sample-programs/basic-8
+++ b/sample-programs/basic-8
@@ -1,22 +1,22 @@
-data Maybe ('a) where {
-    Nothing : Maybe ('a)
-    Just : 'a -> Maybe ('a)
+data Maybe (a) where {
+    Nothing : Maybe (a)
+    Just : forall a. a -> Maybe (a)
 };
 
-fromJust : Maybe ('a) -> 'a ;
+fromJust : Maybe (a) -> a ;
 fromJust a =
     case a of {
         Just a => a
     };
 
-fromMaybe : 'a -> Maybe ('a) -> 'a ;
+fromMaybe : a -> Maybe (a) -> a ;
 fromMaybe a b =
     case b of {
         Just a => a;
         Nothing => a
     };
 
-maybe : 'b -> ('a -> 'b) -> Maybe ('a) -> 'b;
+maybe : b -> (a -> b) -> Maybe (a) -> b;
 maybe b f ma =
     case ma of {
         Just a => f a;
diff --git a/src/Main.hs b/src/Main.hs
index 7e3922d..0a00cd6 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -11,7 +11,8 @@ import Grammar.Print (printTree)
 import Renamer.Renamer (rename)
 import System.Environment (getArgs)
 import System.Exit (exitFailure, exitSuccess)
-import TypeChecker.TypeChecker (typecheck)
+
+-- import TypeChecker.TypeChecker (typecheck)
 
 main :: IO ()
 main =
@@ -28,12 +29,12 @@ main' s = do
     putStrLn $ printTree parsed
 
     putStrLn "\n-- Renamer --"
-    let renamed = rename parsed
+    renamed <- fromRenamerErr . rename $ parsed
     putStrLn $ printTree renamed
 
-    putStrLn "\n-- TypeChecker --"
-    typechecked <- fromTypeCheckerErr $ typecheck renamed
-    putStrLn $ show typechecked
+    -- putStrLn "\n-- TypeChecker --"
+    -- typechecked <- fromTypeCheckerErr $ typecheck renamed
+    -- putStrLn $ show typechecked
 
     -- putStrLn "\n-- Lambda Lifter --"
     -- let lifted = lambdaLift typechecked
@@ -55,6 +56,16 @@ fromCompilerErr =
         )
         pure
 
+fromRenamerErr :: Err a -> IO a
+fromRenamerErr =
+    either
+        ( \err -> do
+            putStrLn "\nRENAME ERROR"
+            putStrLn err
+            exitFailure
+        )
+        pure
+
 fromSyntaxErr :: Err a -> IO a
 fromSyntaxErr =
     either
diff --git a/src/Renamer/Renamer.hs b/src/Renamer/Renamer.hs
index d056868..aac8b16 100644
--- a/src/Renamer/Renamer.hs
+++ b/src/Renamer/Renamer.hs
@@ -1,56 +1,101 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
 
-module Renamer.Renamer where
+module Renamer.Renamer (rename) where
 
 import Auxiliary (mapAccumM)
+import Control.Applicative (Applicative (liftA2))
+import Control.Monad.Except (ExceptT, runExceptT)
+import Control.Monad.Identity (Identity, runIdentity)
 import Control.Monad.State (
     MonadState,
-    State,
-    evalState,
+    StateT,
+    evalStateT,
     gets,
     modify,
  )
-import Data.List (foldl')
+import Data.Function (on)
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.Tuple.Extra (dupe)
-import Debug.Trace (trace)
 import Grammar.Abs
 
 -- | Rename all variables and local binds
-rename :: Program -> Program
-rename (Program bs) = Program $ evalState (runRn $ mapM (renameSc initNames) bs) 0
+rename :: Program -> Either String Program
+rename (Program defs) = Program <$> renameDefs defs
+
+renameDefs :: [Def] -> Either String [Def]
+renameDefs defs = runIdentity $ runExceptT $ evalStateT (runRn $ mapM renameDef defs) initCxt
   where
-    -- initNames = Map.fromList $ map (\(Bind name _ _ _ _) -> dupe name) bs
-    initNames = Map.fromList $ foldl' saveIfBind [] bs
-    saveIfBind acc (DBind (Bind name _ _ _ _)) = dupe name : acc
-    saveIfBind acc _ = acc
-    renameSc :: Names -> Def -> Rn Def
-    renameSc old_names (DBind (Bind name t _ parms rhs)) = do
-        (new_names, parms') <- newNames old_names parms
-        rhs' <- snd <$> renameExp new_names rhs
-        pure . DBind $ Bind name t name parms' rhs'
-    renameSc _ def = pure def
+    initNames = Map.fromList [dupe name | DBind (Bind name _ _) <- defs]
+
+    renameDef :: Def -> Rn Def
+    renameDef = \case
+        DSig (Sig name typ) -> DSig . Sig name <$> renameTVars typ
+        DBind (Bind name vars rhs) -> do
+            (new_names, vars') <- newNames initNames vars
+            rhs' <- snd <$> renameExp new_names rhs
+            pure . DBind $ Bind name vars' rhs'
+        DData (Data (Indexed cname types) constrs) -> do
+            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
+            collectTVars tvars = \case
+                TAll tvar t -> collectTVars (tvar : tvars) t
+                TIndexed _ -> tvars
+                -- Should be monad error
+                TVar v -> [v]
+                _ -> error ("Bad data type definition: " ++ show types)
+
+    renameConstr :: [(TVar, TVar)] -> Constructor -> Constructor
+    renameConstr new_types (Constructor name typ) =
+        Constructor name $ substituteTVar new_types typ
+
+substituteTVar :: [(TVar, TVar)] -> Type -> Type
+substituteTVar new_names typ = case typ of
+    TLit _ -> typ
+    TVar tvar
+        | Just tvar' <- lookup tvar new_names ->
+            TVar tvar'
+        | otherwise ->
+            typ
+    TFun t1 t2 -> on TFun substitute' t1 t2
+    TAll tvar t
+        | Just tvar' <- lookup tvar new_names ->
+            TAll tvar' $ substitute' t
+        | otherwise ->
+            TAll tvar $ substitute' t
+    TIndexed (Indexed name typs) -> TIndexed . Indexed name $ map substitute' typs
+    _ -> error ("Impossible " ++ show typ)
+  where
+    substitute' = substituteTVar new_names
+
+initCxt :: Cxt
+initCxt = Cxt 0 0
+
+data Cxt = Cxt
+    { var_counter :: Int
+    , tvar_counter :: Int
+    }
 
 -- | Rename monad. State holds the number of renamed names.
-newtype Rn a = Rn {runRn :: State Int a}
-    deriving (Functor, Applicative, Monad, MonadState Int)
+newtype Rn a = Rn {runRn :: StateT Cxt (ExceptT String Identity) a}
+    deriving (Functor, Applicative, Monad, MonadState Cxt)
 
 -- | Maps old to new name
-type Names = Map Ident Ident
-
-renameLocalBind :: Names -> Bind -> Rn (Names, Bind)
-renameLocalBind old_names (Bind name t _ parms rhs) = do
-    (new_names, name') <- newName old_names name
-    (new_names', parms') <- newNames new_names parms
-    (new_names'', rhs') <- renameExp new_names' rhs
-    pure (new_names'', Bind name' t name' parms' rhs')
+type Names = Map LIdent LIdent
 
 renameExp :: Names -> Exp -> Rn (Names, Exp)
 renameExp old_names = \case
     EId n -> pure (old_names, EId . fromMaybe n $ Map.lookup n old_names)
-    ELit (LInt i1) -> pure (old_names, ELit (LInt i1))
+    ELit lit -> pure (old_names, ELit lit)
     EApp e1 e2 -> do
         (env1, e1') <- renameExp old_names e1
         (env2, e2') <- renameExp old_names e2
@@ -59,17 +104,21 @@ renameExp old_names = \case
         (env1, e1') <- renameExp old_names e1
         (env2, e2') <- renameExp old_names e2
         pure (Map.union env1 env2, EAdd e1' e2')
-    ELet i e1 e2 -> do
-        (new_names, e1') <- renameExp old_names e1
-        (new_names', e2') <- renameExp new_names e2
-        pure (new_names', ELet i e1' e2')
+
+    -- TODO fix shadowing
+    ELet name rhs e -> do
+        (new_names, name') <- newName old_names name
+        (new_names', rhs') <- renameExp new_names rhs
+        (new_names'', e') <- renameExp new_names' e
+        pure (new_names'', ELet name' rhs' e')
     EAbs par e -> do
         (new_names, par') <- newName old_names par
         (new_names', e') <- renameExp new_names e
         pure (new_names', EAbs par' e')
     EAnn e t -> do
         (new_names, e') <- renameExp old_names e
-        pure (new_names, EAnn e' t)
+        t' <- renameTVars t
+        pure (new_names, EAnn e' t')
     ECase e injs -> do
         (new_names, e') <- renameExp old_names e
         (new_names', injs') <- renameInjs new_names injs
@@ -88,21 +137,58 @@ renameInj ns (Inj init e) = do
 
 renameInit :: Names -> Init -> Rn (Names, Init)
 renameInit ns i = case i of
-    InitConstr cs vars -> do
+    InitConstructor cs vars -> do
         (ns_new, vars') <- newNames ns vars
-        return (ns_new, InitConstr cs vars')
+        return (ns_new, InitConstructor cs vars')
     rest -> return (ns, rest)
 
+renameTVars :: Type -> Rn Type
+renameTVars typ = case typ of
+    TAll tvar t -> do
+        tvar' <- nextNameTVar tvar
+        t' <- renameTVars $ substitute tvar tvar' t
+        pure $ TAll tvar' t'
+    TFun t1 t2 -> liftA2 TFun (renameTVars t1) (renameTVars t2)
+    _ -> pure typ
+
+substitute ::
+    TVar -> -- α
+    TVar -> -- α_n
+    Type -> -- A
+    Type -- [α_n/α]A
+substitute tvar1 tvar2 typ = case typ of
+    TLit _ -> typ
+    TVar tvar'
+        | tvar' == tvar1 -> TVar tvar2
+        | otherwise -> typ
+    TFun t1 t2 -> on TFun substitute' t1 t2
+    TAll tvar t -> TAll tvar $ substitute' t
+    TIndexed (Indexed name typs) -> TIndexed . Indexed name $ map substitute' typs
+    _ -> error "Impossible"
+  where
+    substitute' = substitute tvar1 tvar2
+
 -- | Create a new name and add it to name environment.
-newName :: Names -> Ident -> Rn (Names, Ident)
+newName :: Names -> LIdent -> Rn (Names, LIdent)
 newName env old_name = do
     new_name <- makeName old_name
     pure (Map.insert old_name new_name env, new_name)
 
 -- | Create multiple names and add them to the name environment
-newNames :: Names -> [Ident] -> Rn (Names, [Ident])
+newNames :: Names -> [LIdent] -> Rn (Names, [LIdent])
 newNames = mapAccumM newName
 
 -- | Annotate name with number and increment the number @prefix ⇒ prefix_number@.
-makeName :: Ident -> Rn Ident
-makeName (Ident prefix) = gets (\i -> Ident $ prefix ++ "_" ++ show i) <* modify succ
+makeName :: LIdent -> Rn LIdent
+makeName (LIdent prefix) = do
+    i <- gets var_counter
+    let name = LIdent $ prefix ++ "_" ++ show i
+    modify $ \cxt -> cxt{var_counter = succ cxt.var_counter}
+    pure name
+
+nextNameTVar :: TVar -> Rn TVar
+nextNameTVar (MkTVar (LIdent s)) = do
+    i <- gets tvar_counter
+    let tvar = MkTVar . LIdent $ s ++ "_" ++ show i
+    modify $ \cxt -> cxt{tvar_counter = succ cxt.tvar_counter}
+    pure tvar
diff --git a/src/TypeChecker/Bugs.md b/src/TypeChecker/Bugs.md
deleted file mode 100644
index a265cde..0000000
--- a/src/TypeChecker/Bugs.md
+++ /dev/null
@@ -1,83 +0,0 @@
-## Bugs
-
-None known at this moment
-
-main\_bug should not typecheck
-
-```hs
-apply : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c ;
-apply f x = \y. f x y ;
-
-id : 'a -> 'a ;
-id x = x ;
-
-add : _Int -> _Int -> _Int ;
-add x y = x + y ;
-
-main_bug : _Int -> _Int -> _Int ;
-main_bug= (apply id) add ;
-
-idadd : _Int -> _Int -> _Int ;
-idadd = id add ;
-```
-
-main\_bug should typecheck
-
-```hs
-apply : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c ;
-apply f x = \y. f x y ;
-
-id : 'a -> 'a ;
-id x = x ;
-
-add : _Int -> _Int -> _Int ;
-add x y = x + y ;
-
-main_bug : _Int -> _Int -> _Int ;
-main_bug = apply (id add) ;
-
-idadd : _Int -> _Int -> _Int ;
-idadd = id add ;
-```
-
-## Fixed bugs
-
-* 1
-
-```hs
-fmap : ('a -> 'b) -> Maybe ('a) -> Maybe ('b) ;
-fmap f x =
-    case x of {
-        Just x => Just (f x) ;
-        Nothing => Nothing
-    }
-```
-
-* 2
-
-```hs
-data Maybe ('a) where {
-    Nothing : Maybe ('a)
-    Just : 'a -> Maybe ('a)
-};
-
-id : 'a -> 'a ;
-id x = x ;
-
-main : Maybe ('a -> 'a) ; 
-main = Just id;
-```
-
-But this does
-```hs
-data Maybe ('a) where {
-    Nothing : Maybe ('a)
-    Just : 'a -> Maybe ('a)
-};
-
-id : 'b -> 'b ;
-id x = x ;
-
-main : Maybe ('a -> 'a) ; 
-main = Just id;
-```
diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs
index 1339212..4e072d2 100644
--- a/src/TypeChecker/TypeChecker.hs
+++ b/src/TypeChecker/TypeChecker.hs
@@ -4,541 +4,543 @@
 -- | 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.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
-            )
+-- {- | 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
+--             )
 
-{- | Freshen all polymorphic variables, regardless of name
-| freshenType "d" (a -> b -> c) becomes (d -> d -> d)
--}
+-- {- | Freshen all polymorphic variables, regardless of name
+
+{- | 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))
-
-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
-
-retType :: Type -> Type
-retType (TArr _ t2) = retType t2
-retType a = a
-
-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
-
-    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)
-
-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)
-
-{- | 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
 
-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
+-- 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
 
-isPoly :: Type -> Bool
-isPoly (TPol _) = True
-isPoly _ = False
+-- retType :: Type -> Type
+-- retType (TArr _ t2) = retType t2
+-- retType a = a
 
-inferExp :: Exp -> Infer (Type, T.Exp)
-inferExp e = do
-    (s, t, e') <- algoW e
-    let subbed = apply s t
-    return (subbed, replace subbed e')
+-- 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
 
-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
+--     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)
 
-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')
+-- 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)
 
-    -- \| ------------------
-    -- \|   Γ ⊢ i : Int, ∅
+-- {- | 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
 
-    ELit lit ->
-        let lt = litType lit
-         in return (nullSubst, lt, T.ELit lt lit)
-    -- \| x : σ ∈ Γ   τ = inst(σ)
-    -- \| ----------------------
-    -- \|     Γ ⊢ x : τ, ∅
+-- 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
 
-    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
+-- isPoly :: Type -> Bool
+-- isPoly (TPol _) = True
+-- isPoly _ = False
 
-    -- \| τ = newvar   Γ, x : τ ⊢ e : τ', S
-    -- \| ---------------------------------
-    -- \|     Γ ⊢ w λx. e : Sτ → τ', S
+-- inferExp :: Exp -> Infer (Type, T.Exp)
+-- inferExp e = do
+--     (s, t, e') <- algoW e
+--     let subbed = apply s t
+--     return (subbed, replace subbed e')
 
-    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')
+-- 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
 
-    -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S₁
-    -- \| s₂ = mgu(s₁τ₀, Int)    s₃ = mgu(s₂τ₁, Int)
-    -- \| ------------------------------------------
-    -- \|        Γ ⊢ e₀ + e₁ : Int, S₃S₂S₁S₀
-    -- This might be wrong
+-- 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')
 
-    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'
-                )
+--     -- \| ------------------
+--     -- \|   Γ ⊢ i : Int, ∅
 
-    -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S1
-    -- \| τ' = newvar    S₂ = mgu(S₁τ₀, τ₁ → τ')
-    -- \| --------------------------------------
-    -- \|       Γ ⊢ e₀ e₁ : S₂τ', S₂S₁S₀
+--     ELit lit ->
+--         let lt = litType lit
+--          in return (nullSubst, lt, T.ELit lt lit)
+--     -- \| x : σ ∈ Γ   τ = inst(σ)
+--     -- \| ----------------------
+--     -- \|     Γ ⊢ x : τ, ∅
 
-    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')
+--     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₀Γ, x : S̅₀Γ̅(τ) ⊢ e₁ : τ', S₁
-    -- \| ----------------------------------------------
-    -- \|        Γ ⊢ let x = e₀ in e₁ : τ', S₁S₀
+--     -- \| τ = newvar   Γ, x : τ ⊢ e : τ', S
+--     -- \| ---------------------------------
+--     -- \|     Γ ⊢ w λx. e : Sτ → τ', S
 
-    -- The bar over S₀ and Γ means "generalize"
+--     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')
 
-    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₀Γ ⊢ e₁ : τ₁, S₁
+--     -- \| s₂ = mgu(s₁τ₀, Int)    s₃ = mgu(s₂τ₁, Int)
+--     -- \| ------------------------------------------
+--     -- \|        Γ ⊢ e₀ + e₁ : Int, S₃S₂S₁S₀
+--     -- This might be wrong
 
--- | 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
-                ]
+--     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'
+--                 )
 
-{- | 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
+--     -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S1
+--     -- \| τ' = newvar    S₂ = mgu(S₁τ₀, τ₁ → τ')
+--     -- \| --------------------------------------
+--     -- \|       Γ ⊢ e₀ e₁ : S₂τ', S₂S₁S₀
 
--- | 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
+--     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')
 
-{- | 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
+--     -- \| Γ ⊢ e₀ : τ, S₀     S₀Γ, x : S̅₀Γ̅(τ) ⊢ e₁ : τ', S₁
+--     -- \| ----------------------------------------------
+--     -- \|        Γ ⊢ let x = e₀ in e₁ : τ', S₁S₀
 
--- | Compose two substitution sets
-compose :: Subst -> Subst -> Subst
-compose m1 m2 = M.map (apply m1) m2 `M.union` m1
+--     -- The bar over S₀ and Γ means "generalize"
 
--- TODO: Split this class into two separate classes, one for free variables
---       and one for applying substitutions
+--     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)
 
--- | A class representing free variables functions
-class FreeVars t where
-    -- | Get all free variables from t
-    free :: t -> Set Ident
+-- -- | 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
+--                 ]
 
-    -- | Apply a substitution to t
-    apply :: Subst -> t -> t
+-- {- | 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
 
-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
+-- -- | 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
 
-    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))
+-- {- | 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
 
-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)
+-- -- | Compose two substitution sets
+-- compose :: Subst -> Subst -> Subst
+-- compose m1 m2 = M.map (apply m1) m2 `M.union` m1
 
-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)
+-- -- TODO: Split this class into two separate classes, one for free variables
+-- --       and one for applying substitutions
 
-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)
+-- -- | A class representing free variables functions
+-- class FreeVars t where
+--     -- | Get all free variables from t
+--     free :: t -> Set Ident
 
-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)
+--     -- | Apply a substitution to t
+--     apply :: Subst -> t -> t
 
-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)
+-- 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
 
--- | Apply substitutions to the environment.
-applySt :: Subst -> Infer a -> Infer a
-applySt s = local (\st -> st{vars = apply s (vars st)})
+--     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))
 
--- | Represents the empty substition set
-nullSubst :: Subst
-nullSubst = M.empty
+-- 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)
 
--- | 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
+-- 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)
 
--- | 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)})
+-- 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)
 
--- | 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})
+-- 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)
 
--- | Insert a function signature into the environment
-insertSig :: Ident -> Type -> Infer ()
-insertSig i t = modify (\st -> st{sigs = M.insert i t (sigs st)})
+-- 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)
 
--- | Insert a constructor with its data type
-insertConstr :: Ident -> Type -> Infer ()
-insertConstr i t =
-    modify (\st -> st{constructors = M.insert i t (constructors st)})
+-- -- | Apply substitutions to the environment.
+-- applySt :: Subst -> Infer a -> Infer a
+-- applySt s = local (\st -> st{vars = apply s (vars st)})
 
--------- PATTERN MATCHING ---------
+-- -- | Represents the empty substition set
+-- nullSubst :: Subst
+-- nullSubst = M.empty
 
-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)
+-- -- | 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
 
-{- | 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)
+-- -- | 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)})
 
-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
+-- -- | 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})
 
-flattenType :: Type -> [Type]
-flattenType (TArr a b) = flattenType a ++ flattenType b
-flattenType a = [a]
+-- -- | Insert a function signature into the environment
+-- insertSig :: Ident -> Type -> Infer ()
+-- insertSig i t = modify (\st -> st{sigs = M.insert i t (sigs st)})
 
-litType :: Literal -> Type
-litType (LInt _) = TMono "Int"
+-- -- | Insert a constructor with its data type
+-- insertConstr :: Ident -> Type -> Infer ()
+-- insertConstr i t =
+--     modify (\st -> st{constructors = M.insert i t (constructors st)})
+
+-- -------- PATTERN MATCHING ---------
+
+-- 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)
+
+-- {- | 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"
diff --git a/src/TypeChecker/TypeCheckerIr.hs b/src/TypeChecker/TypeCheckerIr.hs
index 016dd8a..2b3c702 100644
--- a/src/TypeChecker/TypeCheckerIr.hs
+++ b/src/TypeChecker/TypeCheckerIr.hs
@@ -2,178 +2,178 @@
 
 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 (..),
+--     Literal (..),
+--     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 Type
+--     , constructors :: Map Ident 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 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 Inj = Inj (Init, Type) Exp
-    deriving (C.Eq, C.Ord, C.Read, C.Show)
+-- data Inj = Inj (Init, Type) Exp
+--     deriving (C.Eq, C.Ord, C.Read, C.Show)
 
-data Def = DBind Bind | DData Data
-    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 Id = (Ident, Type)
+-- type Id = (Ident, Type)
 
-data Bind = Bind Id Exp
-    deriving (C.Eq, C.Ord, C.Show, C.Read)
+-- data Bind = Bind Id Exp
+--     deriving (C.Eq, C.Ord, C.Show, C.Read)
 
-instance Print [Def] where
-    prt _ [] = concatD []
-    prt _ (x : xs) = concatD [prt 0 x, doc (showString "\n"), prt 0 xs]
+-- instance Print [Def] where
+--     prt _ [] = concatD []
+--     prt _ (x : xs) = concatD [prt 0 x, doc (showString "\n"), prt 0 xs]
 
-instance Print Def where
-    prt i (DBind bind) = prt i bind
-    prt i (DData d) = prt i d
+-- instance Print Def where
+--     prt i (DBind bind) = prt i bind
+--     prt i (DData d) = prt i d
 
-instance Print Program where
-    prt i (Program sc) = prPrec i 0 $ prt 0 sc
+-- instance Print Program where
+--     prt i (Program sc) = prPrec i 0 $ prt 0 sc
 
-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 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 [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 [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]
 
-prtIdPs :: Int -> [Id] -> Doc
-prtIdPs i = prPrec i 0 . concatD . map (prtIdP i)
+-- prtIdPs :: Int -> [Id] -> Doc
+-- prtIdPs i = prPrec i 0 . concatD . map (prtIdP i)
 
-prtId :: Int -> Id -> Doc
-prtId i (name, t) =
-    prPrec i 0 $
-        concatD
-            [ prt 0 name
-            , doc $ showString ":"
-            , prt 0 t
-            ]
+-- prtId :: Int -> Id -> Doc
+-- prtId i (name, t) =
+--     prPrec i 0 $
+--         concatD
+--             [ prt 0 name
+--             , doc $ showString ":"
+--             , prt 0 t
+--             ]
 
-prtIdP :: Int -> Id -> Doc
-prtIdP i (name, t) =
-    prPrec i 0 $
-        concatD
-            [ doc $ showString "("
-            , prt 0 name
-            , doc $ showString ":"
-            , prt 0 t
-            , doc $ showString ")"
-            ]
+-- 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 _ (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"
-                    ]
-                )
+-- 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"
+--                     ]
+--                 )
 
-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 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 [Inj] where
+--     prt _ [] = concatD []
+--     prt _ [x] = concatD [prt 0 x]
+--     prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
diff --git a/test_program b/test_program
index d916d03..f14962d 100644
--- a/test_program
+++ b/test_program
@@ -1,24 +1,4 @@
-data Maybe ('a) where {
-    Nothing : Maybe ('a)
-    Just : 'a -> Maybe ('a)
-};
-
-fromJust : Maybe ('a) -> 'a ;
-fromJust a =
-    case a of {
-        Just a => a
-    };
-
-fromMaybe : 'a -> Maybe ('a) -> 'a ;
-fromMaybe a b =
-    case b of {
-        Just a => a;
-        Nothing => a
-    };
-
-maybe : 'b -> ('a -> 'b) -> Maybe ('a) -> 'b;
-maybe b f ma =
-    case ma of {
-        Just a => f a;
-        Nothing => b
-    }
+data Maybe (a) where {
+    Nothing : Maybe (a)
+    Just : a -> Maybe (a)
+}