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

Signatures with private types can make modules less constrained #6011

Closed
vicuna opened this issue May 8, 2013 · 4 comments
Closed

Signatures with private types can make modules less constrained #6011

vicuna opened this issue May 8, 2013 · 4 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented May 8, 2013

Original bug ID: 6011
Reporter: @mmottl
Assigned to: @garrigue
Status: assigned (set by @garrigue on 2017-03-15T00:46:05Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.00.1
Category: typing
Related to: #6467 #6485
Monitored by: @mmottl

Bug description

The following code behaves in a very unintuitive way that seems like a bug:

module FA (U : sig end) : sig type t = private int end = struct type t = int end
module FB (U : sig end) = FA (U)
(* module FB (U : sig end) : sig type t = private int end = FA (U) *)
module M : sig type t = private int end = FB (struct end)

It will fail with:

File "foo.ml", line 4, characters 42-57:
Error: Signature mismatch:
       Modules do not match:
         sig type t end
       is not included in
         sig type t = private int end
       Type declarations do not match:
         type t
       is not included in
         type t = private int
       File "foo.ml", line 4, characters 20-35: Expected declaration
       File "foo.ml", line 1, characters 35-50: Actual declaration
EXIT STATUS 2

However, using the commented-out definition of functor FB instead of the previous one will make the file pass the type checker. This is weird, because adding a signature should make a module more constrained, not less so.

It seems that without "type t = private int" acting as a reminder in the definition of FB, the compiler will forget about it and treat type t as fully abstract from then on, even though it shouldn't be.

@vicuna
Copy link
Author

vicuna commented May 8, 2013

Comment author: @garrigue

This is a classical "double equation problem".
When strengthening the type of FB, one can choose either "type t = private int" or "type t = FA(U).t".
In general the second one is better, since it keeps the equation with FA.
However, if you apply FB to an unnamed module, you have to discard the equation, and you end up with less information than "private int".
I suppose one could also fall back to "private int" when discarding the equation. However, this would still be fragile, and I suppose I need a full soundness proof before doing that...

By the way, if you don't care about applicative functor, you can force choosing "private int" by using the option -no-app-funct. It is known to solve typing problems such as this one.

@vicuna
Copy link
Author

vicuna commented May 8, 2013

Comment author: @mmottl

Ah, indeed, I should have seen this. It's been a long time since I last ran into this kind of issue. The presence of the private type confused me about the true nature of the problem. The simplest workaround (simpler than adding signatures) is to just bind "struct end" to a module name and substitute that in the functor argument. This is good enough for me.

It seems to me that it should be possible to keep the equation "type t = private int", because the right hand side of this type equation contains types only that were defined outside of U (and hence FA (U)). Not sure this condition is always sufficient. Assuming this improvement is sound, I wouldn't be surprised if it could prevent most practical occurrences of this problem.

@vicuna
Copy link
Author

vicuna commented Apr 14, 2016

Comment author: @lpw25

This issue keeps coming up, and always confuses people. Can we just fall back to "private int" in this case? It seems obviously sound since X = Y & Y > Z clearly implies that X > Z.

@yallop
Copy link
Member

yallop commented Apr 5, 2019

The code is now accepted (as of 4.08.0+beta2).

@yallop yallop closed this as completed Apr 5, 2019
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

3 participants