notations are not printed correctly

[JasonGross]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

class ArrSort (α : Sort u1) (cell_level : Nat) where
  Arr : α → α → Sort u2
class Arr (α : Sort u1) (γ : Sort u2) (cell_level : Nat) where
  Arr : α → α → γ
infix:70 " ~> " => Arr.Arr (cell_level := 1)
infix:70 " ≈> " => Arr.Arr (cell_level := 2)
@[defaultInstance, reducible, inline]
instance ArrOfArrSort {α : Sort _} {cell_level} [ArrSort α cell_level] : Arr α (Sort _) cell_level := { Arr := ArrSort.Arr cell_leve\
l }
namespace Preorder
  structure Preorder where
    Obj : Type u0
    Arr : Obj → Obj → Type u1
  def Unit : Preorder.{u0,u1} := { Obj := ULift _root_.Unit , Arr := λ _ _ => ULift _root_.Unit }
  instance OfNat1 : OfNat Preorder.Preorder (nat_lit 1) := { ofNat := Unit }
  structure Fun (A B : Preorder.{u0,u1}) where
  @[inline, reducible] scoped instance as_1cell.has_arr : ArrSort Preorder 2 := { Arr := Fun }
  structure Fun2 {A B : Preorder.{u0,u1}} (f g : Fun A B) where
  @[inline, reducible] scoped instance as_1cell.has_arr2 {A B : Preorder.{u0,u1}} : _root_.ArrSort (Fun A B) 3 := { Arr := Fun2 }
end Preorder
namespace Procat
structure Procat where
  Obj : Type u0
  Arr : Obj → Obj → Preorder.Preorder.{u1,u2}
@[inline, reducible] scoped instance internal.has_arr {C : Procat} : Arr C.Obj Preorder.Preorder 1 := { Arr := C.Arr }
namespace internal
open Preorder.as_1cell
scoped infix :70 (priority:=high) " ~> " => _root_.Arr.Arr (self:=has_arr)
def compose (C : Procat) {a b c : C.Obj} (f : 1 ≈> (a ~> b)) (g : 1 ≈> (b ~> c)) : 1 ≈> (a ~> c)
  := by { done }
/-
Messages (1)
29:10:
unsolved goals
C : Procat
a b c : C.Obj
f : Arr.Arr 2 1 (Arr.Arr 1 a b)
g : Arr.Arr 2 1 (Arr.Arr 1 b c)
⊢ Arr.Arr 2 1 (Arr.Arr 1 a c)
-/

Why is it that the parsing works fine, but the notations are not reprinted?

Versions

$ lean --version

Lean (version 4.0.0-nightly-2021-03-19, commit 1af02dc, Release)

$ uname -a
Linux JasonGross-X1 4.19.128-microsoft-standard #1 SMP Tue Jun 23 12:58:10 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 20.04.2 LTS
Release:        20.04
Codename:       focal
$ cmd.exe /C ver
'\\wsl$\Ubuntu\home\jgross\Documents\GitHub\lean-tools'
CMD.EXE was started with the above path as the current directory.
UNC paths are not supported.  Defaulting to Windows directory.

Microsoft Windows [Version 10.0.19041.804]

[Kha]

This is the current heuristic for deriving a pretty printer from a notation:

lean4/src/Lean/Elab/Syntax.lean

Lines 443 to 445 in 19b24e3

	/-- Try to derive a `SimpleDelab` from a notation.
	The notation must be of the form `notation ... => c var_1 ... var_n`
	where `c` is a declaration in the current scope and the `var_i` are a permutation of the LHS vars. -/

It does not yet handle constant arguments like (cell_level := 1)

[leodemoura]

@Kha Will this ever be fixed? The appUnexpander works at the Syntax level. To make this kind of example work it seems we would need to do it at the "delaborator" level.
I think what is missing is a "warning" message telling the user that pretty-print support was not generated for the given notation declaration. Users could avoid the "warning" by using a new (parser_only := true) parameter at notation.

[Kha]

@leodemoura In theory, notation could synthesize delabs for common cases (where no notation parameter is used as a binder) such as this one. The warning still sounds good though. I would suggest simple (print := false)/(parse := false) parameters, with the latter being useful in cases such as https://github.com/larsk21/iris-lean/blob/master/src/Iris/Proofmode/Display.lean.