Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007851OCamltypingpublic2018-09-20 08:372018-09-20 14:05
Reportergarrigue 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version4.07.0 
Target Version4.08.0+devFixed in Version 
Summary0007851: Module type of allows to transform a malformed module type into a vicious signature, breaking soundness
DescriptionBy removing some equations from the type of a module (using nondep_subtyping for instance), one can make it malformed. Then by further abstracting in with "module type of", and instantiating with "with type", it is possible to break soundness.

Discovered during https://github.com/ocaml/ocaml/pull/2051 [^]
Steps To Reproducetype (_,_) eq = Eq : ('a,'a) eq
module F(X : Set.OrderedType) = struct
  type x = Set.Make(X).t and y = Set.Make(X).t
  type t = E of (x,x) eq
  type u = t = E of (x,y) eq
end;;
module M = F(struct type t let compare = compare end);;
module type S = module type of M;;
module rec M1 : S with type x = int and type y = bool = M1;;
let (E eq : M1.u) = (E Eq : M1.t);;
let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x;;
cast eq 3;;
- : M1.y = <unknown constructor>
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0019373)
garrigue (manager)
2018-09-20 08:54

While this is a soundness issue, one really has to go through all these steps to trigger it, so it is not that urgent.
(0019374)
lpw25 (developer)
2018-09-20 10:41

I think this would be fixed if `module type of` always returned the strengthened module type. Although it's probably still not great to have modules with ill-formed module types.
(0019375)
lpw25 (developer)
2018-09-20 10:46

Just for clarity, the example without functor application or GADTs:

  module F(X : sig type t end) = struct
      type x = X.t
      type y = X.t
      type t = E of x
      type u = t = E of y
  end;;

  module M = F(struct type t end);;

  module type S = module type of M;;

  module rec M1 : S with type x = int and type y = bool = M1;;

  let bool_of_int x =
    let (E y : M1.u) = (E x : M1.t) in
    y;;

  bool_of_int 3;;
(0019376)
garrigue (manager)
2018-09-20 12:18

> I think this would be fixed if `module type of` always returned the strengthened module type.

Indeed I expected this comment, which is very true. Unfortunately, as long as we do not drop completely the compatibility mode, the problem will stay around.

Thanks for the example without GADTs. Since we're just relying on the local equality, there is indeed no need for them, meaning that this bug is in OCaml at least since the introduction of module type of (which I think came after module rec, but I may have the order wrong).

This is really the kind of situation where a post-checker, such as Pierrick Couderc's, would come handy.
Not sure how hard it would be to check for well-formedness inside the compiler: equations are used in many places, so this essentially amounts to re-constructing the whole type.

- Issue History
Date Modified Username Field Change
2018-09-20 08:37 garrigue New Issue
2018-09-20 08:37 garrigue Status new => assigned
2018-09-20 08:37 garrigue Assigned To => garrigue
2018-09-20 08:54 garrigue Note Added: 0019373
2018-09-20 10:41 lpw25 Note Added: 0019374
2018-09-20 10:46 lpw25 Note Added: 0019375
2018-09-20 12:18 garrigue Note Added: 0019376


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker