Trace class `Meta.synthInstance.answer` is not registered

[mattrobball]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In Lean.Meta.SynthInstance.addAnswer, there is a trace for Meta.synthInstance.answer but it is not registered at the bottom of the file.

Context

In Zulip, we were struggling under a failure of typeclass synthesis for nested function types. This trace would have made it much easier. For reference, I put the code of addAnswer below.

def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
  withMCtx cNode.mctx do
  if cNode.size ≥ (← read).maxResultSize then
      trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
  else
    withTraceNode `Meta.synthInstance.answer
      (fun _ => return m!"{checkEmoji} {← instantiateMVars (← inferType cNode.mvar)}") do
    let answer ← mkAnswer cNode
    -- Remark: `answer` does not contain assignable or assigned metavariables.
    let key := cNode.key
    let entry ← getEntry key
    if isNewAnswer entry.answers answer then
      let newEntry := { entry with answers := entry.answers.push answer }
      modify fun s => { s with tableEntries := s.tableEntries.insert key newEntry }
      entry.waiters.forM (wakeUp answer)

You can see it is set up to report answers constructed from too many instances but simply not plugged in.

Steps to Reproduce

1. type set_option trace.Meta.synthInstance.answer true

Expected behavior: set_option trace.Meta.synthInstance.answer true should furnish the traces already in the code.

Actual behavior: It fails with unknown option 'trace.Meta.synthInstance.answer'

Versions

"4.7.0, commit fbedb79b4694ef86162694b1b1b8c489ecbd71ac"

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[mattrobball]

I have branch which adds the trace messages in addAnswer to the newAnswer trace class. If this is favorable, let me know and I will PR.

[kim-em]

@mattrobball, yes please. Please ping me on the PR, it seems a straightforward bug fix.

[mattrobball]

@thorimur had identified a more exhaustive list of such things

[thorimur]

Here's a link to the message, and here are the ones I identified:

Lean/PrettyPrinter/Delaborator/Basic.lean: PrettyPrinter.delab.input
Lean/Meta/Tactic/Simp/SimpAll.lean: Meta.Tactic.simp.all
Lean/Meta/DecLevel.lean: Meta.isLevelDefEq.step
Lean/Meta/SizeOf.lean: Meta.sizeOf.minor
Lean/Meta/SizeOf.lean: Meta.sizeOf.minor.step
Lean/Meta/SizeOf.lean: Meta.sizeOf.aux
Lean/Meta/SizeOf.lean: Meta.sizeOf.loop
Lean/Elab/StructInst.lean: Elab.struct.modifyOp
Lean/Elab/Quotation.lean: Elab.match_syntax.onMatch
Lean/Elab/Term.lean: Elab.implicitForall
Lean/Elab/SyntheticMVars.lean: Elab.defaultInstance
Lean/Elab/MutualDef.lean: Elab.definition.mkClosure
Lean/Elab/Binders.lean: Elab.autoParam
Lean/Elab/Binders.lean: Elab.let.decl