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

Non backward compatible change in type comparison #6159

Closed
vicuna opened this issue Sep 4, 2013 · 5 comments
Closed

Non backward compatible change in type comparison #6159

vicuna opened this issue Sep 4, 2013 · 5 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Sep 4, 2013

Original bug ID: 6159
Reporter: mbarbin
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:26:30Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.01.0+beta/+rc
Fixed in version: 4.02.0+dev
Category: typing
Related to: #6005 #6333

Bug description

Let'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".

@vicuna
Copy link
Author

vicuna commented Sep 4, 2013

Comment author: @lpw25

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

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

@vicuna
Copy link
Author

vicuna commented Sep 4, 2013

Comment author: mbarbin

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

@vicuna
Copy link
Author

vicuna commented Sep 5, 2013

Comment author: @lpw25

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:

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

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

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

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

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.

@vicuna
Copy link
Author

vicuna commented Oct 29, 2013

Comment author: turpin

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

@vicuna
Copy link
Author

vicuna commented Apr 4, 2014

Comment author: @garrigue

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 #6333 for details).
As a result this code is accepted again.

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