Check constructors are fully applied in case trees

This is necessary to build case trees correctly, and without this, we
can get mysterious and hard to debug run time errors!

src/Core/CaseBuilder.idr

@@ -525,8 +525,10 @@ groupCons fc fn pvars cs
     -- variable we're doing the case split on
     addGroup (PAs fc n p) pprf pats rhs acc
          = addGroup p pprf pats (substName n (Local fc (Just True) _ pprf) rhs) acc
-    addGroup (PCon _ n t a pargs) pprf pats rhs acc
-         = addConG n t pargs pats rhs acc
+    addGroup (PCon cfc n t a pargs) pprf pats rhs acc
+         = if a == length pargs
+              then addConG n t pargs pats rhs acc
+              else throw (CaseCompile cfc fn (NotFullyApplied n))
     addGroup (PTyCon _ n a pargs) pprf pats rhs acc
          = addConG n 0 pargs pats rhs acc
     addGroup (PArrow _ _ s t) pprf pats rhs acc

src/Core/Core.idr

@@ -21,6 +21,7 @@ public export
 data CaseError = DifferingArgNumbers
                | DifferingTypes
                | MatchErased (vars ** (Env Term vars, Term vars))
+               | NotFullyApplied Name
                | UnknownType
 
 -- All possible errors, carrying a location
@@ -210,6 +211,8 @@ Show Error where
   show (CaseCompile fc n (MatchErased (_ ** (env, tm))))
       = show fc ++ ":Attempt to match on erased argument " ++ show tm ++
                    " in " ++ show n
+  show (CaseCompile fc n (NotFullyApplied c))
+      = show fc ++ ":Constructor " ++ show c ++ " is not fully applied"
   show (MatchTooSpecific fc env tm)
       = show fc ++ ":Can't match on " ++ show tm ++ " as it is has a polymorphic type"
   show (BadDotPattern fc env reason x y)

src/Idris/Error.idr

@@ -201,6 +201,8 @@ perror (CaseCompile _ n DifferingTypes)
     = pure $ "Patterns for " ++ show n ++ " require matching on different types"
 perror (CaseCompile _ n UnknownType)
     = pure $ "Can't infer type to match in " ++ show n
+perror (CaseCompile fc n (NotFullyApplied cn))
+    = pure $ "Constructor " ++ show !(toFullNames cn) ++ " is not fully applied"
 perror (CaseCompile fc n (MatchErased (_ ** (env, tm))))
     = pure $ "Attempt to match on erased argument " ++ !(pshow env tm) ++
              " in " ++ show n

tests/Main.idr

@@ -28,7 +28,7 @@ idrisTests
        "basic011", "basic012", "basic013", "basic014", "basic015",
        "basic016", "basic017", "basic018", "basic019", "basic020",
        "basic021", "basic022", "basic023", "basic024", "basic025",
-       "basic026", "basic027", "basic028", "basic029",
+       "basic026", "basic027", "basic028", "basic029", "basic030",
        "coverage001", "coverage002", "coverage003", "coverage004",
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",

tests/idris2/basic030/arity.idr

@@ -0,0 +1,8 @@
+data MyN = MkN Nat Nat
+
+foo : Nat -> Nat -> Nat
+foo x y = case MkN x of
+               MkN z => y
+
+main : IO ()
+main = printLn (foo 2 2)

tests/idris2/basic030/expected

@@ -0,0 +1,3 @@
+1/1: Building arity (arity.idr)
+arity.idr:5:16--5:22:While processing right hand side of Main.foo at arity.idr:4:1--7:1:
+Constructor Main.MkN is not fully applied

tests/idris2/basic030/run

@@ -0,0 +1,3 @@
+$1 --check arity.idr
+
+rm -rf build