From bdbf85405a0e251908c248a771d10f84c58b6027 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Dec 2013 19:47:27 -0800 Subject: [PATCH] feat(library/elaborator): add extra occurs-check test The idea is to catch the inconsistency in constraints such as: ctx |- ?m[inst:0 v] == fun x, ?m a x Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index d92a03db60..77e82bdac5 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -428,6 +428,10 @@ class elaborator::imp { return assign(a, b, c, is_lhs) ? Processed : Failed; } } else { + if (!is_metavar(b) && has_metavar(b, a)) { + m_conflict = justification(new unification_failure_justification(c)); + return Failed; + } local_entry const & me = head(metavar_lctx(a)); if (me.is_lift()) { if (!has_free_var(b, me.s(), me.s() + me.n(), m_state.m_menv)) {