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
Comments
Comment author: @garrigue This is a classical "double equation problem". 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. |
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. |
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. |
The code is now accepted (as of 4.08.0+beta2). |
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:
It will fail with:
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.
The text was updated successfully, but these errors were encountered: