Idris2
Idris2 copied to clipboard
Underscore name of an implicit argument in a signature of an interface function does not work
Steps to Reproduce
%default total
interface S where
pop : {_ : Unit} -> Unit
S where
pop = ?fooo
The signature may have an auto
-implicit parameter with any quantity, in fact. But the name must be _
.
Expected Behavior
Code typechecks
Observed Behavior
Error: While processing right hand side of Stack implementation at X:15:1--20:14. {conArg:2503} is not a valid argument
in pop s
Lack of name, of any non-_
name, of explicitness of a parameter makes the bug disappear.