> But consider that I think it obvious that (every)thing should cover all things, this would include instantiations of types as well as the types themselves.

> But consider that I think it obvious that (every)thing should cover all things, this would include instantiations of types as well as the types themselves. Types are there to describe the values that can be manipulated by your program. So "as well as the types themselves" is only a concern if your language can manipulate types as first-class values. And this is not so different from all the other types in your language, at this point. What property should a value hold to belong to the "everything" type, then?