make canonical instances appear as _

Author: robertmaxton42

Mathlib/Topology/Defs/Basic.lean

@@ -198,11 +198,11 @@ scoped notation (name := IsClosed_of) "IsClosed[" t "]" => @IsClosed _ t
 /-- Notation for `closure` with respect to a non-standard topology. -/
 scoped notation (name := closure_of) "closure[" t "]" => @closure _ t
 
-/-- Notation for `Continuous` with respect to a non-standard topologies. -/
+/-- Notation for `Continuous` with respect to non-standard topologies. -/
 scoped notation (name := Continuous_of) "Continuous[" t₁ ", " t₂ "]" =>
   @Continuous _ _ t₁ t₂
 
-open Topology Lean.PrettyPrinter.Delaborator
+open Topology Lean.PrettyPrinter.Delaborator Delab.Noncanonical
 
 /-- Delaborator for `IsOpen[_]`. -/
 @[scoped app_delab IsOpen] meta def delabIsOpen : Delab := delabUnary 2 1 fun x ↦ `(IsOpen[$x])
@@ -216,7 +216,8 @@ meta def delabIsClosed : Delab := delabUnary 2 1 fun x ↦ `(IsClosed[$x])
 
 /-- Delaborator for `Continuous[_, _]`. -/
 @[scoped app_delab Continuous]
-meta def delabContinuous : Delab := delabBinary 4 2 3 fun x y ↦ `(Continuous[$x, $y])
+meta def delabContinuous : Delab :=
+  delabBinary 4 2 3 (fun x y ↦ `(Continuous[$x, $y])) (some `(_))
 
 end Topology
 

Mathlib/Util/DelabNonCanonical.lean

@@ -6,6 +6,7 @@ Authors: Robert Maxton
 module
 
 public import Mathlib.Init
+public meta import Lean.Meta
 public meta import Lean.PrettyPrinter.Delaborator.Builtins
 
 /-! Delab checking canonicity.
@@ -18,17 +19,22 @@ Synthesized instances are considered 'canonical' for this purpose.
 public meta section
 open Lean Meta PrettyPrinter.Delaborator SubExpr
 
+
+def Lean.Meta.isCanonicalInstance (inst : Expr) : MetaM Bool := do
+  let type ← inferType inst
+  let .some synthInst ← trySynthInstance type | return false
+  isDefEqI inst synthInst
+
 /-- 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)`.
+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)
-  withReducibleAndInstances <| return (← Meta.isDefEq inst synthInst, instD)
+  if ← isCanonicalInstance inst then
+    return (true, ← annotateTermInfo <| ← `(_))
+  else
+    return (false, ← delab)
+namespace Delab.Noncanonical
 
 /-- Delaborate an expression with arity `arity` into a unary notation `mkStx` iff the argument
 `arg` is a non-canonical instance (is not defeq to what is synthesized for its type, or else
@@ -39,12 +45,19 @@ def delabUnary (arity arg : Nat) (mkStx : Term → DelabM Term) : Delab :=
     mkStx instD
 
 /-- Delaborate an expression with arity `arity` into a binary notation `mkStx` iff either
-argument `arg₁` or `arg₂` are non-canonical instance (are not defeq to what is synthesized for
-its type, or else instance synthesis fails). -/
-def delabBinary (arity arg₁ arg₂ : Nat) (mkStx : Term → Term → DelabM Term) : Delab :=
+argument `arg₁` or `arg₂` are non-canonical instances (are not defeq to what is synthesized for
+its type, or else instance synthesis fails). If `hole` is not `none`, it is used
+in place of a canonical instance. -/
+def delabBinary (arity arg₁ arg₂ : Nat) (mkStx : Term → Term → DelabM Term)
+    (hole : Option (DelabM Term) := none) : Delab :=
   withOverApp arity <| whenPPOption Lean.getPPNotation do
     let (canonα?, instDα) ← withNaryArg arg₁ delabCheckingCanonical
     let (canonβ?, instDβ) ← withNaryArg arg₂ delabCheckingCanonical
-    -- fall through to normal delab if both canonical
     if canonα? && canonβ? then failure
     mkStx instDα instDβ
+--     let hole ← hole.sequence
+--     mkStx (replace? hole canonα? instDα) (replace? hole canonβ? instDβ)
+-- where
+--   replace? h b i := bif b then h.getD i else i
+
+end Delab.Noncanonical

MathlibTest/Delab/TopologicalSpace.lean

@@ -119,14 +119,12 @@ section applied
 -- in either or both slots do trigger the delab and that
 -- `instTopologicalSpaceNat`, `sierpinskiSpace` does not.
 
-/-- info: [Continuous[τ₁, sierpinskiSpace] p, Continuous[τ₂, sierpinskiSpace] p,
-  Continuous[induced g inferInstance, inferInstance] g] : List Prop -/
+/-- info: [Continuous[τ₁, _] p, Continuous[τ₂, _] p, Continuous[induced g inferInstance, inferInstance] g] : List Prop -/
 #guard_msgs(info) in
 #check [Continuous[τ₁, sierpinskiSpace] p, Continuous[τ₂, sierpinskiSpace] p,
   Continuous[induced g inferInstance, inferInstance] g]
 
-/-- info: [Continuous[instTopologicalSpaceNat, σ₁] p, Continuous[instTopologicalSpaceNat, σ₂] p,
-  Continuous[inferInstance, coinduced h inferInstance] h] : List Prop -/
+/-- info: [Continuous[_, σ₁] p, Continuous[_, σ₂] p, Continuous[inferInstance, coinduced h inferInstance] h] : List Prop -/
 #guard_msgs(info) in
 #check [Continuous[instTopologicalSpaceNat, σ₁] p, Continuous[instTopologicalSpaceNat, σ₂] p,
   Continuous[inferInstance, coinduced h inferInstance] h]
@@ -143,25 +141,32 @@ section unapplied
 
 -- Same as above, except for unapplied operators.
 
-/-- info: [Continuous[τ₁, sierpinskiSpace], Continuous[τ₂, sierpinskiSpace]]
+/-- info: [Continuous[τ₁, _], Continuous[τ₂, _]]
 : List ((ℕ → Prop) → Prop) -/
 #guard_msgs(info) in
 #check [Continuous[τ₁, sierpinskiSpace], Continuous[τ₂, sierpinskiSpace]]
 
+-- Note: This is *not* the desired behavior. Treat it instead as a 'bug tracker.'
+-- When `(try)SynthInstance` in `$check` is fixed, this should no longer trigger the delab
+-- on the right, so we should get `Continuous[induced g inferInstance, _]`.
 /-- info:
-Continuous[induced g inferInstance, inferInstanceAs (TopologicalSpace α)] : (β → α) → Prop -/
+Continuous[induced g inferInstance, inst✝] : (β → α) → Prop -/
 #guard_msgs(info) in
-#check Continuous[induced g inferInstance, inferInstanceAs (TopologicalSpace α)]
+#check Continuous[induced g inferInstance, inferInstanceAs% (TopologicalSpace α)]
 
-/-- info: [Continuous[instTopologicalSpaceNat, σ₁], Continuous[instTopologicalSpaceNat, σ₂]]
+/-- info: [Continuous[_, σ₁], Continuous[_, σ₂]]
 : List ((ℕ → Prop) → Prop) -/
 #guard_msgs(info) in
 #check [Continuous[instTopologicalSpaceNat, σ₁], Continuous[instTopologicalSpaceNat, σ₂]]
 
+
+-- As above, this is not the desired behavior. When `(try)SynthInstance` in `#check` is fixed,
+-- this should no longer trigger the delab on the left, so we should get
+-- `Continuous[_, coinduced h inferInstance]`.
 /-- info:
-Continuous[inferInstanceAs (TopologicalSpace α), coinduced h inferInstance] : (α → β) → Prop -/
+Continuous[inst✝, coinduced h inferInstance] : (α → β) → Prop -/
 #guard_msgs(info) in
-#check Continuous[inferInstanceAs (TopologicalSpace α), coinduced h inferInstance]
+#check Continuous[inferInstanceAs% (TopologicalSpace α), coinduced h inferInstance]
 
 /-- info: [Continuous[induced p inferInstance, coinduced p inferInstance], Continuous]
 : List ((ℕ → Prop) → Prop) -/