Prettyprinter prints fun x x => ...

Stream: lean4

[Michael Stoll]

The following seems to be a bug in the prettyprinter.

example : (fun (_ _ : Nat) ↦ 0) = fun _ _ ↦ 0 := by
  -- goal prints as `(fun x x => 0) = fun x x => 0`
  rfl

(It is the same when one of the _'s is replaced by x.) I would expect it to print fun x x_1 => 0 instead.

[Kim Morrison]

You could open a bug report, I think.

[Kyle Miller]

This one I believe is not a bug, even if it's odd. There's a feature called 'safe shadowing' when the pretty printer comes up with binder names, where it allows shadowing a variable if that variable is not used in the body of the function.

If somehow there are examples where this is confusing, it would be worth collecting them.

Here are some examples:

#check fun x x => 0           -- fun x x ↦ 0
#check fun x x => x           -- fun x x ↦ x
#check fun x x => clear% x; x -- fun x x_1 ↦ x

The second one I would agree is a bit suspect.

The rule makes a lot more sense with let expressions, since shadowing variables is how you simulate mutation in a functional language:

#check let x := 1; let x := 2; 0
/-
let x := 1;
let x := 2;
0 : ℕ
-/
#check let x := 1; let x := 2; x
/-
let x := 1;
let x := 2;
x : ℕ
-/
#check let x := 1; let x := 2; clear% x; x
/-
let x := 1;
let x_1 := 2;
x : ℕ
-/

[Michael Stoll]

Kyle Miller said:

The second one I would agree is a bit suspect.

fun x x ↦ x is definitely hard to parse; one has to be aware of the semantics of shadowing variables and think for a couple of seconds to figure out which x is meant in the function value. I agree that with let bindings, this is not really a problem as people are probably used to thinking sequentially in that context.

I don't have a good solution other than perhaps special-casing this kind of situation in the prettyprinter (i.e., don't repeat variable names in the argument list of a signle fun or something along these lines).