Also, what is the inferred type of, for example f x y = x + length y ? It can be Int -> [a] -> Int [Int] -> [a] -> [Int] and neither is more general than the other. And this is a simple function.
Int -> [a] -> Int, since this is the type it will get in the original type system.
So I can't apply f to lists, but I could if I inline its body. This means that I cannot arbitrarily refactor a piece of code by moving parts of it into separate definitions: subexpressions are given some extra meanings only if they are physically placed in certain contexts. This is bad.
This is a misunderstanding. the transformation of f l y , where l :: [Int] for instance, should depend only on the type of f and not its definition. It is the call to f, not f itself, that becomes transformed. No inlining takes place.
Ah, so what uses of f are correct depends on its definition, not type! Sorry, this is way to radical.
Types exist to formalize possible ways a value can be used. HM allows to determine most general types variables in a let-block (or: of a module) before their uses, so separate compilation is possible. In your system typechecking of a function's definition is done each time it is used!
No. See above. Björn Lisper