metacoq Universe inconsistency with MetaCoq and stdpp

The following code gives an error with MetaCoq 1.3.1+8.17 and coq-stdpp 1.9.0

From stdpp Require gmap.
From MetaCoq.Erasure Require EWcbvEval.

This gives the error:

Universe inconsistency. Cannot enforce Basics.flip.u0 =
Coq.MSets.MSetInterface.3 because Coq.MSets.MSetInterface.3
<= Coq.Lists.List.321 <= base.MRet.u0 <= fin_maps.MapFold.u2
< Basics.flip.u0.

This behavior was introduced in #1007 and might be related to the change here https://github.com/MetaCoq/metacoq/blame/67097a400c5889c03fd1f3f232b75d5391031a25/pcuic/theories/PCUICConfluence.v#L1426

Jun 17 '24 21:06 4ever2

@yannl35133 made that PR, so he may have some insights here...

Jun 21 '24 14:06 spitters

This https://github.com/MetaCoq/metacoq/commit/fa4b728f2ecd74f7503d682bccfe31facc8d7747 commit fixes the issue. Thanks for the help. I see that the commit was not included in the 1.3.2 release. This issue is blocking upgrading a few of our projects, so any chance that it can be included in the next release?

Sep 03 '24 10:09 4ever2

Sorry for missing this, the fix is now in all the branches and will be part of the next release.

Sep 03 '24 11:09 mattam82

Thanks @mattam82 for the prompt response!

Sep 03 '24 12:09 spitters