idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.5k stars 375 forks source link

Underscore name of an implicit argument in a signature of an interface function does not work #3291

Open buzden opened 4 months ago

buzden commented 4 months ago

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.