chore: change chatty test to interactive test (#8348)

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -1,85 +0,0 @@
-[Elab.info] 
-  • command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
-    • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨6, 0⟩-⟨6, 26⟩
-    • option trace.Elab.info @ ⟨6, 11⟩-⟨6, 26⟩
-1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
-context:
-α✝ β : Type
-x : Fam2 α✝ β
-α : Type
-a : α
-⊢ α
-[Elab.info] 
-  • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
-    • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
-      • [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
-      • α : Type @ ⟨7, 13⟩-⟨7, 14⟩
-    • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-    • Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
-      • [.] Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
-      • Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
-      • α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
-        • [.] α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
-        • α : Type @ ⟨7, 26⟩-⟨7, 27⟩
-      • β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
-        • [.] β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
-        • β : Type @ ⟨7, 28⟩-⟨7, 29⟩
-    • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-    • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
-      • [.] β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
-      • β : Type @ ⟨7, 33⟩-⟨7, 34⟩
-    • CustomInfo(Lean.Elab.InlayHint)
-    • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†!-⟨7, 7⟩†!
-    • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-    • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-    • CustomInfo(Lean.Elab.Term.BodyInfo)
-      • Partial term @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.Quotation.elabMatchSyntax
-      • match α, β, x, a with
-        | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
-        | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
-        • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
-          • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
-          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-        • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
-          • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
-          • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-        • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-        • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-        • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
-        • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
-          • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
-        • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.608 -> _uniq.325
-        • FVarAlias α: _uniq.607 -> _uniq.323
-        • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
-        • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-        • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-        • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
-        • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
-        • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
-        • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
-          • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
-        • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.639 -> _uniq.325
-        • FVarAlias n: _uniq.638 -> _uniq.323
-        • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
-          • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
-          • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
-    • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
-[Elab.info] 
-  • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi

tests/lean/interactive/1018unknowMVarIssue.lean

@@ -1,10 +1,14 @@
+/-!
+The expected type used to show "unknown metavariable '?_uniq.31828'" because of missing
+backtracking of the info tree.
+-/
+
 inductive Fam2 : Type → Type → Type 1 where
   | any : Fam2 α α
   | nat : Nat → Fam2 Nat Nat
 
-set_option pp.rawOnError true
-set_option trace.Elab.info true
 example (a : α) (x : Fam2 α β) : β :=
   match x with
   | Fam2.any   => _
+                --^ $/lean/plainTermGoal
   | Fam2.nat n => n

tests/lean/interactive/1018unknowMVarIssue.lean.expected.out

@@ -0,0 +1,5 @@
+{"textDocument": {"uri": "file:///1018unknowMVarIssue.lean"},
+ "position": {"line": 11, "character": 18}}
+{"range":
+ {"start": {"line": 11, "character": 18}, "end": {"line": 11, "character": 19}},
+ "goal": "α✝ β : Type\nx : Fam2 α✝ β\nα : Type\na : α\n⊢ α"}