Regression with Coq 8.20: ill-typed term with universe issue

[Armael]

trafficstars

With @JulesViennotFranca and @fpottier we encountered an instance of code that works fine with Coq 8.19 and Equations 1.3+8.19, but produces an ill-typed term (due to universe issues, it seems) with Coq 8.20 and Equations 1.3.1+8.20.

Unfortunately I couldn't manage to come up with a super minimal example. I created a trimmed down branch of our development where the issue still shows here: https://github.com/JulesViennotFranca/VerifiedCatenableDeque/tree/universe_issue_8_20 . Running dune build is enough to reproduce the issue, which shows up at the end of mini.v:

File "./theory/cadeque/mini.v", line 41, characters 0-4:
Error: Illegal application: 
The term "green_buffer" of type "Type -> ckind -> Type"
cannot be applied to the terms
 "A" : "Type"
 "tlvl" : "ckind"
The 1st term has type "Type@{semi_cadeque.u1}" which should be a subtype of
 "Type@{green_buffer.u0}".

(NB: The file theory/cadeque/models.v, a dependency of mini.v, takes around 20 minutes to compile...)

[Armael]

(Any workaround that would allow our development to compile with Coq 8.20 is welcome, we really have no idea of what is going on...)

[mattam82]

Ok, on my TODO, but I've no idea when I'll get around it. Did you manage to work around it?

[Armael]

No not really, we just sticked to 8.19 for now.

[fpottier]

Just a quick note to indicate that nothing has changed on our side: we are submitting a paper on this work, which is accepted by Rocq 8.19 but rejected by Rocq 8.20. I wanted to try Rocq 9.0 but we need two packages which apparently are not available yet, namely hammer and aac-tactics.