Display of types in the documentation hides `@`

Stream: mathlib4

[Adomas Baliuka]

For exampe, nhds_mono is defined as

theorem nhds_mono {t₁ t₂ : TopologicalSpace α} {a : α} (h : t₁ ≤ t₂) :
     @nhds α t₁ a ≤ @nhds α t₂ a := ...

but the docs display it as

theorem nhds_mono {α : Type u} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {a : α} (h : t₁ ≤ t₂) :
    nhds a ≤ nhds a

Is it "obvious from the context" (not the same as "can be figured out from the context") what the two sides of the comparison mean here and everything is as it should be? Or is this unfortunate but a tradeoff that must be accepted? Or could this be improved?

[Kyle Miller]

This is a limitation of the pretty printer. The @ annotation is not preserved during elaboration, and the pretty printer would have to guess to make certain arguments explicit. Printing it as nhds a ≤ nhds a is wrong, but a human reader might be able to figure out what it's supposed to be.

Potentially the pretty printer could guess to make @nhds α t₁ a explicit since nhds a elaborates to @nhds α t₂ a

[Jannis Limperg]

How about this heuristic: if an argument a of a function f does not appear in any later argument of f, then it should be displayed explicitly. This would make t₁ and t₂ above explicit, but not α.

I imagine this heuristic might be overzealous in some situations, but it is at least always clear.

[Kyle Miller]

That would make a + b print as @HAdd.hAdd _ _ _ someInstExpression a b, right?

[Jannis Limperg]

True, add an exception for instance arguments. :sweat_smile:

[Ruben Van de Velde]

But isn't the case in the OP an instance argument?

[Kyle Miller]

The Ideal Algorithm would be to resynthesize each instance argument to obtain the canonical instance, and then checking whether the provided instance is defeq to the canonical one. However, this would make pretty printing a lot slower.

I could see doing an approximation for just local instances. It'd help a lot with this Order module.