trySynthInstance and trace/message generators

Stream: lean4

[Robert Maxton]

Moving this out of metaprogramming as it's leaning closer to "possible lean bug": It seems that synthInstance and trySynthInstance has different behavior when called within something like #check or trace_state; it does not consider local variables.

[Robert Maxton]

Example in original context:

import Mathlib.Topology.Order

namespace TopologicalSpace
open Topology Lean Meta PrettyPrinter.Delaborator SubExpr

/-- When the delab reader is pointed at an expression for an instance, returns `(true, t)`
**iff** instance synthesis succeeds and produces a defeq instance; otherwise returns `(false, t)`.
-/
def delabCheckingCanonical : DelabM (Bool × Term) := do
  let instD ← delab
  let inst ← getExpr
  let type ← inferType inst
  -- if there is no synthesized instance, still return `false`
  -- (because `inst` is still non-canonical)
  let .some synthInst ← Meta.trySynthInstance type | return (false, instD)
  return (← Meta.isDefEq inst synthInst, instD)

/-- Delaborate unary notation referring to non-standard topologies. -/
def delabUnary (mkStx : Term → DelabM Term) : Delab :=
  withOverApp 2 <| whenPPOption Lean.getPPNotation do
    let (false, instD) ← withNaryArg 1 delabCheckingCanonical | failure
    mkStx instD

/-- Delaborate binary notation referring to non-standard topologies. -/
def delabBinary (mkStx : Term → Term → DelabM Term) : Delab :=
  withOverApp 4 <| whenPPOption Lean.getPPNotation do
    -- fall through to normal delab if both canonical
    let (canonα?, instDα) ← withNaryArg 2 delabCheckingCanonical
    let (canonβ?, instDβ) ← withNaryArg 3 delabCheckingCanonical
    if canonα? && canonβ? then failure
    mkStx instDα instDβ

/-- Delaborator for `IsOpen[_]`. -/
@[app_delab IsOpen] def delabIsOpen : Delab := delabUnary fun x ↦ `(IsOpen[$x])

/-- Delaborator for `IsClosed[_]`. -/
@[app_delab IsClosed] def delabIsClosed : Delab := delabUnary fun x ↦ `(IsClosed[$x])

/-- Delaborator for `closure[_]`. -/
@[app_delab closure] def delabClosure : Delab := delabUnary fun x ↦ `(closure[$x])

/-- Delaborator for `Continuous[_, _]`. -/
@[app_delab Continuous] def delabContinuous : Delab := delabBinary fun x y ↦ `(Continuous[$x, $y])

end TopologicalSpace

open scoped Topology

#synth TopologicalSpace ℕ

/--
  trace: α : Type u_1
σ : TopologicalSpace α
s : Set α
⊢ IsOpen s
-/
#guard_msgs(trace) in
example {α : Type*} [σ : TopologicalSpace α] (s : Set α) : IsOpen[σ] s := by
  trace_state
  sorry

/--
  trace: s : Set ℕ
⊢ IsOpen s
-/
#guard_msgs(trace) in
example (s : Set ℕ) : IsOpen[inferInstance] s := by
  trace_state
  sorry

[Robert Maxton]

In both tests, within the infoview, IsOpen[_] s is correctly reduced to simply IsOpen s as intended, as the given instance is defeq to the canonical instance.

However, in the first case, that 'canonical' instance is provided as a local variable [σ : TopologicalSpace α], and within trace_state trySynthInstance fails to find an instance, as can be confirmed by swapping it out for synthInstance and reading the resulting error. In the second case, the instance is a bit more 'canonical', being an actually-registered external instance on the fixed type ℕ, and the corresponding #guard_msgs succeeds.

[Robert Maxton]

Is this a bug in Lean, or as intended? And either way, is there a workaround? The delab itself works fine, and worst case I suppose I can restrict my unit tests to the case of a type with an externally-registered instance, but I would like to have a properly complete set of unit tests and I do consider this part of the intended behavior of the IsOpen[_] delaborator.

[Aaron Liu]

Maybe you need to with some context?

[Robert Maxton]

... Sorry, I have no idea what you meant by that

[Robert Maxton]

Unless you mean some function of the form withFoo, but then I still don't know what contexts might be relevant ^.^;