Request help with type error

Learning
1

Hi.

I have the following:

module Make_enum(X:sig type t end) = struct
  open X

  (* nts are even, tms are odd; we maintain a mapping *)
  type t_enum = {
    mutable free:int;
  }

  let make = 
    let enum = { free=0 } in 
    let somefun = fun (s:t) -> 3 in
    fun f -> f ~somefun
end 

type t' = Something

module X = struct type t = t' end

module Made = Make_enum(X)

let f = Made.make @@ fun ~somefun -> somefun

Unfortunately there is a type error in the last line (let f = …):

File "tmp.ml", line 21, characters 37-44:
Error: This expression has type t' -> int
       but an expression was expected of type 'a
       The type constructor t' would escape its scope

I don’t understand this because t’ is in scope.

On the other hand, the following is fine:

module Make_enum(X:sig type t end) = struct
  open X

  (* nts are even, tms are odd; we maintain a mapping *)
  type t_enum = {
    mutable free:int;
  }

  let make () = 
    let enum = { free=0 } in 
    let somefun = fun (s:t) -> 3 in
    fun f -> f ~somefun
end 

type t' = Something

module X = struct type t = t' end

module Made = Make_enum(X)

let f = Made.make () @@ fun ~somefun -> somefun

But I’m not sure why this is fine when the first example isn’t.

Thanks

2

BTW this is OCaml 4.04.2

3

The root cause of your issue is that you first version of make is weakly polymorphic due to the value restriction. Using 4.06 notation, its type is

     val make : (somefun:(X.t -> int) -> '_weak1) -> '_weak1

Then when you apply Made.make, the typechecker try to unify '_weak1 with t' but this is not allowed because t' was defined after the introduction of '_weak1. A simpler example of this problem can be seen in

let x = ref []
type t = A
;;
x := [A]

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

The scope error is the typechecker pointing at the fact that 'weak2 was introduced before the definition of t.

The simplest way to fix your issue might be to make make polymorphic by moving the definition of the mutable enum before the definition of make:

  let enum = { free=0 }
  let make = 
    let somefun = fun (s:t) -> 3 in
    fun f -> f ~somefun
4

Ah, OK. Thank you.

5

I think if I had seen the inferred module signature I would have spotted the weakly polymorphic type var. Your explanation makes perfect sense.

Thanks

6

For those looking at this in the future, I will point out this great article on the value restriction: https://ocamlverse.github.io/content/weak_type_variables.html

2 Likes