Solution to the monomorphism restriction/implicit parameter problem

[Ben Rudiak-Gould]

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