From a6c53cf9748341663542307aa47ea8a59084cdae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 28 Jul 2022 15:13:10 -0700
Subject: [PATCH] fix: fixes #1380

---
 src/Lean/Elab/BuiltinTerm.lean    |  5 +++--
 src/Lean/Elab/SyntheticMVars.lean | 14 ++++++++++++++
 tests/lean/run/1380.lean          |  9 +++++++++
 3 files changed, 26 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/1380.lean

diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 229faee57e..71c396afb5 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -150,10 +150,11 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 
 /-- `by tac` constructs a term of the expected type by running the tactic(s) `tac`. -/
 @[builtinTermElab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
-  tryPostponeIfNoneOrMVar expectedType?
   match expectedType? with
   | some expectedType => mkTacticMVar expectedType stx
-  | none => throwError ("invalid 'by' tactic, expected type has not been provided")
+  | none =>
+    tryPostpone
+    throwError ("invalid 'by' tactic, expected type has not been provided")
 
 @[builtinTermElab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index e3f363cc2f..e39661db26 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -329,6 +329,20 @@ mutual
     /- Recall, `tacticCode` is the whole `by ...` expression. -/
     let code := tacticCode[1]
     instantiateMVarDeclMVars mvarId
+    /-
+    TODO: consider using `runPendingTacticsAt` at `mvarId` local context and target type.
+    Issue #1380 demonstrates that the goal may still contain pending metavariables.
+    It happens in the following scenario we have a term `foo A (by tac)` where `A` has been postponed
+    and contains nested `by ...` terms. The pending metavar list contains two metavariables: ?m1 (for `A`) and
+    `?m2` (for `by tac`). When `A` is resumed, it creates a new metavariable `?m3` for the nested `by ...` term in `A`.
+    `?m3` is after `?m2` in the to-do list. Then, we execute `by tac` for synthesizing `?m2`, but its type depends on
+    `?m3`. We have considered putting `?m3` at `?m2` place in the to-do list, but this is not super robust.
+    The ideal solution is to make sure a tactic "resolves" all pending metavariables nested in their local contex and target type
+    before starting tactic execution. The procedure would be a generalization of `runPendingTacticsAt`. We can try to combine
+    it with `instantiateMVarDeclMVars` to make sure we do not perform two traversals.
+    Regarding issue #1380, we addressed the issue by avoiding the elaboration postponement step. However, the same issue can happen
+    in more complicated scenarios.
+    -/
     try
       let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
          withTacticInfoContext tacticCode (evalTactic code)
diff --git a/tests/lean/run/1380.lean b/tests/lean/run/1380.lean
new file mode 100644
index 0000000000..d5816d8a6c
--- /dev/null
+++ b/tests/lean/run/1380.lean
@@ -0,0 +1,9 @@
+theorem Nat.ne_of_gt {a b : Nat} (h : a < b) : b ≠ a := sorry
+theorem Nat.lt_succ_iff {m n : Nat} : m < succ n ↔ m ≤ n := sorry
+
+variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1)
+theorem foo (_: ¬ Fin.mk v₂ hv₂ = Fin.mk v₁ hv₁ ): True := trivial
+set_option trace.Meta.Tactic.simp true in
+example (hv: v₁ < v₂) : True := foo n v₁ v₂ ‹_› ‹_› (by simp only[hv, Fin.mk.injEq, Nat.ne_of_gt, Nat.lt_succ_iff])
+
+#check Fin.mk.injEq