[ ux ] Improve error messages in obscure cases

src/Deriving/DepTyCheck/Gen/Entry.idr

@@ -159,10 +159,16 @@ checkTypeIsGen checkSide sig = do
   -- Target type family's arguments' first checks --
   --------------------------------------------------
 
-  -- check all the arguments of the target type are variable names, not complex expressions
-  targetTypeArgs <- for targetTypeArgs $ \case
-    IVar _ (UN argName) => pure argName
-    nonVarArg => failAt (getFC nonVarArg) "Target type's argument must be a variable name"
+  -- check all the arguments of the target type are correct variable names, not complex expressions
+  targetTypeArgs <- do
+    let inGivenOrGenerated : UserName -> Bool
+        inGivenOrGenerated n = any (\(_, n', _) => n == n') givenParams || any (\(n', _) => n == n') paramsToBeGenerated
+    let err : Name -> String -> String
+        err n suffix = "Name `\{show n}` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); \{suffix}"
+    for targetTypeArgs $ \case
+      IVar fc un@(UN argName) => if inGivenOrGenerated argName then pure argName else failAt fc $ err un "did you forget to add one?"
+      IVar fc mn@(MN {}) => failAt fc $ err mn "looks like it is an implicit parameter of some underdeclared type; specify types with more precision"
+      nonVarArg => failAt (getFC nonVarArg) "Target type's argument must be a variable name, got `\{show nonVarArg}`"
 
   -- check that all arguments names are unique
   let [] = findDiffPairWhich (==) targetTypeArgs

tests/derivation/core/norec part noext 001-neg/expected

@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name
+Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name, got `Prelude.Basics.Bool`
 
 DerivedGen:1
  5 | %default total

tests/derivation/core/norec part noext 002-neg/expected

@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name
+Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name, got `Prelude.Basics.Bool`
 
 DerivedGen:1
  5 | %default total

tests/derivation/core/norec part w_ext 004-neg/expected

@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name
+Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name, got `String`
 
 DerivedGen:1
  06 | 

tests/derivation/core/norec part w_ext 005-neg/expected

@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name
+Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name, got `String`
 
 DerivedGen:1
  06 | 

tests/derivation/core/norec part w_ext 006-neg/expected

@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name
+Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name, got `String`
 
 DerivedGen:1
  06 | 

tests/derivation/core/norec t-p.--.. w_ext 001/expected

@@ -1,12 +1,12 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type `a` is not a top-level data definition
+Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 5 | %default total
- 6 | 
- 7 | %language ElabReflection
- 8 | 
- 9 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (Maybe a)
-                                   ^^^
+ 06 | 
+ 07 | %language ElabReflection
+ 08 | 
+ 09 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (Maybe a)
+ 10 | checkedGen = deriveGen
+      ^^^^^^^^^^^^^^^^^^^^^^
 

tests/derivation/core/norec t-p.--.. w_ext 002/expected

@@ -1,12 +1,12 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type `b` is not a top-level data definition
+Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 5 | %default total
- 6 | 
- 7 | %language ElabReflection
- 8 | 
- 9 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty b) => (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (a, b)
-                                   ^^^
+ 06 | 
+ 07 | %language ElabReflection
+ 08 | 
+ 09 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty b) => (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (a, b)
+ 10 | checkedGen = deriveGen
+      ^^^^^^^^^^^^^^^^^^^^^^
 

tests/derivation/core/norec t-p.--.. w_ext 003-neg/expected

@@ -1,12 +1,12 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: All arguments of the target type must be different
+Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 5 | %default total
- 6 | 
- 7 | %language ElabReflection
- 8 | 
- 9 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (a, a)
-                                                                        ^^
+ 06 | 
+ 07 | %language ElabReflection
+ 08 | 
+ 09 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (a, a)
+ 10 | checkedGen = deriveGen
+      ^^^^^^^^^^^^^^^^^^^^^^
 

tests/derivation/core/norec t-p.--.. w_ext 004-neg/expected

@@ -1,12 +1,12 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name
+Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 5 | %default total
- 6 | 
- 7 | %language ElabReflection
- 8 | 
- 9 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => (Fuel -> Gen MaybeEmpty b) => Gen MaybeEmpty (a, b, a)
-                                                                                                         ^^
+ 06 | 
+ 07 | %language ElabReflection
+ 08 | 
+ 09 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => (Fuel -> Gen MaybeEmpty b) => Gen MaybeEmpty (a, b, a)
+ 10 | checkedGen = deriveGen
+      ^^^^^^^^^^^^^^^^^^^^^^
 

tests/derivation/core/norec t-p.--.. w_ext 005/expected

@@ -1,12 +1,12 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type `a` is not a top-level data definition
+Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 10 | 
  11 | Show a => Show (X a) where
  12 |   show (MkX m) = "MkX \{show m}"
  13 | 
  14 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (X a)
-                                    ^^^
+ 15 | checkedGen = deriveGen
+      ^^^^^^^^^^^^^^^^^^^^^^
 

tests/derivation/core/norec t-p.--.. w_ext 006/expected

@@ -1,12 +1,12 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target type `a` is not a top-level data definition
+Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 10 | 
  11 | Show a => Show b => Show (X a b) where
  12 |   show (MkX m) = "MkX \{show m}"
  13 | 
  14 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => (Fuel -> Gen MaybeEmpty b) => Gen MaybeEmpty (X a b)
-                                    ^^^
+ 15 | checkedGen = deriveGen
+      ^^^^^^^^^^^^^^^^^^^^^^
 

tests/derivation/inputvalidation/bad-args-in-target-type/expected

@@ -1,5 +1,5 @@
 1/1: Building ValidateInput (ValidateInput.idr)
-Error: While processing right hand side of genY_Int. Error during reflection: Target type's argument must be a variable name
+Error: While processing right hand side of genY_Int. Error during reflection: Target type's argument must be a variable name, got `Int`
 
 ValidateInput:1
  10 |   MkY : Y Int String

tests/derivation/inputvalidation/params-before-fuel/ValidateInput.idr

@@ -0,0 +1,16 @@
+module ValidateInput
+
+import Deriving.DepTyCheck.Gen
+
+%language ElabReflection
+
+%default total
+
+data X : Fin n -> Fin n -> Type where
+  MkX : X {n=10} 5 6
+
+n_is_fully_out : Fuel -> (a, b : _) -> Gen MaybeEmpty $ X a b
+n_is_fully_out = deriveGen @{MainCoreDerivator @{LeastEffort}}
+
+n_mentioned_in_wrong_place : Fuel -> (a, b : Fin n) -> Gen MaybeEmpty $ X a b
+n_mentioned_in_wrong_place = deriveGen @{MainCoreDerivator @{LeastEffort}}

tests/derivation/inputvalidation/params-before-fuel/expected

@@ -0,0 +1,47 @@
+1/1: Building ValidateInput (ValidateInput.idr)
+Error: While processing right hand side of n_is_fully_out. Sorry, I can't find any elaboration which works. All errors:
+Possible error:
+    Error during reflection: Name `{n:3660}` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); looks like it is an implicit parameter of some underdeclared type; specify types with more precision
+
+    ValidateInput:1
+     09 | data X : Fin n -> Fin n -> Type where
+     10 |   MkX : X {n=10} 5 6
+     11 | 
+     12 | n_is_fully_out : Fuel -> (a, b : _) -> Gen MaybeEmpty $ X a b
+     13 | n_is_fully_out = deriveGen @{MainCoreDerivator @{LeastEffort}}
+          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Possible error:
+    Error during reflection: No arguments in the generator function signature, at least a fuel argument must be present
+
+    ValidateInput:2
+     09 | data X : Fin n -> Fin n -> Type where
+     10 |   MkX : X {n=10} 5 6
+     11 | 
+     12 | n_is_fully_out : Fuel -> (a, b : _) -> Gen MaybeEmpty $ X a b
+     13 | n_is_fully_out = deriveGen @{MainCoreDerivator @{LeastEffort}}
+                           ^^^^^^^^^
+
+Error: While processing right hand side of n_mentioned_in_wrong_place. Sorry, I can't find any elaboration which works. All errors:
+Possible error:
+    Error during reflection: Name `n` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
+
+    ValidateInput:3
+     12 | n_is_fully_out : Fuel -> (a, b : _) -> Gen MaybeEmpty $ X a b
+     13 | n_is_fully_out = deriveGen @{MainCoreDerivator @{LeastEffort}}
+     14 | 
+     15 | n_mentioned_in_wrong_place : Fuel -> (a, b : Fin n) -> Gen MaybeEmpty $ X a b
+     16 | n_mentioned_in_wrong_place = deriveGen @{MainCoreDerivator @{LeastEffort}}
+          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Possible error:
+    Error during reflection: No arguments in the generator function signature, at least a fuel argument must be present
+
+    ValidateInput:4
+     12 | n_is_fully_out : Fuel -> (a, b : _) -> Gen MaybeEmpty $ X a b
+     13 | n_is_fully_out = deriveGen @{MainCoreDerivator @{LeastEffort}}
+     14 | 
+     15 | n_mentioned_in_wrong_place : Fuel -> (a, b : Fin n) -> Gen MaybeEmpty $ X a b
+     16 | n_mentioned_in_wrong_place = deriveGen @{MainCoreDerivator @{LeastEffort}}
+                                       ^^^^^^^^^
+

tests/derivation/inputvalidation/params-before-fuel/run

@@ -0,0 +1 @@
+../_common/run

tests/derivation/inputvalidation/params-before-fuel/validate-input.ipkg

@@ -0,0 +1 @@
+../_common/validate-input.ipkg

tests/derivation/inputvalidation/unexpected-gen-target/expected

@@ -1,5 +1,5 @@
 1/1: Building ValidateInput (ValidateInput.idr)
-Error: While processing right hand side of genOfConcreteGen. Error during reflection: Target type's argument must be a variable name
+Error: While processing right hand side of genOfConcreteGen. Error during reflection: Target type's argument must be a variable name, got `Test.DepTyCheck.Gen.Emptiness.MaybeEmpty`
 
 ValidateInput:1
  12 |   MkY : Y Int String