From 25cb1bf6a114856a3fcb5de60a3093206199d1f4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 22 Jun 2014 14:08:54 -0700
Subject: [PATCH] fix(kernel/converter): use type_checker::scope to make sure
 we restore the cache, and remove constraints when is_def_eq fails in the
 converter

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/converter.cpp  | 15 ++++++++++++---
 src/kernel/type_checker.h | 21 +++++++++++----------
 2 files changed, 23 insertions(+), 13 deletions(-)

diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 0c31d5720..1b1a05117 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -404,6 +404,7 @@ struct default_converter : public converter {
 
         // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
         if (is_app(t_n) && is_app(s_n)) {
+            type_checker::scope scope(c);
             buffer<expr> t_args;
             buffer<expr> s_args;
             expr t_fn = get_app_args(t_n, t_args);
@@ -414,26 +415,34 @@ struct default_converter : public converter {
                     if (!is_def_eq(t_args[i], s_args[i], c, jst))
                         break;
                 }
-                if (i == t_args.size())
+                if (i == t_args.size()) {
+                    scope.keep();
                     return true;
+                }
             }
         }
 
         if (m_env.prop_proof_irrel()) {
             // Proof irrelevance support for Prop/Bool (aka Type.{0})
+            type_checker::scope scope(c);
             expr t_type = infer_type(c, t);
-            if (is_prop(t_type, c) && is_def_eq(t_type, infer_type(c, s), c, jst))
+            if (is_prop(t_type, c) && is_def_eq(t_type, infer_type(c, s), c, jst)) {
+                scope.keep();
                 return true;
+            }
         }
 
         list<name> const & cls_proof_irrel = m_env.cls_proof_irrel();
         if (!is_nil(cls_proof_irrel)) {
             // Proof irrelevance support for classes
+            type_checker::scope scope(c);
             expr t_type = whnf(infer_type(c, t), c);
             if (std::any_of(cls_proof_irrel.begin(), cls_proof_irrel.end(),
                             [&](name const & cls_name) { return is_app_of(t_type, cls_name); }) &&
-                is_def_eq(t_type, infer_type(c, s), c, jst))
+                is_def_eq(t_type, infer_type(c, s), c, jst)) {
+                scope.keep();
                 return true;
+            }
         }
 
         if (has_metavar(t_n) || has_metavar(s_n)) {
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 3db9c41df..da90d5d4f 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -67,16 +67,6 @@ class type_checker {
     buffer<constraint>         m_cs;        // temporary cache of constraints
     bool                       m_cache_cs;  // true if we should cache the constraints; false if we should send to m_add_cnstr_fn
 
-    struct scope {
-        type_checker &   m_tc;
-        unsigned         m_old_cs_size;
-        bool             m_old_cache_cs;
-        bool             m_keep;
-        scope(type_checker & tc);
-        ~scope();
-        void keep();
-    };
-
     friend class converter; // allow converter to access the following methods
     name mk_fresh_name() { return m_gen.next(); }
     optional<expr> expand_macro(expr const & m);
@@ -93,6 +83,17 @@ class type_checker {
     expr infer_type(expr const & e);
     bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst);
     extension_context & get_extension() { return m_tc_ctx; }
+public:
+    class scope {
+        type_checker &   m_tc;
+        unsigned         m_old_cs_size;
+        bool             m_old_cache_cs;
+        bool             m_keep;
+    public:
+        scope(type_checker & tc);
+        ~scope();
+        void keep();
+    };
 
 public:
     /**