possible parsing bug: invalid {...} notation

Stream: lean4

[Alexander Bentkamp]

Is this a bug in the parser?

----- Works:
class A

class B
  where
  lt (a : Nat) [A] : Bool

instance : B where
  lt (a : Nat) [A] := true

----- Does not work:
class X

class Y
  where
  lt [X] : Bool

instance : Y where
  lt [X] := true
-- invalid {...} notation, exactly one explicit source is required when using '[<index>] := <value>' update notation

[Damiano Testa]

Assuming that I understood what you want, it "works" with curly brackets:

instance : Y where
  lt {a} := true

[Damiano Testa]

(or nothing at all!)

[Alexander Bentkamp]

Another workaround I found:

instance : Y where
  lt := fun [X] => true

[Damiano Testa]

My second comment was very cryptic: this also works

instance : Y where
  lt := true

[Alexander Bentkamp]

I got it, thanks!

[Damiano Testa]

You can see that the typeclass assumption is auto-introduced here.

[Damiano Testa]

I think that there is a lot of matching and assignment that it would be nice to have in that position, but not much is actually implemented (EDIT: or feasible).

[Alexander Bentkamp]

So, yeah, in practice this is unlikely to be a real issue. Still, the behavior is inconsistent and probably not intended.

[Alexander Bentkamp]

Anyway, I am happy with the workarounds you and I found.

[Damiano Testa]

At the very least, the error message could be more explicit about what the issue is, I think.

[Kyle Miller]

It's not a bug exactly, but a complication from structure notation. The where ... syntax is essentially a macro for := { ... }, and in { ... } you can use [...] to update array-like fields (internally called a "modifyOp"), like in

structure S where
  xs : Array Nat

def S.change0 (s : S) (x : Nat) : S := { s with xs[0] := x }

It only works with with though, which isn't present in where syntax, so the restriction is a little pointless here.

Something that is a little counterintuitive is that in where/{...} notation, the binder lists are effectively fun binder lists. The binder list here comes from the expected type, so all you need to do is provide identifiers, not (...)/[...]/{...}/{{...}} brackets. In this case, since the X parameter is implicit, it's automatically introduced anyway:

instance : Y where
  lt := true

Damiano already pointed this one out, but this is the reason for not needing to mention the parameter at all.

[Kyle Miller]

(One way this could be improved is to put noWs into the modifyOp parser. There's no reason to accept xs [0] := x.)

[Damiano Testa]

Oh, I did not realise that the error message was coming from a modifyOp!