feat: non-unfoldable defs note on apply

Author: Kha

src/Lean/Meta/Check.lean

@@ -194,6 +194,24 @@ def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
     throwError "invalid {declKind} declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}"
   | _ => unreachable!
 
+/-- Adds note about definitions not unfolded because of the module system, if any. -/
+def mkUnfoldAxiomsNote (givenType expectedType : Expr) : MetaM MessageData := do
+  let env ← getEnv
+  if env.header.isModule then
+    let origDiag := (← get).diag
+    try
+      let _ ← observing <| withOptions (diagnostics.set · true)  <| isDefEq givenType expectedType
+      let blocked := (← get).diag.unfoldAxiomCounter.toList.filterMap fun (n, count) => do
+        let count := count - origDiag.unfoldAxiomCounter.findD n 0
+        guard <| count > 0 && getOriginalConstKind? env n matches some .defn
+        return m!"{.ofConstName n} ↦ {count}"
+      if !blocked.isEmpty then
+        return MessageData.note m!"The following definitions were not unfolded because \
+          their definition is not exposed:{indentD <| .joinSep blocked Format.line}"
+    finally
+      modify ({ · with diag := origDiag })
+  return .nil
+
 /--
 Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
 Adds the type’s types unless they are defeq.
@@ -226,19 +244,7 @@ def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr)
       let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
       let trailing := trailing?.map (m!"\n" ++ ·) |>.getD .nil
       pure m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}{trailing}")
-    let env ← getEnv
-    if env.header.isModule then
-      let origDiag := (← get).diag
-      let _ ← observing <| withOptions (diagnostics.set · true)  <| isDefEq givenType expectedType
-      let blocked := (← get).diag.unfoldAxiomCounter.toList.filterMap fun (n, count) => do
-        let count := count - origDiag.unfoldAxiomCounter.findD n 0
-        guard <| count > 0 && getOriginalConstKind? env n matches some .defn
-        return m!"{.ofConstName n} ↦ {count}"
-      if !blocked.isEmpty then
-        msg := msg ++ MessageData.note m!"The following definitions were not unfolded because \
-          their definition is not exposed:{indentD <| .joinSep blocked Format.line}"
-      modify ({ · with diag := origDiag })
-    return msg
+    return msg ++ (← mkUnfoldAxiomsNote givenType expectedType)
 
 def throwAppTypeMismatch (f a : Expr) : MetaM α := do
   -- Clarify that `a` is "last" only if it may be confused with some preceding argument; otherwise,

src/Lean/Meta/Tactic/Apply.lean

@@ -34,7 +34,7 @@ private def throwApplyError {α} (mvarId : MVarId)
     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}"
+      with the goal{indentExpr targetType}{note}{← mkUnfoldAxiomsNote conclusionType targetType}"
 
 def synthAppInstances (tacticName : Name) (mvarId : MVarId) (mvarsNew : Array Expr) (binderInfos : Array BinderInfo)
     (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit := do

tests/pkg/module/Module/Imported.lean

@@ -27,6 +27,23 @@ Note: The following definitions were not unfolded because their definition is no
 #guard_msgs in
 example : f = 1 := rfl
 
+/--
+error: Tactic `apply` failed: could not unify the conclusion of `@rfl`
+  ?a = ?a
+with the goal
+  f = 1
+
+Note: The full type of `@rfl` is
+  ∀ {α : Sort ?u.115} {a : α}, a = a
+
+Note: The following definitions were not unfolded because their definition is not exposed:
+  f ↦ 1
+
+⊢ f = 1
+-/
+#guard_msgs in
+example : f = 1 := by apply rfl
+
 /-! Theorems should be exported without their bodies -/
 
 /--