0004850: Bad interaction between subtyping and recursive modules

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0004850

OCaml

OCaml typing

public

2009-08-24 18:01

2012-08-06 18:25

Reporter

frisch

Assigned To

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

acknowledged

Resolution

open

Platform

OS Version

Product Version

3.11.1

Target Version

4.01.0+dev

Fixed in Version

Summary

0004850: Bad interaction between subtyping and recursive modules

Description

The 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)
end

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?

Tags

recmod

Attached Files

Relationships

Notes
(0007909) 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