fix: universe parameter order discrepancy between theorem and def (…

…#4408)

Before this commit, the `theorem` and `def` declarations had different
universe parameter orders.
For example, the following `theorem`:
```
theorem f (a : α) (f : α → β) : f a = f a := by
  rfl
```
was elaborated as
```
theorem f.{u_2, u_1} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
  fun {α} {β} a f => Eq.refl (f a)
```
However, if we declare `f` as a `def`, the expected order is produced.
```
def f.{u_1, u_2} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
  fun {α} {β} a f => Eq.refl (f a)
```

This commit fixes this discrepancy.

@semorrison @jcommelin: This might be a disruptive change to Mathlib,
but it is better to fix the issue asap. I am surprised nobody has
complained about this issue before. I discovered it while trying to
reduce discrepancies between `theorem` and `def` elaboration.

src/Lean/Elab/DeclUtil.lean

@@ -75,9 +75,11 @@ def sortDeclLevelParams (scopeParams : List Name) (allUserParams : List Name) (u
   match allUserParams.find? fun u => !usedParams.contains u && !scopeParams.elem u with
   | some u => throw s!"unused universe parameter '{u}'"
   | none   =>
+    -- Recall that `allUserParams` (like `scopeParams`) are in reverse order. That is, the last declared universe is the first element of the list.
+    -- The following `foldl` will reverse the elements and produce a list of universe levels using the user given order.
     let result := allUserParams.foldl (fun result levelName => if usedParams.elem levelName then levelName :: result else result) []
     let remaining := usedParams.filter (fun levelParam => !allUserParams.elem levelParam)
     let remaining := remaining.qsort Name.lt
-    pure $ result ++ remaining.toList
+    return result ++ remaining.toList
 
 end Lean.Elab

src/Lean/Elab/Term.lean

@@ -737,7 +737,8 @@ def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax :=
 def levelMVarToParam (e : Expr) (except : LMVarId → Bool := fun _ => false) : TermElabM Expr := do
   let levelNames ← getLevelNames
   let r := (← getMCtx).levelMVarToParam (fun n => levelNames.elem n) except e `u 1
-  setLevelNames (levelNames ++ r.newParamNames.toList)
+  -- Recall that the most recent universe is the first element of the field `levelNames`.
+  setLevelNames (r.newParamNames.reverse.toList ++ levelNames)
   setMCtx r.mctx
   return r.expr
 

tests/lean/run/3965.lean

@@ -198,7 +198,7 @@ theorem principal_nfp_blsub₂' (op : Ordinal → Ordinal → Ordinal) (o : Ordi
   · refine ⟨n+1, ?_⟩
     rw [Function.iterate_succ']
     -- universe 0 also works here
-    exact lt_blsub₂.{0} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
+    exact lt_blsub₂.{_, _, 0} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
   · sorry
 
 

tests/lean/run/4171.lean

@@ -701,7 +701,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
   mul := { hom := M.X.mul }
   mul_one := by
     ext
-    simp [foo.{v₁ + 1}] -- specifying the universe level explicitly works!
+    simp [foo.{_, v₁ + 1}] -- specifying the universe level explicitly works!
 
 theorem foo' {V} [Quiver V] {X Y x} :
     @Quiver.Hom.unop V _ X Y no_index (Opposite.op (unop := x)) = x := rfl

tests/lean/run/univParamIssue.lean

@@ -0,0 +1,39 @@
+theorem f1 (a : α) (f : α → β) : f a = f a := by
+  rfl
+
+/--
+info: theorem f1.{u_1, u_2} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
+fun {α} {β} a f => Eq.refl (f a)
+-/
+#guard_msgs in
+#print f1
+
+theorem f2 {α : Sort u} {β : Sort v} (a : α) (f : α → β) : f a = f a := by
+  rfl
+
+/--
+info: theorem f2.{u, v} : ∀ {α : Sort u} {β : Sort v} (a : α) (f : α → β), f a = f a :=
+fun {α} {β} a f => Eq.refl (f a)
+-/
+#guard_msgs in
+#print f2
+
+theorem f3.{u,v} {α : Sort u} {β : Sort v} (a : α) (f : α → β) : f a = f a := by
+  rfl
+
+/--
+info: theorem f3.{u, v} : ∀ {α : Sort u} {β : Sort v} (a : α) (f : α → β), f a = f a :=
+fun {α} {β} a f => Eq.refl (f a)
+-/
+#guard_msgs in
+#print f3
+
+def g (a : α) (f : α → β) : f a = f a := by
+  rfl
+
+/--
+info: def g.{u_1, u_2} : ∀ {α : Sort u_1} {β : Sort u_2} (a : α) (f : α → β), f a = f a :=
+fun {α} {β} a f => Eq.refl (f a)
+-/
+#guard_msgs in
+#print g