From c5f13e9ffbeb7f103655668a97c706806e2a8d4d Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Tue, 4 Feb 2025 17:58:01 +0300 Subject: [PATCH] [ ux ] Improve error messages in obscure cases --- src/Deriving/DepTyCheck/Gen/Entry.idr | 14 ++++-- .../core/norec part noext 001-neg/expected | 2 +- .../core/norec part noext 002-neg/expected | 2 +- .../core/norec part w_ext 004-neg/expected | 2 +- .../core/norec part w_ext 005-neg/expected | 2 +- .../core/norec part w_ext 006-neg/expected | 2 +- .../core/norec t-p.--.. w_ext 001/expected | 14 +++--- .../core/norec t-p.--.. w_ext 002/expected | 14 +++--- .../norec t-p.--.. w_ext 003-neg/expected | 14 +++--- .../norec t-p.--.. w_ext 004-neg/expected | 14 +++--- .../core/norec t-p.--.. w_ext 005/expected | 6 +-- .../core/norec t-p.--.. w_ext 006/expected | 6 +-- .../bad-args-in-target-type/expected | 2 +- .../params-before-fuel/ValidateInput.idr | 16 +++++++ .../params-before-fuel/expected | 47 +++++++++++++++++++ .../inputvalidation/params-before-fuel/run | 1 + .../params-before-fuel/validate-input.ipkg | 1 + .../unexpected-gen-target/expected | 2 +- 18 files changed, 116 insertions(+), 45 deletions(-) create mode 100644 tests/derivation/inputvalidation/params-before-fuel/ValidateInput.idr create mode 100644 tests/derivation/inputvalidation/params-before-fuel/expected create mode 120000 tests/derivation/inputvalidation/params-before-fuel/run create mode 120000 tests/derivation/inputvalidation/params-before-fuel/validate-input.ipkg diff --git a/src/Deriving/DepTyCheck/Gen/Entry.idr b/src/Deriving/DepTyCheck/Gen/Entry.idr index f683ae3b3..db999df68 100644 --- a/src/Deriving/DepTyCheck/Gen/Entry.idr +++ b/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 diff --git a/tests/derivation/core/norec part noext 001-neg/expected b/tests/derivation/core/norec part noext 001-neg/expected index 020a98a89..2d00ab875 100644 --- a/tests/derivation/core/norec part noext 001-neg/expected +++ b/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 diff --git a/tests/derivation/core/norec part noext 002-neg/expected b/tests/derivation/core/norec part noext 002-neg/expected index e206a685d..3a2d93575 100644 --- a/tests/derivation/core/norec part noext 002-neg/expected +++ b/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 diff --git a/tests/derivation/core/norec part w_ext 004-neg/expected b/tests/derivation/core/norec part w_ext 004-neg/expected index 6cfc3bb28..5b19cca99 100644 --- a/tests/derivation/core/norec part w_ext 004-neg/expected +++ b/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 | diff --git a/tests/derivation/core/norec part w_ext 005-neg/expected b/tests/derivation/core/norec part w_ext 005-neg/expected index 69a049e97..4f6e650e4 100644 --- a/tests/derivation/core/norec part w_ext 005-neg/expected +++ b/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 | diff --git a/tests/derivation/core/norec part w_ext 006-neg/expected b/tests/derivation/core/norec part w_ext 006-neg/expected index 3a34363f9..0b754a6ba 100644 --- a/tests/derivation/core/norec part w_ext 006-neg/expected +++ b/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 | diff --git a/tests/derivation/core/norec t-p.--.. w_ext 001/expected b/tests/derivation/core/norec t-p.--.. w_ext 001/expected index 154569e26..bf4d804e3 100644 --- a/tests/derivation/core/norec t-p.--.. w_ext 001/expected +++ b/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 + ^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/derivation/core/norec t-p.--.. w_ext 002/expected b/tests/derivation/core/norec t-p.--.. w_ext 002/expected index cd7f60e18..0bb2a3b17 100644 --- a/tests/derivation/core/norec t-p.--.. w_ext 002/expected +++ b/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 + ^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/derivation/core/norec t-p.--.. w_ext 003-neg/expected b/tests/derivation/core/norec t-p.--.. w_ext 003-neg/expected index 8380c3efe..81b00ce82 100644 --- a/tests/derivation/core/norec t-p.--.. w_ext 003-neg/expected +++ b/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 + ^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/derivation/core/norec t-p.--.. w_ext 004-neg/expected b/tests/derivation/core/norec t-p.--.. w_ext 004-neg/expected index 84bc89dd3..8338f8d9e 100644 --- a/tests/derivation/core/norec t-p.--.. w_ext 004-neg/expected +++ b/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 + ^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/derivation/core/norec t-p.--.. w_ext 005/expected b/tests/derivation/core/norec t-p.--.. w_ext 005/expected index 1455dba74..738e6862c 100644 --- a/tests/derivation/core/norec t-p.--.. w_ext 005/expected +++ b/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 + ^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/derivation/core/norec t-p.--.. w_ext 006/expected b/tests/derivation/core/norec t-p.--.. w_ext 006/expected index 8df6a2362..5788a7402 100644 --- a/tests/derivation/core/norec t-p.--.. w_ext 006/expected +++ b/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 + ^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/derivation/inputvalidation/bad-args-in-target-type/expected b/tests/derivation/inputvalidation/bad-args-in-target-type/expected index 0caef74a1..1c5034316 100644 --- a/tests/derivation/inputvalidation/bad-args-in-target-type/expected +++ b/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 diff --git a/tests/derivation/inputvalidation/params-before-fuel/ValidateInput.idr b/tests/derivation/inputvalidation/params-before-fuel/ValidateInput.idr new file mode 100644 index 000000000..d284922e6 --- /dev/null +++ b/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}} diff --git a/tests/derivation/inputvalidation/params-before-fuel/expected b/tests/derivation/inputvalidation/params-before-fuel/expected new file mode 100644 index 000000000..3e8d5c032 --- /dev/null +++ b/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}} + ^^^^^^^^^ + diff --git a/tests/derivation/inputvalidation/params-before-fuel/run b/tests/derivation/inputvalidation/params-before-fuel/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/inputvalidation/params-before-fuel/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/inputvalidation/params-before-fuel/validate-input.ipkg b/tests/derivation/inputvalidation/params-before-fuel/validate-input.ipkg new file mode 120000 index 000000000..5d949b2f9 --- /dev/null +++ b/tests/derivation/inputvalidation/params-before-fuel/validate-input.ipkg @@ -0,0 +1 @@ +../_common/validate-input.ipkg \ No newline at end of file diff --git a/tests/derivation/inputvalidation/unexpected-gen-target/expected b/tests/derivation/inputvalidation/unexpected-gen-target/expected index 03e9f3126..34ab47dda 100644 --- a/tests/derivation/inputvalidation/unexpected-gen-target/expected +++ b/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