Relax the restriction that list literals can only contain elements of type Type.

[ocharles]

The type inference rules for list literals states

Note that the above rules forbid List elements that are Types. More generally, if the element type is not a Type then that is a type error.

Is there a good reason to have this restriction? What is the problem of changing

Γ ⊢ t : T₀   Γ ⊢ T₀ : Type   Γ ⊢ [ ts… ] : List T₁   T₀ ≡ T₁
────────────────────────────────────────────────────────────
Γ ⊢ [ t, ts… ] : List T₀

to

Γ ⊢ t : T₀   Γ ⊢ [ ts… ] : List T₁   T₀ ≡ T₁
────────────────────────────────────────────────────────────
Γ ⊢ [ t, ts… ] : List T₀

?

[ocharles]

I suppose one follow-on complication is:

List is a function from a Type to another Type:

──────────────────────
Γ ⊢ List : Type → Type

Would no longer be true. Perhaps at this point we're stuck.

[Gabriella439]

@ocharles: Yeah, the only way this would work is if List became a keyword that had to be saturated with the element type instead of a built-in

[ocharles]

Well, that, or implicit arguments to specify the type of the type being applied to the list

[MonoidMusician]

what we need is ✨ universe polymorphism ✨