Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007234OCamltypingpublic2016-04-19 19:302017-09-24 17:32
Reporterstedolan 
Assigned Togarrigue 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.03.0+dev / +beta1 
Summary0007234: Compatibility check wrong for abstract type constructors
Description        OCaml version 4.03.0+dev19-2016-04-15

# type (_, _) eq = Eq : ('a, 'a) eq | Neq : int -> ('a, 'b) eq
module F (T : sig type _ t end) = struct
  let f (type a) (Neq n : (a, a T.t) eq) = n
end
module M = F (struct type 'a t = 'a end)
let _ = M.f Eq;;
Segmentation fault

The 'Eq' case should not be judged impossible, and the exhaustiveness check should fail but does not. This is a regression since 4.02.3, which correctly prints an exhaustivity warning and then raises Match_failure.
TagsNo tags attached.
Attached Files

- Relationships
related to 0006992closedgarrigue Segfault from bug in GADT/module typing 

-  Notes
(0015823)
garrigue (manager)
2016-04-20 07:46

Fixed in 4.03 and trunk by commits 06a0538 and a8a5da413.

New behavior is only not to add an equation when there is a contractiveness problem, so that both this PR and PR#6992 can be solved simultaneously (i.e., error message for PR#6992 changes)

- Issue History
Date Modified Username Field Change
2016-04-19 19:30 stedolan New Issue
2016-04-20 06:42 garrigue Relationship added related to 0006992
2016-04-20 07:46 garrigue Note Added: 0015823
2016-04-20 07:46 garrigue Status new => resolved
2016-04-20 07:46 garrigue Fixed in Version => 4.03.0+dev / +beta1
2016-04-20 07:46 garrigue Resolution open => fixed
2016-04-20 07:46 garrigue Assigned To => garrigue
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:32 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker