fix(library/compiler/erase_irrelevant): preserve builtin runtime types

`uint32` is a definition, and `type_checker::whnf` unfolds it.
To preserve the information at `erase_irrelevant`, we use a custom
`whnf_type` method that stops reduction as soon as a builtin runtime
type is found.

src/kernel/type_checker.h

@@ -65,10 +65,8 @@ private:
     optional<expr> reduce_recursor(expr const & e);
     optional<expr> reduce_proj(expr const & e);
     expr whnf_fvar(expr const & e);
-    expr whnf_core(expr const & e);
     optional<constant_info> is_delta(expr const & e) const;
     optional<expr> unfold_definition_core(expr const & e);
-    optional<expr> unfold_definition(expr const & e);
 
     bool is_def_eq_binding(expr t, expr s);
     bool is_def_eq(level const & l1, level const & l2);
@@ -133,6 +131,9 @@ public:
     /** \brief Mare sure type of \c e is a sort, and return it. Throw an exception otherwise. */
     expr ensure_type(expr const & e) { return ensure_sort(infer(e), e); }
     expr eta_expand(expr const & e);
+
+    expr whnf_core(expr const & e);
+    optional<expr> unfold_definition(expr const & e);
 };
 
 void initialize_type_checker();

src/library/compiler/erase_irrelevant.cpp

@@ -71,10 +71,27 @@ class erase_irrelevant_fn {
         return result;
     }
 
+    bool is_prop(expr const & e) {
+        return type_checker(m_st, m_lctx).is_prop(e);
+    }
+
+    expr whnf_type(expr e) {
+        type_checker tc(m_st, m_lctx);
+        while (true) {
+            expr e1 = tc.whnf_core(e);
+            if (is_runtime_builtin_type(e1))
+                return e1;
+            if (auto next_e = tc.unfold_definition(e1)) {
+                e = *next_e;
+            } else {
+                return e;
+            }
+        }
+    }
+
     expr mk_runtime_type(expr e, bool atomic_only = false) {
         try {
-            type_checker tc(m_st, m_lctx);
-            e = tc.whnf(e);
+            e = whnf_type(e);
             if (is_constant(e)) {
                 name const & c = const_name(e);
                 if (is_runtime_scalar_type(c))
@@ -88,7 +105,7 @@ class erase_irrelevant_fn {
                 return mk_app(app_fn(e), t);
             } else if (is_sort(e)) {
                 return is_zero(sort_level(e)) ? mk_Prop() : mk_Type();
-            } else if (tc.is_prop(e)) {
+            } else if (is_prop(e)) {
                 return mk_true();
             } else {
                 return mk_enf_object_type();

src/library/compiler/util.h

@@ -121,6 +121,9 @@ bool is_enf_object_type(expr const & e);
 
 /* Return true if `n` is the name of a type with builtin support in the code generator. */
 bool is_runtime_builtin_type(name const & n);
+inline bool is_runtime_builtin_type(expr const & e) {
+    return is_constant(e) && is_runtime_builtin_type(const_name(e));
+}
 
 /* Return true if `n` is the name of a type that is treated as a scalar type by the code generator. */
 bool is_runtime_scalar_type(name const & n);