fix(kernel/default_converter): broken optimization

we must also check the universe levels when applying the optimization for
constraints of the form:

            f.{l_1 ... l_k} a_1 ... a_n  =?= f.{l_1' ... l_k'} b_1 ... b_n

The optimization tries to avoid unfolding f if we can establish that
a_i is definitionally equal to b_i for each i in [1, n]

closes #581

src/kernel/default_converter.cpp

@@ -487,6 +487,7 @@ pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, exp
                         // skip the delta-reduction step.
                         // If the flag use_conv_opt() is not true, then we skip this optimization
                         if (!is_opaque(*d_t) && d_t->use_conv_opt() &&
+                            is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n)), cs) &&
                             is_def_eq_args(t_n, s_n, cs))
                             return to_bcs(true, cs);
                     }

tests/lean/run/forest_height.lean

@@ -62,7 +62,7 @@ find_decl bool.ff ≠ bool.tt
 
 -- map using well-founded recursion. We could have used the default recursor.
 -- this is just a test for the definitional package
-definition map.F {A B : Type} (f : A → B) (tf₁ : tree_forest A) : (Π tf₂ : tree_forest A, tf₂ ≺ tf₁ → map.res B tf₂) → map.res B tf₁ :=
+definition map.F {A B : Type₁} (f : A → B) (tf₁ : tree_forest A) : (Π tf₂ : tree_forest A, tf₂ ≺ tf₁ → map.res B tf₂) → map.res B tf₁ :=
 sum.cases_on tf₁
   (λ t : tree A, tree.cases_on t
     (λ a₁ f₁ (r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inl (tree.node a₁ f₁) → map.res B tf₂),
@@ -91,7 +91,7 @@ sum.cases_on tf₁
           (pr₂ rf₁),
        sigma.mk (sum.inr (forest.cons nt₁ nf₁)) rfl))
 
-definition map {A B : Type} (f : A → B) (tf : tree_forest A) : map.res B tf :=
+definition map {A B : Type₁} (f : A → B) (tf : tree_forest A) : map.res B tf :=
 well_founded.fix (@map.F A B f) tf
 
 eval map succ (sum.inl (tree.node 2 (forest.cons (tree.node 1 (forest.nil nat)) (forest.nil nat))))

tests/lean/run/level_bug1.lean

@@ -0,0 +1,4 @@
+definition f (a : Type) := Π r : Type, (a → r) → r
+
+definition blah2 : Π {a  : Type} {r  : Type} (sa : f a) (k  : a → r), sa r k = sa r k :=
+λ (a  : Type) (r  : Type) (sa : f a) (k  : a → r), rfl

tests/lean/run/level_bug2.lean

@@ -0,0 +1,4 @@
+definition f (a : Type) := Π r : Type, (a → r) → r
+
+definition blah2 {a  : Type} {r  : Type} (sa : f a) (k  : a → r) : sa r k = sa r k :=
+rfl

tests/lean/run/level_bug3.lean

@@ -0,0 +1,11 @@
+variables {a r : Type}
+
+definition f a := Πr, (a -> r) -> r
+
+lemma blah2 (sa : f a) (k : (a -> r)) :
+  sa r k = sa r k :=
+  sorry
+
+lemma blah3 (sa : f a) (k : (a -> r)) :
+  sa r k = sa r k :=
+  rfl

tests/lean/slow/path_groupoids.lean

@@ -573,7 +573,7 @@ path.rec_on b (path.rec_on a (concat_1p _)^)
 -- Structure corresponding to the coherence equations of a bicategory.
 
 -- The "pentagonator": the 3-cell witnessing the associativity pentagon.
-definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) :
+definition pentagon {A : Type₁} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) :
   whiskerL p (concat_p_pp q r s)
     ⬝ concat_p_pp p (q ⬝ r) s
     ⬝ whiskerR (concat_p_pp p q r) s