Explanation: Every ❰List❱ documents the type of its elements with a type annotation, like this: ┌──────────────────────────┐ │ [1, 2, 3] : List Integer │ A ❰List❱ of three ❰Integer❱s └──────────────────────────┘ ⇧ The type of the ❰List❱'s elements, which are ❰Integer❱s ┌───────────────────┐ │ [] : List Integer │ An empty ❰List❱ └───────────────────┘ ⇧ You still specify the type even when the ❰List❱ is empty The element type must be a type and not something else. For example, the following element types are $_NOT valid: ┌──────────────┐ │ ... : List 1 │ └──────────────┘ ⇧ This is an ❰Integer❱ and not a ❰Type❱ ┌─────────────────┐ │ ... : List Type │ └─────────────────┘ ⇧ This is a ❰Kind❱ and not a ❰Type❱ Even if the ❰List❱ is empty you still must specify a valid type You declared that the ❰List❱'s elements should have type: ↳ $txt0 ... which is not a ❰Type❱