|Anonymous | Login | Signup for a new account||2018-11-18 09:42 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007838||OCaml||typing||public||2018-08-13 22:57||2018-08-29 12:01|
|Target Version||Fixed in Version|
|Summary||0007838: -principal causes assertion failure in type checker|
|Description||Consider the following code in file "foo.ml":|
module Make (X : sig val f : [ `A ] -> unit end) = struct
let make f1 f2 arg = match arg with `A -> f1 arg; f2 arg
let f = make X.f (fun _ -> ())
Executing "ocaml -principal foo.ml" will yield:
Fatal error: exception File "typing/btype.ml", line 177, characters 9-15: Assertion failed
The problem will only appear with "-principal" and does not seem to exist in versions before OCaml 4.07.0.
|Tags||No tags attached.|
I had a look this afternoon and I believe this is an old bug in Ctype.copy that was uncovered by the introduction of more calls to generalize_structure in type_cases (by https://github.com/ocaml/ocaml/pull/1609/commits/d43ccfc5d48ce86202de3c7c4f58317602d6d417 [^] ).
I'm guessing (but I don't really understand that part of the code) the issue is that in the Tvariant case, we're mutating more.desc, without necessarily having saved it before (e.g. when more.desc is Tnil and partial = Some _).
I'll let someone who knows that part look into the issue further.
Please see https://github.com/ocaml/ocaml/pull/2001 [^] for a fix.
Thomas' analysis is correct.
The introduction of the partial parameter in Ctype.copy created a wrong case where more was modified without being copied (since it was not generalized).
As to why it was not triggered before, I believe this is more related to the fact that partial copy is only invoked in type_cases, and this was limited to pattern-matches containing explicit GADT constructors, or polymorphic variants both in the pattern and in the argument type, which is not the case here. In 4.07, this is called always with in principal mode.
Sorry, the analysis of why the bug didn't occur before is wrong: the condition for partial_instance has not changed, just the place where it is computed.
On the other hand I do not see how the extra generalizations in type_cases could be related to that: they only occur after the copy.
Anyway, this original code was incorrect, and I believe this is just by chance that this was not triggered before.
|https://github.com/ocaml/ocaml/pull/2001 [^] has been merged on 4.07 and cherry-picked onto trunk.|
|2018-08-13 22:57||mottl||New Issue|
|2018-08-22 18:00||trefis||Note Added: 0019312|
|2018-08-22 23:47||garrigue||Note Added: 0019313|
|2018-08-22 23:47||garrigue||Assigned To||=> garrigue|
|2018-08-22 23:47||garrigue||Status||new => confirmed|
|2018-08-23 01:18||garrigue||Note Added: 0019314|
|2018-08-29 12:01||trefis||Note Added: 0019317|
|2018-08-29 12:01||trefis||Status||confirmed => resolved|
|2018-08-29 12:01||trefis||Resolution||open => fixed|
|Copyright © 2000 - 2011 MantisBT Group|