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

fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints

Browse source 
This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-06 13:04:26 -08:00
parent d46cf5fdd5
commit fa03ae2a26
2 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1205,7 +1205,15 @@ class elaborator::imp {
return true;
}
if (a.kind() != b.kind() && !has_metavar(a) && !has_metavar(b)) {
// If 'a' and 'b' have different kinds, and 'a' and 'b' are not metavariables,
// and 'a' and 'b' are not applications where the function contains metavariables,
// then it is not possible to unify 'a' and 'b'.
// We need the last condition because if 'a'/'b' are applications containing metavariables,
// then they can be reduced when the metavariable is assigned
// Here is an example:
// |- (?m Type) << Type
// If ?m is assigned to the identity function (fun x, x), then the constraint can be solved.
if (a.kind() != b.kind() && !is_metavar(a) && !is_metavar(b) && !(is_app(a) && has_metavar(arg(a, 0))) && !(is_app(b) && has_metavar(arg(b, 0)))) {
m_conflict = justification(new unification_failure_justification(c));
return false;
}

6
tests/lean/elab1.lean.expected.out
View file

@ -135,7 +135,11 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
Assumed: a
Assumed: b
Assumed: H
Error (line: 20, pos: 59) failed to synthesize metavar, its type is not a proposition
Failed to solve
⊢ if ?M::0 ?M::1 ⊤ ≺ b
Normalize
⊢ ?M::0 ⇒ ?M::1 ≺ b
(line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
Failed to solve
⊢ b ≈ a
Substitution