Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

include of sub-module in recursively-defined module causes loss of type equality #6467

Closed
vicuna opened this issue Jun 23, 2014 · 3 comments
Closed

Comments

@vicuna
Copy link

vicuna commented Jun 23, 2014

Original bug ID: 6467
Reporter: @mshinwell
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-03-14T07:45:08Z)
Resolution: duplicate
Priority: normal
Severity: minor
Version: 4.01.0
Target version: undecided
Category: typing
Tags: recmod
Related to: #5058 #6011
Monitored by: @gasche

Bug description

The following code compiles.

module rec Element : sig
type t
val remove_from_container : t -> unit
end = struct
type t = {
level : Container.t;
}

let remove_from_container t =
Container.remove_element t.level t
end and Container : sig
type t
val remove_element : t -> Element.t -> unit
end = struct
type t = {
mutable elements : Element.t list;
}

let remove_element t element =
t.elements <-
List.filter (fun element' -> not (element == element')) t.elements
end

I would like to wrap the first definition of type [t] inside a module [T], like this:

module rec Element : sig
type t
val remove_from_container : t -> unit
end = struct
module T = struct
type t = {
level : Container.t;
}
end
include T

let remove_from_container t =
Container.remove_element t.level t
end and Container : sig
type t
val remove_element : t -> Element.t -> unit
end = struct
type t = {
mutable elements : Element.t list;
}

let remove_element t element =
t.elements <-
List.filter (fun element' -> not (element == element')) t.elements
end

This causes an error on the call to "Container.remove_element":

File "recmodules.ml", line 13, characters 37-38:
Error: This expression has type t = T.t
but an expression was expected of type Element.t

Is it expected that this causes an error? It seems surprising.

@vicuna
Copy link
Author

vicuna commented Jun 23, 2014

Comment author: @garrigue

This looks like an instance of the so-called double view problem: the same type seen from inside and outside a module ends up being not equal.
OCaml tries to solve it by adding an equation which makes local types point to their external definition.
However, this does not work if the type already has an equation, which is the case if it is a result of using "include".

In this respect, this is just a duplicate of some existing PR, if someone can find it...

@vicuna
Copy link
Author

vicuna commented Jun 23, 2014

Comment author: @gasche

I use the "site:caml.inria.fr/mantis" feature of Google to efficiently search the Mantis.

The double vision problem has been mentioned a couple of times, but not in this setting; there are other situations (unrelated to recursive modules) where the restriction of having a single equation was discussed, notably:
#6011: #6011
#5058: #5058

@vicuna
Copy link
Author

vicuna commented Apr 8, 2016

Comment author: @stedolan

As a practical matter, this is difficult only because of the abstract types. You can sidestep the issue by first defining the modules transparently, and sealing in a separate step:

https://gist.github.com/stedolan/fbdc974dbf96be8959908fed3be2ada7

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants