> It just inverts the priority: instead of consistency being the default and expressivity being opt-in (as in Agda, with the `type-in-type` pragma), it is expressive by default, and consistency is an opt-in. I strongly believe that is the right way.

I'm cautiously optimistic, but skeptical. Type:Type typically makes compilation non-terminating, which is not great. Is my program just taking a long time to compile, or is it in a loop?

Also, I'm a strong believer in the adage, "you cannot add security, you must remove insecurity". A similar sentiment would seem to apply to "inconsistency".