|Anonymous | Login | Signup for a new account||2016-06-25 03:37 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006011||OCaml||OCaml typing||public||2013-05-08 05:01||2016-04-18 16:33|
|Target Version||4.03.1+dev||Fixed in Version|
|Summary||0006011: Signatures with private types can make modules less constrained|
|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:
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.
|Tags||No tags attached.|
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.
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.
|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.|
|2013-05-08 05:01||mottl||New Issue|
|2013-05-08 07:13||garrigue||Note Added: 0009255|
|2013-05-08 16:13||mottl||Note Added: 0009258|
|2013-06-18 16:09||doligez||Status||new => confirmed|
|2013-06-18 16:09||doligez||Target Version||=> 4.02.0+dev|
|2013-07-12 18:15||doligez||Target Version||4.02.0+dev => 4.01.1+dev|
|2014-05-25 20:20||doligez||Target Version||4.01.1+dev => 4.02.0+dev|
|2014-06-23 14:14||gasche||Relationship added||related to 0006467|
|2014-07-14 10:53||gasche||Relationship added||related to 0006485|
|2014-07-21 23:14||doligez||Target Version||4.02.0+dev => 4.03.0+dev / +beta1|
|2016-04-14 16:06||lpw25||Note Added: 0015740|
|2016-04-18 16:33||doligez||Target Version||4.03.0+dev / +beta1 => 4.03.1+dev|
|Copyright © 2000 - 2011 MantisBT Group|