search

buzden / deptycheck

Facilities for generating dependently-typed data
https://deptycheck.readthedocs.io
Mozilla Public License 2.0
24 stars 7 forks source link

Bad file position in an error message when something wrong with an argument of a function type with a named argument #179

Open buzden opened 3 months ago

buzden commented 3 months ago

Derived generators currently cannot have unnamed explicit arguments, e.g. this is wrong and should fail:

gen : Fuel -> ((a : Nat) -> Nat) -> Gen MaybeEmpty Nat
gen = deriveGen

Also, there cannot be any unused explicit arguments, e.g. this is wrong and should fail:

gen' : Fuel -> (d : (a : Nat) -> Nat) -> Gen MaybeEmpty Nat
gen' = deriveGen

And both these derivation indeed fail, as should. But their error messages are a bit misleading:

Error: While processing right hand side of gen. Error during reflection:
Explicit argument must be named and must not shadow any other name

<filename>:12:17--12:18
 11 |
 12 | gen : Fuel -> ((a : Nat) -> Nat) -> Gen MaybeEmpty Nat
                      ^
Error: While processing right hand side of gen'. Error during reflection:
Given parameter is not used in the target type

<filename>:15:22--15:23
 14 |
 15 | gen' : Fuel -> (d : (a : Nat) -> Nat) -> Gen MaybeEmpty Nat
                           ^

They should highlight the whole type, or at least argument's name (if present) instead, something like this:

Error: While processing right hand side of gen. Error during reflection:
Explicit argument must be named and must not shadow any other name

<filename>:12:17--12:18
 11 |
 12 | gen : Fuel -> ((a : Nat) -> Nat) -> Gen MaybeEmpty Nat
                     ^^^^^^^^^^^^^^^^

and one of these:

Error: While processing right hand side of gen'. Error during reflection:
Given parameter is not used in the target type

<filename>:15:22--15:23
 14 |
 15 | gen' : Fuel -> (d : (a : Nat) -> Nat) -> Gen MaybeEmpty Nat
                      ^

or

Error: While processing right hand side of gen'. Error during reflection:
Given parameter is not used in the target type

<filename>:15:22--15:23
 14 |
 15 | gen' : Fuel -> (d : (a : Nat) -> Nat) -> Gen MaybeEmpty Nat
                          ^^^^^^^^^^^^^^^^

or

Error: While processing right hand side of gen'. Error during reflection:
Given parameter is not used in the target type

<filename>:15:22--15:23
 14 |
 15 | gen' : Fuel -> (d : (a : Nat) -> Nat) -> Gen MaybeEmpty Nat
                      ^^^^^^^^^^^^^^^^^^^^
spcfox commented 2 months ago

It looks like an Idris bug:

> getFC `((Nat) -> Nat)
MkFC (Virtual Interactive) (0, 8) (0, 20)
> getFC `((arg : Nat) -> Nat)
MkFC (Virtual Interactive) (0, 9) (0, 12)

In the second case, FC points only to the name of the argument.

spcfox commented 2 months ago

Same problem with messages from the Idris2 compiler:

Error: While processing right hand side of test1. When unifying:
    Type
and:
    ()
Mismatch between: Type and ().

BadMessages:4:9--4:21
 1 | module BadMessages
 2 |
 3 | test1 : ()
 4 | test1 = (Nat) -> Nat
             ^^^^^^^^^^^^

Error: While processing right hand side of test2. When unifying:
    Type
and:
    ()
Mismatch between: Type and ().

BadMessages:7:10--7:13
 3 | test1 : ()
 4 | test1 = (Nat) -> Nat
 5 |
 6 | test2 : ()
 7 | test2 = (arg : Nat) -> Nat
              ^^^
spcfox commented 2 weeks ago

Reported https://github.com/idris-lang/Idris2/issues/3417