Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005749OCamltypingpublic2012-08-31 23:202012-10-04 13:22
Assigned To 
PlatformOSOS Version
Product Version4.00.0 
Target VersionFixed in Version 
Summary0005749: Module "includes" not equivalent to rebinding for types using first-class modules
DescriptionThe following code fails with a signature mismatch:

module type Spec = sig
  module type M = sig end
  type t = (module M) list

module Make (Spec : Spec) : sig type t = Spec.t end = struct
  include Spec
  (* type t = Spec.t *)

But commenting out "include Spec" while uncommenting the succeeding line containing the rebinding works without problems.

The compiler presumably treats the module type bound in the functor body as different from the one in the Spec-module. Since the type of first-class modules has to be the same nominally, not just structurally, this might explain the observed error message. But here the equivalence really goes beyond structure, the "include" guarantees that both module types refer to the same thing. I'm not sure, but maybe this situation can be improved?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
frisch (developer)
2012-09-03 19:21

This seems hard to fix. Within the functor's body, the include statement basically amounts to inlining:

  module type M = sig end
  type t = (module M) list

which produces a different module type name M. We would like to keep both equations "type t = (module M) list" and "type t = Spec.t", but this is not possible in the current type system.

I don't see a simple solution. At some point, it would be interesting to explore relaxing the nominal comparison of module types in package types, but I'm sure it will raise a lot of other tricky issues.

Did you find this problematic case in "real code"?
mottl (reporter)
2012-09-04 01:21

Oh well, I guess we will have to live with that until the day that some superhero rewrites the type system from scratch.

Yes, I ran into this in "real code" (experimenting with ways to represent operators on covariance functions), but it's still easy enough to work around this problem.

- Issue History
Date Modified Username Field Change
2012-08-31 23:20 mottl New Issue
2012-09-03 19:21 frisch Note Added: 0008010
2012-09-04 01:21 mottl Note Added: 0008011
2012-09-06 16:43 doligez Target Version => 4.00.1+dev
2012-09-27 14:33 doligez Severity minor => feature
2012-09-27 14:33 doligez Status new => acknowledged
2012-09-27 14:33 doligez Target Version 4.00.1+dev =>
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker