feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker

We should not rely on this feature. It can be quite expensive.
We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as

   is_convertible(num, Nat)

If is_convertible starts unfolding opaque definitions, we would keep expanding num.

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

src/builtin/optional.lean

@@ -39,11 +39,11 @@ theorem injectivity {A : (Type U)} {a a' : A} : some a = some a' → a = a'
       from (congr1 a eq_reps) ◂ (refl a)
 
 theorem distinct {A : (Type U)} (a : A) : some a ≠ none
-:= assume N : some a = none,
+:= not_intro (assume N : some a = none,
    have eq_reps : (λ x, x = a) = (λ x, false),
       from abst_inj (inhab A) (some_pred a) (none_pred A) N,
    show false,
-      from (congr1 a eq_reps) ◂ (refl a)
+      from (congr1 a eq_reps) ◂ (refl a))
 
 definition value {A : (Type U)} (n : optional A) (H : is_some n) : A
 := ε (inhabited_ex_intro H) (λ x, some x = n)
@@ -52,11 +52,11 @@ theorem is_some_some {A : (Type U)} (a : A) : is_some (some a)
 := exists_intro a (refl (some a))
 
 theorem not_is_some_none {A : (Type U)} : ¬ is_some (@none A)
-:= assume N : is_some (@none A),
+:= not_intro (assume N : is_some (@none A),
    obtain (w : A) (Hw : some w = @none A),
       from N,
    show false,
-      from absurd Hw (distinct w)
+      from absurd Hw (distinct w))
 
 theorem value_some {A : (Type U)} (a : A) (H : is_some (some a)) : value (some a) H = a
 := have eq1  : some (value (some a) H) = some a,

src/builtin/sum.lean

@@ -72,7 +72,7 @@ theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
                       ... = some b2                           : refl (some b2))
 
 theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
-:= assume N : inl a B = inr A b,
+:= not_intro (assume N : inl a B = inr A b,
      have eq1   : inl a B = abst (pair (some a) none) (inhabl (inhabited_intro a) B),
         from refl (inl a B),
      have eq2   : inr A b = abst (pair none (some b)) (inhabl (inhabited_intro a) B),
@@ -80,7 +80,7 @@ theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
      have rep_eq : (pair (some a) none) = (pair none (some b)),
         from abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2),
      show false,
-        from absurd (proj1_congr rep_eq) (optional::distinct a)
+        from absurd (proj1_congr rep_eq) (optional::distinct a))
 
 theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃ b, n = inr A b)
 := let pred : (proj1 (rep n) = none) ≠ (proj2 (rep n) = none) := P_rep n

src/kernel/type_checker.cpp

@@ -61,9 +61,6 @@ class type_checker::imp {
             m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU1, jst));
             return u;
         }
-        u = normalize(e, ctx, true);
-        if (is_type(u) || is_bool(u))
-            return u;
         throw type_expected_exception(env(), ctx, s);
     }
 
@@ -83,9 +80,6 @@ class type_checker::imp {
             m_uc->push_back(mk_eq_constraint(ctx, e, p, jst));
             return p;
         }
-        r = normalize(e, ctx, true);
-        if (is_pi(r))
-            return r;
         throw function_expected_exception(env(), ctx, s);
     }
 
@@ -107,9 +101,6 @@ class type_checker::imp {
             m_uc->push_back(mk_eq_constraint(ctx, e, p, jst));
             return p;
         }
-        r = normalize(e, ctx, true);
-        if (is_sigma(r))
-            return r;
         throw pair_expected_exception(env(), ctx, s);
     }
 
@@ -145,12 +136,7 @@ class type_checker::imp {
                     m_uc->push_back(mk_eq_constraint(ctx, t, p, jst));
                     t        = get_pi_body(p, a);
                 } else {
-                    t = normalize(t, ctx, true);
-                    if (is_pi(t)) {
-                        t = get_pi_body(t, a);
-                    } else {
-                        throw function_expected_exception(env(), ctx, e);
-                    }
+                    throw function_expected_exception(env(), ctx, e);
                 }
             }
         }
@@ -418,10 +404,6 @@ class type_checker::imp {
             m_uc->push_back(mk_convertible_constraint(ctx, given, expected, mk_justification()));
             return true;
         }
-        new_given    = normalize(new_given, ctx, true);
-        new_expected = normalize(new_expected, ctx, true);
-        if (is_convertible_core(new_given, new_expected))
-            return true;
         return false;
     }
 
@@ -493,10 +475,6 @@ public:
             return true;
         expr new_t1 = normalize(t1, ctx, false);
         expr new_t2 = normalize(t2, ctx, false);
-        if (new_t1 == new_t2)
-            return true;
-        new_t1 = normalize(new_t1, ctx, true);
-        new_t2 = normalize(new_t2, ctx, true);
         return new_t1 == new_t2;
     }
 
@@ -521,7 +499,7 @@ public:
         if (is_bool(t))
             return true;
         else
-            return is_bool(normalize(t, ctx, true));
+            return is_bool(normalize(t, ctx, false));
     }
 
     expr ensure_pi(expr const & e, context const & ctx, optional<metavar_env> const & menv) {

tests/lean/opaque.lean

@@ -1,5 +1,4 @@
 import macros
-import pair
 import subtype
 import optional
 using subtype

tests/lean/opaque.lean.expected.out

@@ -1,7 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
   Imported 'macros'
-  Imported 'pair'
   Imported 'subtype'
   Imported 'optional'
   Using: subtype

tests/lean/sum2.lean

@@ -72,7 +72,7 @@ theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
                       ... = some b2                           : refl (some b2))
 
 theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
-:= assume N : inl a B = inr A b,
+:= not_intro (assume N : inl a B = inr A b,
      have eq1   : inl a B = abst (pair (some a) none) (inhabl (inhabited_intro a) B),
         from refl (inl a B),
      have eq2   : inr A b = abst (pair none (some b)) (inhabl (inhabited_intro a) B),
@@ -80,7 +80,7 @@ theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
      have rep_eq : (pair (some a) none) = (pair none (some b)),
         from abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2),
      show false,
-        from absurd (proj1_congr rep_eq) (optional::distinct a)
+        from absurd (proj1_congr rep_eq) (optional::distinct a))
 
 theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃ b, n = inr A b)
 := let pred : (proj1 (rep n) = none) ≠ (proj2 (rep n) = none) := P_rep n

tests/lean/sum3.lean

@@ -72,7 +72,7 @@ theorem inr_inj {A B : (Type U)} {b1 b2 : B} : inr A b1 = inr A b2 → b1 = b2
                       ... = some b2                           : refl (some b2))
 
 theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
-:= assume N : inl a B = inr A b,
+:= not_intro (assume N : inl a B = inr A b,
      have eq1   : inl a B = abst (pair (some a) none) (inhabl (inhabited_intro a) B),
         from refl (inl a B),
      have eq2   : inr A b = abst (pair none (some b)) (inhabl (inhabited_intro a) B),
@@ -80,7 +80,7 @@ theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
      have rep_eq : (pair (some a) none) = (pair none (some b)),
         from abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2),
      show false,
-        from absurd (proj1_congr rep_eq) (optional::distinct a)
+        from absurd (proj1_congr rep_eq) (optional::distinct a))
 
 set_opaque optional false
 set_opaque subtype false