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
Comments
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"). |
Comment author: @xavierleroy I'm unsure how to go about this issue. I'm afraid it will stay for a while :-( |
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. |
Comment author: @garrigue Disassign myself, as I'm not competent on recursive modules. |
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. |
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
The text was updated successfully, but these errors were encountered: