From 1395bebc44ac7bcf868c22a9417cbf16f3ee14f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Jan 2017 18:01:23 -0800 Subject: [PATCH] feat(library/type_context): avoid typing errors due to reducibility when checking types at metavariable assignment --- src/library/type_context.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index d91d76efeb..3969c5e1c4 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -1778,6 +1778,15 @@ bool type_context::process_assignment(expr const & m, expr const & v) { try { expr t1 = infer(mvar); expr t2 = infer(new_v); + /* TODO(Leo): check whether using transparency_mode::All hurts performance. + We use Semireducible to make sure we will not fail an unification step + ?m := t + because we cannot establish that the types of ?m and t are definitionally equal + due to the current transparency setting. + This change is consistent with the general approach used in the rest of the code + base where spurious typing errors due reducibility are avoided by using + relaxed_is_def_eq. */ + transparency_scope _(*this, transparency_mode::All); if (!is_def_eq_core(t1, t2)) { lean_trace(name({"type_context", "is_def_eq_detail"}), scope_trace_env scope(env(), *this);