why simple lambda notation fails?

Stream: lean4

[Asei Inoue]

class Plus (α β γ : Type) where
  plus : α → β → γ

infixl:65 " + " => Plus.plus

-- works
instance : Plus Nat (List Nat) (List Nat) where
  plus n ns := List.map (fun x => n + x) ns

-- why this fails?
instance : Plus Nat (List Nat) (List Nat) where
  /-
  ambiguous, possible interpretations
    n + x✝¹ : ?m.1676

    n + x✝ : Nat
  -/
  plus n ns := List.map (n + ·) ns

[Kyle Miller]

Make sure to include all the code in your mwe. I am guessing you are missing an infix or notation that redefines +.

[Asei Inoue]

@Kyle Miller Thank you!! I edited my question.

[Kyle Miller]

Then that's the problem, you've defined your own + notation, and it's telling you that n + · is ambiguous.

[Kyle Miller]

Generally you shouldn't be definining your own Plus and + when there's HAdd and + already available.

[Asei Inoue]

Sorry, my explanation wasn't good enough.

[Asei Inoue]

My question here is why writing explicit lambda expressions using fun does not result in an error, but using bracket syntax fails.

[Asei Inoue]

It is correct that the + sign is covered by an error, but not both. The reason for the difference is what I want to know.

[Asei Inoue]

If (n + ·) is a macro that expands to fun x => n + x, it seemed natural that both would have the same error.

[Kyle Miller]

I'm not sure why the first one works (I take that back, it works because it's able to disambiguate after trying to elaborate it both ways)

[Kyle Miller]

I'm not sure why these are different

[Kyle Miller]

On a nightly build of Lean, I'm getting a different error on (n + ·):

application type mismatch
  List.map fun x x => n + x
argument
  fun x x => n + x
has type
  ?m.1610 → Nat → Nat : Type ?u.1609
but is expected to have type
  ?m.1610 → Nat : Type ?u.1609

[Kyle Miller]

I'm not sure how it's getting two arguments.

[Kyle Miller]

Oh, I see... It's triggered by the ambiguous notation.

Here's some of the elaboration trace.

[Elab.app.args] args: [(Term.paren "(" (choice («term_+__1» `n "+" (Term.cdot "·")) («term_+_» `n "+" (Term.cdot "·"))) ")"), `ns]

The key is that cdot appears twice, so it gets two arguments. This is a funny oversight in how cdot expansion handles choice nodes.

[Kyle Miller]

What version of Lean are you using?

[Kyle Miller]

(And in any case, the answer is "don't overload +". There are things that won't work correctly if you do. Still, it's good that it uncovered this bug.)

[Floris van Doorn]

I get the same error as Asei on 4.9.0-rc3.

[Kyle Miller]

I see it on 4.10.0-rc2 as well. (Edit: not locally, just in the playground link for Asei's original post... Edit edit: I had commented out the first instance in testing, but it's necessary to get "ambiguous" error.)

[Kyle Miller]

Found the explanation for what changed recently: lean4#4596 disambiguates more strongly, removing alternatives when there are stuck metavariables.

[Kyle Miller]

However, the same bug with cdot notation was there even then. Something to notice is that in the error

  ambiguous, possible interpretations
    n + x✝¹ : ?m.1676

    n + x✝ : Nat

you can see both x✝¹ and x✝. There are two variables, not one.

[Kyle Miller]

Reported: lean4#4832