Pretty printer fails to handle weakly inserted implicit argument

[shingtaklam1324]

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.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

open tactic

meta def st : tactic unit :=
do
  g :: _ ← get_goals,
  e ← to_expr ```(hst ha),
  tactic.exact e,
  trace e

example (α : Type) (S T : set α) (a : α) (ha : a ∈ S) (hst : S ⊆ T) : a ∈ T :=
begin
  st
end

Expected behavior: [What you expect to happen]

Output message should be hst ha

Actual behavior: [What actually happens]

Outputs hst a ha

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Occurs on every version I have installed. (From 3.4.2 to 3.17.1)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

This is most likely the issue causing leanprover-community/mathlib#3093

[shingtaklam1324]

Here's another example. The trace outputs are different, despite e not changing (right?). If the tactic.exact e line is commented out, then the two traces both output hst ha as expected.

open tactic

meta def st : tactic unit :=
do
  e ← to_expr ```(hst ha),
  trace e,        -- hst ha
  tactic.exact e,
  trace e         -- hst a ha

example (α : Type) (S T : set α) (a : α) (ha : a ∈ S) (hst : S ⊆ T) : a ∈ T :=
begin
  st
end

[kmill]

Some self-contained examples:

open tactic lean lean.parser interactive interactive.types

meta def tactic.interactive.trace_exact (q : parse texpr) : tactic unit := do
  tgt : expr ← target,
  e ← i_to_expr_strict ``(%%q : %%tgt),
  tactic.exact e,
  tactic.trace e

variables {α : Type*}

example (S T : set α) (hst : ∀ ⦃x⦄, x ∈ S → x ∈ T) (y : α) (h : y ∈ S) : y ∈ T :=
by trace_exact hst h
-- hst y h

example (S T : set α) (hst : ∀ {x}, x ∈ S → x ∈ T) (y : α) (h : y ∈ S) : y ∈ T :=
by trace_exact hst h
-- hst y h