[ test ] Add tests for error msgs when there are bad function arguments

buzden · Jan 15, 2025 · 05bd0fb · 05bd0fb
1 parent 3d9c571
commit 05bd0fb
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 24 deletions.
diff --git a/tests/derivation/inputvalidation/bad-param-names/ValidateInput.idr b/tests/derivation/inputvalidation/bad-param-names/ValidateInput.idr
@@ -14,6 +14,9 @@ data Y : Type -> Type -> Type where
 genY_unnamed_argument : Fuel -> (a, b : Type) -> Nat -> Gen MaybeEmpty $ Y a b
 genY_unnamed_argument = deriveGen
 
+gen_unnamed_fun : Fuel -> ((a : Nat) -> Nat) -> Gen MaybeEmpty Nat
+gen_unnamed_fun = deriveGen
+
 --- Arguments shadowing ---
 
 genY_shadowed_by_auto_argument : DecEq a => Fuel -> (a : Type) -> (b : Type) -> Gen MaybeEmpty $ Y a b

diff --git a/tests/derivation/inputvalidation/bad-param-names/expected b/tests/derivation/inputvalidation/bad-param-names/expected
@@ -3,29 +3,39 @@ Error: While processing right hand side of genY_unnamed_argument. Error during r
 
 ValidateInput:1
  10 |   MkY : Y Int String
- 11 | 
+ 11 |
  12 | --- Not all arguments are named ---
- 13 | 
+ 13 |
  14 | genY_unnamed_argument : Fuel -> (a, b : Type) -> Nat -> Gen MaybeEmpty $ Y a b
                                                        ^^^
 
-Error: While processing right hand side of genY_shadowed_by_auto_argument. Error during reflection: Explicit argument must be named and must not shadow any other name
+Error: While processing right hand side of gen_unnamed_fun. Error during reflection: Explicit argument must be named and must not shadow any other name
 
 ValidateInput:2
+ 13 |
+ 14 | genY_unnamed_argument : Fuel -> (a, b : Type) -> Nat -> Gen MaybeEmpty $ Y a b
  15 | genY_unnamed_argument = deriveGen
- 16 | 
- 17 | --- Arguments shadowing ---
- 18 | 
- 19 | genY_shadowed_by_auto_argument : DecEq a => Fuel -> (a : Type) -> (b : Type) -> Gen MaybeEmpty $ Y a b
+ 16 |
+ 17 | gen_unnamed_fun : Fuel -> ((a : Nat) -> Nat) -> Gen MaybeEmpty Nat
+                                 ^^^^^^^^^^^^^^^^
+
+Error: While processing right hand side of genY_shadowed_by_auto_argument. Error during reflection: Explicit argument must be named and must not shadow any other name
+
+ValidateInput:3
+ 18 | gen_unnamed_fun = deriveGen
+ 19 |
+ 20 | --- Arguments shadowing ---
+ 21 |
+ 22 | genY_shadowed_by_auto_argument : DecEq a => Fuel -> (a : Type) -> (b : Type) -> Gen MaybeEmpty $ Y a b
                                                                ^^^^
 
 Error: While processing right hand side of genY_shadowed_by_other_argument. Error during reflection: Explicit argument must be named and must not shadow any other name
 
-ValidateInput:3
- 18 | 
- 19 | genY_shadowed_by_auto_argument : DecEq a => Fuel -> (a : Type) -> (b : Type) -> Gen MaybeEmpty $ Y a b
- 20 | genY_shadowed_by_auto_argument = deriveGen
- 21 | 
- 22 | genY_shadowed_by_other_argument : Fuel -> (a : Type) -> (b : Type) -> (a : Type) -> Gen MaybeEmpty $ Y a b
+ValidateInput:4
+ 21 |
+ 22 | genY_shadowed_by_auto_argument : DecEq a => Fuel -> (a : Type) -> (b : Type) -> Gen MaybeEmpty $ Y a b
+ 23 | genY_shadowed_by_auto_argument = deriveGen
+ 24 |
+ 25 | genY_shadowed_by_other_argument : Fuel -> (a : Type) -> (b : Type) -> (a : Type) -> Gen MaybeEmpty $ Y a b
                                                                                  ^^^^
 
diff --git a/tests/derivation/inputvalidation/odd-or-lacking-gen-params/ValidateInput.idr b/tests/derivation/inputvalidation/odd-or-lacking-gen-params/ValidateInput.idr
@@ -27,3 +27,6 @@ genY_with_repeating_name_difflytyped' = deriveGen
 
 genY_unused_argument : Fuel -> (a, b : Type) -> (c : Nat) -> Gen MaybeEmpty $ Y a b
 genY_unused_argument = deriveGen
+
+gen_unused_function_argument : Fuel -> (d : (a : Nat) -> Nat) -> Gen MaybeEmpty Nat
+gen_unused_function_argument = deriveGen
diff --git a/tests/derivation/inputvalidation/odd-or-lacking-gen-params/expected b/tests/derivation/inputvalidation/odd-or-lacking-gen-params/expected
@@ -3,19 +3,19 @@ Error: While processing right hand side of genY_with_unrelated. Error during ref
 
 ValidateInput:1
  10 |   MkY : Y Int String
- 11 | 
+ 11 |
  12 | --- Unrelated stuff in the resulting dpair ---
- 13 | 
+ 13 |
  14 | genY_with_unrelated : Fuel -> (a : Type) -> Gen MaybeEmpty (b : Type ** n : Nat ** Y a b)
                                                                                   ^^^
 
 Error: While processing right hand side of genY_with_repeating_name_equityped. Error during reflection: Argument of dependent pair under the resulting `Gen` must be named
 
 ValidateInput:2
- 13 | 
+ 13 |
  14 | genY_with_unrelated : Fuel -> (a : Type) -> Gen MaybeEmpty (b : Type ** n : Nat ** Y a b)
  15 | genY_with_unrelated = deriveGen
- 16 | 
+ 16 |
  17 | genY_with_repeating_name_equityped : Fuel -> (a : Type) -> Gen MaybeEmpty (b : Type ** b : Type ** Y a b)
                                                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
@@ -26,10 +26,10 @@ and:
 Mismatch between: Nat and Type.
 
 ValidateInput:3
- 16 | 
+ 16 |
  17 | genY_with_repeating_name_equityped : Fuel -> (a : Type) -> Gen MaybeEmpty (b : Type ** b : Type ** Y a b)
  18 | genY_with_repeating_name_equityped = deriveGen
- 19 | 
+ 19 |
  20 | genY_with_repeating_name_difflytyped : Fuel -> (a : Type) -> Gen MaybeEmpty (b : Type ** b : Nat ** Y a b)
                                                                                                               ^
 
@@ -38,7 +38,7 @@ Error: No type declaration for ValidateInput.genY_with_repeating_name_difflytype
 ValidateInput:4
  17 | genY_with_repeating_name_equityped : Fuel -> (a : Type) -> Gen MaybeEmpty (b : Type ** b : Type ** Y a b)
  18 | genY_with_repeating_name_equityped = deriveGen
- 19 | 
+ 19 |
  20 | genY_with_repeating_name_difflytyped : Fuel -> (a : Type) -> Gen MaybeEmpty (b : Type ** b : Nat ** Y a b)
  21 | genY_with_repeating_name_difflytyped = deriveGen
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -50,20 +50,30 @@ and:
 Mismatch between: Nat and Type.
 
 ValidateInput:5
- 19 | 
+ 19 |
  20 | genY_with_repeating_name_difflytyped : Fuel -> (a : Type) -> Gen MaybeEmpty (b : Type ** b : Nat ** Y a b)
  21 | genY_with_repeating_name_difflytyped = deriveGen
- 22 | 
+ 22 |
  23 | genY_with_repeating_name_difflytyped' : Fuel -> (a : Type) -> Gen MaybeEmpty (b : Nat ** b : Type ** Y a b)
                                                                                                ^^^^^^^^
 
 Error: While processing right hand side of genY_unused_argument. Error during reflection: Given parameter is not used in the target type
 
 ValidateInput:6
  24 | genY_with_repeating_name_difflytyped' = deriveGen
- 25 | 
+ 25 |
  26 | --- Not all arguments are used ---
- 27 | 
+ 27 |
  28 | genY_unused_argument : Fuel -> (a, b : Type) -> (c : Nat) -> Gen MaybeEmpty $ Y a b
                                                            ^^^
 
+Error: While processing right hand side of gen_unused_function_argument. Error during reflection: Given parameter is not used in the target type
+
+ValidateInput:7
+ 27 |
+ 28 | genY_unused_argument : Fuel -> (a, b : Type) -> (c : Nat) -> Gen MaybeEmpty $ Y a b
+ 29 | genY_unused_argument = deriveGen
+ 30 |
+ 31 | gen_unused_function_argument : Fuel -> (d : (a : Nat) -> Nat) -> Gen MaybeEmpty Nat
+                                                  ^^^^^^^^^^^^^^^^
+