You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is the reason for the bad error messages. Example:
unnamed:()
unnamed = (Nat) ->Natnamed:()
named = (arg:Nat) ->Nat
Error: While processing right hand side of unnamed. When unifying:
Type
and:
()
Mismatch between: Type and ().
BadMessages:4:11--4:23
1 | module BadMessages
2 |
3 | unnamed : ()
4 | unnamed = (Nat) -> Nat
^^^^^^^^^^^^
Error: While processing right hand side of named. When unifying:
Type
and:
()
Mismatch between: Type and ().
BadMessages:7:10--7:13
3 | unnamed : ()
4 | unnamed = (Nat) -> Nat
5 |
6 | named : ()
7 | named = (arg : Nat) -> Nat
^^^
Expected Behavior
FC points to whole type
Observed Behavior
FC points to the name of the argument
The text was updated successfully, but these errors were encountered:
FC of Pi-type with named argument points to the name of the argument instead of whole type.
Steps to Reproduce
This is the reason for the bad error messages. Example:
Expected Behavior
FC points to whole type
Observed Behavior
FC points to the name of the argument
The text was updated successfully, but these errors were encountered: