From 4af474010a438afd7cb3c0f5b5095cc4733a31bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 4 Jul 2014 18:49:05 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): unintended use of local
 instances

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/class.cpp      | 5 +++++
 src/frontends/lean/class.h        | 2 ++
 src/frontends/lean/elaborator.cpp | 5 +++--
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp
index 97876251f..c30470335 100644
--- a/src/frontends/lean/class.cpp
+++ b/src/frontends/lean/class.cpp
@@ -95,6 +95,11 @@ environment add_instance(environment const & env, name const & n) {
     return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n));
 }
 
+bool is_class(environment const & env, name const & c) {
+    class_state const & s = class_ext::get_state(env);
+    return s.m_instances.contains(c);
+}
+
 list<name> get_class_instances(environment const & env, name const & c) {
     class_state const & s = class_ext::get_state(env);
     if (auto it = s.m_instances.find(c))
diff --git a/src/frontends/lean/class.h b/src/frontends/lean/class.h
index 7f6b3c95e..6a18e492d 100644
--- a/src/frontends/lean/class.h
+++ b/src/frontends/lean/class.h
@@ -15,6 +15,8 @@ namespace lean {
 environment add_class(environment const & env, name const & n);
 /** \brief Add a new 'class instance' to the environment. */
 environment add_instance(environment const & env, name const & n);
+/** \brief Return true iff \c c was declared with \c add_class . */
+bool is_class(environment const & env, name const & c);
 /** \brief Return the instances of the given class. */
 list<name> get_class_instances(environment const & env, name const & c);
 
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 42e4a3778..b5df409fe 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -374,7 +374,8 @@ public:
     }
 
     bool is_class(expr const & type) {
-        return !empty(get_class_instances(type));
+        expr f = get_app_fn(type);
+        return is_constant(f) && ::lean::is_class(m_env, const_name(f));
     }
 
     bool may_be_class(expr const & type) {
@@ -394,7 +395,7 @@ public:
             context ctx = m_ctx;
             justification j = mk_justification("failed to apply class instances", some_expr(m));
             auto choice_fn = [=](expr const & mvar, expr const & mvar_type, substitution const & s, name_generator const & /* ngen */) {
-                if (!is_constant(get_app_fn(mvar_type)))
+                if (!is_class(mvar_type))
                     return lazy_list<constraints>(constraints());
                 list<expr> local_insts;
                 if (m_use_local_instances) {