[typecheck] Add error message for ctor match args mistmatch

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"
 

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

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

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

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
         ]

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;