Hello, it's been a couple of months since this was submitted to the committee, so I'd be interested to get some feedback. In summary, this proposal introduces a mechanism for defining new kinds without having to promote a datatype, thus avoiding pollution of the value level name space with unused constructors. This is not a particularly new idea, and folks have been asking for it for at least 6 years now (e.g., see #6024). A few of our projects at work make use of a lot of type-level indexing (using GATs, etc.) and while things mostly work pretty well, the clunkiness of having to promote datatypes when you just want to define a new kind is something that keeps popping up over and over again, which is why I was motivated to submit the proposal. Thoughts? -Iavor