Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005863OCamltypingpublic2012-12-25 14:052013-06-28 18:12
Assigned To 
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 [^] , but that is probably not a realistic medium-term change.)
TagsNo tags attached.
Attached Files

- Relationships
related to 0005343closedgarrigue 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
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker