Idris2
Idris2 copied to clipboard
confusing error message for unannotated definition in `where` block attached to polymorphic function
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
.
this may be related to #2592