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

Typing of recursive modules to permissive #4709

Closed
vicuna opened this issue Feb 5, 2009 · 5 comments
Closed

Typing of recursive modules to permissive #4709

vicuna opened this issue Feb 5, 2009 · 5 comments

Comments

@vicuna
Copy link

vicuna commented Feb 5, 2009

Original bug ID: 4709
Reporter: Julien Signoles
Status: confirmed (set by @garrigue on 2017-03-14T03:06:12Z)
Resolution: open
Priority: normal
Severity: minor
Platform: x86
OS: Linux Ubuntu
Version: 3.11.0
Target version: later
Category: typing
Tags: recmod
Related to: #4336

Bug description

Hello,

I guess that the following program should not be typable, but it is with ocaml 3.11.0 and 3.10.2. It was not typable with ocaml 3.10.0.

=====
module F(X:sig type t end) = struct type t = X.t end

module rec A : sig type t end = struct type t = int end
and B: sig type t = int end = F(A)

It seems that the explicit signature of A (with t abstract) is not used for typing B. Instead, that the inferred signature of A (with t = int) which is used. Thus program abstraction is broken.

Whenever I give a wrong type to the signature of B (e.g. type t = float), the program does not typed. So type safety is not broken. Ouf :).

Additional information

The given program does not compile with ocaml 3.10.0 (don't try for ocaml 3.10.1). The expected error message is given.

=====
Signature mismatch:
Modules do not match:
sig type t = A.t end
is not included in
sig type t = int end
Type declarations do not match: type t = A.t is not included in type t = int

@vicuna
Copy link
Author

vicuna commented Feb 5, 2009

Comment author: Julien Signoles

Seem to be related to the fix of bug 4336 (which was: "Recursive modules can be used to break type safety").

@vicuna
Copy link
Author

vicuna commented Mar 28, 2009

Comment author: @xavierleroy

I'm unsure how to go about this issue. I'm afraid it will stay for a while :-(

@vicuna
Copy link
Author

vicuna commented Aug 6, 2012

Comment author: @xavierleroy

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

@vicuna
Copy link
Author

vicuna commented Mar 14, 2017

Comment author: @garrigue

Disassign myself, as I'm not competent on recursive modules.
Note that soundness is not broken, so this seems to be very low priority.

@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

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