lean4#6269 warnings for declaration/`export` conflicts

Stream: PR reviews

[Kyle Miller]

This isn't a request to review lean4#6269 per se, but I would appreciate if someone would review the warnings that it turns up in branch#lean-pr-testing-6269 and make PRs to mathlib to resolve them (or let me know if the warnings make no sense!)

Background: Issue lean4#5258 suggested that if a declaration exists and would conflict with an export, or vice versa, there ought to be a warning. This Lean PR goes most of the way there, warning at the point of a declaration or an export that an ambiguity is about to be created, though it doesn't go so far as to make sure that if you import two modules, one with a declaration and another with an alias for the same name, that there will be an ambiguity.

Pinging @Jireh Loreaux

[Jireh Loreaux]

I will take a look, but I can't for the next 36-48 hours.

[Edward van de Meent]

a common theme here seems to be _root_.trans, i.e. trans refers to docs#trans as alias of either docs#Trans.trans or docs#IsTrans.trans

[Edward van de Meent]

deduplicating this seems to be a large part of adapting to this PR

[Edward van de Meent]

later on (after moving docs#trans), it seems there are some errors typeclass instance problem is stuck, it is often due to metavariables Trans _ _ _ due to using trans without disambiguation.

[Edward van de Meent]

(see for my partial attempt at finding all issues branch#blizzard_inc/lean-pr-testing-6269 , and here for the comparison against branch#lean-pr-testing-6269)

[Ruben Van de Velde]

That's already a pain today. Can we just fix trans?

[Kim Morrison]

@Edward van de Meent, sorry I think I'm missing some context here. What was your proposed fix for trans?

[Edward van de Meent]

Just namespace one

[Edward van de Meent]

And then disambiguate every occurrence

[Edward van de Meent]

Or, well, I think that's the solution? I haven't looked at this for a month

[Kim Morrison]

I guess I was hoping for a suggestion as to which one. :-)

[Edward van de Meent]

right...
docs#Trans.trans is exported into the _root_ namespace in prelude, while docs#trans is an actual separate definition... looking at the diff of the salvage attempt i made, it looks like usually the intended value is indeed docs#IsTrans.trans which trans is basically an alias of. (it's a separate declaration, but defeq up to argument binder types).

Since mathlib typically will use _root_.trans, i'd say for mathlib it'd be ideal if Trans.trans does not get exported... then again, i think mathlib can also do just fine only referring to IsTrans.trans...

[Edward van de Meent]

other things to consider here is that i don't think we can deprecate exports, while we can deprecate declarations.

[Edward van de Meent]

ultimately, i'd say _root_.trans really should be called IsTrans.trans
Making this change requires _root_.trans to be deprecated, the current IsTrans.trans field to be renamed (to something like trans' or is_trans, maybe?), and the actual moving of the declaration.

[Edward van de Meent]

(sorry for the multiple messages, i was still getting it all straight in my head)

[Kim Morrison]

Okay. On the Lean side, I can consider removing the export Trans (trans); this barely hurts Lean at all (lean#6809). However it is a breaking change without a deprecation.

What about:

• Mathlib (perhaps: you) deprecates _root_.trans.
• On the next release, I add _root_.trans in Lean as a deprecated alias for Trans.trans, and remove the export (and Mathlib removes its _root_.trans
• On the release after that, I delete _root_.trans from Lean, and Mathlib (+anyone downstream) is free to use _root_.trans as desired.

[Edward van de Meent]

sounds like a plan

[Edward van de Meent]

btw, i'm assuming deprecating _root_.trans includes replacing it as i suggested?

[Edward van de Meent]

because deprecating without replacement is non-trivial. (deprecating with replacement is also non-trivial, but still easier)