Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006007OCamlOCaml typingpublic2013-05-06 10:362013-05-06 14:28
Reporterfpottier 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionno change required 
PlatformLinux, MacOSOSOS Version
Product Version4.00.1 
Target VersionFixed in Version 
Summary0006007: Type-checker rejects cyclic type abbreviation even though -rectypes is activated
DescriptionThis problem concerns ocamlc -rectypes. If I define a cyclic type
abbreviation foo as follows, it is accepted:

type 'a foo = 'a foo list (* accepted *)

However, I wish to abstract away the type list, so I place this
definition in the body of a functor, which expects list as an
argument. Then, the definition is rejected by ocaml 4.00.1:

module M (X : sig type 'a list end) = struct
  type 'a foo = 'a foo X.list
  (* accepted by ocaml 3.11.2; rejected by ocaml 4.00.1 *)
end

Is this a bug or is there a good reason to reject this definition?
Thanks!
Francois.
TagsNo tags attached.
Attached Files? file icon abbrev.ml [^] (209 bytes) 2013-05-06 10:36 [Show Content]

- Relationships
child of 0005343resolvedgarrigue ocaml -rectypes is unsound wrt module subtyping 

-  Notes
(0009247)
garrigue (manager)
2013-05-06 11:37

There is indeed a good reason: we don't know whether X.list is contractive,
and if it were not, foo would not be well-founded (leading to a potential
unsoundness).
See PR#5343 for details.
(0009248)
fpottier (reporter)
2013-05-06 13:42

Hi Jacques,
I have looked at PR#5343. I understand. Indeed, unless we allow declaring
that an unknown type constructor is contractive, I do not see how
to allow this code. Too bad... Thanks for the quick reply.

- Issue History
Date Modified Username Field Change
2013-05-06 10:36 fpottier New Issue
2013-05-06 10:36 fpottier File Added: abbrev.ml
2013-05-06 11:35 garrigue Relationship added child of 0005343
2013-05-06 11:37 garrigue Note Added: 0009247
2013-05-06 11:37 garrigue Status new => resolved
2013-05-06 11:37 garrigue Resolution open => no change required
2013-05-06 11:37 garrigue Assigned To => garrigue
2013-05-06 13:42 fpottier Note Added: 0009248


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker