🌌 Universe Polymorphism in Rocq — impredicativity crimes and how to avoid them

Lmao, essentially yes, but there are caveats 😹

The key insight is that universe polymorphism gives local bindings for universes and constraints, so generic definitions become reusable at different levels. It provides the same kind of code reuse you get from ML-style parametric polymorphism, except the structure of the universe hierarchy is way more complex than bare polymorphic type variables.

The big gotcha when you "slam polymorphism everywhere": there's actually a performance penalty. Using polymorphism is at least linear in the number of fresh universe variables produced during a proof — benchmarks showed around a 10% increase in compilation time on the standard library when all primitive types were made polymorphic.

My actual strategy:

1. Use Polymorphic prefix selectively on definitions that genuinely need it
2. Use Monomorphic prefix for things that should have global constraints
3. Use Set Printing Universes. liberally when debugging — you need to see the @{u} annotations to understand what's happening

When you declare universe bounds explicitly, Rocq shows you exactly what constraints were generated. This makes debugging SO much easier than staring at an inconsistency error with no context.

Can we talk about impredicativity crimes specifically? Because I think OP is dancing around the real danger zone: Prop vs Set vs the Type hierarchy.

The Calculus of Inductive Constructions has Prop as an impredicative sort — you can quantify over arbitrarily large types inside Prop and the result still lives in Prop. This is what makes classical logic encodings work.

Now, the historical crime: impredicative Set. In old versions of Coq, Set was impredicative by default. Later versions made Set predicative to avoid inconsistency with classical axioms. In particular, you have to watch out when using impredicative Set with axioms of choice — combined with excluded middle or predicate extensionality, you get inconsistency.

The reason Type can't be impredicative is even more fundamental — if it were, you could encode Girard's System U in Rocq, and System U is known to be inconsistent (via Hurkens' paradox). The encoding lives at Logic/Hurkens.v in the standard library if you want to witness the crime in situ.

Adding to this: a predicative system enforces the constraint that, when an object is defined using some sort of quantifier, none of the quantifiers may ever be instantiated with the object itself. Russell's paradox is exactly what happens when you break this — "the set of all sets that do not contain themselves" is a self-referential quantification nightmare.

OK but here's the practical thing OP probably needs: the parameters vs indices trick. This bit me HARD last week.

The rule: parameters introduce ≤ constraints while constructor arguments introduce < constraints. That strict inequality is what causes the "cannot enforce X < X" crimes. Always prefer parameters when possible!

WAIT this is the thing I was missing 😱🐱 okay that actually explains SO much. I had a whole polymorphic record that was inducing strict inequalities when it didn't need to.

So I rewrote my container using cumulative inductive types and now it's actually sane:

The *u annotation means the universe u is irrelevant — so mylist@{i} A and mylist@{j} B are convertible as long as A and B are. This is exactly what I needed for my generic container! 🎉

Now I just need to understand cumulativity variance annotations (=, +, * for invariant, covariant, irrelevant) and I think I'll be set. Any resources beyond the Rocq manual?

Something I want to add to this thread about sort polymorphism, which is a newer feature and I feel like nobody talks about it.

Universe polymorphism handles Type@{u} levels, but it originally couldn't instantiate universe parameters with Prop or SProp. If you tried:

Definitions which quantify over sort qualities are called sort polymorphic. It lets you write a single definition that works uniformly across Prop, SProp, and Type universes. All sort quality variables must be explicitly bound between the two | separators in the universe declaration.

When no explicit instantiation is provided or _ is used, a temporary variable is generated — useful for local reasoning without committing to a specific sort.

Resources for OP and anyone else deep in this rabbit hole:

📖 Adam Chlipala's CPDT — Chapter on Universes — old but still accurate for the fundamentals
📄 Sozeau & Tabareau ITP 2014 — the original universe polymorphism paper for Coq
📚 Rocq Reference Manual — Polymorphic Universes — dry but comprehensive
🧵 CGPA thread on Hurkens' paradox — if you want to see what happens without predicativity constraints

Also one more practical crime to be aware of — when you mix polymorphic and monomorphic code, unification can force universe identifications that you didn't intend:

The subtle thing is that unification of a polymorphic inductive type instantiated at the same parameters but different universes will force their identification. This mainly bites you when mixing polymorphic and monomorphic code, and can always be avoided with explicit Type annotations to raise the lowest level using cumulativity.

ok i fixed my container. here's the post-mortem in case anyone finds themselves in the same situation 🐱

The original problem: I had a polymorphic record holding a monad-like structure, and I was trying to reuse it at two different universe levels in the same proof. The universe unification was forcing u1 = u2 when I needed u1 ≤ u2.

Root cause: My record had a field whose type appeared on the left of an arrow, making the universe invariant rather than covariant. One small refactor to move that to a parameter and add Cumulative fixed it completely.

Lessons:
✅ Use Set Printing Universes. first, always, before anything else
✅ Prefer parameters over constructor arguments
✅ Mark definitions as Polymorphic explicitly rather than using the global flag
✅ Watch out for invariant universes from left-of-arrow appearances
❌ Don't mix polymorphic and monomorphic code carelessly
❌ Don't use -impredicative-set unless you know exactly what you're doing

thank you everyone, this forum is the only reason i haven't abandoned formal verification for interpretive dance 🐾💜