From b44b3aeffb85483bf20b2f44d8f412847363f283 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 Sep 2020 09:21:22 -0700
Subject: [PATCH] fix: error position for unsolved goals

---
 src/Lean/Elab/SyntheticMVars.lean | 33 ++++++++++++++++++++++++-------
 src/Lean/Elab/Tactic/Basic.lean   |  4 +---
 src/Lean/Elab/Term.lean           |  4 ++--
 3 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 3310842bbc..3839c6a30a 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -26,14 +26,33 @@ def ensureAssignmentHasNoMVars (mvarId : MVarId) : TermElabM Unit := do
 val ← instantiateMVars (mkMVar mvarId);
 when val.hasExprMVar $ throwError ("tactic failed, result still contain metavariables" ++ indentExpr val)
 
-def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
-modifyThe Meta.State $ fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId };
-remainingGoals ← liftTacticElabM mvarId $ do { evalTactic tacticCode; getUnsolvedGoals };
+private partial def getTacticRCurly? : Syntax → Option Syntax
+| stx =>
+  if stx.isOfKind `Lean.Parser.Term.byTactic then
+    getTacticRCurly? $ stx.getArg 1
+  else if stx.isOfKind `Lean.Parser.Tactic.seq && stx.getArgs.size == 1 then
+    getTacticRCurly? $ stx.getArg 0
+  else if stx.isOfKind `Lean.Parser.Tactic.nestedTacticBlockCurly then
+    some (stx.getArg 2)
+  else
+    none
+
+private def getTacticErrorRef (tacticCode : Syntax) : TermElabM Syntax := do
 ref ← getRef;
-let tailRef := ref.getTailWithPos.getD ref;
-withRef tailRef do
-unless remainingGoals.isEmpty (reportUnsolvedGoals remainingGoals);
-ensureAssignmentHasNoMVars mvarId
+match getTacticRCurly? tacticCode with
+| some rcurly => pure $ replaceRef rcurly ref
+| none        => pure $ replaceRef tacticCode ref
+
+def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
+/- Recall, `tacticCode` is the whole `by ...` expression.
+   We store the `by` because in the future we want to save the initial state information at the `by` position. -/
+let code := tacticCode.getArg 1;
+modifyThe Meta.State $ fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId };
+remainingGoals ← liftTacticElabM mvarId $ do { evalTactic code; getUnsolvedGoals };
+ref ← getTacticErrorRef tacticCode;
+withRef ref do
+  unless remainingGoals.isEmpty (reportUnsolvedGoals remainingGoals);
+  ensureAssignmentHasNoMVars mvarId
 
 /-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
 private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSorry := true) : TermElabM Expr :=
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index e224f28018..86bcce81fd 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -22,9 +22,7 @@ def goalsToMessageData (goals : List MVarId) : MessageData :=
 MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
 
 def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit := do
-ref ← getRef;
-let tailRef := ref.getTailWithPos.getD ref;
-throwErrorAt tailRef $ "unsolved goals" ++ Format.line ++ goalsToMessageData goals
+throwError $ "unsolved goals" ++ Format.line ++ goalsToMessageData goals
 
 namespace Tactic
 
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 5708cce7d0..b99f055721 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1032,7 +1032,7 @@ fun stx expectedType? => do
   registerMVarErrorContext mvar.mvarId! stx;
   pure mvar
 
-def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
+private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
 mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque `main;
 let mvarId := mvar.mvarId!;
 ref ← getRef;
@@ -1043,7 +1043,7 @@ pure mvar
 @[builtinTermElab byTactic] def elabByTactic : TermElab :=
 fun stx expectedType? =>
   match expectedType? with
-  | some expectedType => mkTacticMVar expectedType (stx.getArg 1)
+  | some expectedType => mkTacticMVar expectedType stx
   | none => throwError ("invalid 'by' tactic, expected type has not been provided")
 
 /-- Main loop for `mkPairs`. -/