Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005863OCamlOCaml typingpublic2012-12-25 14:052013-06-28 18:12
Reportergasche 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.00.0 
Target VersionlaterFixed in Version 
Summary0005863: Allow contractibility annotation in abstract types interface
DescriptionThe fix to PR#5343 has the compiler safely assume that abstract types are possibly non-contractive. This has the downside of making the following example fail:

# #rectypes;;
# module Fixpoint (M : sig type 'a t end) = struct type fix = fix M.t end;;
# module Nat = Fixpoint(struct type 'a t = 'a option end);;

Since 4.00.0 this doesn't compile anymore, as "fix" is rejected because M.t is potentially non-contractive.

Could we have a way to specify in a signature that a type is contractive?

  type 'a t : contractive

(Another option would be to have a type comparison check that is robust in present of type cycles, as in http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.225.6241 [^] , but that is probably not a realistic medium-term change.)
TagsNo tags attached.
Attached Files

- Relationships
related to 0005343resolvedgarrigue ocaml -rectypes is unsound wrt module subtyping 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2012-12-25 14:05 gasche New Issue
2012-12-25 14:06 gasche Relationship added related to 0005343
2013-06-28 18:12 doligez Status new => acknowledged


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker