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?
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, Interactive Theorem Proving - 5th International Conference, ITP 2014
Beta Ziliani & Matthieu Sozeau: A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading, ACM SIGPLAN International Conference on Functional Programming 2015.
$\begingroup$ What if those simplifications are omitted? $\endgroup$– BobFeb 4, 2019 at 12:12
$\begingroup$ Then you get a combinatorial explosion and your computer releases blue smoke. 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. $\endgroup$ Feb 4, 2019 at 13:00
$\begingroup$ 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? $\endgroup$– BobFeb 4, 2019 at 13:15
2$\begingroup$ You might also want to mention "Type Checking with Universes" by Harper and Pollack; this is what Coq's algorithm is based on. $\endgroup$ Feb 5, 2019 at 17:29
3$\begingroup$ According to 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. $\endgroup$ Feb 5, 2019 at 17:33