From 8142726923f4bdba628a76b380ff11d897c8ebb8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Oct 2013 15:41:22 -0700 Subject: [PATCH] fix(type_inferer): bug when inferring the type of free variables Signed-off-by: Leonardo de Moura --- src/library/type_inferer.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index ffb2666e3..d1bb6ee99 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -119,9 +119,12 @@ class type_inferer::imp { break; } case expr_kind::Var: { - context_entry const & ce = lookup(ctx, var_idx(e)); - if (ce.get_domain()) - return ce.get_domain(); + auto p = lookup_ext(ctx, var_idx(e)); + context_entry const & ce = p.first; + if (ce.get_domain()) { + context const & ce_ctx = p.second; + return lift_free_vars(ce.get_domain(), ctx.size() - ce_ctx.size()); + } // Remark: the case where ce.get_domain() is not // available is not considered cheap. break;