Improved error message and created document for known bugs.

src/TypeChecker/Bugs.md

@@ -0,0 +1,43 @@
+## Bugs
+
+### Polymorphic type variables are global?
+
+This doesn't work (occurs check failed, can't unify `(a -> a) = a`
+```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;
+```
+
+### 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
+    }
+```

src/TypeChecker/TypeChecker.hs

@@ -272,7 +272,7 @@ unify t0 t1 = case (trace ("LEFT: " ++ show t0) t0, trace ("RIGHT: " ++ show t1)
 occurs :: Ident -> Type -> Infer Subst
 occurs _ (TPol _) = return nullSubst
 occurs i t = if S.member i (free t)
-                then throwError "Occurs check failed"
+                then throwError $ unwords ["Occurs check failed, can't unify", printTree (TPol i), "with", printTree t]
                 else return $ M.singleton i t
 
 -- | Generalize a type over all free variables in the substitution set

test_program

@@ -1,43 +1,50 @@
-data Bool () where {
+-- data Bool () where {
-    True : Bool () 
+--     True : Bool () 
-    False : Bool ()
+--     False : Bool ()
-};
+-- };
-
+-- 
-data List ('a) where {
+-- data List ('a) where {
-    Nil : List ('a) 
+--     Nil : List ('a) 
-    Cons : ('a) -> List ('a) -> List ('a)
+--     Cons : ('a) -> List ('a) -> List ('a)
-};
+-- };
 
 data Maybe ('a) where {
     Nothing : Maybe ('a)
     Just : 'a -> Maybe ('a)
 };
 
-data Either ('a 'b) where {
-    Left : 'a -> Either ('a 'b)
-    Right : 'b -> Either ('a 'b)
-};
-
-safeHead : List ('a) -> Maybe ('a) ;
-safeHead xs =
-    case xs of {
-        Nil => Nothing ;
-        Cons x xs => Just x
-    };
-
-main : Maybe (_Int) ;
-main = safeHead (Cons 0 (Cons 1 Nil)) ;
-
-maybeToEither : Either ('a 'b) ->  Maybe ('a) ;
-maybeToEither e =
-    case e of {
-        Left y => Nothing ;
-        Right x => Just x
-    };
-
 id : 'a -> 'a ;
 id x = x ;
 
--- Bug, occurs check failed
+main : Maybe ('a -> 'a) ; 
-holdFn : Maybe ('b -> 'b) ;
+main = Just id;
-holdFn = Just id ;
+
+-- data Either ('a 'b) where {
+--     Left : 'a -> Either ('a 'b)
+--     Right : 'b -> Either ('a 'b)
+-- };
+
+-- safeHead : List ('a) -> Maybe ('a) ;
+-- safeHead xs =
+--     case xs of {
+--         Nil => Nothing ;
+--         Cons x xs => Just x
+--     };
+
+-- main : Maybe (_Int) ;
+-- main = safeHead (Cons 0 (Cons 1 Nil)) ;
+-- 
+-- maybeToEither : Either ('a 'b) ->  Maybe ('a) ;
+-- maybeToEither e =
+--     case e of {
+--         Left y => Nothing ;
+--         Right x => Just x
+--     };
+-- 
+-- -- Bug. f not included in the case-expression context
+-- fmap : ('a -> 'b) -> Maybe ('a) -> Maybe ('b) ;
+-- fmap f x =
+--     case x of {
+--         Just x => Just (f x) ;
+--         Nothing => Nothing
+--     }