Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007838OCamltypingpublic2018-08-13 22:572018-08-29 12:01
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.07.0 
Target VersionFixed in Version 
Summary0007838: -principal causes assertion failure in type checker
DescriptionConsider the following code in file "":

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" will yield:

  Fatal error: exception File "typing/", 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
trefis (manager)
2018-08-22 18:00

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 [^] ).

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.
garrigue (manager)
2018-08-22 23:47

Please see [^] 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.
garrigue (manager)
2018-08-23 01:18

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.
trefis (manager)
2018-08-29 12:01 [^] has been merged on 4.07 and cherry-picked onto trunk.

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker