Anonymous | Login | Signup for a new account 2019-02-24 06:19 CET
 Main | My View | View Issues | Change Log | Roadmap

View Issue Details  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 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. 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...) 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? 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