You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
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:
The text was updated successfully, but these errors were encountered: