Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006752OCamltypingpublic2015-01-13 10:292016-12-10 02:56
Reporterguesdon 
Assigned Togarrigue 
PrioritynormalSeveritytweakReproducibilityhave not tried
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.02.1 
Target Version4.02.3+devFixed in Version4.03.0+dev / +beta1 
Summary0006752: Extensible variant types and scope escaping
DescriptionHere 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.
TagsNo tags attached.
Attached Files

- Relationships
related to 0007152closedgarrigue A typing equality is lost in 4.03 branch compared to 4.02.3 
related to 0007313assignedgarrigue Typing regression between 4.03 and 4.04 branch with signature coercion. 
related to 0007401closedgarrigue regression in type inference with 4.04.0+beta2 
related to 0007414resolvedgarrigue Soundness bug with non-generalized type variable and functors 

-  Notes
(0013067)
guesdon (manager)
2015-01-13 10:34

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.
(0013070)
gasche (developer)
2015-01-13 10:49

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
(0013075)
lpw25 (developer)
2015-01-13 12:37

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`).
(0013091)
garrigue (manager)
2015-01-14 05:16

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.
(0013132)
garrigue (manager)
2015-01-17 05:01

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 :-)
(0013135)
yallop (developer)
2015-01-17 13:25

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
(0013141)
garrigue (manager)
2015-01-19 07:18

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?
(0013146)
yallop (developer)
2015-01-19 17:03

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.
(0015995)
garrigue (manager)
2016-06-24 10:50

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 PR#7152).
(0016518)
gasche (developer)
2016-11-04 16:59

Is 0007401 caused by this change?

  https://caml.inria.fr/mantis/view.php?id=7401 [^]
(0016946)
garrigue (manager)
2016-12-10 02:56
edited on: 2016-12-10 02:57

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


- Issue History
Date Modified Username Field Change
2015-01-13 10:29 guesdon New Issue
2015-01-13 10:34 guesdon Note Added: 0013067
2015-01-13 10:34 guesdon Severity major => tweak
2015-01-13 10:49 gasche Note Added: 0013070
2015-01-13 12:37 lpw25 Note Added: 0013075
2015-01-14 00:18 doligez Status new => feedback
2015-01-14 00:18 doligez Target Version => 4.02.3+dev
2015-01-14 05:16 garrigue Note Added: 0013091
2015-01-17 05:01 garrigue Note Added: 0013132
2015-01-17 05:01 garrigue Status feedback => resolved
2015-01-17 05:01 garrigue Fixed in Version => 4.03.0+dev / +beta1
2015-01-17 05:01 garrigue Resolution open => fixed
2015-01-17 05:01 garrigue Assigned To => garrigue
2015-01-17 13:25 yallop Note Added: 0013135
2015-01-19 07:18 garrigue Note Added: 0013141
2015-01-19 17:03 yallop Note Added: 0013146
2016-06-23 01:30 garrigue Relationship added related to 0007152
2016-06-24 10:50 garrigue Note Added: 0015995
2016-08-03 00:52 garrigue Relationship added related to 0007313
2016-11-04 16:59 gasche Note Added: 0016518
2016-11-04 16:59 gasche Relationship added related to 0007401
2016-12-10 02:55 garrigue Relationship added related to 0007414
2016-12-10 02:56 garrigue Note Added: 0016946
2016-12-10 02:56 garrigue Note Edited: 0016946 View Revisions
2016-12-10 02:57 garrigue Note Edited: 0016946 View Revisions
2017-02-23 16:45 doligez Category OCaml typing => typing


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker