From 43aa6eb87fd9de7c20ab28d841ca1daa1aef9352 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Nov 2016 11:44:05 -0700 Subject: [PATCH] fix(library/class): bug in whnf_pred predicate --- src/library/class.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/class.cpp b/src/library/class.cpp index 350bf12ac4..cc0cdecc27 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -186,7 +186,9 @@ environment add_instance_core(environment const & env, name const & n, unsigned class_state S = class_ext::get_state(env); type_context::tmp_locals locals(ctx); while (true) { - type = ctx.whnf_pred(type, [&](expr const & e) { return !is_constant(e) || !S.m_instances.contains(const_name(e)); }); + type = ctx.whnf_pred(type, [&](expr const & e) { + expr const & fn = get_app_fn(e); + return !is_constant(fn) || !S.m_instances.contains(const_name(fn)); }); if (!is_pi(type)) break; expr x = locals.push_local_from_binding(type);