[Merged by Bors] - fix(frontends/lean/definition_cmds): put auto-bound universes before explicit

[digama0]

For compatibility with lean 4. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/list.2Etraverse/near/313206118

[gebner]

I'm not sure I can reproduce this. The following file produces the same order of universe parameters in both Lean 3 and Lean 4:

universe a universe z
def foo (α : Type a) (β : Type _) (γ : Type z) := α × β × γ
set_option pp.universes true
#print foo

$ lean +leanprover-community/lean:3.49.1 788.lean
def {a z u_1} foo : Type a → Type u_1 → Type z → Type (max a u_1 z) :=
λ (α : Type a) (β : Type u_1) (γ : Type z), α × β × γ
$ lean +leanprover/lean4:nightly-2022-11-30 788.lean
def foo.{a, z, u_1} : Type a → Type u_1 → Type z → Type (max a z u_1) :=
fun α β γ => Prod.{a, max z u_1} α (Prod.{u_1, z} β γ)

Also do we really want this order (and not change Lean 4)? Also please add a test.

[digama0]

You are right, this isn't the issue. The mystery _aux_param_0 is actually in the definition of List.traverse._main:

namespace list
universes u v

protected def traverse {F : Type u → Type v} [applicative F] {α β : Type*} (f : α → F β) :
  list α → F (list β)
| [] := pure []
| (x :: xs) := list.cons <$> f x <*> traverse xs

set_option pp.universes true
#print list.traverse._main

end list

def {_aux_param_0 u v} list.traverse._main : Π {F : Type u → Type v} [_inst_1 : applicative.{u v} F] {α : Type _aux_param_0} {β : Type u},
  (α → F β) → list.{_aux_param_0} α → F (list.{u} β) := ...

I think cause is actually this line:

lean/src/library/aux_definition.cpp

Line 111 in 44be9cd

std::sort(m_level_params.begin(), m_level_params.end());

which sorts the newly generated universe parameters alphabetically, after introducing fresh variables using the _aux_param_i naming convention which of course will put them first. I think we should just remove the sort and let them be ordered by appearance in the term.

[gebner]

Let's just try this out.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build emscripten
• Build linux aarch64 Release
• Build linux Debug
• Build linux Release
• Build macos Debug
• Build macos Release
• Build sanitized
• Build windows Release

[gebner]

Apparently this also broke Lean 4 compatibility in the example I posted:

universe a universe z
def foo (α : Type a) (β : Type _) (γ : Type z) := α × β × γ
set_option pp.universes true
#print foo

Now prints u_1 a z instead of a z u_1. I think we should just revert this PR.