Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

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

Open buzden opened this issue 8 months ago • 0 comments

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.

buzden avatar May 28 '24 14:05 buzden