Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0004850OCamltypingpublic2009-08-24 18:012016-03-25 16:00
Assigned To 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product Version3.11.1 
Target VersionlaterFixed in Version 
Summary0004850: Bad interaction between subtyping and recursive modules
DescriptionThe following code is accepted by the type-checker:

module X: sig
  type 'a t
  val f: int t -> unit t
end = struct
  type 'a t = {x: int}
  let f x = (x : int t :> unit t)

If one turns it into a recursive module, the type-checkers complains with:

Error: Type int t = int X.t is not a subtype of unit t = unit X.t

The problem comes from:
1) Ctype.subtype_rec expands abbreviations of type constructors with arity > 0.
2) The typing of recursive modules introduces extra type manifests to type declarations (cf "anchor" in Typemod).

I guess the problem could occur with explicit type manifest as well, but in that case the user is in control of it. I'm unsure about the correct behavior of subtyping w.r.t. type abbreviation, but I'd clearly prefer it if turning a non-recursive module definition into a recursive did not not break type-checking.

Does restricting expansion to cases where the manifest is explicitly given by the programmer seem reasonable?
Attached Files

- Relationships

-  Notes
xleroy (administrator)
2012-08-06 18:24

I've been sleeping on these PR for too long, and still have no idea how to address them. Unassigning them from myself.

- Issue History
Date Modified Username Field Change
2009-08-24 18:01 frisch New Issue
2011-05-31 16:21 doligez Status new => assigned
2011-05-31 16:21 doligez Assigned To => xleroy
2012-06-20 11:15 frisch Category OCaml general => OCaml typing
2012-07-11 14:21 doligez Target Version => 4.01.0+dev
2012-07-12 06:10 frisch Tag Attached: recmod
2012-07-31 13:36 doligez Target Version 4.01.0+dev => 4.00.1+dev
2012-08-06 18:22 xleroy Target Version 4.00.1+dev => 4.01.0+dev
2012-08-06 18:24 xleroy Note Added: 0007909
2012-08-06 18:25 xleroy Assigned To xleroy =>
2012-08-06 18:25 xleroy Status assigned => acknowledged
2013-08-12 15:47 doligez Target Version 4.01.0+dev => 4.01.1+dev
2014-05-25 20:20 doligez Target Version 4.01.1+dev => 4.02.0+dev
2014-07-31 16:10 doligez Target Version 4.02.0+dev => 4.02.1+dev
2014-09-04 00:25 doligez Target Version 4.02.1+dev => undecided
2014-09-26 17:44 doligez Target Version undecided => 4.03.0+dev / +beta1
2016-03-25 16:00 doligez Target Version 4.03.0+dev / +beta1 => later
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker