Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006467OCamlOCaml typingpublic2014-06-23 12:282014-07-16 17:16
Reportershinwell 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version4.01.0 
Target Version4.02.1+devFixed in Version 
Summary0006467: include of sub-module in recursively-defined module causes loss of type equality
DescriptionThe 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.
Tagsrecmod
Attached Files

- Relationships
related to 0006011confirmed Signatures with private types can make modules less constrained 
related to 0005058acknowledged improve type checking of applicative functors 

-  Notes
(0011773)
garrigue (manager)
2014-06-23 14:07

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...
(0011774)
gasche (developer)
2014-06-23 14:14
edited on: 2014-06-23 14:16

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:
  PR#6011: http://caml.inria.fr/mantis/view.php?id=6011 [^]
  PR#5058: http://caml.inria.fr/mantis/view.php?id=5058 [^]


- Issue History
Date Modified Username Field Change
2014-06-23 12:28 shinwell New Issue
2014-06-23 12:28 shinwell Status new => assigned
2014-06-23 12:28 shinwell Assigned To => garrigue
2014-06-23 14:07 garrigue Note Added: 0011773
2014-06-23 14:14 gasche Note Added: 0011774
2014-06-23 14:14 gasche Relationship added related to 0006011
2014-06-23 14:14 gasche Relationship added related to 0005058
2014-06-23 14:16 gasche Note Edited: 0011774 View Revisions
2014-06-23 14:16 gasche Note Edited: 0011774 View Revisions
2014-07-16 17:16 doligez Tag Attached: recmod
2014-07-16 17:16 doligez Target Version => 4.02.1+dev


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker