From 026f66652611f4f99627eeff1af0765796e186fe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Dec 2013 11:22:13 -0800 Subject: [PATCH] feat(kernel/type_checker): use expression before normalization in the unification constraints generated by the typechecker Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 9796596b0..5e6736742 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -68,7 +68,7 @@ class type_checker::imp { expr B = m_menv->mk_metavar(extend(ctx, g_x_name, A)); expr p = mk_pi(g_x_name, A, B); justification jst = mk_function_expected_justification(ctx, s); - m_uc->push_back(mk_eq_constraint(ctx, r, p, jst)); + m_uc->push_back(mk_eq_constraint(ctx, e, p, jst)); return p; } throw function_expected_exception(env(), ctx, s); @@ -86,7 +86,7 @@ class type_checker::imp { return Type(); if (has_metavar(u) && m_menv && m_uc) { justification jst = mk_type_expected_justification(ctx, s); - m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst)); + m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU, jst)); return u; } throw type_expected_exception(env(), ctx, s);