79609938a8
Before this commit, each `isDefEq u v` invocation would fail if there were pending universe level constraints. This commit, moves the postponed universe constraints back to the `MetaM` state. It also adds the combinator ```lean withoutPostponingUniverseConstraints x ``` which executes `x` and throws an error if there are pending universe constraints. We use the combinator at `elabApp` and `elabBinders`. Without this commit, we would fail to elaborate simple terms such as ```lean Functor.map Prod.fst (x s) ``` because after elaborating `Prod.fst` and trying to ensure its type match the expected one, we would be stuck at the universe constraint: ``` u =?= max u ?v ``` Another benefit of the new approach is better error messages. Instead of getting a mysterious type mismatch constraint, we get a list of universe contraints the system is stuck at. cc @Kha
15 lines
467 B
Text
15 lines
467 B
Text
protected.lean:10:7: error: unknown identifier 'x'
|
|
sorryAx ?m : ?m
|
|
Foo.x : Nat
|
|
Foo.y : Nat
|
|
protected.lean:22:7: error: unknown identifier 'y'
|
|
sorryAx ?m : ?m
|
|
z : Nat
|
|
protected.lean:25:14: error: protected declarations must be in a namespace
|
|
protected.lean:28:14: error: unknown identifier 'f'
|
|
8
|
|
protected.lean:38:14: error: unknown identifier 'g'
|
|
protected.lean:47:6: error: unknown identifier 'g'
|
|
protected.lean:47:0: error: failed to synthesize
|
|
Lean.HasEval ?m
|
|
8
|