michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/elaborator): add extra occurs-check test

Browse source 
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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-14 19:47:27 -08:00
parent 160a8379ef
commit bdbf85405a
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/elaborator/elaborator.cpp
View file

@ -428,6 +428,10 @@ class elaborator::imp {
return assign(a, b, c, is_lhs) ? Processed : Failed; return assign(a, b, c, is_lhs) ? Processed : Failed;
} }
} else { } 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)); local_entry const & me = head(metavar_lctx(a));
if (me.is_lift()) { if (me.is_lift()) {
if (!has_free_var(b, me.s(), me.s() + me.n(), m_state.m_menv)) { if (!has_free_var(b, me.s(), me.s() + me.n(), m_state.m_menv)) {