From 21501ccfa4d67d0e8ded8224af332cb49fa43559 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Oct 2015 17:47:25 -0700 Subject: [PATCH] fix(library/type_inference): temporary hack for solving universe unification problems We need a better solution. It turns out the universe constraints are not as simple as we expected. --- src/library/type_inference.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/library/type_inference.cpp b/src/library/type_inference.cpp index 639c13cb4..98babd6b8 100644 --- a/src/library/type_inference.cpp +++ b/src/library/type_inference.cpp @@ -238,8 +238,8 @@ bool type_inference::is_def_eq(level const & l1, level const & l2) { } } - level new_l1 = normalize(l1); - level new_l2 = normalize(l2); + level new_l1 = normalize(instantiate_uvars(l1)); + level new_l2 = normalize(instantiate_uvars(l2)); if (ignore_universe_def_eq(new_l1, new_l2)) return true; @@ -644,8 +644,8 @@ auto type_inference::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reduct if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) { if (!is_opaque(*d_t)) { scope s(*this); - if (is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n))) && - is_def_eq_args(t_n, s_n)) { + if (is_def_eq_args(t_n, s_n) && + is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n)))) { s.commit(); return reduction_status::DefEqual; } @@ -736,8 +736,8 @@ bool type_inference::is_def_eq_core(expr const & t, expr const & s) { if (is_app(t_n) && is_app(s_n)) { scope s(*this); - if (is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n)) && - is_def_eq_args(t_n, s_n)) { + if (is_def_eq_args(t_n, s_n) && + is_def_eq_core(get_app_fn(t_n), get_app_fn(s_n))) { s.commit(); return true; }