How do you have a type typed "Type" when implementing a programming language?
I think what you might have found in your previous researches might be a pure type system.
In a pure type system, to avoid having &quot;Type&quot; being a &quot;Type&quot; at the same level that &quot;Int&quot; is a &quot;Type&quot;, you would define another layer of &quot;Types&quot; where you would define &quot;Type&quot; as the entire first layer (and you would define this layer in the next one, and so on)
In practice, you could define your base types as &quot;types&quot;, and the next layer would be kinds. The type &quot;type&quot; would be a kind. You might also want to consider functions of types to types as another kind.