From 38c1c182ef67e409cd26628c9edcdf2e43cb365b Mon Sep 17 00:00:00 2001
From: Dominic Orchard <dom.orchard@gmail.com>
Date: Thu, 7 Mar 2024 17:08:40 +0000
Subject: [PATCH] add missing pattern arity check

---
 frontend/src/Language/Granule/Checker/Monad.hs             | 6 ++++--
 frontend/src/Language/Granule/Checker/Patterns.hs          | 7 ++++++-
 frontend/tests/cases/negative/polymorphism/patternArity.gr | 4 ++++
 .../cases/negative/polymorphism/patternArity.gr.output     | 3 +++
 4 files changed, 17 insertions(+), 3 deletions(-)
 create mode 100644 frontend/tests/cases/negative/polymorphism/patternArity.gr
 create mode 100644 frontend/tests/cases/negative/polymorphism/patternArity.gr.output

diff --git a/frontend/src/Language/Granule/Checker/Monad.hs b/frontend/src/Language/Granule/Checker/Monad.hs
index 273f58e47..d9cd22c2c 100644
--- a/frontend/src/Language/Granule/Checker/Monad.hs
+++ b/frontend/src/Language/Granule/Checker/Monad.hs
@@ -581,7 +581,7 @@ data CheckerError
   | PatternTypingMismatch
     { errLoc :: Span, errPat :: Pattern (), tyExpected :: Type, tyActual :: Type }
   | PatternArityError
-    { errLoc :: Span, errId :: Id }
+    { errLoc :: Span, errId :: Id, expectedArgs :: Int, actualArgs :: Int }
   | UnboundVariableError
     { errLoc :: Span, errId :: Id }
   | UnboundTypeVariable
@@ -886,7 +886,9 @@ instance UserMsg CheckerError where
   msg PatternArityError{..}
     = "Data constructor `"
       <> pretty errId
-      <> "` is applied to too many arguments."
+      <> "` is applied to wrong number of arguments. Expecting "
+      <> show expectedArgs <> " but pattern match has "
+      <> show actualArgs <> " patterns."
 
   msg UnboundVariableError{..} = "`" <> pretty errId <> "`"
 
diff --git a/frontend/src/Language/Granule/Checker/Patterns.hs b/frontend/src/Language/Granule/Checker/Patterns.hs
index a8ae2546b..28c2a8296 100644
--- a/frontend/src/Language/Granule/Checker/Patterns.hs
+++ b/frontend/src/Language/Granule/Checker/Patterns.hs
@@ -184,7 +184,12 @@ ctxtFromTypedPattern' outerBoxTy _ pos ty p@(PConstr s _ rf dataC tyVarBindsRequ
   mConstructor <- lookupDataConstructor s dataC
   case mConstructor of
     Nothing -> throw UnboundDataConstructor{ errLoc = s, errId = dataC }
-    Just (tySch@(Forall _ tyVarBinders _ _), coercions, indices) -> do
+    Just (tySch@(Forall _ tyVarBinders _ innerType), coercions, indices) -> do
+
+      -- Check pattern arity
+      if (arity innerType /= length ps)
+        then throw $ PatternArityError s dataC (arity innerType) (length ps)
+        else return ()
 
       case outerBoxTy of
         -- Hsup if you only have more than one premise (and have an enclosing grade)
diff --git a/frontend/tests/cases/negative/polymorphism/patternArity.gr b/frontend/tests/cases/negative/polymorphism/patternArity.gr
new file mode 100644
index 000000000..090f10eeb
--- /dev/null
+++ b/frontend/tests/cases/negative/polymorphism/patternArity.gr
@@ -0,0 +1,4 @@
+data Vec a = Nil a | Cons a (Vec a)
+
+extract : Vec Int -> Int
+extract (Cons x) = x
\ No newline at end of file
diff --git a/frontend/tests/cases/negative/polymorphism/patternArity.gr.output b/frontend/tests/cases/negative/polymorphism/patternArity.gr.output
new file mode 100644
index 000000000..9a64b729f
--- /dev/null
+++ b/frontend/tests/cases/negative/polymorphism/patternArity.gr.output
@@ -0,0 +1,3 @@
+Type checking failed: blappy.gr:
+Pattern arity error: blappy.gr:4:10:
+Data constructor `Cons` is applied to wrong number of arguments. Expecting 2 but pattern match has 1 patterns.
\ No newline at end of file