feat(kernel/level): improve universe level normalization procedure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/inductive_cmd.cpp

@@ -481,6 +481,7 @@ struct inductive_cmd_fn {
             level r = r_lvls[0];
             for (unsigned i = 1; i < r_lvls.size(); i++)
                 r = mk_max(r, r_lvls[i]);
+            r = normalize(r);
             if (is_not_zero(r))
                 return normalize(r);
             else

src/kernel/level.cpp

@@ -641,9 +641,28 @@ level normalize(level const & l) {
         std::sort(args.begin(), args.end(), is_norm_lt);
         buffer<level> & rargs = todo;
         rargs.clear();
-        rargs.push_back(args[0]);
-        auto p_prev = to_offset(args[0]);
-        for (unsigned i = 1; i < args.size(); i++) {
+        unsigned i = 0;
+        if (is_explicit(args[i])) {
+            // find max explicit univierse
+            while (i+1 < args.size() && is_explicit(args[i+1]))
+                i++;
+            lean_assert(is_explicit(args[i]));
+            unsigned k = to_offset(args[i]).second;
+            // an explicit universe k is subsumed by succ^k(l)
+            unsigned j = i+1;
+            for (; j < args.size(); j++) {
+                if (to_offset(args[j]).second >= k)
+                    break;
+            }
+            if (j < args.size()) {
+                // explicit universe was subsumed by succ^k'(l) where k' >= k
+                i++;
+            }
+        }
+        rargs.push_back(args[i]);
+        auto p_prev = to_offset(args[i]);
+        i++;
+        for (; i < args.size(); i++) {
             auto p_curr = to_offset(args[i]);
             if (p_prev.first == p_curr.first) {
                 if (p_prev.second < p_curr.second) {

tests/lean/run/coe3.lean

@@ -0,0 +1,30 @@
+import standard
+
+namespace setoid
+  inductive setoid : Type :=
+  | mk_setoid: Π (A : Type), (A → A → Bool) → setoid
+
+  definition carrier (s : setoid)
+  := setoid_rec (λ a eq, a) s
+
+  definition eqv {s : setoid} : carrier s → carrier s → Bool
+  := setoid_rec (λ a eqv, eqv) s
+
+  infix `≈`:50 := eqv
+
+  coercion carrier
+
+  inductive morphism (s1 s2 : setoid) : Type :=
+  | mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
+
+  set_option pp.universes true
+
+  check mk_morphism
+  check λ (s1 s2 : setoid), s1
+  check λ (s1 s2 : Type), s1
+
+  inductive morphism2 (s1 : setoid) (s2 : setoid) : Type :=
+  | mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
+
+  check mk_morphism2
+end

tests/lean/run/coe4.lean

@@ -0,0 +1,34 @@
+import standard
+
+namespace setoid
+  inductive setoid : Type :=
+  | mk_setoid: Π (A : Type'), (A → A → Bool) → setoid
+
+  set_option pp.universes true
+
+  check setoid
+  definition test : Type.{2} := setoid.{0}
+
+  definition carrier (s : setoid)
+  := setoid_rec (λ a eq, a) s
+
+  definition eqv {s : setoid} : carrier s → carrier s → Bool
+  := setoid_rec (λ a eqv, eqv) s
+
+  infix `≈`:50 := eqv
+
+  coercion carrier
+
+  inductive morphism (s1 s2 : setoid) : Type :=
+  | mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
+
+  check mk_morphism
+  check λ (s1 s2 : setoid), s1
+  check λ (s1 s2 : Type), s1
+
+  inductive morphism2 (s1 : setoid) (s2 : setoid) : Type :=
+  | mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
+
+  check morphism2
+  check mk_morphism2
+end