better rendering for type errors and evaluation

5 files changed, 30 insertions, 10 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
index 2e1814e..ab590c6 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
@@ -14,6 +14,7 @@ import GHC.Generics (Generic)
 import qualified Minilang.Lambda.Eval as Eval
 import Minilang.Lambda.Unify (Type (..), UnifyError, apply, unify)
 import Prelude hiding (lookup)
+import qualified Minilang.Lambda.Unify as Unify
 
 data ATerm ann
   = Var Text ann
@@ -25,6 +26,9 @@ data TypeError
   = UnifyError UnifyError
   deriving (Show, Eq)
 
+render :: TypeError -> Text
+render (UnifyError ue) = Unify.render ue
+
 fromTerm :: Eval.Term -> ATerm ()
 fromTerm (Eval.Var x) = Var x ()
 fromTerm (Eval.Lam x body) = Lam x (fromTerm body) ()
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
index f3fff04..96e9990 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
@@ -46,10 +46,17 @@ apply subs t =
   foldr (\(x, s) -> subst s x) t subs
 
 data UnifyError
-  = MismatchHead Text Text [Type] [Type]
-  | Circularity Identifier Type
+  = Circularity Identifier Type
   deriving (Show, Eq)
 
+render :: UnifyError -> Text
+render (Circularity x t) =
+  "Cannot unify type variable "
+    <> x
+    <> " with type "
+    <> pretty t
+    <> " due to circularity: The variable already occurs in the type."
+
 unifyOne :: Type -> Type -> Either UnifyError Substitution
 unifyOne (TyVar x) (TyVar y) = if x == y then Right [] else Right [(x, TyVar y)]
 unifyOne (f :-> g) (f' :-> g') =
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs b/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs
index cbc7988..3583020 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs
@@ -29,6 +29,7 @@ import System.Console.Haskeline
 import System.Directory (listDirectory)
 import Minilang.Lambda.Parser (resugar, pretty)
 import qualified Minilang.Lambda.Unify as Unify
+import Minilang.REPL.Pure (render)
 
 -- * Haskeline REPL
 
@@ -44,19 +45,13 @@ instance MonadREPL Haskeline where
     case i of
       Nothing -> pure EOF
       Just (pack -> t) -> pure $ interpret t
-  output = hoist . outputStrLn . render
+  output = hoist . outputStrLn . unpack . render
   prompt = pure ()
   load = fmap (first FileError) . hoist . lift . try . Text.readFile . unpack
 
   getEnv = get
   setEnv = put
 
-render :: Out -> String
-render = \case
-  Msg t -> unpack t
-  Evaluated term typ -> unpack $ pretty (resugar term) <> " : " <> Unify.pretty typ
-  other -> show other
-
 completion :: CompletionFunc IO
 completion = completion' . first reverse
 
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
index c90ecde..9c31987 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
@@ -16,6 +16,7 @@ import Minilang.Lambda.Eval (newEnv)
 import Minilang.Lambda.Infer (infer, newContext)
 import Minilang.Lambda.Parser (desugar, parse)
 import Minilang.REPL.Types
+import qualified Minilang.Lambda.Infer as Infer
 
 -- | Run a REPL session
 runREPL ::
@@ -41,7 +42,7 @@ handleUserInput txt = do
     Right expr -> do
       let term = desugar expr
       case infer term of
-        Left typeError -> output (Msg $ pack $ show typeError)
+        Left typeError -> output (Msg $ Infer.render typeError)
         Right typ -> do
           let v = fromDeBruijn $ eval (toDeBruijn term)
           output (Evaluated v typ)
diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
index 4eb3f4d..f6279c1 100644
--- a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
@@ -23,6 +23,19 @@ spec = parallel $
                      "y : b"
                    ]
 
+    it "defaults to try to typecheck terms" $ do
+      let out =
+            withInput
+              [ "(let ((Succ (lam (n z s) (s n))) \
+                \ (Zero (lam (z s) z))) \
+                \ (Succ (Succ Zero)))"
+              ]
+
+      out
+        `shouldBe` [ "Bye!",
+                     "Cannot unify type variable f with type (e -> f -> e) -> e due to circularity: The variable already occurs in the type."
+                   ]
+
     it "shows error when trying to load a non-existent file" $ do
       withInput [":load foo"]
         `shouldBe` [ "Bye!",