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:

  • $\begingroup$ What if those simplifications are omitted? $\endgroup$ – Bob Feb 4 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$ – Andrej Bauer Feb 4 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$ – Bob Feb 4 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$ – Jason Gross Feb 5 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$ – Jason Gross Feb 5 at 17:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.