From 38058450d465952af6cfcc24155fcfcbe802373f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Sep 2014 15:22:50 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): whnf may produce assertion
 violation if term contains free variables

---
 src/frontends/lean/elaborator.cpp | 4 ++--
 src/kernel/type_checker.h         | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 53fdbd8c5..9b037cf2a 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -136,7 +136,7 @@ elaborator_context::elaborator_context(environment const & env, io_state const &
 optional<name> is_ext_class(type_checker & tc, expr type) {
     type = tc.whnf(type).first;
     if (is_pi(type)) {
-        return is_ext_class(tc, binding_body(type));
+        return is_ext_class(tc, instantiate(binding_body(type), mk_local(tc.mk_fresh_name(), binding_domain(type))));
     } else {
         expr f = get_app_fn(type);
         if (!is_constant(f))
@@ -460,7 +460,7 @@ class elaborator {
                 type = m_elab.whnf(type).first;
                 if (!is_pi(type))
                     break;
-                type = binding_body(type);
+                type = instantiate(binding_body(type), ::lean::mk_local(m_elab.m_ngen.next(), binding_domain(type)));
                 pre  = copy_tag(m_meta, ::lean::mk_app(pre, copy_tag(m_meta, mk_strict_expr_placeholder())));
             }
             try {
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 761b3bc51..2a8e78b08 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -94,7 +94,6 @@ class type_checker {
     level_param_names const *  m_params;
 
     friend class converter; // allow converter to access the following methods
-    name mk_fresh_name() { return m_gen.next(); }
     pair<expr, expr> open_binding_body(expr const & e);
     pair<expr, constraint_seq> ensure_sort_core(expr e, expr const & s);
     pair<expr, constraint_seq> ensure_pi_core(expr e, expr const & s);
@@ -126,7 +125,7 @@ public:
 
     environment const & env() const { return m_env; }
     name_generator mk_ngen() { return m_gen.mk_child(); }
-
+    name mk_fresh_name() { return m_gen.next(); }
     /**
        \brief Return the type of \c t.