Perhaps it's best to say that for the time being, they should regard polymorphic expressions like [] as either one symbol denoting different values of different types or one value having many types, whichever they feel more comfortable with.
I would like to be able to say that [ ] is one symbol denoting different values of different types and that the compiler picks which value it denotes given the context. But the example program disallows that--which is how I came up with the example in the first place. let xs = [] ys = 1:xs zs = 'a': xs in ... xs is not bound to a value with a concrete type (like [Int] or [Char]) at compile time. Even after compilation xs :: [a]. To say that [ ] is a value having many different types seems to be saying more or less the same thing, namely that compilation doesn't pick a particular concrete type. So what are the other options? I still like the idea of saying that [ ] is a function that takes a type as an argument and generates a value. (I believe this was your explanation at one point.) I realize that it isn't a function at the Haskell level. But it makes intuitive sense to say that the compiler generates such a function, which is what is bound to xs. It is that function that gets executed when the program is run. I know that for optimization purposes it may be compiled down past that interpretation and I also know that this function isn't a Haskell function. But if one were giving an operational semantics for what's going on (which I guess is what the Core effectively is) that seems to be the most transparent explanation.