<p>It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at:</p>

<ul>
<li><p>Matthieu Sozeau and Nicolas Tabareau: <a href="https://www.irif.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf" rel="noreferrer">Universe Polymorphism in Coq</a>, Interactive Theorem Proving - 5th International Conference, ITP 2014</p></li>
<li><p>Beta Ziliani &amp; Matthieu Sozeau: <a href="https://www.irif.fr/~sozeau/research/publications/A_Unification_Algorithm_for_Coq_featuring_Universe_Polymorphism_and_Overloading-ICFP15.pdf" rel="noreferrer">A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading</a>, ACM SIGPLAN International Conference on Functional Programming 2015.</p></li>
</ul>

CC BY-SA 4.0
2019-02-04T12:12:40.900Z
What if those simplifications are omitted?
Bob
CC BY-SA 4.0
2019-02-04T13:00:24.797Z
Then you get a combinatorial explosion and your computer releases [blue smoke](http://www.jargon.net/jargonfile/m/magicsmoke.html). Also, if the downvoter would care to explain the downvote, I could improve the answer. I know it's terse, but this really is not the place for a general introduction on how universe constraints are handled.
Andrej Bauer
CC BY-SA 4.0
2019-02-04T13:15:51.117Z
Assuming I have a very good ventilation and that I omit the simplifications, will a distant descendant of mine get the most general universe and constraint assignment?
Bob
CC BY-SA 4.0
2019-02-04T13:44:10.123Z
I am not entirely sure but I think there isn’t always the most general form of universe polymorphism. And even if there is one, that doesn’t mean it’s a useful thing to have. For instance the most general form may not tell you whether it’s consistent. You’d just get a bunch of constraints and it’s up to you to tell whether they’re consistent.
Andrej Bauer
CC BY-SA 4.0
2019-02-05T17:29:35.667Z
You might also want to mention "Type Checking with Universes" by Harper and Pollack; this is what Coq's algorithm is based on.
Jason Gross
CC BY-SA 4.0
2019-02-05T17:33:02.980Z
According to https://link.springer.com/chapter/10.1007/3-540-50940-2_39 "We show type synthesis is effective in CCω. Even if explicit universe levels are erased from a term it is possible to compute a “schematic type” for that term, and a set of constraints, that characterize all types of all well-typed instances of the term. "  So I suspect there is in fact a "most general" set of universes and constraints, or perhaps multiple equivalent sets.
Jason Gross
CC BY-SA 4.0
2019-02-06T06:42:35.027Z
I thought the current Coq universe polymorphisms algorithm is an extension of Harper & Pollack's algorithm. Since it uses fairly general constraints, I hesitate to just conclude there is a good notion of "most general".
Andrej Bauer
CC BY-SA 4.0
2019-02-04T10:13:12.153Z
2019-02-04T10:13:12.153Z
Andrej Bauer
<p>When making a universe polymorphic definition in Coq, universes and their constraints are automatically inferred. Are they somewhat the most general ones (in a sense similar to the principal type property in ML)? Or are they just the result of arbitrary heuristics? Or something in between?</p>

<type-theory><coq><type-inference><calculus-of-constructions><polymorphism>
Universe polymorphism: the inference of universes and their constraints
Bob
# Universe polymorphism: the inference of universes and their constraints

(Asked by: username_0 on 2019-02-04)

When making a universe polymorphic definition in Coq, universes and their constraints are automatically inferred. Are they somewhat the most general ones (in a sense similar to the principal type property in ML)? Or are they just the result of arbitrary heuristics? Or something in between?

**Tags:** type-theory, coq, type-inference, calculus-of-constructions, polymorphism


---

## 1 answers

### Answer by username_1 on 2019-02-04. Score: 5 | Accepted answer

It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at:

* Matthieu Sozeau and Nicolas Tabareau: [Universe Polymorphism in Coq](https://www.irif.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf), Interactive Theorem Proving - 5th International Conference, ITP 2014
* Beta Ziliani & Matthieu Sozeau: [A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading](https://www.irif.fr/~sozeau/research/publications/A_Unification_Algorithm_for_Coq_featuring_Universe_Polymorphism_and_Overloading-ICFP15.pdf), ACM SIGPLAN International Conference on Functional Programming 2015.

> **Comments:**
> **username_0**: What if those simplifications are omitted?  
> **username_1**: Then you get a combinatorial explosion and your computer releases [blue smoke](http://www.jargon.net/jargonfile/m/magicsmoke.html). Also, if the downvoter would care to explain the downvote, I could improve the answer. I know it's terse, but this really is not the place for a general introduction on how universe constraints are handled.  
> **username_0**: Assuming I have a very good ventilation and that I omit the simplifications, will a distant descendant of mine get the most general universe and constraint assignment?  
> **username_1**: I am not entirely sure but I think there isn’t always the most general form of universe polymorphism. And even if there is one, that doesn’t mean it’s a useful thing to have. For instance the most general form may not tell you whether it’s consistent. You’d just get a bunch of constraints and it’s up to you to tell whether they’re consistent.  
> **username_2**: You might also want to mention "Type Checking with Universes" by Harper and Pollack; this is what Coq's algorithm is based on.  
> **username_2**: According to https://link.springer.com/chapter/10.1007/3-540-50940-2_39 "We show type synthesis is effective in CCω. Even if explicit universe levels are erased from a term it is possible to compute a “schematic type” for that term, and a set of constraints, that characterize all types of all well-typed instances of the term. "  So I suspect there is in fact a "most general" set of universes and constraints, or perhaps multiple equivalent sets.  
> **username_1**: I thought the current Coq universe polymorphisms algorithm is an extension of Harper & Pollack's algorithm. Since it uses fairly general constraints, I hesitate to just conclude there is a good notion of "most general".  

---

