Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extensible variant types and scope escaping #6752

Closed
vicuna opened this Issue Jan 13, 2015 · 11 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Jan 13, 2015

Original bug ID: 6752
Reporter: @zoggy
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2015-01-17T04:01:34Z)
Resolution: fixed
Priority: normal
Severity: tweak
Version: 4.02.1
Target version: 4.02.3+dev
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Related to: #7152 #7313 #7401 #7414
Monitored by: @gasche @hcarty

Bug description

Here is some code for an exercise:
module Common =
struct
type 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
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

Compiling it gives an unexpectec (at least for me) error:

ocamlc -c bug.ml

File "bug.ml", line 24, 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

The indicated line is
let () = Common.extend_handle handle

I've encountered (and understood) such an error before, but not with extensible types.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 13, 2015

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 13, 2015

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 13, 2015

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).

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 14, 2015

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 17, 2015

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 :-)

@vicuna vicuna closed this Jan 17, 2015

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 17, 2015

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 19, 2015

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?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jan 19, 2015

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jun 24, 2016

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).

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Nov 4, 2016

Comment author: @gasche

Is #7401 caused by this change?

#7401

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Dec 10, 2016

Comment author: @garrigue

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.