notation doesn't work with implicit arguments

Stream: lean4

[Junyan Xu]

Is it possible to specify an implicit argument in a notation without preventing the notation from being displayed? In the following snippet, the notations fin2 and fin3 parse correctly but doesn't display as intended.

notation "fin1" => Fin 1
notation "fin2" => @Fin 2
notation "fin3" => Fin (n := 3)

example : fin1 = fin2 ∧ fin2 = fin3 := by
  /- unsolved goals
⊢ fin1 = Fin 2 ∧ Fin 2 = Fin 3 -/

In this case n is actually explicit in Fin n so we can just use fin1, but when we have a def with an implicit argument to start with, for example docs#Polynomial.X, I have to make an abbrev Polynomial.X' (R) [Semiring R] := Polynomial.X (R := R) and do notation "Y" => Polynomial.X' (Polynomial _) etc. (to distinguish the two variables in R[X][X]).

When diagnosing this problem I discovered this example that may offer some hints:

notation "idN" => id Nat

#check idN -- idN : Type

notation "ℕ" => Nat

#check idN -- id ℕ : Type

notation "idN1" => id ℕ

#check idN1   -- idN1 : Type
#check idN    -- idN1 : Type
#check id Nat -- idN1 : Type
#check id ℕ   -- idN1 : Type

In short, if Nat is given a notation, then a notation involving something applied to Nat will not display, and you have to use Nat's notation to define subsequent notations involving Nat. In the second #check idN, it seems that the pretty printer does one step (replace Nat by ℕ) and then stops. I wonder whether what's happening with the notations with implicit argument is also that the pretty printer sees @Fin 2 or Fin (n := 3), replaces it with Fin 2 or Fin 3 and then stops, without going further to replace them by fin2 or fin3.

It has to be something applied to Nat instead of Nat alone though: if you just give Nat a new notation it will just work:

notation "N" => Nat
#check N -- N : Type

notation "N1" => Nat
#check N1 -- N1 : Type
#check N  -- N1 : Type

I appreciate your input and diagnosis on this issue.

[Junyan Xu]

(deleted)

[Kyle Miller]

The pretty printer generator for notation is fairly simple. Your first example is completely explained by the following observation:

notation "fin1" => Fin 1 -- generates a pretty printer
notation "fin2" => @Fin 2 -- does not generate a pretty printer
notation "fin3" => Fin (n := 3) -- does not generate a pretty printer

I have been planning on adding a warning message to notation when it does not succeed in generating a pretty printer, along with an option to acknowledge the warning. For example, it might look like notation (prettyPrinter := false) "fin2" => @Fin 2 to turn off the warning.

[Kyle Miller]

For the Nat examples, the sorts of pretty printers that notation generates (app unexpanders) are evaluated "inside-out". That is, leaves-first root-last. Also, the last app unexpander to be defined is the one that takes precedence. This explains why idN1 applies in each case, if you add in the fact that app unexpanders operate by matching syntax, hence why it works only because ℕ is in the RHS pattern.

[Kyle Miller]

If you are using mathlib, you can use notation3, which creates delaborators instead of app unexpanders. The delaborators it generates additionally operate "outside-in".

[Kyle Miller]

There are some thoughts about making notation generate delaborators as well

[Junyan Xu]

Thanks! notation3 seems to work with my intended application to Polynomial. I recall the notation Y also had issues back in mathlib3, but maybe notation3 fixed those :)

[Kyle Miller]

Let me know what you find!

[Junyan Xu]

The only place I find the notation3 doesn't work perfectly is:

import Mathlib.Algebra.Polynomial.Basic
notation3 "Y" => Polynomial.X (R := Polynomial _)
open Polynomial
variable (R : Type*) [Ring R]
noncomputable section
example : R[X][X] := -Y -- failed to synthesize instance Neg ?m.2233[X][X]
example : R[X][X] := Y -- works
example : R[X][X] := Y + C X -- works
example : R[X][X] := -(Y : R[X][X]) -- works
example : R[X][X] := -X -- works