Pretty printer fails to handle weakly inserted implicit argument

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.
    • 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

Start with the self-contained Lean reproduction in the issue and inspect the pretty-printer path exercised by trace e after tactic.exact. Compare the output for the weakly inserted implicit argument with the expected hst ha; done means the example prints hst ha rather than hst a ha.