Comment author: @zoggy

Adding a type annotation in the Common module:

let (q : msg Queue.t) = Queue.create ()

solves the problem. The error message is quite confusing, though.

Comment author: @gasche

I believe there is a bug in the type-checker: it seems to believe that Common.handle_msg is defined before Common.msg, and thus understand the unification of handle_msg's weak variable with Common.msg as a scope escape.

Your workaround is correct (it removes the weak variable: pass Common's definition to a toplevel and you'll see it), you could also simply write in handle_msg's definition (fun (_ : msg) -> ...).

The reason why I believe the type-checker is wrong about the ordering is that the following variant, which is careful to define the extensible type outside the Common module, does not fail:

module A = struct type msg = .. end

module Common =
  struct
    type msg = A.msg = ..

    let handle_msg = ref (fun _ -> failwith "Unable to handle message")
    let extend_handle f =
    let old = !handle_msg in
    handle_msg := f old

    let q = Queue.create ()
    let add msg = Queue.add msg q
    let handle_queue_messages () = Queue.iter !handle_msg q
  end

module M1 =
  struct
    type Common.msg += Reload of string | Alert of string

    let handle fallback = function
      Reload s -> print_endline ("Reload "^s)
    | Alert s -> print_endline ("Alert "^s)
    | x -> fallback x

    let () = Common.extend_handle handle
    let () = Common.add (Reload "config.file")
    let () = Common.add (Alert "Initialisation done")
  end

Comment author: @lpw25

This is not related to extensible variants, the same thing happens for regular variants:

module Common =
  struct
    type msg = Msg

    let handle_msg = ref (function _ -> failwith "Unable to handle message")
    let extend_handle f =
    let old = !handle_msg in
    handle_msg := f old

    let q = Queue.create ()
    let add msg = Queue.add msg q
    let handle_queue_messages () = Queue.iter !handle_msg q
  end

module M1 =
  struct
    let handle fallback = function
      Common.Msg -> print_endline ("Msg")

    let () = Common.extend_handle handle
    let () = Common.add (Reload "config.file")
    let () = Common.add (Alert "Initialisation done")
  end

gives the error:

File "test.ml", line 20, characters 34-40:
Error: This expression has type (Common.msg -> unit) -> Common.msg -> unit
       but an expression was expected of type
         (Common.msg -> unit) -> Common.msg -> unit
       The type constructor Common.msg would escape its scope

Nor do I think it is a bug in the type-checker. It is simply a more involved example of:

# let x = ref [];;
val x : '_a list ref = {contents = []}

# type t = T;;
type t = T

# x := [T];;
Characters 6-7:
  x := [T];;
        ^
Error: This expression has type t but an expression was expected of type t
       The type constructor t would escape its scope

You have a monomorphic type variable and you are unifying it with a type which is defined after the monomorphic type variable was created.

It looks odd in this case because t is defined before handle_msg (which creates the monomorphic type variable). However, you are unifying the variable with Common.t not t, and Common.t is defined when Common is defined (i.e. after the definition of handle_msg).

Comment author: @garrigue

Note first that there is a simple workaround:
let q : msg Queue.t = Queue.create ()

Whether this is a bug or not is not completely clear to me: we would like it to work for principality, but non-generalized type variables already break principality at times.

Comment author: @garrigue

Fixed in trunk at revision 15783.

The fix is to create the identifier for the module before typing it, so that references inside the module are recognized as being created after it.
I think this is sound, but I didn't check the proof :-)

Comment author: @yallop

I'm not sure about creating the module identifier in advance. It seems that we end up with invalid signatures, at least with the current implementation:

$ cat m.ml
module M = struct
let x = ref None
type t = T
end

let () = M.x := Some M.T
$ ocamlc -i sound.ml
module M : sig val x : M.t option ref type t = T end

Comment author: @garrigue

Good point. However, this is only one case of such signatures, and this is not unsound. Do you see any case where this use of references could cause unsoundness?

Comment author: @yallop

I'm not sure I understand the original purpose of the restriction. Would it be unsound in general to allow unification with types that are defined later in a file?

I thought that the restriction was to prevent ill-formedness rather than unsoundness, but I could well be mistaken. I don't see that there's anything about the case of types defined within a named module that warrants special treatment, though.

Comment author: @garrigue

After a private discussion with Alain Frisch and Nicolas Ojeda Bar, it appears that Jeremy's concerns are not purely theoretical: there are practical use cases where well-formedness is required (i.e., to generate type witnesses).

So I reverted to strict scoping in commit e85ba9c.
Fortunately, the only release including the relaxed scoping rule is 4.03.0, which should be short lived.
It is easy to fix the problem in the code by adding a type annotation.

Also note that this does not mean reverting the original commits: I have a feeling that the original behavior only worked by chance (cf #7152).

Comment author: @gasche

Is #7401 caused by this change?

#7401

Comment author: @garrigue

See #7414 for an example of why we need to be stricter.