From cd8dc8670d8ea164544b7b241b4cedf321808958 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Oct 2018 15:51:03 -0700
Subject: [PATCH] fix(library/compiler/erase_irrelevant): visit_constant

---
 src/library/compiler/erase_irrelevant.cpp | 53 ++++++++++-------------
 1 file changed, 24 insertions(+), 29 deletions(-)

diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index 6c7b524a62..48069e35e2 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -97,35 +97,6 @@ class erase_irrelevant_fn {
         }
     }
 
-    expr visit_constant(expr const & e) {
-        lean_assert(!is_enf_neutral(e));
-        name const & c = const_name(e);
-        if (c == get_lc_unreachable_name()) {
-            return mk_enf_unreachable();
-        } else if (c == get_lc_proof_name()) {
-            return mk_enf_neutral();
-        }
-        try {
-            type_checker tc(m_st, m_lctx);
-            expr e_type = tc.whnf(tc.infer(e));
-            if (tc.is_prop(e_type) || is_sort(e_type))
-                return mk_enf_neutral();
-            else
-                return mk_constant(const_name(e));
-        } catch (kernel_exception &) {
-            return mk_constant(const_name(e));
-        }
-    }
-
-    bool is_atom(expr const & e) {
-        switch (e.kind()) {
-        case expr_kind::FVar:   return true;
-        case expr_kind::Lit:    return true;
-        case expr_kind::Const:  return true;
-        default: return false;
-        }
-    }
-
     bool is_irrelevant(expr const & e) {
         try {
             type_checker tc(m_st, m_lctx);
@@ -148,6 +119,30 @@ class erase_irrelevant_fn {
         }
     }
 
+    expr visit_constant(expr const & e) {
+        lean_assert(!is_enf_neutral(e));
+        name const & c = const_name(e);
+        if (c == get_lc_unreachable_name()) {
+            return mk_enf_unreachable();
+        } else if (c == get_lc_proof_name()) {
+            return mk_enf_neutral();
+        }
+        if (is_irrelevant(e)) {
+            return mk_enf_neutral();
+        } else {
+            return mk_constant(const_name(e));
+        }
+    }
+
+    bool is_atom(expr const & e) {
+        switch (e.kind()) {
+        case expr_kind::FVar:   return true;
+        case expr_kind::Lit:    return true;
+        case expr_kind::Const:  return true;
+        default: return false;
+        }
+    }
+
     expr visit_lambda_core(expr e, bool is_minor) {
         flet<local_ctx> save_lctx(m_lctx, m_lctx);
         buffer<expr> bfvars;