From fe63fa62157048026a8c3778d39607b8a58c36a7 Mon Sep 17 00:00:00 2001
From: sebastianselander <sebastian.selander@gmail.com>
Date: Sun, 5 Mar 2023 13:24:56 +0100
Subject: [PATCH] Improved error message and created document for known bugs.

---
 src/TypeChecker/Bugs.md        | 43 +++++++++++++++++++
 src/TypeChecker/TypeChecker.hs |  2 +-
 test_program                   | 75 +++++++++++++++++++---------------
 3 files changed, 85 insertions(+), 35 deletions(-)
 create mode 100644 src/TypeChecker/Bugs.md

diff --git a/src/TypeChecker/Bugs.md b/src/TypeChecker/Bugs.md
new file mode 100644
index 0000000..ce95446
--- /dev/null
+++ b/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
+    }
+```
diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs
index 09d5204..53e3678 100644
--- a/src/TypeChecker/TypeChecker.hs
+++ b/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
diff --git a/test_program b/test_program
index 5f6cce9..f8dd9bc 100644
--- a/test_program
+++ b/test_program
@@ -1,43 +1,50 @@
-data Bool () where {
-    True : Bool () 
-    False : Bool ()
-};
-
-data List ('a) where {
-    Nil : List ('a) 
-    Cons : ('a) -> List ('a) -> List ('a)
-};
+-- data Bool () where {
+--     True : Bool () 
+--     False : Bool ()
+-- };
+-- 
+-- data List ('a) where {
+--     Nil : 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
-holdFn : Maybe ('b -> 'b) ;
-holdFn = Just id ;
+main : Maybe ('a -> 'a) ; 
+main = 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
+--     }