show_term and by? change order of elaboration

[kmill]

Description

Using by? in place of by can lead to elaboration errors since show_term uses synthesizeSyntheticMVarsNoPostponing, so the by doesn't a complete expected type.

Context

This issue is motivated by a Lean Zulip message where a user wanted to see what term a by produced.

Steps to Reproduce

Consider the following code, which elaborates with no errors.

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)

def Vect.cast {m n : Nat} (h : m = n) (v : Vect α m) : Vect α n :=
  h ▸ v

def Vect.revHelper (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match xs with
  | .nil => acc
  | .cons y ys =>
    (revHelper ys (.cons y acc)).cast (by rw [Nat.succ_add]; rfl)

Expected behavior: Replacing by with by? should still elaborate.

Actual behavior: Replacing by with by? leads to an error:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?n.succ + ?m
a : Type ?u.713
n m : Nat
xs : Vect a n
acc : Vect a m
n✝ : Nat
y : a
ys : Vect a n✝
⊢ ?m.965 = m + (n✝ + 1)

Versions

4.12.0, commit 225e089 macOS m2

Additional Information

It seems like the TryThis infrastructure needs a hook into the elaborator that can defer processing until all elaboration problems are done, where it can then receive the completed mvar context. In an experiment, hacking it in using .postpone metavariables failed since these can be prematurely forced, even if the entries in the pendingMVars list was after all other mvars.

Maybe there could be a list of "post-elab actions" that are run at the end of synthesizeSyntheticMVarsNoPostponing.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kmill]

This is a duplicate of #5625