Type is a builtin currently, with `Type : Type`, which makes the type system unsound. There are a couple ways of addressing that that we've explored, like the s

Type is a builtin currently, with `Type : Type`, which makes the type system unsound. There are a couple ways of addressing that that we've explored, like the standard universe polymorphism hierarchy of `Type 0 : Type 1 : Type 2 ...`, but we've also looked at more exotic solutions like whether there's actually a self-type lambda encoding of `Type` itself (which would allow for `case` matching on `Type`). Haven't quite figured it out though, so for the moment `Type : Type` is an acceptable shim while we work on getting everything else working.