|Anonymous | Login | Signup for a new account||2016-12-11 12:49 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006433||OCaml||OCaml typing||public||2014-05-19 21:31||2016-04-05 14:56|
|Target Version||4.03.1+dev||Fixed in Version|
|Summary||0006433: Wrong module type signature grabbed when using packed libraries|
|Description||I'm not sure to which extent this qualifies as a bug, but it's at least annoying behavior:|
Lets assume you want to pack several modules into a library module "Foo", e.g. module "Utils":
ocamlopt -c -for-pack Foo utils.ml
Some functionality in the packed modules may only be used internally so you may want to hide it by defining an interface file "foo.mli", which would be compiled as usual:
ocamlopt -c foo.mli
Finally, we pack and create the library "Foo":
ocamlopt -pack utils.cmx -o foo.cmx
ocamlopt -a foo.cmx -o foo.cmxa
Here is the problem: lets assume the developer wants to export everything in module "Utils". Then a seemingly elegant way to do this would be to put the following in the above-mentioned file "foo.mli":
module Utils : module type of Utils
But this has unintended consequences. If a user of library "Foo" now also defines a module "Utils" in their project, the compiler may complain that there are "inconsistent assumptions" about module "Utils".
The apparent reason is that "module type of Utils" in "foo.mli" is now being resolved using the "Utils" interface in the end user's project rather than the one in the library. This is a little strange, because if the end user doesn't define a "Utils" module, then the compiler will correctly refer to the "Utils" interface in the packed library - as intended.
I would say there is no scenario where it would make sense to interpret "module type of" in the above way. It's clear during packing what the referred to signature is.
A workaround for the library developer would be to just copy the whole signature of module "Utils" verbatim into "foo.mli", but this is obviously a cumbersome solution.
Could the semantics of name resolution in this scenario please be changed so that "module type of" refers to the correct context? Thanks!
|Tags||No tags attached.|
While I agree that this behavior is problematic, omitting the reference to Utils has some consequences.
Let's see what is happening: when compiling foo.mli, we open utils.cmi to read its signature.
As a result, utils.cmi's digest gets included in foo.cmi, hence the conflict.
The problem is that, when we compile foo.mli, we have no idea that the goal is to make
a packed module. If we're not building a packed module, the final program may contain
Utils too, and it would be strange to allow that the signature for Utils in Foo is not the real
signature of Utils.
Note also that this is only part of the problem: assume that Utils refers to Aux, which is
also part of Foo. You would expect the references to switch to Foo.Aux, but you have no way
to do that at the mli level.
However I don't see any other good solution. So the trivial one may be the right one:
when typechecking "module type of Utils", and Utils is a persistent module (i.e. a cmi),
register the dependencies of Utils but not utils.cmi itself. This makes sense, because
"module type of" does not strengthen the module type it produces, meaning that
this type is not really the type of Utils, but just something that is textually identical.
While the absence of coherence check might be surprising at times, I believe this is sound.
It seems convincing that there wouldn't be any soundness issue here, since "manual" textual substitution also solves the problem. The generated "foo.cmi" already contains all required signature information so if I understand this correctly, it should really just be a matter of not adding the utils.cmi dependency when "module type of Utils" is being used. Of course, other uses of "Utils" in the signature that do not refer to the exported "Utils"-module would still introduce such dependencies.
As you said, in other (i.e. non-packing) contexts the coherence check might still be expected even with "module type of". Maybe this could be solved by a compiler flag that indicates that compiling "foo.mli" will produce the signature of a packed module. It would be trivial for the developer to add this to the build process, but I'm not sure the extra complexity is justified.
|2014-05-19 21:31||mottl||New Issue|
|2014-05-20 04:55||garrigue||Note Added: 0011523|
|2014-05-20 04:55||garrigue||Assigned To||=> garrigue|
|2014-05-20 04:55||garrigue||Status||new => acknowledged|
|2014-05-20 04:57||garrigue||Relationship added||duplicate of 0006305|
|2014-05-20 15:28||mottl||Note Added: 0011525|
|2014-07-16 18:19||doligez||Target Version||=> 4.02.1+dev|
|2014-09-04 00:25||doligez||Target Version||4.02.1+dev => undecided|
|2014-09-14 22:42||doligez||Target Version||undecided => 4.02.2+dev / +rc1|
|2015-02-06 18:55||doligez||Target Version||4.02.2+dev / +rc1 => 4.03.0+dev / +beta1|
|2016-04-05 14:56||doligez||Target Version||4.03.0+dev / +beta1 => 4.03.1+dev|
|Copyright © 2000 - 2011 MantisBT Group|