Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006159OCamlOCaml typingpublic2013-09-04 23:182014-04-04 05:16
Reportermbarbin 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.01.0+beta/+rc 
Target VersionFixed in Version4.02.0+dev 
Summary0006159: Non backward compatible change in type comparison
DescriptionLet's consider the following piece of code, saved into a.mli:

-----------------------------

module A : sig
  module type T = sig
    type t
  end
  type t =
  | T of (module T)
end

module A2 : (module type of A with type t = A.t)

-----------------------------

$ ocaml-4.01.0+rc1/ocamlopt.opt -c a.mli
File "a.mli", line 9, characters 35-47:
Error: This variant or record definition does not match that of type A.t
       The types for field T are not equal.

This file compiles just fine with ocaml-4.00.1

This is probably related to some other issues about type comparison in presence first class module based on type path name, "A.T.t" <> "A2.T.t".
TagsNo tags attached.
Attached Files

- Relationships
related to 0006005resolvedgarrigue Obj.magic with recursive modules 
related to 0006333resolvedgarrigue Keep equation on module type while strengthening 

-  Notes
(0010312)
lpw25 (developer)
2013-09-05 00:34

I think that the new behavior is correct, and the code was only previously accepted due to the bug fixed in 0006005.

The type comparison hasn't actually changed, it just wasn't being applied at all before.

Your example is essentially equivalent to:

  module A : sig
    type s
    type t =
    | T of s
  end

  module A2 : (module type of A with type t = A.t)

which was accepted in 4.00.1, but is rejected in 4.01.0. This is necessary to avoid code like the following:

  module A : sig
    type s
    type t =
    | T of s
  end = struct
    type s = int
    type t =
    | T of s
  end

  module type S = (module type of A with type s = float and type t = A.t);;

which is accepted in 4.00.1 and creates the obviously nonsense module type:

  module type S = sig type s = float type t = A.t = T of s end
(0010313)
mbarbin (reporter)
2013-09-05 01:19
edited on: 2013-09-05 03:17

Thank you, that is quite interesting. I wonder if this is going to touch a lot of existing code. My intuition is that since there is not much you can do with such nonsense sig types like the one shown there, it is more likely to touch code fragment that are actually building a type sig from a module such that all the type match.

If you take libraries like core or async for example, they make extensive usage of module and signature inclusions to re-shape libraries in a nicer way than their actual implementation or source files structure, and I wonder if this would be worth thinking about a work around to cope with this new limitation, for all practical purposes.

I think it is also worth noting a difference between the initial example and yours
In:
[1]
module A : sig
  module type T = sig
    type t
  end
  type t =
  | T of (module T)
end

everything is concrete, where as in your example, s is abstract.

Note that the following is allowed:

[2]
module A : sig
    type s = int
    type t =
    | T of s
end

module A2 : (module type of A with type t = A.t)

As well as:

[3]
module type T = sig
  type t
end

module A : sig
  type t =
  | T of (module T)
end

module A2 : (module type of A with type t = A.t)

Putting the definition of the module type T inside A results in loosing the equality between A.t and A2.t, despite of this not being too different from any concrete type, like in the example [2] where type s = int

(0010315)
lpw25 (developer)
2013-09-05 11:09

Incorrect signatures must be prevented because they are a
soundness bug, for example (in 4.00.1):

  # module M = struct type s type t = T of s end;;
  module M : sig type s type t = T of s end

  # module type S = (module type of M with type s = int and type t = M.t);;
  module type S = sig type s = int type t = M.t = T of s end

  # module type T = (module type of M with type s = float and type t = M.t);;
  module type T = sig type s = float type t = M.t = T of s end

  # module rec A : S = A;;
  module rec A : S

  # module rec B : T = B;;
  module rec B : T

  # let B.T f = A.T 0;;

  Process ocaml-toplevel segmentation fault

Also, I should have been clearer, my "nonsense" example earlier
was an illustration of an obviously wrong signature, but any
signature that was previously allowed and is now prevented is
incorrect. So there can be no workaround.

Consider all the examples mentioned so far, but with the "module
type of" and "with" constraints expanded out:

1)
  module A : sig
    module type T = sig
      type t
    end
    type t =
    | T of (module T)
  end
   
  module A2 : sig
    module type T = sig
      type t
    end
    type t = A.t =
    | T of (module T)
  end

2)
  module A : sig
    type s
    type t =
    | T of s
  end

  module A2 : sig
    type s
    type t = A.t =
    | T of s
  end

3)
  module A : sig
    type s = int
    type t =
    | T of s
  end

  module A2 : sig
    type s = int
    type t = A.t =
    | T of s
  end

4)
  module type T = sig
    type t
  end

  module A : sig
    type t =
    | T of (module T)
  end

  module A2 : sig
    type t = A.t =
    | T of (module T)
  end

Examples 1 and 2 are incorrect signatures because they equate
unequal types `(module A.T)` and `(module A2.T)` in 1 and `A.s`
and `A2.s` in 2. Example 3 is fine because it equates `A.s` (=
int) and `A2.s` (= int). Example 4 is fine because it
equates `(module T)` with itself.

Note that a module type defintion (like T above) essentially
defines an abstract type `(module T)`. It is abstract in the
sense that it does not compare equal with anything except itself.

Also, note that the above signatures are accepted and rejected
appropriatly in 4.00.1, it is only the bug in handling with
constraints that allowed 1 and 2 to be created.
(0010537)
turpin (reporter)
2013-10-29 14:50

I just encoutered a problem which I think is related to this issue. I don't consider it really as a bug, but as a(nother) really tricky feature of the type system: the "with type t = ..." is now "non-commutative". Here is an example of code which used to compile with 4.00.1, and is rejected by 4.01 (only the BAD module type is rejected, the GOOD one is still OK):

module type MT = sig
    type t = { field : unit }
    type u = T of t
end
module M : MT = struct
    type t = { field : unit }
    type u = T of t
end

module type GOOD = MT with type t = M.t and type u = M.u
module type BAD = MT with type u = M.u and type t = M.t
(0011219)
garrigue (manager)
2014-04-04 05:16

Sorry for not having looked at this PR more carefully before.

Actually the original code is perfectly valid, and was only refused because module types were compared nominally.
In trunk they are now compared structurally (see PR#6333 for details).
As a result this code is accepted again.

- Issue History
Date Modified Username Field Change
2013-09-04 23:18 mbarbin New Issue
2013-09-05 00:34 lpw25 Note Added: 0010312
2013-09-05 00:35 lpw25 Relationship added related to 0006005
2013-09-05 01:19 mbarbin Note Added: 0010313
2013-09-05 03:17 mbarbin Note Edited: 0010313 View Revisions
2013-09-05 11:09 lpw25 Note Added: 0010315
2013-10-29 14:50 turpin Note Added: 0010537
2014-04-02 17:07 doligez Status new => resolved
2014-04-02 17:07 doligez Resolution open => no change required
2014-04-04 05:10 garrigue Relationship added related to 0006333
2014-04-04 05:11 garrigue Assigned To => garrigue
2014-04-04 05:11 garrigue Status resolved => assigned
2014-04-04 05:16 garrigue Note Added: 0011219
2014-04-04 05:16 garrigue Status assigned => resolved
2014-04-04 05:16 garrigue Fixed in Version => 4.02.0+dev
2014-04-04 05:16 garrigue Resolution no change required => fixed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker