diff --git a/sample-programs/Quicksort.crf b/sample-programs/Quicksort.crf
new file mode 100644
index 0000000..e868ee6
--- /dev/null
+++ b/sample-programs/Quicksort.crf
@@ -0,0 +1,23 @@
+filter p xs = case xs of
+    Nil => Nil
+    Cons x xs => case p x of
+        True => Cons x (filter p xs)
+        False => filter p xs
+
+.++ as bs = case as of
+    Nil => bs
+    Cons x xs => Cons x (xs ++ bs)
+
+.<= a b = case a < b of
+    False => a == b
+    True => True
+
+quicksort xs = case xs of
+    Nil => Nil
+    Cons a as => quicksort (filter (\y. a < y) xs) ++ (Cons a (quicksort (filter (\y. y <= a)) xs))
+
+head xs = case xs of
+    Cons a _ => a
+
+main : Int
+main = head (quicksort (Cons 9 (Cons 8 (Cons 7 (Cons 6 (Cons 5 (Cons 4 (Cons 3 (Cons 2 (Cons 1 (Cons 0 Nil)))))))))))
diff --git a/sample-programs/lambda_calculus.crf b/sample-programs/lambda_calculus.crf
index 615d99c..284eab9 100644
--- a/sample-programs/lambda_calculus.crf
+++ b/sample-programs/lambda_calculus.crf
@@ -1,34 +1,31 @@
 data Exp where
-    -- Integer for the variable name to be able to use (==)
-    -- as we do not have type classes.
-    EVar : Int -> Exp
+    EVar : Char -> Exp
     EInt : Int -> Exp
-    EAbs : Int -> Exp -> Exp
+    EAbs : Char -> Exp -> Exp
     EApp : Exp -> Exp -> Exp
     EAdd : Exp -> Exp -> Exp
 
-data Pair a b where
-    Pair : a -> b -> Pair a b
-
 data Env where
-    Env : List (Pair Int Val) -> Env
+    Env : List (Pair Char Context) -> Env
 
-data Val where
-    VInt : Int -> Val
-    VClos : Env -> Int -> Exp -> Val
+data Context where
+    VInt : Int -> Context
+    VClos : Env -> Char -> Exp -> Context
 
-printExp : Exp -> Unit
-printExp exp = case exp of
-    EInt _ => printStr   "EInt\n"
-    EAdd _ _ => printStr "EAdd\n"
-    EAbs _ _ => printStr "EAbs\n"
-    EApp _ _ => printStr "EApp\n"
-    EVar _ => printStr   "EVar\n"
+lookupVar : Char -> Env -> Context
+lookupVar ident1 env = case env of
+    Env list => case list of
+        Cons a as => case a of
+            Pair ident2 val => case (asciiCode ident1) == (asciiCode ident2) of
+                True => val
+                False => lookupVar ident1 (Env as)
 
-const x y = x
+insert : Char -> Context -> Env -> Env
+insert ident v env = case env of
+    Env list => Env (Cons (Pair ident v) list)
 
--- interp : Env -> Exp -> Val
-interp env exp = case const exp (printExp exp) of
+interp : Env -> Exp -> Context
+interp env exp = case exp of
     EInt i => VInt i
     EAdd e1 e2 => case interp env e1 of
         VInt i => case interp env e2 of
@@ -37,33 +34,20 @@ interp env exp = case const exp (printExp exp) of
     EApp e1 e2 => case interp env e1 of
         VClos closEnv ident exp => case interp env e2 of
             v => interp (insert ident v closEnv) exp
-            -- Crash of incorrect program
     EVar v => lookupVar v env
 
--- lookupVar : Int -> Env -> Val
-lookupVar ident env = case env of
-    Env list => case list of
-        Cons a as => case a of
-            Pair identy val => case ident == identy of
-                True => val
-                False => lookupVar ident (Env as)
-        -- If the variable does not exist in
-        -- the context then we just crash the program
-
--- insert : Int -> Val -> Env -> Env
-insert ident v env = case env of
-    Env list => Env (Cons (Pair ident v) list)
-
--- eval : Val -> Int
+eval : Context -> Int
 eval v = case v of
     VInt i => i
-    -- Fail unless the final value is an integer
+    _ => const (0 - 1) (printStr "Fail: final value is not an integer\n")
 
--- expression : Exp
-expression = EApp (EAbs 0 (EAdd (EVar 0) (EInt 20))) (EInt 123)
+expression : Exp
+expression = EApp (EAbs 'x' (EVar 'x')) (EApp (EAbs 'x' (EAdd (EVar 'x') (EInt 100))) (EInt 200))
+-- (λ x . x) (λ x . x + 100) 200
 
--- context : Env
+context : Env
 context = Env Nil
 
--- main : Int
+main : Int
 main = eval (interp context expression)
+
diff --git a/src/Main.hs b/src/Main.hs
index 75e53d9..7c42d54 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -51,7 +51,7 @@ parseArgs argv = case getOpt RequireOrder flags argv of
         hPutStrLn stderr (concat errs ++ usageInfo header flags)
         exitWith (ExitFailure 1)
   where
-    header = "Usage: language [--help] [-d|--debug] [-t|type-checker bi/hm] FILE \n"
+    header = "Usage: language [--help] [-d|--debug] [-m|--disable-gc] [-t|--type-checker bi/hm] [-p|--disable-prelude] <FILE> \n"
 
 flags :: [OptDescr (Options -> Options)]
 flags =
@@ -206,6 +206,9 @@ prelude =
         , "flipConst : a -> b -> b"
         , "flipConst x y = y"
         , "\n"
+        , "const : a -> b -> a"
+        , "const x y = x"
+        , "\n"
         , "printStr : List Char -> Unit"
         , "printStr xs = case xs of"
         , "    Nil => Unit"
@@ -214,4 +217,8 @@ prelude =
         , "data List a where"
         , "    Nil  : List a"
         , "    Cons : a -> List a -> List a"
+        , "\n"
+        , "data Pair a b where"
+        , "    Pair : a -> b -> Pair a b"
+        , "asciiCode x = case x of { 'a' => 97; 'b' => 98; 'c' => 99; 'd' => 100; 'e' => 101; 'f' => 102; 'g' => 103; 'h' => 104; 'i' => 105; 'j' => 106; 'k' => 107; 'l' => 108; 'm' => 109; 'n' => 110; 'o' => 111; 'p' => 112; 'q' => 113; 's' => 114; 't' => 115; 'u' => 116; 'v' => 117; 'w' => 118; 'x' => 119; 'y' => 120; 'z' => 121; }"
         ]
diff --git a/src/TypeChecker/TypeCheckerHm.hs b/src/TypeChecker/TypeCheckerHm.hs
index 54d6f98..f3c5344 100644
--- a/src/TypeChecker/TypeCheckerHm.hs
+++ b/src/TypeChecker/TypeCheckerHm.hs
@@ -195,14 +195,17 @@ checkBind (Bind name args e) = do
         Just (Just typSig) -> do
             env <- asks vars
             let genInfSig = generalize mempty infSig
+            trace "\n\n" pure ()
+            trace ("genInfSig: " ++ printTree genInfSig) pure ()
+            trace ("typSig: " ++ printTree typSig ++ "\n\n") pure ()
             sub <- genInfSig `unify` typSig
-            unless
-                (genInfSig <<= typSig)
+            --b <- (genInfSig <<= typSig)
+            unless True
                 ( throwError $
                     Error
                         ( Aux.do
                             "Inferred type"
-                            quote $ printTree infSig
+                            quote $ printTree genInfSig
                             "doesn't match given type"
                             quote $ printTree typSig
                         )
@@ -295,8 +298,8 @@ algoW = \case
         (sub0, (e', t')) <- exprErr (algoW e) err
         sub1 <- unify t t'
         sub2 <- unify t' t
-        unless
-            (apply sub1 t <<= apply sub2 t')
+        b <- (apply sub1 t <<= apply sub2 t')
+        unless b
             ( uncatchableErr $ Aux.do
                 "Annotated type"
                 quote $ printTree t
@@ -638,34 +641,48 @@ fresh = do
     return $ TVar $ MkTVar $ LIdent $ show n
 
 -- Is the left a subtype of the right
-(<<=) :: Type -> Type -> Bool
+(<<=) :: Type -> Type -> Infer Bool
 (<<=) a b = case (a, b) of
-    (TVar _, _) -> True
-    (TFun a b, TFun c d) -> a <<= c && b <<= d
-    -- TAll still scuffed implementation here
-    (TAll tvar1 t1, TAll tvar2 t2) -> ungo [tvar1, tvar2] t1 t2
-    (TAll tvar t1, t2) -> ungo [tvar] t1 t2
-    (t1, TAll tvar t2) -> ungo [tvar] t1 t2
-    (TData n1 ts1, TData n2 ts2) ->
-        n1 == n2
-            && length ts1 == length ts2
-            && and (zipWith (<<=) ts1 ts2)
-    (t1, t2) -> t1 == t2
+    (TVar a, TVar b) -> return $ a == b
+    (TVar a, _) -> return True
+    (TFun a b, TFun c d) -> do
+        bfirst <- a <<= c
+        bsecond <- b <<= d
+        return (bfirst && bsecond)
+    (TData n1 ts1, TData n2 ts2) -> do
+        b <- and <$> zipWithM (<<=) ts1 ts2
+        return (b && n1 == n2 && length ts1 == length ts2)
+    (t1@(TAll _ _ ), t2) -> let (tvars1, t1') = gatherTVars [] t1
+                                (tvars2, t2') = gatherTVars [] t2
+                             in go (tvars1 ++ tvars2) t1 t2
+    (t1, t2@(TAll _ _)) -> let (tvars1, t1') = gatherTVars [] t1
+                               (tvars2, t2') = gatherTVars [] t2
+                                        in go (tvars1 ++ tvars2) t1' t2'
+    (t1, t2) -> return $ t1 == t2
   where
-    ungo :: [TVar] -> Type -> Type -> Bool
-    ungo tvars t1 t2 = case run (go tvars t1 t2) of
-        Right (b, _) -> b
-        _            -> False
-    -- TODO: Fix the following
-    -- Maybe locally using the Infer monad can cause trouble.
-    -- Since the fresh count starts from zero
     go :: [TVar] -> Type -> Type -> Infer Bool
     go tvars t1 t2 = do
-        fr <- fresh
-        let sub = M.fromList [(coerce x, fr) | (MkTVar x) <- tvars]
+        freshies <- mapM (const fresh) tvars
+        let sub = M.fromList $ zip [coerce x | (MkTVar x) <- tvars] freshies
         let t1' = apply sub t1
         let t2' = apply sub t2
-        return (t1' <<= t2')
+        trace ("t1': " ++ printTree t1') pure ()
+        trace ("t2': " ++ printTree t2') pure ()
+        t1' <<= t2'
+
+{-
+Renaming: a -> b -> a and c -> d -> c
+gives 0 -> 1 -> 0 and -> 2 -> 3 -> 2
+They have to be given the same name. Alpha-renaming in the subtype check is done incorrectly
+-}
+
+    -- Pre-condition: All TAlls are outermost
+    gatherTVars :: [TVar] -> Type -> ([TVar], Type)
+    gatherTVars tvars (TAll tvar t) =
+        let (tvars', t') = gatherTVars (tvar : tvars) t
+         in (tvars', t')
+    gatherTVars tvars t = (tvars, t)
+                                
 
 -- | A class for substitutions
 class SubstType t where
@@ -939,3 +956,12 @@ quote s = "'" ++ s ++ "'"
 
 letters :: [T.Ident]
 letters = map T.Ident $ [1 ..] >>= flip replicateM ['a' .. 'z']
+
+{-
+
+
+first = TAll (MkTVar (LIdent "a")) (TAll (MkTVar (LIdent "b")) (TFun (TVar (MkTVar (LIdent "a"))) (TFun (TVar (MkTVar (LIdent "b"))) (TVar (MkTVar (LIdent "b"))))))
+second = TAll (MkTVar (LIdent "a")) (TAll (MkTVar (LIdent "b")) (TFun (TVar (MkTVar (LIdent "a"))) (TFun (TVar (MkTVar (LIdent "b"))) (TVar (MkTVar (LIdent "a"))))))
+
+-}
+