fix: normalize imax 1 u to u (#7631)

This PR fixes `Lean.Level.mkIMaxAux` (`mk_imax` in the kernel) such that
`imax 1 u` reduces to `u`.

Closes #7096

Author: arthur-adjedj

src/Lean/Level.lean

@@ -295,9 +295,10 @@ private def isAlreadyNormalizedCheap : Level → Bool
 
 /- Auxiliary function used at `normalize` -/
 private def mkIMaxAux : Level → Level → Level
-  | _,    zero => zero
-  | zero, u    => u
-  | u₁,   u₂   => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
+  | _,    zero   => zero
+  | zero, u      => u
+  | succ zero, u => u
+  | u₁,   u₂     => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
 
 /- Auxiliary function used at `normalize` -/
 @[specialize] private partial def getMaxArgsAux (normalize : Level → Level) : Level → Bool → Array Level → Array Level

src/kernel/level.cpp

@@ -93,25 +93,25 @@ level mk_max(level const & l1, level const & l2)  {
     }
 }
 
+static level * g_level_zero = nullptr;
+static level * g_level_one  = nullptr;
+level const & mk_level_zero() { return *g_level_zero; }
+level const & mk_level_one() { return *g_level_one; }
+bool is_one(level const & l) { return l == mk_level_one(); }
+
 level mk_imax(level const & l1, level const & l2) {
     if (is_not_zero(l2))
         return mk_max(l1, l2);
     else if (is_zero(l2))
         return l2;  // imax u 0 = 0  for any u
-    else if (is_zero(l1))
-        return l2;  // imax 0 u = u  for any u
+    else if (is_zero(l1) || is_one(l1))
+        return l2;  // imax 0 u = imax 1 u = u  for any u
     else if (l1 == l2)
         return l1;  // imax u u = u
     else
         return mk_imax_core(l1, l2);
 }
 
-static level * g_level_zero = nullptr;
-static level * g_level_one  = nullptr;
-level const & mk_level_zero() { return *g_level_zero; }
-level const & mk_level_one() { return *g_level_one; }
-bool is_one(level const & l) { return l == mk_level_one(); }
-
 bool operator==(level const & l1, level const & l2) {
     if (kind(l1) != kind(l2)) return false;
     if (hash(l1) != hash(l2)) return false;

tests/lean/binrelTypeMismatch.lean.expected.out

@@ -10,11 +10,11 @@ has type
   Prop : Type
 but is expected to have type
   Bool : Type
-Prop → sorry : Sort (imax 1 u_1)
+Prop → sorry : Sort u_1
 binrelTypeMismatch.lean:20:27-20:28: error: type mismatch
   p
 has type
   Prop : Type
 but is expected to have type
   Bool : Type
-Prop → sorry : Sort (imax 1 u_1)
+Prop → sorry : Sort u_1

tests/lean/run/7096.lean

@@ -0,0 +1,9 @@
+/-!
+# Normalization of imax 1 u
+
+https://github.com/leanprover/lean4/issues/7096
+
+Universe levels of the form `imax 1 u` should normalize to `u`.
+-/
+
+example (α : Sort u) : Sort u := Unit → α

tests/lean/run/issue4726.lean

@@ -2,7 +2,7 @@
 -- A refexive type, with multiple parameters to make sure
 -- we get the order right
 
-inductive N where
+inductive N : Type where
  | cons : (Nat -> Bool → N) -> N