implicit argument in notation rhs

Stream: lean4

[Jakob von Raumer]

It seems counterintuitive that this does not work:

variable (C : Type)

class Foo (A : Type) where
  r : C → C → A

variable {A} [Foo C A]

notation X "~[" A "]" Y => Foo.r (A := A) X Y

variable (X Y : C)

#check X ~[A] Y

variable (B : Type)

#check X ~[B] Y  -- invalid argument name 'B' for function 'Foo.r'

But it seems that the rhs of the notation declaration doesn't bind the (right) A to the term syntax on the lhs of the declaration?

[Aaron Liu]

You'll get better results with something different

variable (C : Type)

class Foo (A : Type) where
  r : C → C → A

variable {A} [Foo C A]

notation X "~[" A "]" Y => @Foo.r _ A _ X Y

variable (X Y : C)

#check X ~[A] Y

variable (B : Type)

#check X ~[B] Y -- failed to synthesize Foo C B

[Yaël Dillies]

Indeed, this is a common gotcha. See docs#Mon_Class.«termγ[_,_]» for an example in mathlib. I don't know of a use case for being able to bind variable names though

[Jakob von Raumer]

@Aaron Liu Which leads to my follow-up question:

notation X "~[" A "]" Y => @Foo.r _ A _ X Y

variable (X Y : C)

example : (X ~[A] Y) = (Y ~[A] X) := by
  sorry  -- ⊢ Foo.r X Y = Foo.r Y X

Why doesn't the notation delab correctly when using that workaround :melt:

[Jakob von Raumer]

(Which currently is the state for morphisms in enriched categories in mathlib, which should be printed as X ⟶[V] Y but aren't)

[Yaël Dillies]

Dumb question: Have you tried notation3?

[Aaron Liu]

Why is notation putting in ($A := $A) when $A is a term and the left hand side expects an ident

[Jakob von Raumer]

Yaël Dillies said:

Dumb question: Have you tried notation3?

notation3 indeed does the right thing (when using @..., not when using (A := ...))

[Jakob von Raumer]

Do notation3 uses count as technical debt?

[Ruben Van de Velde]

No