[ fix #735 ] Make sure type constructors are fully applied

libs/contrib/Syntax/PreorderReasoning/Generic.idr

@@ -8,22 +8,22 @@ infix  1  ...
 
 public export
 data Step : (leq : a -> a -> Type) -> a -> a -> Type where
-  (...) : {leq : a -> a -> Type} ->  (y : a) -> x `leq` y -> Step leq x y
+  (...) : (y : a) -> x `leq` y -> Step leq x y
 
 public export
-data FastDerivation : {leq : a -> a -> Type} -> (x : a) -> (y : a) -> Type where
-  (|~) : (x : a) -> FastDerivation x x
-  (<~) : {leq : a -> a -> Type} -> {x,y : a} 
-         -> FastDerivation {leq = leq} x y -> {z : a} -> (step : Step leq y z) 
-         -> FastDerivation {leq = leq} x z
+data FastDerivation : (leq : a -> a -> Type) -> (x : a) -> (y : a) -> Type where
+  (|~) : (x : a) -> FastDerivation leq x x
+  (<~) : {x, y : a}
+         -> FastDerivation leq x y -> {z : a} -> (step : Step leq y z)
+         -> FastDerivation leq x z
 
-public export  
-CalcWith : Preorder dom leq => {x,y : dom} -> FastDerivation {leq = leq} x y -> x `leq` y
+public export
+CalcWith : Preorder dom leq => {x,y : dom} -> FastDerivation leq x y -> x `leq` y
 CalcWith (|~ x) = reflexive x
 CalcWith ((<~) der (z ... step)) = transitive {po = leq} _ _ _ (CalcWith der) step
 
 public export
-(~~) : {x,y : dom} 
-         -> FastDerivation {leq = leq} x y -> {z : dom} -> (step : Step Equal y z)
-         -> FastDerivation {leq = leq} x z
+(~~) : {x,y : dom}
+         -> FastDerivation leq x y -> {z : dom} -> (step : Step Equal y z)
+         -> FastDerivation leq x z
 (~~) der (z ... Refl) = der

src/Core/CaseBuilder.idr

@@ -605,8 +605,10 @@ groupCons fc fn pvars cs
          = if a == length pargs
               then addConG n t pargs pats pid rhs acc
               else throw (CaseCompile cfc fn (NotFullyApplied n))
-    addGroup (PTyCon _ n a pargs) pprf pats pid rhs acc
-         = addConG n 0 pargs pats pid rhs acc
+    addGroup (PTyCon cfc n a pargs) pprf pats pid rhs acc
+         = if a == length pargs
+           then addConG n 0 pargs pats pid rhs acc
+           else throw (CaseCompile cfc fn (NotFullyApplied n))
     addGroup (PArrow _ _ s t) pprf pats pid rhs acc
          = addConG (UN "->") 0 [s, t] pats pid rhs acc
     -- Go inside the delay; we'll flag the case as needing to force its

tests/Main.idr

@@ -50,11 +50,11 @@ idrisTests
        -- Documentation strings
        "docs001", "docs002",
        -- Evaluator
-       "evaluator001", "evaluator002", "evaluator003",
+       "evaluator001", "evaluator002", "evaluator003", "evaluator004",
        -- Error messages
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",
-       "error011", "error012", "error013",
+       "error011", "error012", "error013", "error014",
        -- Modules and imports
        "import001", "import002", "import003", "import004", "import005",
        -- Interactive editing support

tests/idris2/error014/Issue735.idr

@@ -0,0 +1,13 @@
+module Issue735
+
+-- Not allowed to pattern-match on under-applied constructors
+isCons : (a -> List a -> List a) -> Bool
+isCons (::) = True
+isCons _ = False
+
+interface A a where
+
+-- Not allowed to pattern-match on under-applied type constructors
+test : (kind : Type -> Type) -> Maybe Nat
+test A = Just 1
+test _ = Nothing

tests/idris2/error014/expected

@@ -0,0 +1,15 @@
+1/1: Building Issue735 (Issue735.idr)
+Error: Constructor Prelude.Types.:: is not fully applied.
+
+Issue735.idr:5:8--5:12
+   |
+ 5 | isCons (::) = True
+   |        ^^^^
+
+Error: Constructor Issue735.A is not fully applied.
+
+Issue735.idr:12:6--12:7
+    |
+ 12 | test A = Just 1
+    |      ^
+

tests/idris2/error014/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 Issue735.idr --check
+
+rm -rf build/

tests/idris2/evaluator004/Issue735.idr

@@ -0,0 +1,13 @@
+interface Natty (n : Nat) where
+
+fromNatty : Type -> Nat
+fromNatty (Natty Z) = Z
+fromNatty (Natty (S n)) = S (fromNatty (Natty n))
+fromNatty _ = Z
+
+main : IO ()
+main = ignore $ traverse printLn
+  [ fromNatty (Natty 3)
+  , fromNatty (Natty (2 + 6))
+  , fromNatty (List (Natty 1))
+  ]

tests/idris2/evaluator004/expected

@@ -0,0 +1,10 @@
+1/1: Building Issue735 (Issue735.idr)
+Main> 0
+Main> 3
+Main> 0
+Main> 9
+Main> 
+Bye for now!
+3
+8
+0

tests/idris2/evaluator004/input

@@ -0,0 +1,5 @@
+fromNatty (Natty 0)
+fromNatty (Natty 3)
+fromNatty Nat
+fromNatty (Natty (2 + 7))
+:q

tests/idris2/evaluator004/run

@@ -0,0 +1,4 @@
+$1 --no-banner --no-color --console-width 0 Issue735.idr < input
+$1 --exec main --cg ${IDRIS2_TESTS_CG} Issue735.idr
+
+rm -rf build