I wrote:
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.
I think what I wrote above is misleading. The "explicit" or "enclosing" binding need not be local, or even in a known location, as long as the compiler can prove that there's only one of them. And this is always possible in the case of non-local bindings. E.g.: f () = let g = ?x in (g,g) Each time f is invoked it will be passed exactly one implicit ?x. The compiler has no idea where that value was explicitly bound, but it can still prove that the two uses of g always refer to the same ?x. -- Ben