ocamllabs/ocaml-modular-implicits — pull request #18 by yallop (2014-09-25 13:55:07+00:00)
Title: Add implicit functor arguments to the implicit environment.

The current implementation has a small asymmetry between the arguments to implicit functors and the implicit arguments to functions:

* implicit arguments to functions are drawn from the implicit environment at application sites and bound in the implicit arguments at definition sites:
```ocaml
(* val f : (implicit M:S) -> int -> unit *)
let () = f x (* M is resolved in the implicit environment here *)

let f (implicit M:S) x =
(* M is bound in the implicit environment here *)
...
```

* arguments to implicit functors are drawn from the implicit environment at application sites, but not bound in the implicit environment at
```ocaml
(* implicit functor F(N:T) : S
implicit module N : T
val f : (implicit M:S) -> int -> unit *)
let () = f x (* N is resolved in the implicit environment here *)

implicit functor F(N:T) =
struct
... (* N is NOT bound in the implicit environment here *)
```

This turns out to be slightly irritating in practice. Suppose you have a signature used to define various top-level implicits:

```ocaml
module type EQ = sig
type t
val eq : t -> t -> bool
end

val (=) : (implicit Eq:EQ) -> Eq.t -> Eq.t -> bool
```

You'll typically want to use the top-level definitions when defining implicit functors, but they're not available by default:

```ocaml
implicit functor Eq_pair(A: EQ) (B: EQ) =
struct
type t = A.t * B.t
let eq ((a1, b1) : t) (a2, b2) =
(* Error! no implicit instance for Eq with type t = A.t *)
a1 = a2 && b1 = b2
end
```

Of course, you can always add explicit implicit bindings for the functor arguments at the top of the functor body. However, I'd expect wanting the arguments in the implicit environment to be the more common case by quite some way.

This pull request changes the semantics of implicit functors so that their arguments are added to the implicit environment, as with functions.

(All this is obviated by #12. If we take *that* route, the justification for binding implicit module arguments in the implicit environment is even clearer.)