From d9816b6e213abb88225ef633b81625436945789b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Nov 2015 20:04:16 -0800
Subject: [PATCH] fix(library/type_context): avoid errors in the infer type
 method due to opaque constants

---
 src/library/type_context.cpp | 20 +++++++++++++++-----
 src/library/type_context.h   |  7 +++++++
 2 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 9061c109b..de1be8af9 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -118,6 +118,7 @@ type_context::type_context(environment const & env, io_state const & ios, tmp_lo
     m_ci_multiple_instances = multiple_instances;
     m_ignore_external_mvars = false;
     m_check_types           = true;
+    m_relax_is_opaque       = false;
     // TODO(Leo): use compilation options for setting config
     m_ci_max_depth       = 32;
     m_ci_trans_instances = true;
@@ -144,7 +145,11 @@ bool type_context::is_opaque(declaration const & d) const {
     if (d.is_theorem())
         return true;
     name const & n = d.get_name();
-    return m_proj_info.contains(n) || is_extra_opaque(n);
+    if (m_proj_info.contains(n))
+        return true;
+    if (m_relax_is_opaque)
+        return false;
+    return is_extra_opaque(n);
 }
 
 optional<expr> type_context::expand_macro(expr const & m) {
@@ -301,6 +306,11 @@ expr type_context::whnf(expr const & e) {
     }
 }
 
+expr type_context::relaxed_whnf(expr const & e) {
+    flet<bool> relax(m_relax_is_opaque, true);
+    return whnf(e);
+}
+
 static bool is_max_like(level const & l) {
     return is_max(l) || is_imax(l);
 }
@@ -1054,7 +1064,7 @@ expr type_context::infer_pi(expr const & e0) {
     expr e = e0;
     while (is_pi(e)) {
         expr d      = instantiate_rev(binding_domain(e), ls.size(), ls.data());
-        expr d_type = whnf(infer(d));
+        expr d_type = relaxed_whnf(infer(d));
         ensure_sort(d_type, e0);
         us.push_back(sort_level(d_type));
         expr l  = mk_tmp_local(d, binding_info(e));
@@ -1062,7 +1072,7 @@ expr type_context::infer_pi(expr const & e0) {
         e = binding_body(e);
     }
     e = instantiate_rev(e, ls.size(), ls.data());
-    expr e_type = whnf(infer(e));
+    expr e_type = relaxed_whnf(infer(e));
     ensure_sort(e_type, e0);
     level r = sort_level(e_type);
     unsigned i = ls.size();
@@ -1086,14 +1096,14 @@ void type_context::ensure_pi(expr const & e, expr const & /* ref */) {
 expr type_context::infer_app(expr const & e) {
     buffer<expr> args;
     expr const & f = get_app_args(e, args);
-    expr f_type = infer(f);
+    expr f_type    = infer(f);
     unsigned j        = 0;
     unsigned nargs    = args.size();
     for (unsigned i = 0; i < nargs; i++) {
         if (is_pi(f_type)) {
             f_type = binding_body(f_type);
         } else {
-            f_type = whnf(instantiate_rev(f_type, i-j, args.data()+j));
+            f_type = relaxed_whnf(instantiate_rev(f_type, i-j, args.data()+j));
             ensure_pi(f_type, e);
             f_type = binding_body(f_type);
             j = i;
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 730606cda..b03f30ba1 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -166,6 +166,10 @@ class type_context {
     */
     bool                            m_check_types;
 
+    /** Temporary flag to override/ignore the is_extra_opaque predicate.
+        We use it when inferring types and we want to be sure a type is Pi-type. */
+    bool                            m_relax_is_opaque;
+
     bool is_opaque(declaration const & d) const;
     optional<expr> reduce_projection(expr const & e);
     optional<expr> norm_ext(expr const & e);
@@ -422,6 +426,9 @@ public:
     /** \brief Put the given term in weak-head-normal-form (modulo is_opaque predicate) */
     expr whnf(expr const & e);
 
+    /** \brief Similar to previous method but ignores the is_extra_opaque predicate. */
+    expr relaxed_whnf(expr const & e);
+
     /** \brief Return true if \c e is a proposition */
     bool is_prop(expr const & e);