Oh perhaps I'm not being specific enough. Apologies mate. > If we know this at compile time, because L is a quoted list literal, we have the strongest possible

Oh perhaps I'm not being specific enough. Apologies mate. > If we know this at compile time, because L is a quoted list literal, we have the strongest possible information about what it is, even more precise than most type information. By '(x y z) I'm assuming that it's not a quoted list literal but a let's say list generated by a function at compile time. Where x, y, and z could be of different types like ('(2.5 7) 6 "hello"). It's very hypothetical, and the contents of the list generated cannot possibly be known at compile time. > ... then you're talking about a completely different language that isn't one of the mainstream Lisps. At best a very oddball dialect. And yes, what I'm talking about is building a toy lisp between an ML language and a Lisp to see how much Lispyness you have to trade off for the static typing and the type inference of an ML language. The definition of oddball! In OCaml for example which has static typing and type inference you can't just have a "symbol". Even though symbols are a basic part of Lisp, you can't have really strong type inference for a "symbol" despite it being a fundamental type in the language as for strong type inference you would want to do stuff like have separate operators for adding integers and adding floating point numbers. This is very important for HM's algorithm w, similarly - in that case, car needs to be able to take one type, and return one type for it to comply with algorithm w. I'm trying to see if other people had ever tried implementing something like this. Anyway, great conversation! I think DonaldFisk helped me out already, but thanks!