Module "includes" not equivalent to rebinding for types using first-class modules #5749

vicuna · 2012-08-31T21:20:03Z

Original bug ID: 5749
Reporter: @mmottl
Status: acknowledged (set by @damiendoligez on 2012-09-27T12:33:23Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.00.0
Category: typing
Monitored by: @gasche mehdi "Julien Signoles" @hcarty @mmottl

Bug description

The following code fails with a signature mismatch:

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

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

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?

vicuna · 2012-09-03T17:21:44Z

Comment author: @alainfrisch

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"?

vicuna · 2012-09-03T23:21:02Z

Comment author: @mmottl

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.

yallop · 2019-04-05T09:38:33Z

This is fixed, possibly by #6333, and the example is now accepted as written.

vicuna added typing feature-wish labels Mar 14, 2019

yallop closed this as completed Apr 5, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Module "includes" not equivalent to rebinding for types using first-class modules #5749

Module "includes" not equivalent to rebinding for types using first-class modules #5749

vicuna commented Aug 31, 2012 •

edited by yallop

vicuna commented Sep 3, 2012 •

edited by yallop

vicuna commented Sep 3, 2012

yallop commented Apr 5, 2019

Module "includes" not equivalent to rebinding for types using first-class modules #5749

Module "includes" not equivalent to rebinding for types using first-class modules #5749

Comments

vicuna commented Aug 31, 2012 • edited by yallop

Bug description

vicuna commented Sep 3, 2012 • edited by yallop

vicuna commented Sep 3, 2012

yallop commented Apr 5, 2019

vicuna commented Aug 31, 2012 •

edited by yallop

vicuna commented Sep 3, 2012 •

edited by yallop