Override associativity of notation

Stream: general

[Andrej Bauer]

I would like to use • as an infix left associative operator, but I am unable to successfully override the notation associated with the Mathlib.Algebra.Group.Defs.HSMul class, which specifies • to be right associative. Here's an example:

import Mathlib.Data.Part -- this is what I actually import

class HasApp (A B : Type) (C : outParam Type) where
  app : A → B → C

infixl:73 (priority := high) " • " => HasApp.app

macro_rules | `($x • $y) => `(HasApp.app $x $y)

variable (A : Type) [HasApp A A A]
variable (a b c : A)

#check ((a • b) • c) -- works
#check (a • b • c) -- HSMul still kicks in,  why?

[Kevin Buzzard]

Why not use one of the 37 other dots which unicode has to offer?

[Shreyas Srinivas]

My initial thought was that macro was redundant and using it produced a right infix operator. But this issue persists even after removing it

[Shreyas Srinivas]

The macro is still redundant

[Andrej Bauer]

The macro feels redundant, it's just an attempt.
@Kevin Buzzard : I think I will in fact use one of the other dotst, but I'd like to understand why the code isn't working (I am currently wearing mu computer science hat).

[Shreyas Srinivas]

Yeah I am also curious to find out what's happening

[Sebastian Ullrich]

When parsing the term beginning at a, the infixr notation allows us to parse all of a • b • c while the infixl notation stops after b with the remainder left to be parsed by any "trailing" parsers, as in Pratt's algorithm. At this point, the Lean parser commits to the first interpretation as per the "local longest parse" rule briefly mentioned at https://lean-lang.org/lean4/doc/notation.html.

This right-leaning bias inherited by Pratt parsing is of course an implementation detail that ideally would not be exposed to users. The current local longest parse rule has been designed before we added a packrat-like parser cache, we might revise it in the future.