Anonymous | Login | Signup for a new account 2017-09-23 23:55 CEST
 Main | My View | View Issues | Change Log | Roadmap

View Issue Details  Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005514OCamltypingpublic2012-02-24 01:562017-03-14 11:30
Reporteryminsky
Assigned To
PriorityhighSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen
PlatformOSOS Version
Product Version3.12.1
Target VersionlaterFixed in Version
Summary0005514: "with module" semantics seem broken
DescriptionI just had a frustrating experience debugging some compiler errors
that came up from the use of "with module", and to me, the current
semantics of "with module" seem broken. I brought this up last year,
and it didn't get much traction, so I thought I would try again.

The short version is:

Unlike the sharing constraints from "with type", "with module" can
actually add new structure to the signature it's operating on.
This is profoundly surprising, and can lead to hard to track down
errors. It would be less surprising and easier to work with if
"with module", like "with type", only added sharing constraints.

Now for the long vesion.

Let's build up to the problem. First, we'll define a module signature
S that contains a sub-module M.

module type S = sig
module M : sig type t type s end
end

the types , I can do so by adding a sharing constraint, as follows:

module type S' = S with type M.t = int and type M.s = string

And if you do that in the top-level, you will see the following
definition for S':

module type S' = sig
module M : sig type t = int
type s = string
end
end

which is exactly what you would expect. Now this is where "let
module" comes in. "let module" lets you expose all of the type
equalities in M at once, by exposing the equalities of all the types
in one module with the types in another module N. So, we can do this:

module N = struct type t = int
type s = string
end

module type S'' = S with module M = N

And again, you get what you expect. The signature of S'' is:

module type S'' = sig
module M : sig type t = int
type s = string
end
end

The bad case is where your module M has some extra structure in it.
So, if you write:

module N = struct type t = int
type s = string
let x = 3
end

module type S''' = S with module M = N

Now, however, you'll discover that S''' is actually this interface:

module type S''' = sig
module M : sig type t = int
type s = string
val x : int
end
end

Meaning, rather than just adding some sharing constraints, we've
actually destructively modified the signature S!

It's worth noting that the OCaml manual gives no hint of the current
behavior. Here's what it says in section 6.10.4:

and S with module M = N denotes the signature

sig type t module M: (sig type u=N.u end) end
TagsNo tags attached.
Attached Files

Relationships
 related to 0005460 assigned garrigue Request: Replace/rename/remove module types has duplicate 0006140 closed frisch Semantics of "with module" constraints has duplicate 0007337 resolved gasche Unexpected behaviour of T with module M = N (to me at least) related to 0006365 closed garrigue "with module" may introduce module alias in signature, this breaks Coq