Opt-in consistency in Kind

[sbp]

Kind has a "how I learned to stop worrying and love the Type:Type" vibe. That doesn't make it invalid as a proof language. 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. It is still not implemented, but the language is completely ready for that.

— /u/LangMakers

I couldn't find any issue tracking this feature, so I thought I'd submit one. That way updates can be posted here, discussions can potentially take place, and people can more easily track the outcome. And by people I mean me ;)

[caotic123]

I agree with Victor, I would like to augment that (i am guessing here) we have no intentions to fall into some trivial inconsistency (I mean talking of the trading of consistency vs expressivity). Well, as far I know, Girard's proof is not trivial derived, and if you have no intention of writing this, so you won't easily fall into this, this is also true for a bunch of new problems (UIP+HOTT, injection...).

I am moving this to the discussion section, but @rigille might confirm this later.