`appUnexpander`s referring to local variables

[thejohncrafter]

Prerequisites

• [x] 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

Custom notations that refer to local variables aren't correctly delaborated.

This appears to be related to how appUnexpanders behave : up to my understanding, appUnexpanders only accept function that have a global name.

Also described here.

Related to #435 and #358

Steps to Reproduce

set_option quotPrecheck.allowSectionVars true

variable (O : Type) (rel : O → O → Prop)
infixl:50 " ◃ " => rel

theorem foo : ∀ x y : O, x ◃ y :=
by /- Goal is `∀ (x y : O), rel x y` -/ admit

More precisely :

set_option quotPrecheck.allowSectionVars true

variable (O : Type) (rel : O → O → Prop)
infixl:50 " ◃ " => rel

@[appUnexpander rel] def unexpandRel : Lean.PrettyPrinter.Unexpander
  | `(rel $x $y) => `($x ◃ $y)
  | _ => throw ()

theorem foo : ∀ x y : O, rel x y :=
by /- Goal is `∀ (x y : O), rel x y` -/ admit

Expected behavior: The goal should be ∀ (x y : O), x ◃ y (and the relation should also be correctly pretty printed by #print).

Actual behavior: It is ∀ (x y : O), rel x y (#print's result is wrong too).

Versions

Lean (version 4.0.0-nightly-2021-05-13, commit 0eaa36b38d28, Release) Ubuntu 20.04.2 LTS

Additional Information

There is a workaround :

set_option quotPrecheck.allowSectionVars true

variable (O : Type) (rel : O → O → Prop)
infixl:50 " ◃ " => id rel
@[appUnexpander id] def unexpandAppRel : Lean.PrettyPrinter.Unexpander
  | `(id rel $x $y) => `($x ◃ $y)
  | _ => throw ()

theorem foo : ∀ x y : O, x ◃ y :=
by /- Goal is now `∀ (x y : O), x ◃ y` ! -/ admit

This satisfies appUnexpander's requirement that app have a global name, but it would be best to be able to just refer to a local variable.

Possible extension

It might be interesting to have appUnexpander accept more complex right hand sides : in the current state, and up to my knowledge, it only accepts functions (syntactically, i.e. function applications don't count there, even if they type as function).

For instance, someone might write :

infixl:50 " ◃ " => Group.mul G

which wouldn't be supported at the current state of appUnexpander's implementation