From da293d1ce8f9db9daa6f19ef5c2864ad6031030f Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sat, 11 Jan 2020 17:27:27 +0000
Subject: [PATCH] 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        | 6 ++++--
 src/Core/Core.idr               | 3 +++
 src/Idris/Error.idr             | 2 ++
 tests/Main.idr                  | 2 +-
 tests/idris2/basic030/arity.idr | 8 ++++++++
 tests/idris2/basic030/expected  | 3 +++
 tests/idris2/basic030/run       | 3 +++
 7 files changed, 24 insertions(+), 3 deletions(-)
 create mode 100644 tests/idris2/basic030/arity.idr
 create mode 100644 tests/idris2/basic030/expected
 create mode 100644 tests/idris2/basic030/run

diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr
index 793a458..80bc9a2 100644
--- a/src/Core/CaseBuilder.idr
+++ b/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
diff --git a/src/Core/Core.idr b/src/Core/Core.idr
index a8f10f5..18ca980 100644
--- a/src/Core/Core.idr
+++ b/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)
diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr
index 6e3becf..5a99b2e 100644
--- a/src/Idris/Error.idr
+++ b/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
diff --git a/tests/Main.idr b/tests/Main.idr
index 1d037ec..7771a79 100644
--- a/tests/Main.idr
+++ b/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",
diff --git a/tests/idris2/basic030/arity.idr b/tests/idris2/basic030/arity.idr
new file mode 100644
index 0000000..7709551
--- /dev/null
+++ b/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)
diff --git a/tests/idris2/basic030/expected b/tests/idris2/basic030/expected
new file mode 100644
index 0000000..6ec3dd1
--- /dev/null
+++ b/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
diff --git a/tests/idris2/basic030/run b/tests/idris2/basic030/run
new file mode 100644
index 0000000..2828781
--- /dev/null
+++ b/tests/idris2/basic030/run
@@ -0,0 +1,3 @@
+$1 --check arity.idr
+
+rm -rf build