> I can't get how the following could ever be typed at compile time:
>
>  > if ... then [] else [a]
>
> Is this a 0-list or a 1-list ? do they just put an existential
> variable -> n-list ? If this is it, it seems to me that you won't be
> able to gain much information.

The type system is not rich enough to distinguish between 0-lists' and
1-list's. It is just a list.