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 |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| playground | ||
| plugin | ||
| .gitignore | ||
| common.sh | ||