Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

confusing error message for unannotated definition in `where` block attached to polymorphic function

Open rntz opened this issue 1 year ago • 1 comments

two: Nat
two = 2

bar: a -> a
bar x = x where
 wat = two

yields the error message:

     While processing right hand side of bar. While processing right hand side of wat. When unifying:
         Nat
     and:
         (0 a : Type) -> (x : a) -> ?_
     Mismatch between: Nat and (0 a : Type) -> (x : a) -> ?_.
     
     error-wtftype:6:8--6:11
      2 | two = 2
      3 | 
      4 | bar: a -> a
      5 | bar x = x where
      6 |  wat = two
                 ^^^

which is quite confusing; the type (0 a : Type) -> (x : a) -> ?_ seems to have nothing to do with what I wrote, namely two.

rntz avatar Jul 15 '22 21:07 rntz

this may be related to #2592

rntz avatar Jul 15 '22 21:07 rntz