Bug with rcases combined with substitution

Stream: std4

[Grant Barkley]

It looks like there's a bug when using rcases with substitution, see the following execution. The metavariable (should be) assigned but isn't shown in the pretty printer until later on.

def box : Nat := 1

theorem box_def : box = 1 := rfl

example : 1 = 1 := by
  rcases box_def ▸ box_def with a
  -- a : ?m ⊢ 1 = 1
  show _ -- seems like putting most tactics here also causes the display to fix itself
  -- a : 1 = 1 ⊢ 1 = 1
  exact a

[Grant Barkley]

May be a missing instantiateMVars

[Kyle Miller]

I find this pretty printing behavior to be weird on its own (and note that skip in place of show _ keeps the type as ?m).

Some more examples more localized to rcases:

example : 1 = 1 := by
  rcases box_def ▸ box_def with ⟨⟩
  -- rcases tactic failed: x✝ : ?m.4286 is not an inductive datatype

example : 1 = 1 := by
  rcases (box_def ▸ box_def : 1 = 1) with ⟨⟩
  -- ok
  rfl

[Kyle Miller]

rcases has a whnfD, so it should be instantiating the metavariables it needs to to keep that first error from happening. That makes me wonder if rcases is missing a synthesizeSyntheticMVars?

[Kyle Miller]

Yeah, this suggests it has to do with the fact that \triangle postpones:

open Lean Elab Tactic in
elab "synthMVars " : tactic => withMainContext do
  -- Term.synthesizeSyntheticMVars isn't enough
  Term.synthesizeSyntheticMVarsNoPostponing

example : 1 = 1 := by
  rcases box_def ▸ box_def with a
  -- a : ?m
  synthMVars
  -- a : 1 = 1