I just figured out why the monomorphism restriction interacts so weirdly with implicit parameters, and how to fix it. We all know that when the monomorphism restriction is turned on, the following doesn't work: let f = (<) in (f 1 2, f 'a' 'b') On the other hand, the following does work: let f = (<) in (f 'a' 'b', f 'a' 'b') Why does it work? The answer to this is non-trivial: the compiler must inspect every use of f in the body of the let statement and try to statically deduce what dictionary will be passed in each case. If the deduction succeeds in all cases and the dictionary is the same in all cases, then the compiler can safely pre-apply that dictionary, reducing f to a monotype, without changing the semantics of the program. Otherwise, it can't safely do so, and must abort with an error message. In short, a let value binding of an expression with type-class constraints is valid precisely if the compiler can reduce it to a monotype without changing the semantics of the program. Exactly the same rule should apply to implicit parameters. In the case of implicit parameters, safety is ensured if in every use of the bound variable, its implicit parameter refers to the same explicit binding of that parameter. For example, the expression let g = ?x in (g,g) should be accepted provided there is an enclosing binding of ?x, because in both uses of g the implicit parameter ?x refers to that same binding. On the other hand, an expression like let g = ?x in (g, let ?x = 1 in g) must be rejected, since it necessarily involves two calls to g. A much more important example is this: let ?x = 1 in (let g = ?x in (let ?x = 2 in g)) Here g is used just once, so it can be reduced safely. The value that should be used for the reduction is the value that is in scope where g is used (that is, 2), because that is the only way to preserve the semantics of the program. For some reason, the current implementations use ?x = 1 for the early reduction, even though this alters the semantics of the program. In fact, ?x = 1 is not even in scope at the early reduction point, since by the axiomatic semantics in the Lewis et al. paper, let ?x = 1 in (let g = ?x in (let ?x = 2 in g)) is equivalent to let g = ?x in (let ?x = 1 in (let ?x = 2 in g)) (see section 3.1, bottom left corner of the page). All implementations should be changed so that they do the right thing. There are some complications which I'll discuss in a followup message. -- Ben