This is a long message about the design of implicit parameters. In particular, it is about the interaction of the monomorphism restriction with implicit parameters. This issue was discussed in the original implicit-parameter paper, but I wanted to articulate it afresh and propose some design choices Simon Question 1: can we "inherit" implicit parameters ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: f x = (x::Int) + ?y where f is *not* a top-level binding.
From the RHS of f we'll get the constraint (?y::Int). There are two types we might infer for f:
f :: Int -> Int (so we get ?y from the context of f's definition), or f :: (?y::Int) => Int -> Int At first you might think the first was better, becuase then ?y behaves like a free variable of the definition, rather than having to be passed at each call site. But of course, the WHOLE IDEA is that ?y should be passed at each call site (that's what dynamic binding means) so we'd better infer the second. Question 2: type signatures ~~~~~~~~~~~~~~~~~~~~~~~~~~~ OK, so it it legal to give an explicit, user type signature to f, thus: f :: Int -> Int f x = (x::Int) + ?y At first sight this seems reasonable, but it has the nasty property that adding a type signature changes the dynamic semantics. Consider this: (let f x = (x::Int) + ?y in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+5) vs (let f :: Int -> Int f x = x + ?y in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+6) Indeed, simply inlining f (at the Haskell source level) would change the dynamic semantics. Conclusion: the above type signature is illegal. You'll get a message of the form "could not deduce (?y::Int) from ()". Question 3: monomorphism ~~~~~~~~~~~~~~~~~~~~~~~~ There's a nasty corner case when the monomorphism restriction bites: z = (x::Int) + ?y The argument above suggests that we *must* generalise over the ?y parameter, to get z :: (?y::Int) => Int, but the monomorphism restriction says that we *must not*, giving z :: Int. Why does the momomorphism restriction say this? Because if you have let z = x + ?y in z+z you might not expect the addition to be done twice --- but it will if we follow the argument of Question 2 and generalise over ?y. Possible choices ~~~~~~~~~~~~~~~~ (A) Always generalise over implicit parameters Bindings that fall under the monomorphism restriction can't be generalised Consequences: * Inlning remains valid * No unexpected loss of sharing * But simple bindings like z = ?y + 1 will be rejected, unless you add an explicit type signature (to avoid the monomorphism restriction) z :: (?y::Int) => Int z = ?y + 1 This seems unacceptable (B) Monomorphism restriction "wins" Bindings that fall under the monomorphism restriction can't be generalised Always generalise over implicit parameters *except* for bindings that fall under the monomorphism restriction Consequences * Inlining isn't valid in general * No unexpected loss of sharing * Simple bindings like z = ?y + 1 accepted (get value of ?y from binding site) (C) Always generalise over implicit parameters Bindings that fall under the monomorphism restriction can't be generalised, EXCEPT for implicit parameters Consequences * Inlining remains valid * Unexpected loss of sharing (from the extra generalisation) * Simple bindings like z = ?y + 1 accepted (get value of ?y from occurrence sites) Discussion ~~~~~~~~~~ None of these choices seems very satisfactory. But at least we should decide which we want to do. It's really not clear what is the Right Thing To Do. If you see z = (x::Int) + ?y would you expect the value of ?y to be got from the *occurrence sites* of 'z', or from the valuue of ?y at the *definition* of 'z'? In the case of function definitions, the answer is clearly the former, but less so in the case of non-fucntion definitions. On the other hand, if we say that we get the value of ?y from the definition site of 'z', then inlining 'z' might change the semantics of the program. Choice (C) really says "the monomorphism restriction doesn't apply to implicit parameters". Which is fine, but remember that every innocent binding 'x = ...' that mentions an implicit parameter in the RHS becomes a *function* of that parameter, called at each use of 'x'. Now, the chances are that there are no intervening 'with' clauses that bind ?y, so a decent compiler should common up all those function calls. So I think I strongly favour (C). Indeed, one could make a similar argument for abolishing the monomorphism restriction altogether.