From 088b0fb79519c2d41b28a997a67ea3c0f96e62c1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Oct 2015 12:36:46 -0700 Subject: [PATCH] fix(library/class_instance_resolution): relax has_expr_metavar test at mk_choice --- src/library/class_instance_resolution.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp index 31ab1ab17..7f6072794 100644 --- a/src/library/class_instance_resolution.cpp +++ b/src/library/class_instance_resolution.cpp @@ -973,8 +973,12 @@ struct cienv { mlocal_type(m_main_mvar)); } expr mvar_type = instantiate_uvars_mvars(mlocal_type(mvar)); - if (has_expr_metavar(mvar_type)) + if (has_expr_metavar_relaxed(mvar_type)) { + // Remark: we use has_expr_metavar_relaxed instead of has_expr_metavar, because + // we want to ignore metavariables occurring in the type of local constants occurring in mvar_type. + // This can happen when type class resolution is invoked from the unifier. return false; + } auto cname = is_class(mvar_type); if (!cname) return false;