add missing pattern arity check

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 <> "`"
 

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)

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

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.