From d9afb3ca9643c412da330816d4c3dadd4383f113 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Sep 2014 19:09:18 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): missing constraint --- src/frontends/lean/elaborator.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7eb9c0d51..d4573946b 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -781,11 +781,13 @@ public: f_type = whnf(f_type, cs); if (!is_pi(f_type) && has_metavar(f_type)) { constraint_seq saved_cs = cs; - f_type = whnf(f_type, cs); - if (!is_pi(f_type) && is_meta(f_type)) { + expr new_f_type = whnf(f_type, cs); + if (!is_pi(new_f_type) && is_meta(new_f_type)) { cs = saved_cs; // let type checker add constraint f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs); + } else { + f_type = new_f_type; } } if (!is_pi(f_type)) {