delaborators for non-instances

Stream: mathlib4

[Floris van Doorn]

@Kyle Miller I just saw your PR #11700, and @AntoineChambert-Loir asked me today for something a bit similar.
Suppose you have a term @IsOpen X t s where type-class inference does not find t as the canonical topology on X (because it finds another topology or no topology), then it would be nice if this is printed as IsOpen[t] s (this is notation). Similar for MeasurableSet[m] and whatever-other predicate we have defined this notation for.
Would this be possible as an delaborator (i.e. can a delaborator call type-class inference)? It is probably quite inefficient though, so it probably shouldn't be enabled by default.

[Yaël Dillies]

I think there's a pretty cheap way to achieve this: Make IsOpen[t] s notation for @IsOpen _ t s except that you insert mdata somewhere

[Yaël Dillies]

That won't survive rewriting, though (I think?)

[Kyle Miller]

Yeah, a delaborator has access to MetaM, so it can do synthInstance and do a defeq check.

[Kyle Miller]

Maybe there are some approximations that would generally do the right thing. What sorts of terms are the non-canonical instances? Are they always going to be applications of definitions that aren't themselves global instances? Or would the non-canonicity only appear deeper in the term?

[Floris van Doorn]

I think often these non-instances will be either

• A local constant, when multiple local constants of the same type exist (e.g. X with two topologies on it)
• A definition that is not an instance

I expect that these generally do not occur deeper in the term, since writing that down would be very inconvenient with the current setup (I can imagine having two uniform spaces and considering both topologies, but know of this actually happening in practice). But maybe @Antoine Chambert-Loir knows of an example (I just realized that my ping in the other message didn't work).

[Antoine Chambert-Loir]

The example I had in mind was of the form : to prove that two topologies t and t' on X are equal, use docs#TopologicalSpace.ext_iff_nhds, and you are reduced to prove nhds x = nhds x for all x : X.
If that were written nhds[t] x = nhds[t'] x, that would be much clearer…