From 2e057477ef24b91104ba2b99d1edaeae2c5fb5b0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 15 Nov 2015 18:04:08 -0800
Subject: [PATCH] feat(library/blast/recursor_action): ignore type class
 instances in the recursor action

---
 src/library/blast/recursor_action.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/library/blast/recursor_action.cpp b/src/library/blast/recursor_action.cpp
index ca47ccd4c..dd38a1b65 100644
--- a/src/library/blast/recursor_action.cpp
+++ b/src/library/blast/recursor_action.cpp
@@ -23,6 +23,11 @@ optional<name> is_recursor_action_target(hypothesis_idx hidx) {
         return optional<name>(); // we don't apply recursors to equivalence relations: =, ~, <->, etc.
     if (!h->is_assumption())
         return optional<name>(); // we only consider assumptions
+    if (get_type_context().is_class(type)) {
+        // we don't eliminate type classes instances
+        // TODO(Leo): we may revise that in the future... some type classes instances may be worth eliminating (e.g., decidable).
+        return optional<name>();
+    }
     // TODO(Leo): more restrictions?
     // TODO(Leo): consider user-provided hints
     expr const & I    = get_app_fn(type);