Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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 this issue Aug 13, 2024 · 2 comments
Labels
issue: bad message When library reports some problem badly part: derivation Related to automated derivation of generators status: confirmed bug Something isn't working status: upstream Upstream issue

Comments

@buzden
Copy link
Owner

buzden commented Aug 13, 2024

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
                      ^^^^^^^^^^^^^^^^^^^^
@buzden buzden added status: confirmed bug Something isn't working part: derivation Related to automated derivation of generators issue: bad message When library reports some problem badly labels Aug 13, 2024
@spcfox
Copy link

spcfox commented Sep 10, 2024

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
Copy link

spcfox commented Sep 10, 2024

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
              ^^^

@buzden buzden added the status: upstream Upstream issue label Sep 12, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
issue: bad message When library reports some problem badly part: derivation Related to automated derivation of generators status: confirmed bug Something isn't working status: upstream Upstream issue
Projects
None yet
Development

No branches or pull requests

2 participants