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

Obj.magic with recursive modules #6005

Closed
vicuna opened this issue May 3, 2013 · 5 comments
Closed

Obj.magic with recursive modules #6005

vicuna opened this issue May 3, 2013 · 5 comments
Assignees

Comments

@vicuna
Copy link

@vicuna vicuna commented May 3, 2013

Original bug ID: 6005
Reporter: @diml
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:24:05Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.01.0+dev
Fixed in version: 4.01.0+dev
Category: typing
Related to: #6159
Monitored by: @gasche @jberdine @alainfrisch

Bug description

It seems that consistency of module type constraints is not checked. It is then possible to write Obj.magic by converting a module type to an implementation:

let magic : type a b. a -> b = fun x ->
let module M = struct
module type A = sig type t = X of a end
type u = X of b
module type B = A with type t = u
module rec M : B = M
end in
let M.X x = M.M.X x in
x

@vicuna
Copy link
Author

@vicuna vicuna commented May 3, 2013

Comment author: @garrigue

Indeed, the handling of with definitions is extremely stripped down, and it looks like it was assumed than one could create concrete types with it. Unfortunately this is now possible using recursive modules.

This one is easy to fix, but should look out for other problems...

@vicuna
Copy link
Author

@vicuna vicuna commented May 3, 2013

Comment author: @garrigue

Fixed in trunk at revision 13647.

@vicuna
Copy link
Author

@vicuna vicuna commented Jul 7, 2013

Comment author: @jberdine

Some of my code builds with 4.00.1 but not with trunk, and this fix is the first point where my build fails. There are several points which are affected by this, but here is a simple one. With 4.00.1 we used to be able to write a signature such as:

module Arg : sig
type spec =
| Unit of (unit -> unit) (** Call the function with unit argument )
| Bool of (bool -> unit) (
* Call the function with a bool argument )
(
Added case )
| Set_bool of bool ref (
* Set the reference to the bool artument )
| Set of bool ref (
* Set the reference to true )
| Clear of bool ref (
* Set the reference to false )
| String of (string -> unit) (
* Call the function with a string argument )
| Set_string of string ref (
* Set the reference to the string argument )
| Int of (int -> unit) (
* Call the function with an int argument )
| Set_int of int ref (
* Set the reference to the int argument )
| Float of (float -> unit) (
* Call the function with a float argument )
| Set_float of float ref (
* Set the reference to the float argument )
| Tuple of spec list (
* Take several arguments according to the
spec list )
| Symbol of string list * (string -> unit)
(
* Take one of the symbols as argument and
call the function with the symbol )
| Rest of (string -> unit) (
* Stop interpreting keywords and call the
function with each remaining argument *)

include module type of Arg with type spec := spec
end

Note that the Set_bool case is not included in the spec type defined in the Arg module of the standard library. The type-checker used to be happy with this, but now complains:

Error: This variant or record definition does not match that of type spec
Their 3rd fields have different names, Set_bool and Set.

Is this new more restrictive behavior expected?

Cheers, Josh Berdine

@vicuna
Copy link
Author

@vicuna vicuna commented Jul 28, 2013

Comment author: @garrigue

If seems that the bug was introduced in 3.12.
Until 3.11, your code would not have been accepted, but in 3.12 and 4.00 you can write something like:

module type T = sig type t = A end
type u = B
module type T' = T with type t = u;;

which gives:

module type T' = sig type t = u = A end

Clearly the signature T' is impossible, since u has constructor B, not A.
The same thing can be said about your example too.

@vicuna
Copy link
Author

@vicuna vicuna commented Jul 29, 2013

Comment author: @garrigue

Just for the record: the same limitation is needed for destructive substitutions.
Namely, the type you substitute might be used inside another type definition in the same signature.

module type S = sig
type t = A of int
module M : sig type u = t = A of int end
end
type v = B of bool
module type S' = S with type t := v

In 3.12 and 4.00 this was accepted, and gave the invalid:
module type S' = sig module M : sig type u = v = A of int end end
which you can use to break the type system:

module rec N : S' = N;;

(N.M.A 3 :> v);;

  • : v = B

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

Successfully merging a pull request may close this issue.

None yet
2 participants