feat: apply’s error message should show implicit arguments as needed (#3929)

luckily the necessary functionality already exists in the form of
`addPPExplicitToExposeDiff`. But it is not cheap, and we should not run
this code
when the error message isn’t shown, so we should do this lazily.

We already had `MessageData.ofPPFormat` to assemble the error message
lazily, but it
was restricted to returning `FormatWithInfo`, a data type that doesn’t
admit a nice
API to compose more complex messages (like `Format` or `MessageData`
has; an attempt to
fix that is in #3926).

Therefore we split the functionality of `.ofPPFormat` into
`.ofFormatWithInfo` and `.ofLazy`,
and use `.ofLazy` to compute the more complex error message of `apply`.

Fixes #3232.

---------

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>

RELEASES.md

@@ -155,6 +155,18 @@ fact.def :
 
 * `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed.
 
+* The `MessageData.ofPPFormat` constructor has been removed.
+  Its functionality has been split into two:
+
+  - for lazy structured messages, please use `MessageData.lazy`;
+  - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
+
+  An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
+
+* The `MessageData.ofFormat` constructor has been turned into a function.
+  If you need to inspect `MessageData`,
+  you can pattern-match on `MessageData.ofFormatWithInfos`.
+
 v4.7.0
 ---------
 

src/Lean/CoreM.lean

@@ -332,7 +332,8 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
   We used a similar hack at `Exception.isMaxRecDepth` -/
 def Exception.isMaxHeartbeat (ex : Exception) : Bool :=
   match ex with
-  | Exception.error _ (MessageData.ofFormat (Std.Format.text msg)) => "(deterministic) timeout".isPrefixOf msg
+  | Exception.error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) =>
+    "(deterministic) timeout".isPrefixOf msg
   | _ => false
 
 /-- Creates the expression `d → b` -/

src/Lean/Exception.lean

@@ -130,7 +130,7 @@ been defined yet.
 -/
 def Exception.isMaxRecDepth (ex : Exception) : Bool :=
   match ex with
-  | error _ (MessageData.ofFormat (Std.Format.text msg)) => msg == maxRecDepthErrorMessage
+  | error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) => msg == maxRecDepthErrorMessage
   | _ => false
 
 /--

src/Lean/Message.lean

@@ -39,13 +39,6 @@ structure NamingContext where
   currNamespace : Name
   openDecls : List OpenDecl
 
-/-- Lazily formatted text to be used in `MessageData`. -/
-structure PPFormat where
-  /-- Pretty-prints text using surrounding context, if any. -/
-  pp : Option PPContext → IO FormatWithInfos
-  /-- Searches for synthetic sorries in original input. Used to filter out certain messages. -/
-  hasSyntheticSorry : MetavarContext → Bool := fun _ => false
-
 structure TraceData where
   /-- Trace class, e.g. `Elab.step`. -/
   cls       : Name
@@ -60,10 +53,9 @@ structure TraceData where
 
 /-- Structured message data. We use it for reporting errors, trace messages, etc. -/
 inductive MessageData where
-  /-- Eagerly formatted text. We inspect this in various hacks, so it is not immediately subsumed by `ofPPFormat`. -/
-  | ofFormat          : Format → MessageData
-  /-- Lazily formatted text. -/
-  | ofPPFormat        : PPFormat → MessageData
+  /-- Eagerly formatted text with info annotations.
+  This constructor is inspected in various hacks. -/
+  | ofFormatWithInfos : FormatWithInfos → MessageData
   | ofGoal            : MVarId → MessageData
   /-- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/
   | withContext       : MessageDataContext → MessageData → MessageData
@@ -78,12 +70,45 @@ inductive MessageData where
     Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
   | tagged            : Name → MessageData → MessageData
   | trace (data : TraceData) (msg : MessageData) (children : Array MessageData)
-  deriving Inhabited
+  /-- A lazy message.
+  The provided thunk will not be run until it is about to be displayed.
+  This can save computation in cases where the message may never be seen,
+  e.g. when nested inside a collapsed trace.
+
+  The `Dynamic` value is expected to be a `MessageData`,
+  which is a workaround for the positivity restriction.
+     
+  If the thunked message is produced for a term that contains a synthetic sorry,
+  `hasSyntheticSorry` should return `true`.
+  This is used to filter out certain messages. -/
+  | ofLazy (f : Option PPContext → IO Dynamic) (hasSyntheticSorry : MetavarContext → Bool)
+  deriving Inhabited, TypeName
 
 namespace MessageData
 
+/-- Eagerly formatted text. -/
+def ofFormat (fmt : Format) : MessageData := .ofFormatWithInfos ⟨fmt, .empty⟩
+
+/--
+Lazy message data production, with access to the context as given by
+a surrounding `MessageData.withContext` (which is expected to exist).
+-/
+def lazy (f : PPContext → IO MessageData)
+    (hasSyntheticSorry : MetavarContext → Bool := fun _ => false) : MessageData :=
+  .ofLazy (hasSyntheticSorry := hasSyntheticSorry) fun ctx? => do
+    let msg ← match ctx? with
+      | .none => pure (.ofFormat "(invalid MessageData.lazy, missing context)")
+      | .some ctx => f ctx
+    return Dynamic.mk msg
+
 variable (p : Name → Bool) in
-/-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag` is true. -/
+/-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag`
+is true.
+
+This does not descend into lazily generated subtress (`.ofLazy`); message tags
+of interest (like those added by `logLinter`) are expected to be near the root
+of the `MessageData`, and not hidden inside `.ofLazy`.
+-/
 partial def hasTag : MessageData → Bool
   | withContext _ msg       => hasTag msg
   | withNamingContext _ msg => hasTag msg
@@ -106,26 +131,14 @@ def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext :=
 def ofSyntax (stx : Syntax) : MessageData :=
   -- discard leading/trailing whitespace
   let stx := stx.copyHeadTailInfoFrom .missing
-  .ofPPFormat {
-    pp := fun
-      | some ctx => ppTerm ctx ⟨stx⟩  -- HACK: might not be a term
-      | none     => return stx.formatStx
-  }
+  .lazy fun ctx => ofFormat <$> ppTerm ctx ⟨stx⟩ -- HACK: might not be a term
 
 def ofExpr (e : Expr) : MessageData :=
-  .ofPPFormat {
-    pp := fun
-      | some ctx => ppExprWithInfos ctx e
-      | none     => return format (toString e)
-    hasSyntheticSorry := (instantiateMVarsCore · e |>.1.hasSyntheticSorry)
-  }
+  .lazy (fun ctx => ofFormatWithInfos <$> ppExprWithInfos ctx e)
+        (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry)
 
 def ofLevel (l : Level) : MessageData :=
-  .ofPPFormat {
-    pp := fun
-      | some ctx => ppLevel ctx l
-      | none => return format l
-  }
+  .lazy fun ctx => ofFormat <$> ppLevel ctx l
 
 def ofName (n : Name) : MessageData := ofFormat (format n)
 
@@ -133,7 +146,7 @@ partial def hasSyntheticSorry (msg : MessageData) : Bool :=
   visit none msg
 where
   visit (mctx? : Option MetavarContext) : MessageData → Bool
-  | ofPPFormat f            => f.hasSyntheticSorry (mctx?.getD {})
+  | ofLazy _ f              => f (mctx?.getD {})
   | withContext ctx msg     => visit ctx.mctx msg
   | withNamingContext _ msg => visit mctx? msg
   | nest _ msg              => visit mctx? msg
@@ -144,8 +157,7 @@ where
   | _                       => false
 
 partial def formatAux : NamingContext → Option MessageDataContext → MessageData → IO Format
-  | _,    _,         ofFormat fmt             => return fmt
-  | nCtx, ctx?,      ofPPFormat f             => (·.fmt) <$> f.pp (ctx?.map (mkPPContext nCtx))
+  | _, _,            ofFormatWithInfos fmt    => return fmt.1
   | _,    none,      ofGoal mvarId            => return "goal " ++ format (mkMVar mvarId)
   | nCtx, some ctx,  ofGoal mvarId            => ppGoal (mkPPContext nCtx ctx) mvarId
   | nCtx, _,         withContext ctx d        => formatAux nCtx ctx d
@@ -161,6 +173,11 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
     msg := f!"{msg} {(← formatAux nCtx ctx header).nest 2}"
     let children ← children.mapM (formatAux nCtx ctx)
     return .nest 2 (.joinSep (msg::children.toList) "\n")
+  | nCtx, ctx?,      ofLazy pp _             => do
+    let dyn ← pp (ctx?.map (mkPPContext nCtx))
+    let some msg := dyn.get? MessageData
+      | panic! s!"MessageData.ofLazy: expected MessageData in Dynamic, got {dyn.typeName}"
+    formatAux nCtx ctx? msg
 
 protected def format (msgData : MessageData) : IO Format :=
   formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData

src/Lean/Meta/Tactic/Apply.lean

@@ -8,6 +8,7 @@ import Lean.Util.FindMVar
 import Lean.Meta.SynthInstance
 import Lean.Meta.CollectMVars
 import Lean.Meta.Tactic.Util
+import Lean.PrettyPrinter
 
 namespace Lean.Meta
 /-- Controls which new mvars are turned in to goals by the `apply` tactic.
@@ -50,8 +51,15 @@ def getExpectedNumArgs (e : Expr) : MetaM Nat := do
   let (numArgs, _) ← getExpectedNumArgsAux e
   pure numArgs
 
-private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α :=
-  throwTacticEx `apply mvarId m!"failed to unify{indentExpr eType}\nwith{indentExpr targetType}"
+private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α := do
+  let explanation := MessageData.lazy
+    (f := fun ppctxt => ppctxt.runMetaM do
+        let (eType, targetType) ← addPPExplicitToExposeDiff eType targetType
+        return m!"{indentExpr eType}\nwith{indentExpr targetType}")
+    (hasSyntheticSorry := fun mvarctxt =>
+      (instantiateMVarsCore mvarctxt eType |>.1.hasSyntheticSorry) ||
+      (instantiateMVarsCore mvarctxt targetType |>.1.hasSyntheticSorry))
+  throwTacticEx `apply mvarId m!"failed to unify{explanation}"
 
 def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo)
     (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit :=

src/Lean/PrettyPrinter.lean

@@ -110,16 +110,14 @@ namespace MessageData
 open Lean PrettyPrinter Delaborator
 
 /--
-Turns a `MetaM FormatWithInfos` into a `MessageData` using `.ofPPFormat` and running the monadic value in the given context.
-Uses the `pp.tagAppFns` option to annotate constants with terminfo, which is necessary for seeing the type on mouse hover.
+Turns a `MetaM FormatWithInfos` into a `MessageData.lazy` which will run the monadic value.
+Uses the `pp.tagAppFns` option to annotate constants with terminfo,
+which is necessary for seeing the type on mouse hover.
 -/
-def ofFormatWithInfos
-    (fmt : MetaM FormatWithInfos)
-    (noContext : Unit → Format := fun _ => "<no context, could not generate MessageData>") : MessageData :=
-  .ofPPFormat
-  { pp := fun
-      | some ctx => ctx.runMetaM <| withOptions (pp.tagAppFns.set · true) fmt
-      | none => return noContext () }
+def ofFormatWithInfosM (fmt : MetaM FormatWithInfos) : MessageData :=
+  .lazy fun ctx => ctx.runMetaM <|
+    withOptions (pp.tagAppFns.set · true) <|
+      .ofFormatWithInfos <$> fmt
 
 /-- Pretty print a const expression using `delabConst` and generate terminfo.
 This function avoids inserting `@` if the constant is for a function whose first
@@ -127,13 +125,13 @@ argument is implicit, which is what the default `toMessageData` for `Expr` does.
 Panics if `e` is not a constant. -/
 def ofConst (e : Expr) : MessageData :=
   if e.isConst then
-    .ofFormatWithInfos (PrettyPrinter.ppExprWithInfos (delab := delabConst) e) fun _ => f!"{e}"
+    .ofFormatWithInfosM (PrettyPrinter.ppExprWithInfos (delab := delabConst) e)
   else
     panic! "not a constant"
 
 /-- Generates `MessageData` for a declaration `c` as `c.{<levels>} <params> : <type>`, with terminfo. -/
 def signature (c : Name) : MessageData :=
-  .ofFormatWithInfos (PrettyPrinter.ppSignature c) fun _ => f!"{c}"
+  .ofFormatWithInfosM (PrettyPrinter.ppSignature c)
 
 end MessageData
 

src/Lean/Util/PPExt.lean

@@ -40,6 +40,10 @@ structure PPContext where
   openDecls     : List OpenDecl := []
 
 abbrev PrettyPrinter.InfoPerPos := RBMap Nat Elab.Info compare
+/-- A format tree with `Elab.Info` annotations.
+Each `.tag n _` node is annotated with `infos[n]`.
+This is used to attach semantic data such as expressions
+to pretty-printer outputs. -/
 structure FormatWithInfos where
   fmt : Format
   infos : PrettyPrinter.InfoPerPos

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -128,10 +128,8 @@ where
   }
 
   go (nCtx : NamingContext) : Option MessageDataContext → MessageData → MsgFmtM Format
-  | _,         ofFormat fmt             => withIgnoreTags fmt
-  | none,      ofPPFormat fmt           => (·.fmt) <$> fmt.pp none
-  | some ctx,  ofPPFormat fmt           => do
-    let ⟨fmt, infos⟩ ← fmt.pp (mkPPContext nCtx ctx)
+  | none,      ofFormatWithInfos ⟨fmt, _⟩ => withIgnoreTags fmt
+  | some ctx,  ofFormatWithInfos ⟨fmt, infos⟩ => do
     let t ← pushEmbed <| EmbedFmt.code (mkContextInfo nCtx ctx) infos
     return Format.tag t fmt
   | none,      ofGoal mvarId            => pure $ "goal " ++ format (mkMVar mvarId)
@@ -162,6 +160,11 @@ where
         pure (.strict (← children.mapM (go nCtx ctx)))
     let e := .trace data.cls header data.collapsed nodes
     return .tag (← pushEmbed e) ".\n"
+  | ctx?,     ofLazy f _          => do
+    let dyn ← f (ctx?.map (mkPPContext nCtx))
+    let some msg := dyn.get? MessageData
+      | throw <| IO.userError "MessageData.ofLazy: expected MessageData in Dynamic"
+    go nCtx ctx? msg
 
   /-- Recursively moves child nodes after the first `blockSize` into a new "more" node. -/
   chopUpChildren (cls : Name) (blockSize : Nat) (children : Subarray MessageData) :

tests/lean/issue3232.lean

@@ -0,0 +1,11 @@
+inductive foo {n : Nat} : Prop
+
+-- Check that the error message will print the types with implicit arguments shown
+example (h : @foo 42) : @foo 23 := by
+  apply h
+
+example : (1 : Nat) = 1 := by
+  apply (rfl : (1 : Int) = 1)
+
+example : PUnit.{0} = PUnit.{0} := by
+  apply Eq.refl PUnit.{1} -- TODO: addPPExplicitToExposeDiff is not handling this yet

tests/lean/issue3232.lean.expected.out

@@ -0,0 +1,16 @@
+issue3232.lean:5:2-5:9: error: tactic 'apply' failed, failed to unify
+  @foo 42
+with
+  @foo 23
+h : foo
+⊢ foo
+issue3232.lean:8:2-8:29: error: tactic 'apply' failed, failed to unify
+  @OfNat.ofNat Int 1 instOfNat = 1
+with
+  @OfNat.ofNat Nat 1 (instOfNatNat 1) = 1
+⊢ 1 = 1
+issue3232.lean:11:2-11:25: error: tactic 'apply' failed, failed to unify
+  PUnit = PUnit
+with
+  PUnit = PUnit
+⊢ PUnit = PUnit