From fc2cd3f03f389a764d4559622b152eada152e758 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Tue, 29 Mar 2022 18:00:14 +0100
Subject: [PATCH 1/7] [typecheck] Add error infrastructure for type errors

Add a pretty error for mismatched constructor type in a pattern match
---
 app/Main.hs                                   |  2 +-
 src/MiniJuvix/Syntax/MicroJuvix/Error.hs      | 40 ++++++++++++++++
 .../Syntax/MicroJuvix/Error/Pretty.hs         |  9 ++++
 .../Syntax/MicroJuvix/Error/Pretty/Ansi.hs    | 16 +++++++
 .../Syntax/MicroJuvix/Error/Pretty/Base.hs    | 25 ++++++++++
 .../Syntax/MicroJuvix/Error/Pretty/Text.hs    |  9 ++++
 .../Syntax/MicroJuvix/Error/Types.hs          | 13 +++++
 src/MiniJuvix/Syntax/MicroJuvix/Language.hs   |  1 +
 src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs     |  9 ++++
 .../Syntax/MicroJuvix/Pretty/Base.hs          |  3 ++
 .../Syntax/MicroJuvix/TypeChecker.hs          | 48 +++++++------------
 11 files changed, 143 insertions(+), 32 deletions(-)
 create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error.hs
 create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs
 create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs
 create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
 create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Text.hs
 create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
 create mode 100644 src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs

diff --git a/app/Main.hs b/app/Main.hs
index fdf022d4c..11d2909fc 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -262,7 +262,7 @@ go c = do
       Micro.printPrettyCodeDefault micro
       putStrLn ""
       case Micro.checkModule micro of
-        Left er -> putStrLn er
+        Left er -> printErrorAnsi er
         Right {} -> putStrLn "Well done! It type checks"
     MiniHaskell MiniHaskellOptions {..} -> do
       m <- parseModuleIO _mhaskellInputFile
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
new file mode 100644
index 000000000..ca360c72b
--- /dev/null
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
@@ -0,0 +1,40 @@
+module MiniJuvix.Syntax.MicroJuvix.Error
+  ( module MiniJuvix.Syntax.MicroJuvix.Error,
+    module MiniJuvix.Syntax.MicroJuvix.Error.Pretty,
+    module MiniJuvix.Syntax.MicroJuvix.Error.Types,
+  )
+where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty
+import qualified MiniJuvix.Syntax.MicroJuvix.Error.Pretty as P
+import MiniJuvix.Syntax.MicroJuvix.Error.Types
+import Prettyprinter
+
+data TypeCheckerError
+ = ErrTooManyPatterns
+ | ErrWrongConstructorType WrongConstructorType
+ | ErrConstructorAppArgs
+ | ErrWrongType
+ | ErrExpectedFunctionType
+
+prettyT :: Text -> Doc Eann
+prettyT = pretty
+
+ppTypeCheckerError :: TypeCheckerError -> Doc Eann
+ppTypeCheckerError = \case
+  ErrWrongConstructorType e -> ppError e
+  ErrTooManyPatterns -> prettyT "too many patterns"
+  ErrConstructorAppArgs -> prettyT "constructor has wrong args"
+  ErrWrongType -> prettyT "wrong type"
+  ErrExpectedFunctionType -> prettyT "expected function type"
+
+docStream :: TypeCheckerError -> SimpleDocStream Eann
+docStream = layoutPretty defaultLayoutOptions . ppTypeCheckerError
+
+instance JuvixError TypeCheckerError where
+  renderAnsiText :: TypeCheckerError -> Text
+  renderAnsiText = renderAnsi . docStream
+
+  renderText :: TypeCheckerError -> Text
+  renderText = P.renderText . docStream
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs
new file mode 100644
index 000000000..350ff9756
--- /dev/null
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty.hs
@@ -0,0 +1,9 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Pretty
+  ( module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base,
+    module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi,
+    module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Text)
+where
+
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Text
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs
new file mode 100644
index 000000000..4de4d0da0
--- /dev/null
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Ansi.hs
@@ -0,0 +1,16 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Ansi where
+
+import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as M
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base
+import Prettyprinter
+import Prettyprinter.Render.Terminal
+
+renderAnsi :: SimpleDocStream Eann -> Text
+renderAnsi = renderStrict . reAnnotateS stylize
+
+stylize :: Eann -> AnsiStyle
+stylize a = case a of
+  Highlight -> colorDull Red
+  MicroAnn m -> M.stylize m
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
new file mode 100644
index 000000000..159a9e7fd
--- /dev/null
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
@@ -0,0 +1,25 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base where
+
+import qualified MiniJuvix.Syntax.MicroJuvix.Pretty as M
+import Prettyprinter
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Error.Types
+
+data Eann = Highlight
+  | MicroAnn M.Ann
+
+ppCode :: M.PrettyCode c => c -> Doc Eann
+ppCode = reAnnotate MicroAnn . M.runPrettyCode M.defaultOptions
+
+indent' :: Doc ann -> Doc ann
+indent' = indent 2
+
+class PrettyError e where
+  ppError :: e -> Doc Eann
+
+instance PrettyError WrongConstructorType where
+  ppError e = "Type error during pattern matching."
+    <> line <> "The constructor" <+> (ppCode (e ^. wrongCtorTypeName)) <+> "has type:"
+    <> line <> indent' (ppCode (e ^. wrongCtorTypeActual))
+    <> line <> "but is expected to have type:"
+    <> line <> indent' (ppCode (e ^. wrongCtorTypeExpected))
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Text.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Text.hs
new file mode 100644
index 000000000..83cdf4a7d
--- /dev/null
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Text.hs
@@ -0,0 +1,9 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Text where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Error.Pretty.Base
+import Prettyprinter
+import Prettyprinter.Render.Text
+
+renderText :: SimpleDocStream Eann -> Text
+renderText = renderStrict
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
new file mode 100644
index 000000000..7694645b8
--- /dev/null
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
@@ -0,0 +1,13 @@
+module MiniJuvix.Syntax.MicroJuvix.Error.Types where
+import MiniJuvix.Syntax.MicroJuvix.Language
+import Lens.Micro.Platform (makeLenses)
+
+-- | the type of the constructor used in a pattern does
+-- not match the type of the inductive being matched
+data WrongConstructorType = WrongConstructorType
+  { _wrongCtorTypeName :: Name,
+    _wrongCtorTypeExpected :: Type,
+    _wrongCtorTypeActual :: Type
+  }
+
+makeLenses ''WrongConstructorType
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
index 6a21ec089..7d62d1a1e 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
@@ -29,6 +29,7 @@ data Name = Name
   { _nameText :: Text,
     _nameId :: NameId,
     _nameKind :: NameKind
+    -- TODO: Add Location here so we can print out line numbers
   }
   deriving stock (Show)
 
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs
new file mode 100644
index 000000000..0f9cc47d6
--- /dev/null
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty.hs
@@ -0,0 +1,9 @@
+module MiniJuvix.Syntax.MicroJuvix.Pretty
+  ( module MiniJuvix.Syntax.MicroJuvix.Pretty.Base,
+    module MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi,
+    module MiniJuvix.Syntax.MicroJuvix.Pretty.Ann,
+  ) where
+
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Base
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
index 6f9f17f21..77921b465 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
@@ -22,6 +22,9 @@ defaultOptions =
 class PrettyCode c where
   ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
 
+runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
+runPrettyCode opts = run . runReader opts . ppCode
+
 instance PrettyCode Name where
   ppCode n =
     return $
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
index 0c1a70a18..414969ca6 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
@@ -3,7 +3,7 @@ import MiniJuvix.Prelude
 import MiniJuvix.Syntax.MicroJuvix.Language
 import MiniJuvix.Syntax.MicroJuvix.InfoTable
 import qualified Data.HashMap.Strict as HashMap
-import MiniJuvix.Syntax.MicroJuvix.Pretty.Text
+import MiniJuvix.Syntax.MicroJuvix.Error
 
 type Err = Text
 
@@ -13,10 +13,10 @@ newtype LocalVars = LocalVars {
   deriving newtype (Semigroup, Monoid)
 makeLenses ''LocalVars
 
-checkModule :: Module -> Either Err Module
+checkModule :: Module -> Either TypeCheckerError Module
 checkModule m = run $ runError $ runReader (buildTable m) (checkModule' m)
 
-checkModule' :: Members '[Reader InfoTable, Error Err] r =>
+checkModule' :: Members '[Reader InfoTable, Error TypeCheckerError] r =>
   Module -> Sem r Module
 checkModule' Module {..} = do
   _moduleBody' <- checkModuleBody _moduleBody
@@ -25,7 +25,7 @@ checkModule' Module {..} = do
     ..
     }
 
-checkModuleBody :: Members '[Reader InfoTable, Error Err] r =>
+checkModuleBody :: Members '[Reader InfoTable, Error TypeCheckerError] r =>
   ModuleBody -> Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
   _moduleStatements' <- mapM checkStatement _moduleStatements
@@ -33,7 +33,7 @@ checkModuleBody ModuleBody {..} = do
     _moduleStatements = _moduleStatements'
     }
 
-checkStatement :: Members '[Reader InfoTable, Error Err] r =>
+checkStatement :: Members '[Reader InfoTable, Error TypeCheckerError] r =>
   Statement -> Sem r Statement
 checkStatement s = case s of
   StatementFunction fun -> StatementFunction <$> checkFunctionDef fun
@@ -41,7 +41,7 @@ checkStatement s = case s of
   StatementInductive {} -> return s
   StatementAxiom {} -> return s
 
-checkFunctionDef :: Members '[Reader InfoTable, Error Err] r =>
+checkFunctionDef :: Members '[Reader InfoTable, Error TypeCheckerError] r =>
   FunctionDef -> Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
   info <- lookupFunction _funDefName
@@ -51,26 +51,14 @@ checkFunctionDef FunctionDef {..} = do
     ..
     }
 
-checkExpression :: Members '[Reader InfoTable, Error Err, Reader LocalVars] r =>
+checkExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
   Type -> Expression -> Sem r Expression
 checkExpression t e = do
   t' <- inferExpression' e
-  unlessM (matchTypes t (t' ^. typedType)) (throwErr
-      ("wrong type" <> "\nExpression:" <> renderPrettyCodeDefault e
-      <> "\nInferred type: " <> renderPrettyCodeDefault (t' ^. typedType)
-      <> "\nExpected type: " <> renderPrettyCodeDefault t
-      ))
+  when (t /= t' ^. typedType) (throw ErrWrongType)
   return (ExpressionTyped t')
 
-matchTypes :: Members '[Reader InfoTable] r =>
-  Type -> Type -> Sem r Bool
-matchTypes a b = do
-  a' <- normalizeType a
-  b' <- normalizeType b
-  return $
-    a' == TypeAny || b' == TypeAny || a' == b'
-
-inferExpression :: Members '[Reader InfoTable, Error Err, Reader LocalVars] r =>
+inferExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
    Expression -> Sem r Expression
 inferExpression = fmap ExpressionTyped . inferExpression'
 
@@ -104,13 +92,13 @@ unfoldFunType t = case t of
   TypeFunction (Function l r) -> first (l:) (unfoldFunType r)
   _ -> ([], t)
 
-checkFunctionClause :: forall r. Members '[Reader InfoTable, Error Err] r =>
+checkFunctionClause :: forall r. Members '[Reader InfoTable, Error TypeCheckerError] r =>
   FunctionInfo -> FunctionClause -> Sem r FunctionClause
 checkFunctionClause info FunctionClause{..} = do
   let (argTys, rty) = unfoldFunType (info ^. functionInfoType)
       (patTys, restTys) = splitAt (length _clausePatterns) argTys
       bodyTy = foldFunType restTys rty
-  when (length patTys /= length _clausePatterns) (throwErr "too many patterns")
+  when (length patTys /= length _clausePatterns) (throw ErrTooManyPatterns)
   locals <- mconcat <$> zipWithM checkPattern patTys _clausePatterns
   clauseBody' <- runReader locals (checkExpression bodyTy _clauseBody)
   return FunctionClause {
@@ -118,7 +106,7 @@ checkFunctionClause info FunctionClause{..} = do
     ..
     }
 
-checkPattern :: forall r. Members '[Reader InfoTable, Error Err] r =>
+checkPattern :: forall r. Members '[Reader InfoTable, Error TypeCheckerError] r =>
   Type -> Pattern -> Sem r LocalVars
 checkPattern type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
   where
@@ -128,18 +116,16 @@ checkPattern type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
     PatternVariable v -> return [(v, ty)]
     PatternConstructorApp a -> do
       info <- lookupConstructor (a ^. constrAppConstructor)
-      when (TypeIden (TypeIdenInductive (info ^. constructorInfoInductive)) /= ty) (throwErr "wrong type for constructor")
+      let inductiveTy = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive))
+      when (inductiveTy /= ty) (throw (ErrWrongConstructorType (WrongConstructorType (a ^. constrAppConstructor) ty inductiveTy)))
       goConstr a
     where
     goConstr :: ConstructorApp -> Sem r [(VarName, Type)]
     goConstr (ConstructorApp c ps) = do
       tys <- (^. constructorInfoArgs) <$> lookupConstructor c
-      when (length tys /= length ps) (throwErr "wrong number of arguments in constructor app")
+      when (length tys /= length ps) (throw ErrConstructorAppArgs)
       concat <$> zipWithM go tys ps
 
-throwErr :: Members '[Error Err] r => Err -> Sem r a
-throwErr = throw
-
 -- TODO currently equivalent to id
 normalizeType :: forall r. Members '[Reader InfoTable] r => Type -> Sem r Type
 normalizeType t = case t of
@@ -158,7 +144,7 @@ normalizeType t = case t of
     r' <- normalizeType r
     return (Function l' r')
 
-inferExpression' :: forall r. Members '[Reader InfoTable, Error Err, Reader LocalVars] r =>
+inferExpression' :: forall r. Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
    Expression -> Sem r TypedExpression
 inferExpression' e = case e of
   ExpressionIden i -> inferIden i
@@ -197,4 +183,4 @@ inferExpression' e = case e of
   getFunctionType :: Type -> Sem r Function
   getFunctionType t = case t of
     TypeFunction f -> return f
-    _ -> throwErr ("expected function type " <> show t)
+    _ -> throw ErrExpectedFunctionType

From 615f7d11c03e6dcb11a8bde4269e4b15df7d3a5e Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Tue, 29 Mar 2022 18:01:19 +0100
Subject: [PATCH 2/7] [test] Adds negative typecheck test for constructor

---
 test/Base.hs                                  |  5 ++
 test/Main.hs                                  |  4 +-
 test/TypeCheck.hs                             |  7 +++
 test/TypeCheck/Negative.hs                    | 48 +++++++++++++++++++
 .../MicroJuvix/PatternConstructor.mjuvix      | 13 +++++
 5 files changed, 76 insertions(+), 1 deletion(-)
 create mode 100644 test/TypeCheck.hs
 create mode 100644 test/TypeCheck/Negative.hs
 create mode 100644 tests/negative/MicroJuvix/PatternConstructor.mjuvix

diff --git a/test/Base.hs b/test/Base.hs
index f66ccd062..53b800649 100644
--- a/test/Base.hs
+++ b/test/Base.hs
@@ -9,8 +9,10 @@ import Test.Tasty
 import Test.Tasty.HUnit
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Concrete.Language as M
+import qualified MiniJuvix.Syntax.Abstract.Language as A
 import qualified MiniJuvix.Syntax.Concrete.Parser as M
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
+import qualified MiniJuvix.Translation.ScopedToAbstract as A
 
 parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
 parseModuleIO = fromRightIO id . M.runModuleParserIO
@@ -21,6 +23,9 @@ parseTextModuleIO = fromRightIO id . return . M.runModuleParser "literal string"
 scopeModuleIO :: M.Module 'M.Parsed 'M.ModuleTop -> IO (M.Module 'M.Scoped 'M.ModuleTop)
 scopeModuleIO = fmap snd . fromRightIO' printErrorAnsi . M.scopeCheck1IO "."
 
+translateModuleIO :: M.Module 'M.Scoped 'M.ModuleTop -> IO A.TopModule
+translateModuleIO = fmap snd . fromRightIO id . return . A.translateModule
+
 data AssertionDescr =
   Single Assertion
   | Steps ((String -> IO ()) -> Assertion)
diff --git a/test/Main.hs b/test/Main.hs
index f0c9b0941..d2f4bd982 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -2,12 +2,14 @@ module Main (main) where
 
 import Base
 
+import qualified TypeCheck
 import qualified Scope
 
 negatives :: TestTree
 negatives = testGroup "MiniJuvix tests" $
   [
-  Scope.allTests
+  Scope.allTests,
+  TypeCheck.allTests
   ]
 
 allTests :: TestTree
diff --git a/test/TypeCheck.hs b/test/TypeCheck.hs
new file mode 100644
index 000000000..052d06ba7
--- /dev/null
+++ b/test/TypeCheck.hs
@@ -0,0 +1,7 @@
+module TypeCheck (allTests) where
+
+import Base
+import qualified TypeCheck.Negative as N
+
+allTests :: TestTree
+allTests = testGroup "TypeCheck tests" [N.allTests]
diff --git a/test/TypeCheck/Negative.hs b/test/TypeCheck/Negative.hs
new file mode 100644
index 000000000..6515c7033
--- /dev/null
+++ b/test/TypeCheck/Negative.hs
@@ -0,0 +1,48 @@
+module TypeCheck.Negative (allTests) where
+
+import Base
+import MiniJuvix.Syntax.MicroJuvix.Error
+import qualified MiniJuvix.Syntax.MicroJuvix.TypeChecker as T
+import qualified MiniJuvix.Translation.AbstractToMicroJuvix as A
+
+type FailMsg = String
+
+data NegTest = NegTest
+  { name :: String,
+    relDir :: FilePath,
+    file :: FilePath,
+    checkErr :: TypeCheckerError -> Maybe FailMsg }
+
+testDescr :: NegTest -> TestDescr
+testDescr NegTest {..} = TestDescr {
+  testName = name,
+  testRoot = root </> relDir,
+  testAssertion = Single $ do
+      p <- (parseModuleIO file)
+           >>= scopeModuleIO
+           >>= translateModuleIO
+           >>= (return . A.translateModule)
+           >>= (return . T.checkModule)
+
+      case p of
+        Left err -> whenJust (checkErr err) assertFailure
+        Right _ -> assertFailure "The type checker did not find an error."
+  }
+
+allTests :: TestTree
+allTests = testGroup "TypeCheck negative tests"
+  (map (mkTest . testDescr) tests)
+
+root :: FilePath
+root = "tests/negative"
+
+wrongError :: Maybe FailMsg
+wrongError = Just "Incorrect error"
+
+tests :: [NegTest]
+tests = [
+  NegTest "Constructor in pattern type error" "MicroJuvix"
+    "PatternConstructor.mjuvix" $ \case
+      ErrWrongConstructorType {} -> Nothing
+      _ -> wrongError
+        ]
diff --git a/tests/negative/MicroJuvix/PatternConstructor.mjuvix b/tests/negative/MicroJuvix/PatternConstructor.mjuvix
new file mode 100644
index 000000000..20fe40383
--- /dev/null
+++ b/tests/negative/MicroJuvix/PatternConstructor.mjuvix
@@ -0,0 +1,13 @@
+module PatternConstructor;
+  inductive A {
+    a : A;
+  };
+
+  inductive B {
+    b : B;
+  };
+
+  f : A → B;
+  f b ≔ b;
+
+end;

From e37fa7a8dcbefbf27a3e566f539b8c434e8ce265 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Wed, 30 Mar 2022 10:17:31 +0100
Subject: [PATCH 3/7] [app] Adds microjuvix subcommands for printing /
 typechecking

---
 app/Commands/MicroJuvix.hs | 30 ++++++++++++++++++++++++++++++
 app/Main.hs                | 24 +++++++++++++++---------
 2 files changed, 45 insertions(+), 9 deletions(-)

diff --git a/app/Commands/MicroJuvix.hs b/app/Commands/MicroJuvix.hs
index b4f9156d3..343b030f0 100644
--- a/app/Commands/MicroJuvix.hs
+++ b/app/Commands/MicroJuvix.hs
@@ -6,10 +6,40 @@ import Commands.Extra
 import MiniJuvix.Prelude hiding (Doc)
 import Options.Applicative
 
+data MicroJuvixCommand
+  = Pretty MicroJuvixOptions
+  | TypeCheck MicroJuvixOptions
+
 newtype MicroJuvixOptions = MicroJuvixOptions
   { _mjuvixInputFile :: FilePath
   }
 
+parseMicroJuvixCommand :: Parser MicroJuvixCommand
+parseMicroJuvixCommand =
+  hsubparser $
+    mconcat
+      [ commandPretty
+      , commandTypeCheck
+      ]
+  where
+    commandPretty :: Mod CommandFields MicroJuvixCommand
+    commandPretty = command "pretty" prettyInfo
+
+    commandTypeCheck :: Mod CommandFields MicroJuvixCommand
+    commandTypeCheck = command "typecheck" typeCheckInfo
+
+    prettyInfo :: ParserInfo MicroJuvixCommand
+    prettyInfo =
+      info
+        (Pretty <$> parseMicroJuvix)
+        (progDesc "Translate a MiniJuvix file to MicroJuvix and pretty print the result")
+
+    typeCheckInfo :: ParserInfo MicroJuvixCommand
+    typeCheckInfo =
+      info
+        (TypeCheck <$> parseMicroJuvix)
+        (progDesc "Translate a MiniJuvix file to MicroJuvix and typecheck the result")
+
 parseMicroJuvix :: Parser MicroJuvixOptions
 parseMicroJuvix = do
   _mjuvixInputFile <- parseInputFile
diff --git a/app/Main.hs b/app/Main.hs
index 11d2909fc..20f663214 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -21,6 +21,7 @@ import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text as T
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
 import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as Micro
 import qualified MiniJuvix.Syntax.MicroJuvix.TypeChecker as Micro
+import qualified MiniJuvix.Syntax.MicroJuvix.Language as Micro
 import qualified MiniJuvix.Termination as T
 import qualified MiniJuvix.Termination.CallGraph as A
 import qualified MiniJuvix.Translation.AbstractToMicroJuvix as Micro
@@ -40,7 +41,7 @@ data Command
   | Html HtmlOptions
   | Termination TerminationCommand
   | MiniHaskell MiniHaskellOptions
-  | MicroJuvix MicroJuvixOptions
+  | MicroJuvix MicroJuvixCommand
   | DisplayVersion
 
 data ScopeOptions = ScopeOptions
@@ -174,8 +175,8 @@ parseCommand =
         minfo :: ParserInfo Command
         minfo =
           info
-            (MicroJuvix <$> parseMicroJuvix)
-            (progDesc "Translate a MiniJuvix file to MicroJuvix")
+            (MicroJuvix <$> parseMicroJuvixCommand)
+            (progDesc "Subcommands related to MicroJuvix")
 
     commandMiniHaskell :: Mod CommandFields Command
     commandMiniHaskell = command "minihaskell" minfo
@@ -254,13 +255,11 @@ go c = do
       m <- parseModuleIO _htmlInputFile
       (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       genHtml defaultOptions _htmlRecursive _htmlTheme s
-    MicroJuvix MicroJuvixOptions {..} -> do
-      m <- parseModuleIO _mjuvixInputFile
-      (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
-      (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
-      let micro = Micro.translateModule a
+    MicroJuvix (Pretty MicroJuvixOptions {..}) -> do
+      micro <- miniToMicro root _mjuvixInputFile
       Micro.printPrettyCodeDefault micro
-      putStrLn ""
+    MicroJuvix (TypeCheck MicroJuvixOptions {..}) -> do
+      micro <- miniToMicro root _mjuvixInputFile
       case Micro.checkModule micro of
         Left er -> printErrorAnsi er
         Right {} -> putStrLn "Well done! It type checks"
@@ -302,6 +301,13 @@ go c = do
           Nothing -> putStrLn (n <> " Fails the termination checking")
           Just (T.LexOrder k) -> putStrLn (n <> " Terminates with order " <> show (toList k))
         putStrLn ""
+    where
+      miniToMicro :: FilePath -> FilePath -> IO Micro.Module
+      miniToMicro root p = do
+        m <- parseModuleIO p
+        (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+        (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
+        return (Micro.translateModule a)
 
 main :: IO ()
 main = execParser descr >>= go

From b41b4c4e84ea9b89ea65ad60c034ab7e14fc324c Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Wed, 30 Mar 2022 12:36:13 +0100
Subject: [PATCH 4/7] [typecheck] Add error message for ctor match args
 mistmatch

---
 src/MiniJuvix/Syntax/MicroJuvix/Error.hs      |  7 ++-----
 .../Syntax/MicroJuvix/Error/Pretty/Base.hs    | 21 +++++++++++++++++++
 .../Syntax/MicroJuvix/Error/Types.hs          | 11 +++++++++-
 .../Syntax/MicroJuvix/TypeChecker.hs          | 14 ++++++++++---
 test/TypeCheck/Negative.hs                    | 10 ++++++---
 .../MicroJuvix/PatternConstructorApp.mjuvix   | 13 ++++++++++++
 6 files changed, 64 insertions(+), 12 deletions(-)
 create mode 100644 tests/negative/MicroJuvix/PatternConstructorApp.mjuvix

diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
index ca360c72b..5b80488f2 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
@@ -14,18 +14,15 @@ import Prettyprinter
 data TypeCheckerError
  = ErrTooManyPatterns
  | ErrWrongConstructorType WrongConstructorType
- | ErrConstructorAppArgs
+ | ErrWrongConstructorAppArgs WrongConstructorAppArgs
  | ErrWrongType
  | ErrExpectedFunctionType
 
-prettyT :: Text -> Doc Eann
-prettyT = pretty
-
 ppTypeCheckerError :: TypeCheckerError -> Doc Eann
 ppTypeCheckerError = \case
   ErrWrongConstructorType e -> ppError e
   ErrTooManyPatterns -> prettyT "too many patterns"
-  ErrConstructorAppArgs -> prettyT "constructor has wrong args"
+  ErrWrongConstructorAppArgs e -> ppError e
   ErrWrongType -> prettyT "wrong type"
   ErrExpectedFunctionType -> prettyT "expected function type"
 
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
index 159a9e7fd..477218769 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
@@ -4,6 +4,7 @@ import qualified MiniJuvix.Syntax.MicroJuvix.Pretty as M
 import Prettyprinter
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.MicroJuvix.Error.Types
+import MiniJuvix.Syntax.MicroJuvix.Language
 
 data Eann = Highlight
   | MicroAnn M.Ann
@@ -23,3 +24,23 @@ instance PrettyError WrongConstructorType where
     <> line <> indent' (ppCode (e ^. wrongCtorTypeActual))
     <> line <> "but is expected to have type:"
     <> line <> indent' (ppCode (e ^. wrongCtorTypeExpected))
+
+prettyT :: Text -> Doc Eann
+prettyT = pretty
+
+instance PrettyError WrongConstructorAppArgs where
+  ppError e = "Type error during pattern matching."
+    <> line <> "The constructor:" <+> ctorName <+> "is being matched against" <+> numPats <> ":"
+    <> line <> indent' (ppCode (e ^. wrongCtorAppApp))
+
+    <> line <> "but is expected to be matched against" <+> numTypes <+> "with the following types:"
+    <> line <> indent' (hsep (ctorName : (ppCode <$> (e ^. wrongCtorAppTypes))))
+    where
+      numPats :: Doc ann
+      numPats = pat (length (e ^. wrongCtorAppApp . constrAppParameters))
+      numTypes :: Doc ann
+      numTypes = pat (length (e ^. wrongCtorAppTypes))
+      ctorName :: Doc Eann
+      ctorName = ppCode (e ^. wrongCtorAppApp . constrAppConstructor)
+      pat :: Int -> Doc ann
+      pat n = pretty n <+> plural "pattern" "patterns" n
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
index 7694645b8..bd9aaac6c 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
@@ -1,6 +1,7 @@
 module MiniJuvix.Syntax.MicroJuvix.Error.Types where
+
+import MiniJuvix.Prelude
 import MiniJuvix.Syntax.MicroJuvix.Language
-import Lens.Micro.Platform (makeLenses)
 
 -- | the type of the constructor used in a pattern does
 -- not match the type of the inductive being matched
@@ -10,4 +11,12 @@ data WrongConstructorType = WrongConstructorType
     _wrongCtorTypeActual :: Type
   }
 
+-- | the arguments of a constructor pattern do not match
+-- the expected arguments of the constructor
+data WrongConstructorAppArgs = WrongConstructorAppArgs
+  { _wrongCtorAppApp :: ConstructorApp,
+    _wrongCtorAppTypes :: [Type]
+  }
+
 makeLenses ''WrongConstructorType
+makeLenses ''WrongConstructorAppArgs
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
index 414969ca6..ca3deef53 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
@@ -117,14 +117,22 @@ checkPattern type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
     PatternConstructorApp a -> do
       info <- lookupConstructor (a ^. constrAppConstructor)
       let inductiveTy = TypeIden (TypeIdenInductive (info ^. constructorInfoInductive))
-      when (inductiveTy /= ty) (throw (ErrWrongConstructorType (WrongConstructorType (a ^. constrAppConstructor) ty inductiveTy)))
+      when
+        (inductiveTy /= ty)
+        (throw
+         (ErrWrongConstructorType (WrongConstructorType (a ^. constrAppConstructor) ty inductiveTy)))
       goConstr a
     where
     goConstr :: ConstructorApp -> Sem r [(VarName, Type)]
-    goConstr (ConstructorApp c ps) = do
+    goConstr app@(ConstructorApp c ps) = do
       tys <- (^. constructorInfoArgs) <$> lookupConstructor c
-      when (length tys /= length ps) (throw ErrConstructorAppArgs)
+      when
+        (length tys /= length ps)
+        (throw (ErrWrongConstructorAppArgs (appErr app tys)))
       concat <$> zipWithM go tys ps
+    appErr :: ConstructorApp -> [Type] -> WrongConstructorAppArgs
+    appErr app tys = WrongConstructorAppArgs { _wrongCtorAppApp = app,
+                                               _wrongCtorAppTypes = tys}
 
 -- TODO currently equivalent to id
 normalizeType :: forall r. Members '[Reader InfoTable] r => Type -> Sem r Type
diff --git a/test/TypeCheck/Negative.hs b/test/TypeCheck/Negative.hs
index 6515c7033..4eee22af5 100644
--- a/test/TypeCheck/Negative.hs
+++ b/test/TypeCheck/Negative.hs
@@ -18,11 +18,11 @@ testDescr NegTest {..} = TestDescr {
   testName = name,
   testRoot = root </> relDir,
   testAssertion = Single $ do
-      p <- (parseModuleIO file)
+      p <- parseModuleIO file
            >>= scopeModuleIO
            >>= translateModuleIO
-           >>= (return . A.translateModule)
-           >>= (return . T.checkModule)
+           >>| A.translateModule
+           >>| T.checkModule
 
       case p of
         Left err -> whenJust (checkErr err) assertFailure
@@ -45,4 +45,8 @@ tests = [
     "PatternConstructor.mjuvix" $ \case
       ErrWrongConstructorType {} -> Nothing
       _ -> wrongError
+  , NegTest "Constructor pattern length mismatch" "MicroJuvix"
+    "PatternConstructorApp.mjuvix" $ \case
+      ErrWrongConstructorAppArgs {} -> Nothing
+      _ -> wrongError
         ]
diff --git a/tests/negative/MicroJuvix/PatternConstructorApp.mjuvix b/tests/negative/MicroJuvix/PatternConstructorApp.mjuvix
new file mode 100644
index 000000000..96d9474bb
--- /dev/null
+++ b/tests/negative/MicroJuvix/PatternConstructorApp.mjuvix
@@ -0,0 +1,13 @@
+module PatternConstructorApp;
+  inductive A {
+    a : A -> A;
+  };
+
+  inductive B {
+    b : B;
+  };
+
+  f : A → B;
+  f (a x _) ≔ b;
+
+end;

From a030b97e8ff63b91a313922cefbc5dbfd87bfe3b Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Wed, 30 Mar 2022 20:28:29 +0100
Subject: [PATCH 5/7] [typecheck] Add descriptive messages for remainng errors

---
 src/MiniJuvix/Syntax/MicroJuvix/Error.hs      | 12 ++++----
 .../Syntax/MicroJuvix/Error/Pretty/Base.hs    | 28 ++++++++++++++++---
 .../Syntax/MicroJuvix/Error/Types.hs          | 24 ++++++++++++++++
 src/MiniJuvix/Syntax/MicroJuvix/Language.hs   |  3 +-
 .../Syntax/MicroJuvix/Pretty/Base.hs          | 16 ++++++-----
 .../Syntax/MicroJuvix/TypeChecker.hs          | 27 ++++++++++++------
 .../Translation/AbstractToMicroJuvix.hs       | 16 +++++++----
 test/TypeCheck/Negative.hs                    | 12 ++++++++
 .../MicroJuvix/ExpectedFunctionType.mjuvix    | 12 ++++++++
 .../MicroJuvix/TooManyPatterns.mjuvix         |  8 ++++++
 tests/negative/MicroJuvix/WrongType.mjuvix    | 12 ++++++++
 11 files changed, 137 insertions(+), 33 deletions(-)
 create mode 100644 tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix
 create mode 100644 tests/negative/MicroJuvix/TooManyPatterns.mjuvix
 create mode 100644 tests/negative/MicroJuvix/WrongType.mjuvix

diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
index 5b80488f2..7e7726671 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error.hs
@@ -12,19 +12,19 @@ import MiniJuvix.Syntax.MicroJuvix.Error.Types
 import Prettyprinter
 
 data TypeCheckerError
- = ErrTooManyPatterns
+ = ErrTooManyPatterns TooManyPatterns
  | ErrWrongConstructorType WrongConstructorType
  | ErrWrongConstructorAppArgs WrongConstructorAppArgs
- | ErrWrongType
- | ErrExpectedFunctionType
+ | ErrWrongType WrongType
+ | ErrExpectedFunctionType ExpectedFunctionType
 
 ppTypeCheckerError :: TypeCheckerError -> Doc Eann
 ppTypeCheckerError = \case
   ErrWrongConstructorType e -> ppError e
-  ErrTooManyPatterns -> prettyT "too many patterns"
+  ErrTooManyPatterns e -> ppError e
   ErrWrongConstructorAppArgs e -> ppError e
-  ErrWrongType -> prettyT "wrong type"
-  ErrExpectedFunctionType -> prettyT "expected function type"
+  ErrWrongType e -> ppError e
+  ErrExpectedFunctionType e -> ppError e
 
 docStream :: TypeCheckerError -> SimpleDocStream Eann
 docStream = layoutPretty defaultLayoutOptions . ppTypeCheckerError
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
index 477218769..c78405257 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
@@ -15,6 +15,9 @@ ppCode = reAnnotate MicroAnn . M.runPrettyCode M.defaultOptions
 indent' :: Doc ann -> Doc ann
 indent' = indent 2
 
+prettyT :: Text -> Doc Eann
+prettyT = pretty
+
 class PrettyError e where
   ppError :: e -> Doc Eann
 
@@ -25,14 +28,10 @@ instance PrettyError WrongConstructorType where
     <> line <> "but is expected to have type:"
     <> line <> indent' (ppCode (e ^. wrongCtorTypeExpected))
 
-prettyT :: Text -> Doc Eann
-prettyT = pretty
-
 instance PrettyError WrongConstructorAppArgs where
   ppError e = "Type error during pattern matching."
     <> line <> "The constructor:" <+> ctorName <+> "is being matched against" <+> numPats <> ":"
     <> line <> indent' (ppCode (e ^. wrongCtorAppApp))
-
     <> line <> "but is expected to be matched against" <+> numTypes <+> "with the following types:"
     <> line <> indent' (hsep (ctorName : (ppCode <$> (e ^. wrongCtorAppTypes))))
     where
@@ -44,3 +43,24 @@ instance PrettyError WrongConstructorAppArgs where
       ctorName = ppCode (e ^. wrongCtorAppApp . constrAppConstructor)
       pat :: Int -> Doc ann
       pat n = pretty n <+> plural "pattern" "patterns" n
+
+instance PrettyError WrongType where
+  ppError e = "Type error."
+    <> line <> "The expression" <+> ppCode (e ^. wrongTypeExpression) <+> "has type:"
+    <> line <> indent' (ppCode (e ^. wrongTypeInferredType))
+    <> line <> "but is expected to have type:"
+    <> line <> indent' (ppCode (e ^. wrongTypeExpectedType))
+
+instance PrettyError ExpectedFunctionType where
+  ppError e = "Type error."
+    <> line <> "The expression:"
+    <> line <> indent' (ppCode (e ^. expectedFunctionTypeExpression))
+    <> line <> "is expected to be a function application but" <+> ppCode (e ^. expectedFunctionTypeApp) <+> "has type:"
+    <> line <> indent' (ppCode (e ^. expectedFunctionTypeType))
+
+instance PrettyError TooManyPatterns where
+  ppError e = "Type error in the definition of" <+> ppCode (e ^. tooManyPatternsClause . clauseName) <> "."
+    <> line <> "The function clause:"
+    <> line <> indent' (ppCode (e ^. tooManyPatternsClause))
+    <> line <> "matches too many patterns. It should match the following types:"
+    <> line <> indent' (hsep (ppCode <$> (e ^. tooManyPatternsTypes)))
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
index bd9aaac6c..7104e5595 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
@@ -18,5 +18,29 @@ data WrongConstructorAppArgs = WrongConstructorAppArgs
     _wrongCtorAppTypes :: [Type]
   }
 
+-- | the type of an expression does not match the inferred type
+data WrongType = WrongType
+  { _wrongTypeExpression :: Expression,
+    _wrongTypeExpectedType :: Type,
+    _wrongTypeInferredType :: Type
+  }
+
+-- | The left hand expression of a function application is not
+-- a function type.
+data ExpectedFunctionType = ExpectedFunctionType
+  { _expectedFunctionTypeExpression :: Expression,
+    _expectedFunctionTypeApp :: Expression,
+    _expectedFunctionTypeType :: Type
+  }
+
+-- | A function definition clause matches too many arguments
+data TooManyPatterns = TooManyPatterns
+  { _tooManyPatternsClause :: FunctionClause,
+    _tooManyPatternsTypes :: [Type]
+  }
+
 makeLenses ''WrongConstructorType
 makeLenses ''WrongConstructorAppArgs
+makeLenses ''WrongType
+makeLenses ''ExpectedFunctionType
+makeLenses ''TooManyPatterns
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
index 7d62d1a1e..df196139c 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
@@ -78,7 +78,8 @@ data FunctionDef = FunctionDef
   }
 
 data FunctionClause = FunctionClause
-  { _clausePatterns :: [Pattern],
+  { _clauseName :: FunctionName,
+    _clausePatterns :: [Pattern],
     _clauseBody :: Expression
   }
 
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
index 77921b465..2e54b5fab 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
@@ -171,16 +171,18 @@ instance PrettyCode Pattern where
 instance PrettyCode FunctionDef where
   ppCode f = do
     funDefName' <- ppCode (f ^. funDefName)
-    funDefType' <- ppCode (f ^. funDefType)
-    clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
+    funDefTypeSig' <- ppCode (f ^. funDefTypeSig)
+    clauses' <- mapM ppCode (f ^. funDefClauses)
     return $
       funDefName' <+> kwColonColon <+> funDefType' <> line
         <> vsep (toList clauses')
-    where
-      ppClause fun c = do
-        clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
-        clauseBody' <- ppCode (c ^. clauseBody)
-        return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+
+instance PrettyCode FunctionClause where
+  ppCode c = do
+    funName <- ppCode (c ^. clauseName)
+    clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
+    clauseBody' <- ppCode (c ^. clauseBody)
+    return $ funName <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
 
 instance PrettyCode Backend where
   ppCode = \case
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
index ca3deef53..96c015a5b 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
@@ -55,7 +55,10 @@ checkExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader Lo
   Type -> Expression -> Sem r Expression
 checkExpression t e = do
   t' <- inferExpression' e
-  when (t /= t' ^. typedType) (throw ErrWrongType)
+  let inferredType = t' ^. typedType
+  when (t /= inferredType) (throw (ErrWrongType (WrongType { _wrongTypeExpression = e,
+                                                             _wrongTypeInferredType = inferredType,
+                                                             _wrongTypeExpectedType = t})))
   return (ExpressionTyped t')
 
 inferExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
@@ -94,11 +97,13 @@ unfoldFunType t = case t of
 
 checkFunctionClause :: forall r. Members '[Reader InfoTable, Error TypeCheckerError] r =>
   FunctionInfo -> FunctionClause -> Sem r FunctionClause
-checkFunctionClause info FunctionClause{..} = do
+checkFunctionClause info clause@FunctionClause{..} = do
   let (argTys, rty) = unfoldFunType (info ^. functionInfoType)
       (patTys, restTys) = splitAt (length _clausePatterns) argTys
       bodyTy = foldFunType restTys rty
-  when (length patTys /= length _clausePatterns) (throw ErrTooManyPatterns)
+  when (length patTys /= length _clausePatterns) (throw (ErrTooManyPatterns (TooManyPatterns {
+                                                                                _tooManyPatternsClause = clause,
+                                                                                _tooManyPatternsTypes = patTys})))
   locals <- mconcat <$> zipWithM checkPattern patTys _clausePatterns
   clauseBody' <- runReader locals (checkExpression bodyTy _clauseBody)
   return FunctionClause {
@@ -178,8 +183,9 @@ inferExpression' e = case e of
       return (TypedExpression (info ^. axiomInfoType) (ExpressionIden i))
   inferApplication :: Application -> Sem r TypedExpression
   inferApplication a = do
-    l <- inferExpression' (a ^. appLeft)
-    fun <- getFunctionType (l ^. typedType)
+    let leftExp = a ^. appLeft
+    l <- inferExpression' leftExp
+    fun <- getFunctionType leftExp (l ^. typedType)
     r <- checkExpression (fun ^. funLeft) (a ^. appRight)
     return TypedExpression {
       _typedExpression = ExpressionApplication Application {
@@ -188,7 +194,10 @@ inferExpression' e = case e of
           },
       _typedType = fun ^. funRight
       }
-  getFunctionType :: Type -> Sem r Function
-  getFunctionType t = case t of
-    TypeFunction f -> return f
-    _ -> throw ErrExpectedFunctionType
+    where
+      getFunctionType :: Expression -> Type -> Sem r Function
+      getFunctionType appExp t = case t of
+        TypeFunction f -> return f
+        _ -> throw (ErrExpectedFunctionType (ExpectedFunctionType { _expectedFunctionTypeExpression = e,
+                                                                    _expectedFunctionTypeApp = appExp,
+                                                                    _expectedFunctionTypeType = t}))
diff --git a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
index 3de285817..cee9041a4 100644
--- a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
+++ b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
@@ -73,15 +73,19 @@ goFunction (A.Function l r) = Function (goFunctionParameter l) (goType r)
 goFunctionDef :: A.FunctionDef -> FunctionDef
 goFunctionDef f =
   FunctionDef
-    { _funDefName = goSymbol (f ^. A.funDefName),
-      _funDefType = goType (f ^. A.funDefTypeSig),
-      _funDefClauses = fmap goFunctionClause (f ^. A.funDefClauses)
+    { _funDefName = _funDefName',
+      _funDefTypeSig = goType (f ^. A.funDefTypeSig),
+      _funDefClauses = fmap (goFunctionClause _funDefName') (f ^. A.funDefClauses)
     }
+  where
+    _funDefName' :: Name
+    _funDefName' = goSymbol (f ^. A.funDefName)
 
-goFunctionClause :: A.FunctionClause -> FunctionClause
-goFunctionClause c =
+goFunctionClause :: Name -> A.FunctionClause -> FunctionClause
+goFunctionClause n c =
   FunctionClause
-    { _clausePatterns = map goPattern (c ^. A.clausePatterns),
+    { _clauseName = n,
+      _clausePatterns = map goPattern (c ^. A.clausePatterns),
       _clauseBody = goExpression (c ^. A.clauseBody)
     }
 
diff --git a/test/TypeCheck/Negative.hs b/test/TypeCheck/Negative.hs
index 4eee22af5..f068293b0 100644
--- a/test/TypeCheck/Negative.hs
+++ b/test/TypeCheck/Negative.hs
@@ -49,4 +49,16 @@ tests = [
     "PatternConstructorApp.mjuvix" $ \case
       ErrWrongConstructorAppArgs {} -> Nothing
       _ -> wrongError
+  , NegTest "Type vs inferred type mismatch" "MicroJuvix"
+    "WrongType.mjuvix" $ \case
+      ErrWrongType {} -> Nothing
+      _ -> wrongError
+  , NegTest "Function application with non-function type" "MicroJuvix"
+    "ExpectedFunctionType.mjuvix" $ \case
+      ErrExpectedFunctionType {} -> Nothing
+      _ -> wrongError
+  , NegTest "Function definition clause with two many match patterns" "MicroJuvix"
+    "TooManyPatterns.mjuvix" $ \case
+      ErrTooManyPatterns {} -> Nothing
+      _ -> wrongError
         ]
diff --git a/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix b/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix
new file mode 100644
index 000000000..5b37fb6a0
--- /dev/null
+++ b/tests/negative/MicroJuvix/ExpectedFunctionType.mjuvix
@@ -0,0 +1,12 @@
+module ExpectedFunctionType;
+  inductive A {
+    a : A;
+  };
+
+  inductive B {
+    b : B;
+  };
+
+  f : A;
+  f ≔ a b;
+end;
diff --git a/tests/negative/MicroJuvix/TooManyPatterns.mjuvix b/tests/negative/MicroJuvix/TooManyPatterns.mjuvix
new file mode 100644
index 000000000..446ec489e
--- /dev/null
+++ b/tests/negative/MicroJuvix/TooManyPatterns.mjuvix
@@ -0,0 +1,8 @@
+module TooManyPatterns;
+  inductive A {
+    a : A;
+  };
+
+  f : A -> A;
+  f a _ ≔ a;
+end;
diff --git a/tests/negative/MicroJuvix/WrongType.mjuvix b/tests/negative/MicroJuvix/WrongType.mjuvix
new file mode 100644
index 000000000..d3e6111a7
--- /dev/null
+++ b/tests/negative/MicroJuvix/WrongType.mjuvix
@@ -0,0 +1,12 @@
+module WrongType;
+  inductive A {
+    a : A;
+  };
+
+  inductive B {
+    b : B;
+  };
+
+  f : A;
+  f ≔ b;
+end;

From d297322b7dc1eacff475742eacb6f5297ebaf08a Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Thu, 31 Mar 2022 09:19:36 +0100
Subject: [PATCH 6/7] [typecheck] Updates to error message copy

---
 src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
index c78405257..856cad993 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs
@@ -52,10 +52,9 @@ instance PrettyError WrongType where
     <> line <> indent' (ppCode (e ^. wrongTypeExpectedType))
 
 instance PrettyError ExpectedFunctionType where
-  ppError e = "Type error."
-    <> line <> "The expression:"
+  ppError e = "Type error in the expression:"
     <> line <> indent' (ppCode (e ^. expectedFunctionTypeExpression))
-    <> line <> "is expected to be a function application but" <+> ppCode (e ^. expectedFunctionTypeApp) <+> "has type:"
+    <> line <> "the expression" <+> ppCode (e ^. expectedFunctionTypeApp) <+> "is expected to have a function type but has type:"
     <> line <> indent' (ppCode (e ^. expectedFunctionTypeType))
 
 instance PrettyError TooManyPatterns where

From 07333ecbe9bca815de0af961795e70798688a1f4 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Thu, 31 Mar 2022 09:36:21 +0100
Subject: [PATCH 7/7] [typecheck] fix merge conflicts:

---
 app/Main.hs                                       | 2 +-
 src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs    | 2 +-
 src/MiniJuvix/Translation/AbstractToMicroJuvix.hs | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/app/Main.hs b/app/Main.hs
index 20f663214..c5727efea 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -268,7 +268,7 @@ go c = do
       (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
       let micro = Micro.translateModule a
-      checkedMicro <- fromRightIO' putStrLn (return $ Micro.checkModule micro)
+      checkedMicro <- fromRightIO' printErrorAnsi (return $ Micro.checkModule micro)
       minihaskell <- fromRightIO' putStrLn (return $ Hask.translateModule checkedMicro)
       Hask.printPrettyCodeDefault minihaskell
     Termination (Calls opts@CallsOptions {..}) -> do
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
index 2e54b5fab..ee1f28754 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
@@ -171,7 +171,7 @@ instance PrettyCode Pattern where
 instance PrettyCode FunctionDef where
   ppCode f = do
     funDefName' <- ppCode (f ^. funDefName)
-    funDefTypeSig' <- ppCode (f ^. funDefTypeSig)
+    funDefType' <- ppCode (f ^. funDefType)
     clauses' <- mapM ppCode (f ^. funDefClauses)
     return $
       funDefName' <+> kwColonColon <+> funDefType' <> line
diff --git a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
index cee9041a4..0021f9516 100644
--- a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
+++ b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
@@ -74,7 +74,7 @@ goFunctionDef :: A.FunctionDef -> FunctionDef
 goFunctionDef f =
   FunctionDef
     { _funDefName = _funDefName',
-      _funDefTypeSig = goType (f ^. A.funDefTypeSig),
+      _funDefType = goType (f ^. A.funDefTypeSig),
       _funDefClauses = fmap (goFunctionClause _funDefName') (f ^. A.funDefClauses)
     }
   where