update tests, applyConst

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -293,7 +293,7 @@ def evalApplyLikeTactic (tac : MVarId → Expr → MetaM (List MVarId)) (e : Syn
 
 @[builtin_tactic Lean.Parser.Tactic.apply] def evalApply : Tactic := fun stx =>
   match stx with
-  | `(tactic| apply $e) => evalApplyLikeTactic (·.apply) e
+  | `(tactic| apply $e) => evalApplyLikeTactic (·.apply (term? := some m!"`{e}`")) e
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.constructor] def evalConstructor : Tactic := fun _ =>

src/Lean/Meta/Tactic/Apply.lean

@@ -23,11 +23,16 @@ def getExpectedNumArgs (e : Expr) : MetaM Nat := do
   let (numArgs, _) ← getExpectedNumArgsAux e
   pure numArgs
 
-private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α := do
-  let explanation := MessageData.ofLazyM (es := #[eType, targetType]) do
-    let (eType, targetType) ← addPPExplicitToExposeDiff eType targetType
-    return m!"{indentExpr eType}\nwith{indentExpr targetType}"
-  throwTacticEx `apply mvarId m!"failed to unify{explanation}"
+private def throwApplyError {α} (mvarId : MVarId)
+    (eType : Expr) (conclusionType? : Option Expr) (targetType : Expr)
+    (term? : Option MessageData) : MetaM α := do
+  throwTacticEx `apply mvarId <| MessageData.ofLazyM (es := #[eType, targetType]) do
+    let conclusionType := conclusionType?.getD eType
+    let note := if conclusionType?.isSome then .note m!"The full type of {term?.getD "the term"} is{indentExpr eType}" else m!""
+    let (conclusionType, targetType) ← addPPExplicitToExposeDiff conclusionType targetType
+    let conclusion := if conclusionType?.isNone then "type" else "conclusion"
+    return m!"could not unify the {conclusion} of {term?.getD "the term"}{indentExpr conclusionType}\n\
+      with the goal{indentExpr targetType}{note}"
 
 def synthAppInstances (tacticName : Name) (mvarId : MVarId) (mvarsNew : Array Expr) (binderInfos : Array BinderInfo)
     (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit := do
@@ -159,7 +164,8 @@ private def isDefEqApply (cfg : ApplyConfig) (a b : Expr) : MetaM Bool := do
 /--
 Close the given goal using `apply e`.
 -/
-def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
+def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {})
+    (term? : Option MessageData := none) : MetaM (List MVarId) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `apply
     let targetType ← mvarId.getType
@@ -201,8 +207,13 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
           s.restore
           go (i+1)
       else
-        let (_, _, eType) ← forallMetaTelescopeReducing eType (some rangeNumArgs.start)
-        throwApplyError mvarId eType targetType
+
+        let conclusionType? ← if rangeNumArgs.start = 0 then
+          pure none
+        else
+          let (_, _, r) ← forallMetaTelescopeReducing eType (some rangeNumArgs.start)
+          pure (some r)
+        throwApplyError mvarId eType conclusionType? targetType term?
       termination_by rangeNumArgs.stop - i
     let (newMVars, binderInfos) ← go rangeNumArgs.start
     postprocessAppMVars `apply mvarId newMVars binderInfos cfg.synthAssignedInstances cfg.allowSynthFailures
@@ -218,7 +229,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
 
 /-- Short-hand for applying a constant to the goal. -/
 def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
-  mvar.apply (← mkConstWithFreshMVarLevels c) cfg
+  mvar.apply (← mkConstWithFreshMVarLevels c) cfg (term? := m!"'{.ofConstName c}'")
 
 end Meta
 

src/Lean/Meta/Tactic/Rfl.lean

@@ -90,7 +90,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
     let mut ex? := none
     for lem in ← (reflExt.getState (← getEnv)).getMatch rel do
       try
-        let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
+        let gs ← goal.apply (← mkConstWithFreshMVarLevels lem) (term? := m!"'{.ofConstName lem}'")
         if gs.isEmpty then return () else
           throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
             goalsToMessageData gs}"

tests/lean/issue3232.lean.expected.out

@@ -1,16 +1,16 @@
-issue3232.lean:5:2-5:9: error: tactic 'apply' failed, failed to unify
+issue3232.lean:5:2-5:9: error: tactic 'apply' failed, could not unify the type of `h`
   @foo 42
-with
+with the goal
   @foo 23
 h : foo
 ⊢ foo
-issue3232.lean:8:2-8:29: error: tactic 'apply' failed, failed to unify
+issue3232.lean:8:2-8:29: error: tactic 'apply' failed, could not unify the type of `rfl`
   (1 : Int) = 1
-with
+with the goal
   (1 : Nat) = 1
 ⊢ 1 = 1
-issue3232.lean:11:2-11:25: error: tactic 'apply' failed, failed to unify
+issue3232.lean:11:2-11:25: error: tactic 'apply' failed, could not unify the type of `Eq.refl PUnit`
   PUnit = PUnit
-with
+with the goal
   PUnit = PUnit
 ⊢ PUnit = PUnit

tests/lean/run/1870.lean

@@ -14,10 +14,13 @@ theorem ex1 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNa
   rfl
 
 /--
-error: tactic 'apply' failed, failed to unify
+error: tactic 'apply' failed, could not unify the conclusion of `@congrArg`
   ?_ ?_ = ?_ ?_
-with
+with the goal
   OfNat.ofNat 0 = OfNat.ofNat 1
+
+Note: The full type of `@congrArg` is
+  ∀ {α : Sort _} {β : Sort _} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
 ⊢ OfNat.ofNat 0 = OfNat.ofNat 1
 -/
 #guard_msgs in
@@ -27,10 +30,13 @@ example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 :
   apply rfl
 
 /--
-error: tactic 'apply' failed, failed to unify
+error: tactic 'apply' failed, could not unify the conclusion of `@congrArg`
   ?_ ?_ = ?_ ?_
-with
+with the goal
   OfNat.ofNat 0 = OfNat.ofNat 1
+
+Note: The full type of `@congrArg` is
+  ∀ {α : Sort _} {β : Sort _} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
 ⊢ OfNat.ofNat 0 = OfNat.ofNat 1
 -/
 #guard_msgs in

tests/lean/run/apply_error.lean

@@ -0,0 +1,53 @@
+/--
+error: tactic 'apply' failed, could not unify the conclusion of `h`
+  True
+with the goal
+  False
+
+Note: The full type of `h` is
+  1 = 1 → True
+h : 1 = 1 → True
+⊢ False
+-/
+#guard_msgs in
+example (h : 1 = 1 → True) : False := by
+  apply h
+
+/--
+error: tactic 'apply' failed, could not unify the type of `h`
+  1 = 1 → True
+with the goal
+  2 = 2 → False
+h : 1 = 1 → True
+⊢ 2 = 2 → False
+-/
+#guard_msgs in
+example (h : 1 = 1 → True) : 2 = 2 → False := by
+  apply h
+
+/--
+error: tactic 'apply' failed, could not unify the conclusion of `h`
+  1 = 1 → True
+with the goal
+  2 = 2 → False
+
+Note: The full type of `h` is
+  3 = 3 → 1 = 1 → True
+h : 3 = 3 → 1 = 1 → True
+⊢ 2 = 2 → False
+-/
+#guard_msgs in
+example (h : 3 = 3 → 1 = 1 → True) : 2 = 2 → False := by
+  apply h
+
+/--
+error: tactic 'apply' failed, could not unify the type of `h`
+  True
+with the goal
+  False
+h : True
+⊢ False
+-/
+#guard_msgs in
+example (h : True) : False := by
+  apply h

tests/lean/run/rflTacticErrors.lean

@@ -197,10 +197,13 @@ is not definitionally equal to the right-hand side
 #guard_msgs in
 example : true'' = true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply' failed, failed to unify
+error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl'
   @HEq ?α ?a ?α ?a
-with
+with the goal
   @HEq Bool true'' Bool true
+
+Note: The full type of 'HEq.refl' is
+  ∀ {α : Sort ?u.601} (a : α), HEq a a
 ⊢ HEq true'' true
 -/
 #guard_msgs in
@@ -262,10 +265,13 @@ is not definitionally equal to the right-hand side
 #guard_msgs in
 example : false = true   := by apply_rfl -- Error
 /--
-error: tactic 'apply' failed, failed to unify
+error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl'
   HEq ?a ?a
-with
+with the goal
   HEq false true
+
+Note: The full type of 'HEq.refl' is
+  ∀ {α : Sort ?u.653} (a : α), HEq a a
 ⊢ HEq false true
 -/
 #guard_msgs in
@@ -326,10 +332,13 @@ is not definitionally equal to the right-hand side
 #guard_msgs in
 example : false = true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'apply' failed, failed to unify
+error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl'
   HEq ?a ?a
-with
+with the goal
   HEq false true
+
+Note: The full type of 'HEq.refl' is
+  ∀ {α : Sort ?u.705} (a : α), HEq a a
 ⊢ HEq false true
 -/
 #guard_msgs in
@@ -383,19 +392,25 @@ example : R false true   := by with_reducible apply_rfl -- Error
 -- Inheterogeneous unequal
 
 /--
-error: tactic 'apply' failed, failed to unify
+error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl'
   HEq ?a ?a
-with
+with the goal
   HEq true 1
+
+Note: The full type of 'HEq.refl' is
+  ∀ {α : Sort ?u.774} (a : α), HEq a a
 ⊢ HEq true 1
 -/
 #guard_msgs in
 example : HEq true 1 := by apply_rfl -- Error
 /--
-error: tactic 'apply' failed, failed to unify
+error: tactic 'apply' failed, could not unify the conclusion of 'HEq.refl'
   HEq ?a ?a
-with
+with the goal
   HEq true 1
+
+Note: The full type of 'HEq.refl' is
+  ∀ {α : Sort ?u.815} (a : α), HEq a a
 ⊢ HEq true 1
 -/
 #guard_msgs in