Navigation Menu

Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

module types and type constraints #5143

Closed
vicuna opened this issue Sep 3, 2010 · 5 comments
Closed

module types and type constraints #5143

vicuna opened this issue Sep 3, 2010 · 5 comments

Comments

@vicuna
Copy link

vicuna commented Sep 3, 2010

Original bug ID: 5143
Reporter: montagu
Assigned to: @garrigue
Status: closed (set by @mshinwell on 2017-03-10T08:48:47Z)
Resolution: duplicate
Priority: normal
Severity: feature
Version: 3.12.0
Target version: later
Category: typing

Bug description

Type constraints are not stable under equivalence of module types.

Additional information

module type S1 = sig
type t
type u = t
end

module type S2 = sig
type u
type t = u
end

(* S1 and S2 are equivalent signatures, ie. S1 is included in S2 and S2 is included in S1 *)

module type S1' = S1 with type t = int
(* ok *)

module type S2' = S2 with type t = int
(* fails *)

@vicuna
Copy link
Author

vicuna commented Sep 5, 2010

Comment author: @garrigue

I'm afraid this is not a bug.
Namely, two module types can mutually convertible without
being equal.
The specification of constraints is to replace the current
manifest type with a new one. If the current manifest type
was necessary, this is bound to break something.
You can always write:
module type S2' = S2 with type t = int and type u = int

@vicuna
Copy link
Author

vicuna commented Sep 5, 2010

Comment author: montagu

No: in 3.12,
module type S2' = S2 with type t = int and type u = int

fails, whereas
module type S2' = S2 with type u = int and type t = int

is accepted.

@vicuna
Copy link
Author

vicuna commented Apr 23, 2013

Comment author: @garrigue

Indeed, but I would rather say that the problem is that the order of with constraints is relevant.
Changing this behavior would require changing the algorithm for with constraints, which I believe is part of the specification.

@vicuna
Copy link
Author

vicuna commented Mar 10, 2017

Comment author: @mshinwell

It seems like this is now a feature wish for better documentation?

@vicuna
Copy link
Author

vicuna commented Mar 10, 2017

Comment author: @mshinwell

This is in fact a duplicate of #6360

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants