Closed gmalecha closed 7 years ago
The main problem with switching to Set is that we will not be able to embed constants inside the language anymore unless they also live in Set
. We could generalize this to make all of the uses of Set
be something like Type@{Usyntax}
.
The conclusion of this reasoning is to make it universe polymorphic.
This is a big change. It restricts reified values to live in sort
Set
rather than an arbitraryType
. In addition to reducing the number of universes floating around, it makes universe issues arise sooner (i.e. before the terms are used). For example, it surfaced numerous issues with universe polymorphic definitions.@jesper-bengtson Any objections?