diff --git a/Justfile b/Justfile
index ea2d031..8079213 100644
--- a/Justfile
+++ b/Justfile
@@ -10,6 +10,13 @@ clean:
 test:
     cabal test
 
+ctest:
+    cabal run language sample-programs/basic-1
+    cabal run language sample-programs/basic-2
+    cabal run language sample-programs/basic-3
+    cabal run language sample-programs/basic-4
+    cabal run language sample-programs/basic-5
+
 # compile a specific file
 run FILE:
     cabal run language {{FILE}}
diff --git a/fourmolu.yaml b/fourmolu.yaml
index cf7ab2f..8b96b58 100644
--- a/fourmolu.yaml
+++ b/fourmolu.yaml
@@ -1,14 +1 @@
-indentation: 4
-function-arrows: trailing
-comma-style: leading
-import-export-style: diff-friendly
 indent-wheres: false
-record-brace-space: true
-newlines-between-decls: 1
-haddock-style: multi-line
-haddock-style-module:
-let-style: auto
-in-style: right-align
-respectful: false
-fixities: []
-unicode: never
diff --git a/sample-programs/basic-1 b/sample-programs/basic-1
index f109950..5cb2b2a 100644
--- a/sample-programs/basic-1
+++ b/sample-programs/basic-1
@@ -1,2 +1,2 @@
-
-f = \x. x+1;
+f : _Int -> _Int ;
+f = \x. x+1 ;
diff --git a/sample-programs/basic-2 b/sample-programs/basic-2
index f7d0807..2f0448c 100644
--- a/sample-programs/basic-2
+++ b/sample-programs/basic-2
@@ -1,3 +1,5 @@
+add : _Int -> _Int -> _Int ;
 add x = \y. x+y;
 
-main = (\z. z+z) ((add 4) 6);
+main : _Int ;
+main = (\z. z+z) ((add 4) 6) ;
diff --git a/sample-programs/basic-3 b/sample-programs/basic-3
index 9443439..7ba4971 100644
--- a/sample-programs/basic-3
+++ b/sample-programs/basic-3
@@ -1,2 +1,2 @@
-
-main = (\x. x+x+3) ((\x. x) 2)
+main : _Int ;
+main = (\x. x+x+3) ((\x. x) 2) ;
diff --git a/sample-programs/basic-4 b/sample-programs/basic-4
index 1de7a8c..365e4cb 100644
--- a/sample-programs/basic-4
+++ b/sample-programs/basic-4
@@ -1,2 +1,2 @@
-
+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 9984ddd..e42b5f9 100644
--- a/sample-programs/basic-5
+++ b/sample-programs/basic-5
@@ -1,9 +1,14 @@
-id x = x;
+-- double : _Int -> _Int ;
+-- double n = n + n;
 
-add x y = x + y;
+apply : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c ;
+apply f x = \y. f x y ;
 
-double n = n + n;
+id : 'a -> 'a ;
+id x = x ;
 
-apply f x = \y. f x y;
+add : _Int -> _Int -> _Int ;
+add x y = x + y ;
 
-main = apply (id add) ((\x. x + 1) 1) (double 3);
+main : _Int -> _Int -> _Int ;
+main = (id add) 1 2 ;
diff --git a/src/Main.hs b/src/Main.hs
index bef4a3b..7e3922d 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -3,15 +3,15 @@
 module Main where
 
 -- import           Codegen.Codegen           (compile)
-import           Grammar.ErrM            (Err)
-import           Grammar.Par             (myLexer, pProgram)
-import           Grammar.Print           (printTree)
+import Grammar.ErrM (Err)
+import Grammar.Par (myLexer, pProgram)
+import Grammar.Print (printTree)
 
 -- import           LambdaLifter.LambdaLifter (lambdaLift)
-import           Renamer.Renamer         (rename)
-import           System.Environment      (getArgs)
-import           System.Exit             (exitFailure, exitSuccess)
-import           TypeChecker.TypeChecker (typecheck)
+import Renamer.Renamer (rename)
+import System.Environment (getArgs)
+import System.Exit (exitFailure, exitSuccess)
+import TypeChecker.TypeChecker (typecheck)
 
 main :: IO ()
 main =
diff --git a/src/TypeChecker/Bugs.md b/src/TypeChecker/Bugs.md
index 616f0fe..a7875d1 100644
--- a/src/TypeChecker/Bugs.md
+++ b/src/TypeChecker/Bugs.md
@@ -1,8 +1,22 @@
 ## Bugs
 
-### Polymorphic type variables are global?
+None known at this moment
+
+## 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
 
-This doesn't work (occurs check failed, can't unify `(a -> a) = a`
 ```hs
 data Maybe ('a) where {
     Nothing : Maybe ('a)
@@ -29,16 +43,3 @@ id x = x ;
 main : Maybe ('a -> 'a) ; 
 main = Just id;
 ```
-UPDATE: Might have found a fix. Need to be tested.
-
-### The function f is not carried into the case-expression
-
-Code example that does not type check
-```hs
-fmap : ('a -> 'b) -> Maybe ('a) -> Maybe ('b) ;
-fmap f x =
-    case x of {
-        Just x => Just (f x) ;
-        Nothing => Nothing
-    }
-```
diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs
index e1a6a2c..607dcfe 100644
--- a/src/TypeChecker/TypeChecker.hs
+++ b/src/TypeChecker/TypeChecker.hs
@@ -61,7 +61,7 @@ freshenData (Data (Constr name ts) constrs) = do
   where
     freshenType :: Ident -> Type -> Type
     freshenType iden = \case
-        (TPol a) -> TPol iden
+        (TPol _) -> TPol iden
         (TArr a b) -> TArr (freshenType iden a) (freshenType iden b)
         (TConstr (Constr a ts)) ->
             TConstr (Constr a (map (freshenType iden) ts))
diff --git a/tests/Tests.hs b/tests/Tests.hs
index 5c52939..6e20745 100644
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -1,20 +1,26 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
 {-# HLINT ignore "Use <$>" #-}
 {-# HLINT ignore "Use camelCase" #-}
 
 module Main where
 
-import           Data.Either               (isLeft, isRight)
-import           Data.Map                  (Map)
-import qualified Data.Map                  as M
-import           Grammar.Abs
-import           Test.Hspec
-import           Test.QuickCheck
-import           TypeChecker.TypeChecker
-import qualified TypeChecker.TypeCheckerIr as T
-import           TypeChecker.TypeCheckerIr (Ctx (..), Env (..), Error, Infer,
-                                            Poly (..))
+import Data.Either (isLeft, isRight)
+import Data.Map (Map)
+import Data.Map qualified as M
+import Grammar.Abs
+import Test.Hspec
+import Test.QuickCheck
+import TypeChecker.TypeChecker
+import TypeChecker.TypeCheckerIr (
+    Ctx (..),
+    Env (..),
+    Error,
+    Infer,
+    Poly (..),
+ )
+import TypeChecker.TypeCheckerIr qualified as T
 
 main :: IO ()
 main = hspec $ do
@@ -67,10 +73,11 @@ infer_eabs = describe "algoW used on EAbs" $ do
     it "should infer the argument type as polymorphic if it is not used in the lambda" $ do
         let lambda = EAbs "x" (ELit (LInt 0))
         getType lambda `shouldSatisfy` isArrowPolyToMono
+
     it "should infer a variable as function if used as one" $ do
         let lambda = EAbs "f" (EAbs "x" (EApp (EId "f") (EId "x")))
         let isOk (Right (TArr (TArr (TPol _) (TPol _)) (TArr (TPol _) (TPol _)))) = True
-            isOk _                                                                = False
+            isOk _ = False
         getType lambda `shouldSatisfy` isOk
 
 infer_eapp = describe "algoW used on EApp" $ do
@@ -81,9 +88,21 @@ infer_eapp = describe "algoW used on EApp" $ do
             let ctx = Ctx (M.singleton (Ident (x :: String)) t)
             getTypeC env ctx (EApp (EId (Ident x)) (EId (Ident x))) `shouldBe` Left "Occurs check failed"
 
+churf_id :: Bind 
+churf_id = Bind "id" (TArr (TPol "a") (TPol "a")) "id" ["x"] (EId "x")
+
+churf_add :: Bind
+churf_add = Bind "add" (TArr (TMono "Int") (TArr (TMono "Int") (TMono "Int"))) "add" ["x", "y"] (EAdd (EId "x") (EId "y"))
+
+churf_main :: Bind
+churf_main = Bind "main" (TArr (TMono "Int") (TArr (TMono "Int") (TMono "Int"))) "main" [] (EApp (EId "id") (EId "add"))
+
+test_bug :: IO ()
+test_bug = undefined
+
 isArrowPolyToMono :: Either Error Type -> Bool
 isArrowPolyToMono (Right (TArr (TPol _) (TMono _))) = True
-isArrowPolyToMono _                                 = False
+isArrowPolyToMono _ = False
 
 -- | Empty environment
 getType :: Exp -> Either Error Type