Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007723OCamltypingpublic2018-02-11 15:012018-04-05 18:21
Assigned Tolpw25 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0007723: with type removes module aliases, which breaks soundness
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
      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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
lpw25 (developer)
2018-02-11 15:03

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].
garrigue (manager)
2018-02-28 05:35

As it seems that you know the solution, could you provide a patch (or is it already in progress)?
lpw25 (developer)
2018-02-28 09:19

Sure. I'll have a look sometime next week.
lpw25 (developer)
2018-04-05 18:21

PR: [^]

- Issue History
Date Modified Username Field Change
2018-02-11 15:01 lpw25 New Issue
2018-02-11 15:03 lpw25 Note Added: 0018869
2018-02-28 05:35 garrigue Note Added: 0018930
2018-02-28 09:19 lpw25 Note Added: 0018931
2018-04-03 03:43 garrigue Assigned To => lpw25
2018-04-03 03:43 garrigue Status new => assigned
2018-04-05 18:21 lpw25 Note Added: 0018977

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker