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

with type removes module aliases, which breaks soundness #7723

Closed
vicuna opened this issue Feb 11, 2018 · 6 comments
Closed

with type removes module aliases, which breaks soundness #7723

vicuna opened this issue Feb 11, 2018 · 6 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Feb 11, 2018

Original bug ID: 7723
Reporter: @lpw25
Assigned to: @lpw25
Status: assigned (set by @garrigue on 2018-04-03T01:43:15Z)
Resolution: open
Priority: normal
Severity: minor
Category: typing
Monitored by: @Drup @gasche

Bug description

[with type] will remove module aliases. This allows inconsistent module types to be made, which can then be realized through recursive modules and used to break soundness. I don't think this can cause segfaults, but it does, for example, allow us to prove that all [Set] types are equal if their element type is equal:

type (_, _) eq = Refl : ('a, 'a) eq

module Equal (M : Set.OrderedType) (N : Set.OrderedType with type t = M.t) : sig
  val eq : (Set.Make(M).t, Set.Make(N).t) eq
end = struct
  type meq = Eq of (Set.Make(M).t, Set.Make(M).t) eq
  module type S = sig
    module N = M
    type neq = meq = Eq of (Set.Make(M).t, Set.Make(N).t) eq
  end
  module type T = S with type N.t = M.t with module N := N;;
  module rec T : T = T
  let eq =
    let T.Eq eq = Eq Refl in
    eq
end
@vicuna
Copy link
Author

vicuna commented Feb 11, 2018

Comment author: @lpw25

The solution here is that the module type expression:

S with type N.t = M.t

in the above example should check that [N.t] does equal [M.t] and then return [S] unaltered -- leaving [N] as a module alias to [M].

@vicuna
Copy link
Author

vicuna commented Feb 28, 2018

Comment author: @garrigue

As it seems that you know the solution, could you provide a patch (or is it already in progress)?

@vicuna
Copy link
Author

vicuna commented Feb 28, 2018

Comment author: @lpw25

Sure. I'll have a look sometime next week.

@vicuna
Copy link
Author

vicuna commented Apr 5, 2018

Comment author: @lpw25

PR: #1698

@yallop
Copy link
Member

yallop commented Apr 15, 2019

@lpw25: can this be closed now that #1698 is merged?

@lpw25
Copy link
Contributor

lpw25 commented Apr 15, 2019

Yeah, I think this is fine now.

@lpw25 lpw25 closed this as completed Apr 15, 2019
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

3 participants