Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006005OCamltypingpublic2013-05-03 11:382015-12-11 19:24
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.01.0+dev 
Target VersionFixed in Version4.01.0+dev 
Summary0006005: Obj.magic with recursive modules
DescriptionIt 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
TagsNo tags attached.
Attached Files

- Relationships
related to 0006159closedgarrigue Non backward compatible change in type comparison 

-  Notes
garrigue (manager)
2013-05-03 16:12

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...
garrigue (manager)
2013-05-03 16:41

Fixed in trunk at revision 13647.
jjb (reporter)
2013-07-07 19:36

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

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
garrigue (manager)
2013-07-28 13:10

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.
garrigue (manager)
2013-07-29 04:12

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
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 <unknown constructor>

- Issue History
Date Modified Username Field Change
2013-05-03 11:38 dim New Issue
2013-05-03 16:12 garrigue Note Added: 0009243
2013-05-03 16:12 garrigue Assigned To => garrigue
2013-05-03 16:12 garrigue Status new => confirmed
2013-05-03 16:41 garrigue Note Added: 0009244
2013-05-03 16:41 garrigue Status confirmed => resolved
2013-05-03 16:41 garrigue Fixed in Version => 4.01.0+dev
2013-05-03 16:41 garrigue Resolution open => fixed
2013-07-07 19:36 jjb Note Added: 0009719
2013-07-28 13:10 garrigue Note Added: 0009926
2013-07-29 04:12 garrigue Note Added: 0009958
2013-09-05 00:35 lpw25 Relationship added related to 0006159
2015-12-11 19:24 xleroy Status resolved => closed
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker