You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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=sigmodule type M=sigendtypet = (moduleM) listendmoduleMake (Spec : Spec) : sigtype t =Spec.t end=structincludeSpec(* 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?
The text was updated successfully, but these errors were encountered:
This seems hard to fix. Within the functor's body, the include statement basically amounts to inlining:
module type M=sigendtypet = (moduleM) 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"?
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.
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:
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?
The text was updated successfully, but these errors were encountered: