Why can't OCaml infer the following type:

Question

Consider the following code

module type Foo = sig 
  type t
  val do_with_t : t -> unit
end

let any_foo t (module F : Foo) = F.do_with_t t

Which is rejected with the following lovely type error:

Error: This expression has type F.t but an expression was expected of type F.t
      The type constructor F.t would escape its scope

But is accepted once I add the following type annotion:

let any_foo (type s) (t:s) (module F : Foo with type t = s) = F.do_with_t t

The sharing constraint makes sense to me so my question is why can't OCaml infer the type signature from my usage of t inside the function.

Answer 1

I'm no expert, but here is my take on this.

The real error is the last bit of the message:

The type constructor F.t would escape its scope

To understand the error message, lets first rewrite any_foo without pattern matching the argument, and renaming the argument to make the explanation easier to follow:

let any_foo arg foo = 
  let (module F : Foo) = foo in
    F.do_with_t arg

You are using first class modules here, and are unpacking the variable foo into a new module F, in the scope of that let statement.

Now lets consider the type of the argument arg that can be inferred from this fact. Clearly, the type is F.t, but critically this is a type that is only known in the current scope, because module F is only known in the current scope.

Now lets attempt to define the type of the resulting any_foo function:

val any_foo : F.t -> (module Foo) -> unit

And there is your problem, you are trying to expose the newly minted type F.t from deep within the function scope. In other words, you are expecting the caller to know the type that only exists inside your function. Or, to put it another way, you are expecting the type F.t to "escape" its scope to a wider audience.

The solution, explained

Now that we know the problem, we can recognize the need to explain to the compiler that this type exists in the "outside" scope, and that the argument arg is of that type.

In other words, we need to add a constraint to our newly minted module F to say that the type of the argument arg is equal to the type t inside our new module F. For that we can use a locally abstract type.

Continuing with the same function, we can add a locally abstract type a, and constrain the module F with it:

let (type a) any_foo arg foo = 
  let (module F : Foo with type t = a) = foo in
    F.do_with_t arg

Lets consider the type of any_foo now.

val any_foo : 'a -> (module Foo with type t = 'a) -> unit

No problems there.

For completeness, lets return to our pattern matching version:

let (type a) any_foo arg (module F : Foo with type t = a) =
  F.do_with_t arg

Answer 2

This does not really answer your question, but in your case you just need to introduce a fresh type variable s:

let any_foo (type s) t (module F : Foo with type t = s) = F.do_with_t t

i.e. you don't need (t:s) as the type inference will work fine here.