Solution to the monomorphism restriction/implicit parameter problem

[Ben Rudiak-Gould]

Complications:

  * In my examples it's easy to tell whether all uses of the implicit
    parameter refer to the same explicit binding, but it may be difficult
    when recursion is involved. This problem has already arisen in the
    case of type class constraints, and has been solved, so I'm confident
    it can be solved for implicit parameters too. Unfortunately, the two
    cases are not quite the same:

        f :: (Num a) => a -> b
        f x = f (x+1)
        g :: (?x :: Int) -> b
        g = g {?x = ?x+1}

    Here all calls of f use the same implicit argument, but calls of g use
    different ones.

  * It might be harder to pre-apply the implicit value if it's not in
    scope at the early application point, as in:

        let g = ?x in ([deeply nested expr...] let ?x = [...] in g)

    But referential transparency means that it can always be done; it's
    just tricky.

  * It's not really necessary for safety that all uses of the implicit
    parameter refer to the same explicit binding; they just need to refer
    to the same value. So this could be accepted:

        let ?x = 1 in (let g = ?x in (g, let ?x = 1 in g))

    even though it would be rejected if one of the 1s were changed to
    something else. Cases like this would be rare, though, and it's not
    clear that programs of this type should really be accepted anyway,
    since the safety is rather fragile.

None of these complications threatens the overall validity of the
monomorphism restriction, because the algorithm on which the monomorphism
restriction is based is heuristic anyway: the only requirement is that
when it says a reduction is safe, it mustn't be wrong. If the complicated
cases end up being too complicated, it's perfectly acceptable to give up
and say they're unsafe.

This one is a slightly different story:

  * Pre-application might introduce space leaks. My intuition says to
    ignore this issue, because (1) let-abstraction always has the
    potential of introducing space leaks, and (2) Even if you explicitly
    write something like "length [1..1000000] + length (tail [1..1000000])"
    the compiler is allowed to combine the two lists without telling you,
    even though this introduces a space leak.


-- Ben