From a1c8a941f06b42104f92d1385f7dcea2802dc198 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 11 Jun 2024 01:37:52 +0200
Subject: [PATCH] fix: universe parameter order discrepancy between `theorem`
 and `def` (#4408)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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        |  4 ++-
 src/Lean/Elab/Term.lean            |  3 ++-
 tests/lean/run/3965.lean           |  2 +-
 tests/lean/run/4171.lean           |  2 +-
 tests/lean/run/univParamIssue.lean | 39 ++++++++++++++++++++++++++++++
 5 files changed, 46 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/univParamIssue.lean

diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean
index b4e6624e72..3d52b625ed 100644
--- a/src/Lean/Elab/DeclUtil.lean
+++ b/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
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 4bbdb2757e..3122d1e062 100644
--- a/src/Lean/Elab/Term.lean
+++ b/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
 
diff --git a/tests/lean/run/3965.lean b/tests/lean/run/3965.lean
index 63ad457978..d8ae0101f1 100644
--- a/tests/lean/run/3965.lean
+++ b/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
 
 
diff --git a/tests/lean/run/4171.lean b/tests/lean/run/4171.lean
index 4dec00f314..70f4b9998d 100644
--- a/tests/lean/run/4171.lean
+++ b/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
diff --git a/tests/lean/run/univParamIssue.lean b/tests/lean/run/univParamIssue.lean
new file mode 100644
index 0000000000..1f949e6d29
--- /dev/null
+++ b/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