0005863: Allow contractibility annotation in abstract types interface

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005863

OCaml

OCaml typing

public

2012-12-25 14:05

2012-12-25 14:06

Reporter

gasche

Assigned To

Priority

normal

Severity

feature

Reproducibility

N/A

Status

new

Resolution

open

Platform

OS Version

Product Version

4.00.0

Target Version

later

Fixed in Version

Summary

0005863: Allow contractibility annotation in abstract types interface

Description

The 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 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.225.6241 [^] , but that is probably not a realistic medium-term change.)

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

Notes
There are no notes attached to this issue.