0005343: ocaml -rectypes is unsound wrt module subtyping - MantisBT

Mantis Bug Tracker

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0005343

OCaml

OCaml general

public

2011-08-19 12:18

2013-05-06 11:35

Reporter

garrigue

Assigned To

garrigue

Priority

normal

Severity

minor

Reproducibility

always

Status

resolved

Resolution

fixed

Platform

OS

OS Version

Product Version

3.12.1

Target Version

Fixed in Version

4.01.0+dev

Summary

0005343: ocaml -rectypes is unsound wrt module subtyping

Description

The following example should not be accepted...

module M : sig
  type 'a t
  type u = u t and v = v t
  val f : int -> u
  val g : v -> bool
end = struct
  type 'a t = 'a
  type u = int and v = bool
  let f x = x
  let g x = x
end;;

# let h x = M.g (M.f x);;
val h : int -> bool = <fun>
# h 3;;
- : bool = <unknown constructor>

Tags

No tags attached.

Relationships

parent of	0006007	resolved	garrigue	Type-checker rejects cyclic type abbreviation even though -rectypes is activated
related to	0005863	new		Allow contractibility annotation in abstract types interface

Notes
(0006218) garrigue (manager) 2011-12-10 03:52	Fixed in trunk. Leave 3.12 alone, as the problem is minor (hard to trigger by error), and this may break some programs.

(0008549) garrigue (manager) 2012-12-02 03:51	Fixed again in trunk, revision 13107. Abstract types in the current module were assumed to be contractive, which is not true in the case of signatures. Still think about making them contractive if they were not defined in the signature, but an outer implementation.

Issue History
Date Modified	Username	Field	Change
2011-08-19 12:18	garrigue	New Issue
2011-12-10 03:10	garrigue	Assigned To	=> garrigue
2011-12-10 03:10	garrigue	Status	new => assigned
2011-12-10 03:52	garrigue	Note Added: 0006218
2011-12-10 03:52	garrigue	Status	assigned => resolved
2011-12-10 03:52	garrigue	Fixed in Version	=> 3.13.0+dev
2011-12-10 03:52	garrigue	Resolution	open => fixed
2012-09-25 20:07	xleroy	Status	resolved => closed
2012-12-02 03:51	garrigue	Note Added: 0008549
2012-12-02 03:51	garrigue	Status	closed => resolved
2012-12-02 03:51	garrigue	Fixed in Version	3.13.0+dev => 4.01.0+dev
2012-12-25 14:06	gasche	Relationship added	related to 0005863
2013-05-06 11:35	garrigue	Relationship added	parent of 0006007

Copyright © 2000 - 2011 MantisBT Group