Also, I have decided it's a silly idea because elements of a list all have to have the same type.

and also in Haskell lists are infinite, so that is probably causing the interpreter to barf working out the intermediate types.

Maybe it would work in something with a Vect n type in Idris