The paper makes the (somewhat radical) case for not generalising local bindings at all; which would at a stroke remove most of the issues of the MR. (We'd still need to think about the top level.)
We'd love to know what any of you think of the idea.
I read the paper (except section 5 which is very technical). I like that it makes (let x = ... in ...) behave the same as (\x -> ...) (...) . Understanding how to respond to type inference and error messages is hard enough without having additional differences in innocent-looking code. Do you think my hope is reasonable that not-generalizing could lead to better error messages? I don't quite understand the issues[*], but I suspect that not-generalizing would at least make *me* less confused when fixing error messages because there are fewer different typechecker behaviors to think about. I guess it's still possible to use explicit type-signatures to make let-bindings polymorphic, in a way that is difficult or impossible for lambda or case? (I guess for lambda, it would require making the lambda into a rank-2 function, though I'm not sure how to do that syntactically.) [*] e.g., the gmapT / rank-2 example confuses me; would it work if (...blah...) were passed directly to gmapT without the let? Also, does it happen to solve the 2^n worst-case typechecking? -Isaac