Universe polymorphism in Lean backend

[dylanede]

Currently, generic parameters are generated with sort Type, and much of the Lean backend library uses Type (but not all of it - I see Type u in quite a few places). This effectively restricts what can be contained inside external type definitions to Type or Prop. Is there a particular reason for this, or could all instances of Type be replaced with Type u or even Type*?