From aa56578a294352c1fa8c9c329dcce1246c2b795b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 19 Mar 2019 10:18:41 -0700
Subject: [PATCH] fix(library/compiler/compiler): assertion violations

---
 src/kernel/declaration.h          |  9 +++++++--
 src/library/compiler/compiler.cpp | 13 +++++++++----
 2 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h
index 6c19f6849a..2bcbaba7de 100644
--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -458,8 +458,13 @@ public:
     names const & get_lparams() const { return to_constant_val().get_lparams(); }
     unsigned get_num_lparams() const { return length(get_lparams()); }
     expr const & get_type() const { return to_constant_val().get_type(); }
-    bool has_value() const { return is_theorem() || is_definition(); }
-    expr const & get_value() const { lean_assert(has_value()); return static_cast<expr const &>(cnstr_get_ref(to_val(), 1)); }
+    bool has_value(bool allow_opaque = false) const {
+        return is_theorem() || is_definition() || (allow_opaque && is_opaque());
+    }
+    expr const & get_value(bool allow_opaque = false) const {
+        lean_assert(has_value(allow_opaque));
+        return static_cast<expr const &>(cnstr_get_ref(to_val(), 1));
+    }
     reducibility_hints const & get_hints() const;
 
     axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(to_val()); }
diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index fa9f2acccc..45cfe67150 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -42,8 +42,9 @@ static name get_real_name(name const & n) {
 }
 
 static comp_decls to_comp_decls(environment const & env, names const & cs) {
+    bool allow_opaque = true;
     return map2<comp_decl>(cs, [&](name const & n) {
-            return comp_decl(get_real_name(n), env.get(n).get_value());
+            return comp_decl(get_real_name(n), env.get(n).get_value(allow_opaque));
         });
 }
 
@@ -143,6 +144,10 @@ bool is_main_fn_type(expr const & type) {
     }
 }
 
+static bool has_synthetic_sorry(constant_info const & cinfo) {
+    return cinfo.is_definition() && has_synthetic_sorry(cinfo.get_value());
+}
+
 environment compile(environment const & env, options const & opts, names cs) {
     if (!is_codegen_enabled(opts))
         return env;
@@ -171,9 +176,9 @@ environment compile(environment const & env, options const & opts, names cs) {
 
     for (name const & c : cs) {
         lean_assert(!is_extern_constant(env, c));
-        if ((!env.get(c).is_definition() && !env.get(c).is_opaque()) || has_synthetic_sorry(env.get(c).get_value())) {
-            return env;
-        }
+        constant_info cinfo = env.get(c);
+        if (!cinfo.is_definition() && !cinfo.is_opaque()) return env;
+        if (has_synthetic_sorry(cinfo)) return env;
     }
 
     comp_decls ds = to_comp_decls(env, cs);