Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007723OCamltypingpublic2018-02-11 15:012018-02-11 19:32
Reporterlpw25 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusnewResolutionopen 
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
      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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0018869)
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].

- Issue History
Date Modified Username Field Change
2018-02-11 15:01 lpw25 New Issue
2018-02-11 15:03 lpw25 Note Added: 0018869


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker