perf(library/type_context): process function before arguments

src/library/type_context.cpp

@@ -2456,8 +2456,8 @@ bool type_context::is_def_eq_core_core(expr const & t, expr const & s) {
 
     if (is_app(t_n) && is_app(s_n)) {
         scope s(*this);
-        if (is_def_eq_args(t_n, s_n) &&
-            is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n)) &&
+        if (is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n)) &&
+            is_def_eq_args(t_n, s_n) &&
             process_postponed(s)) {
             s.commit();
             return true;

tests/lean/run/simplifier_canonize_subsingletons.lean

@@ -60,9 +60,9 @@ end lambda
 
 namespace dont_crash_when_locals_incompatible
 
-universe variable l
+universe variables l
 constants (ss : Π {A : Type.{l}}, A → Type.{l})
-          [ss_ss : ∀ (T : Type*) (t : T), subsingleton (ss t)]
+          [ss_ss : ∀ (T : Type l) (t : T), subsingleton (ss t)]
           (A : Type.{l}) (a : A)
           (ss₁ ss₂ : ss a)
 
@@ -77,7 +77,7 @@ example : (λ (s : ss a), ss₁) = (λ (s : ss a), s) := by simp
 -- first. We do however avoid the error of replacing ss₁ with the local s.
 -- TODO(dhs): the more robust solution is to maintain a set of canonical (_ : ss a)
 -- for each subsingleton type, analogous to the defeq_canonizer.
-example : (λ (s : ss a), s) = (λ (s : ss a), ss₁) :=
+lemma ex : (λ (s : ss a.{1}), s) = (λ (s : ss a.{1}), ss₁) :=
 by do try simp,
       f ← mk_const `funext,
       apply f,