Mantis Bug Tracker
Main | My View | View Issues | Change Log | Roadmap
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007285OCamltypingpublic2016-07-06 15:282017-09-24 17:33
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version4.03.0 
Target VersionFixed in Version4.04.0 +dev / +beta1 / +beta2 
Summary0007285: Relaxed value restriction broken with principal
DescriptionIn principal mode `generalize_structure` is used for contravariant variables. However, `generalize_structure` ignores variables which have already been generalized. This means that instead of generalizing variables which occur only in covariant positions, we generalize any variable which is first encountered in a covariant position.

For example, the following code is allowed and results in a segmentation fault:

          OCaml version 4.03.0

  # #principal true;;
  # module M : sig
      type (+'a, -'b) foo
      val apply : ('a, 'b) foo -> 'b -> 'a
      val f : unit -> ('a, 'a) foo
    end = struct
      type ('a, 'b) foo = 'b -> 'a
      let apply f x = f x
      let f () =
        let r = ref None in
          fun x ->
            match !r with
            | None -> r := Some x; x
            | Some y -> r := Some x; y
    end;;
  module M :
    sig
      type (+'a, -'b) foo
      val apply : ('a, 'b) foo -> 'b -> 'a
      val f : unit -> ('a, 'a) foo
    end
  # let f = M.f ();;
  val f : ('a, 'a) M.foo = <abstr>
  # M.apply f 0;;
  - : int = 0
  # print_endline (M.apply f "World");;

  Process ocaml-toplevel segmentation fault (core dumped)

Reversing the order of the type arguments of `M.foo` gives a type error as expected, since the variable is encountered in a contravariant position first.
Tagstestsuite, typing
Attached Files

- Relationships

-  Notes
(0016042)
gasche (administrator)
2016-07-06 16:01

 A rather bad bug indeed. (Unlike some other tricky type-system bugs,) I think we could have caught this one with a slightly more proactive testing strategy, testing as much generalization behaviors as possible. Marking the issue as testsuite-related in case people are interested in working on this.
(0016044)
garrigue (manager)
2016-07-07 11:12

 Fixed in trunk by commit 9d77b26.

Part of the reason it went undetected is that -principal was not used much until recently.
And I admit that the change to generalize_contravariant was stupid (it should have come with a few tests...)
(0016045)
frisch (developer)
2016-07-07 11:56

 > it went undetected is that -principal was not used much until recently.

Has something changed recently which makes -principal easier to use, or is it an empirical observation?
(0016046)
garrigue (manager)
2016-07-07 12:06

 -principal didn't change, but it is now used for the compiler itself, giving it more visibility.

- Issue History
Date Modified Username Field Change
2016-07-06 15:28 lpw25 New Issue
2016-07-06 16:01 gasche Note Added: 0016042
2016-07-06 16:01 gasche Tag Attached: testsuite
2016-07-06 16:01 gasche Tag Attached: typing
2016-07-07 11:12 garrigue Note Added: 0016044
2016-07-07 11:12 garrigue Status new => resolved
2016-07-07 11:12 garrigue Fixed in Version => 4.04.0 +dev / +beta1 / +beta2
2016-07-07 11:12 garrigue Resolution open => fixed
2016-07-07 11:12 garrigue Assigned To => garrigue
2016-07-07 11:56 frisch Note Added: 0016045
2016-07-07 12:06 garrigue Note Added: 0016046
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:33 xleroy Status resolved => closed

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker