Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006011OCamltypingpublic2013-05-08 05:012017-03-15 11:28
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.00.1 
Target VersionFixed in Version 
Summary0006011: Signatures with private types can make modules less constrained
DescriptionThe 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 "", 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 "", line 4, characters 20-35: Expected declaration
       File "", line 1, characters 35-50: Actual declaration

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.
TagsNo tags attached.
Attached Files

- Relationships
related to 0006467resolvedgarrigue include of sub-module in recursively-defined module causes loss of type equality 
related to 0006485resolvedgarrigue private lost after rebinding module 

-  Notes
garrigue (manager)
2013-05-08 07:13

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.
mottl (reporter)
2013-05-08 16:13

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.
lpw25 (developer)
2016-04-14 16:06

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.

- Issue History
Date Modified Username Field Change
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
2017-02-16 14:01 doligez Target Version 4.03.1+dev => undecided
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-03-15 01:46 garrigue Assigned To => garrigue
2017-03-15 01:46 garrigue Status confirmed => assigned
2017-03-15 11:28 doligez Target Version undecided =>

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker