Canonical Structures containing `Type` and algebraic universes

[Janno]

Version

8.8+alpha (and 8.7.1)

Description of the problem

The following snippet fails. I expected it to succeed (after #5368 was fixed, at least).

Set Universe Polymorphism. Unset Universe Minimization ToSet.
Structure NoProof := no_proof { np_type : Type }.
Canonical Structure NP_Type := no_proof Type. 
Check (fun np (T : np_type np) => I) _ Type.

Error message:

Error:
The term "Type@{Top.7}" has type "Type@{Top.7+1}"
while it is expected to have type "np_type@{Top.6} ?np".

[ppedrot]

This has nothing to do with universe polymorphism, the same issue arises without the flag. The problem stems from the fact that we're trying to unify the algebraic universe Type@{Top.7+1} with one that is not allowed to be algebraic, resulting in a failure. I think that some place is missing a universe refreshing, but I'm far from understanding the expected invariants in unification to pinpoint the place it starts to go wrong.

Calling @mattam82 for help, he probably know better.

[Janno]

@mattam82 did you ever manage to look at this bug? We are using our own Sort polymorphism more and more in Mtac2 and this bug is making us write out Type/Prop distinctions everywhere (as opposed to inferring them with canonical structures).

[SkySkimmer]

3d81ccd seems to fix, let's see how it does in CI/benching.

[mattam82]

It looks more like a canonical structure resolution failure to me. E.g:

Set Debug Unification.
<prompt>Coq < 27 || 0 < </prompt>Check (fun np (T : np_type np) => I) _ Type.


Type@{Top.28+1}|
np_type|ZApp(?X3)

Type@{Top.28+1}|
?X3|ZCase(fun np_type : Type@{Top.21} => np_type)

I would expect canonical structure resolution to instantiate ?3 with NP_Type and then just add an i+1 <= j constraint.