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

Module type of allows to transform a malformed module type into a vicious signature, breaking soundness #7851

Open
vicuna opened this issue Sep 20, 2018 · 5 comments

Comments

Projects
None yet
4 participants
@vicuna
Copy link

commented Sep 20, 2018

Original bug ID: 7851
Reporter: @garrigue
Assigned to: @garrigue
Status: assigned (set by @garrigue on 2018-09-20T06:37:44Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.07.0
Target version: 4.08.0+dev/beta1/beta2
Category: typing
Monitored by: @nojb @gasche @yallop @yakobowski

Bug description

By 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 #2051

Steps to reproduce

type (,) 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 =
@vicuna

This comment has been minimized.

Copy link
Author

commented Sep 20, 2018

Comment author: @garrigue

While this is a soundness issue, one really has to go through all these steps to trigger it, so it is not that urgent.

@vicuna

This comment has been minimized.

Copy link
Author

commented Sep 20, 2018

Comment author: @lpw25

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Sep 20, 2018

Comment author: @lpw25

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;;

@vicuna

This comment has been minimized.

Copy link
Author

commented Sep 20, 2018

Comment author: @garrigue

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.

@vicuna vicuna added the typing label Mar 14, 2019

@vicuna vicuna added this to the 4.08.0 milestone Mar 14, 2019

@vicuna vicuna added the bug label Mar 20, 2019

@nojb nojb modified the milestones: 4.08.0, 4.08 Mar 29, 2019

garrigue added a commit to garrigue/ocaml that referenced this issue Apr 2, 2019

garrigue added a commit to garrigue/ocaml that referenced this issue Apr 19, 2019

@garrigue garrigue closed this in 4fe08b2 Apr 19, 2019

garrigue added a commit that referenced this issue Apr 19, 2019

garrigue added a commit that referenced this issue Apr 19, 2019

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Apr 19, 2019

We are not yet sure all instances of this problem are fixed, but the specific example (and @lpw25 's version) are fixed by #8570, commits 4fe08b2 in trunk and 8cb7888 in 4.08.

@garrigue garrigue reopened this Apr 19, 2019

@damiendoligez damiendoligez removed this from the 4.08 milestone May 14, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.