notations are not printed correctly

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 1af02dcaca3c, 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]

Start with the self-contained Lean reproducer in the issue and compare how its custom notations are parsed with how the resulting expressions are printed. Investigate the notation parsing and pretty-printing paths; done means the displayed goals reprint the relevant notations instead of the expanded Arr.Arr forms.