Fix #5197, handling of algebraic universes

They were allowed to stay in terms in some cases. We now ensure that if
an evar is defined as e.g. fun x => Type@{foo}, foo is properly
refreshed to be non-algebraic as it could otherwise appear in the term
and break the invariant.

Also cleanup the implementation of refresh_universes to avoid using a
mutable reference and simply rely on the Constr.map smartmap idiom
instead.

This might have compatibility issues, e.g. in HoTT where maybe more
non-algebraic proxy universes could be generated, we'll see.

For the bug report proper, there is a lack of bidirectional
type-checking that makes the initial definition fail (there's a
non-canonical choice of dependency if we don't consider the typing
constraint). With the Program bidir hint it passes.

0 files changed, 0 insertions, 0 deletions