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: 7374 Reporter:@lpw25 Assigned to:@garrigue Status: resolved (set by @garrigue on 2016-09-29T08:42:39Z) Resolution: fixed Priority: normal Severity: minor Version: 4.04.0 +dev / +beta1 / +beta2 Target version: 4.04.0 +dev / +beta1 / +beta2 Fixed in version: 4.04.0 +dev / +beta1 / +beta2 Category: typing Child of:#5998 Monitored by:@gasche@yallop
Bug description
The contractiveness check ignores constraints, which makes it unsound. For example:
type ('a, 'b) eq = Refl : ('a, 'a) eq
let trans : type a b x . (a, x) eq -> (b, x) eq -> (a, b) eq =
fun Refl Refl -> Refl
let cast : type a b . (a, b) eq -> a -> b =
fun Refl x -> x
module type S = sig
type 'a t constraint 'a = [`Rec of 'b]
end
module Fix (X : S) : sig
type t
val uniq : ('a, [Rec of 'a] X.t) eq -> ('a, t) eq end = struct type t = [Rec of 'a] X.t as 'a
let uniq : type a . (a, [`Rec of a] X.t) eq -> (a, t) eq =
fun Refl -> Refl
end
module Id = struct
type 'a t = 'b
constraint 'a = [ `Rec of 'b ]
end
Actually the problem was not in the contractiveness check itself, but in the handling of arguments of non-contractive types: since they are not contractive, we must assume that subcomponents could be extracted, and any occurence could be returned.
I'm not sure, but isn't that overly conservative? In general subcomponents cannot be extracted. They can only be extracted when they appear in the constraints on the type's parameters.
It is true, but better safe than sorry, and this check is only about trying to create a recursive type involving an abstract type using a GADT unification , not very usual code.
In particular, if we allow this for non-constrained type parameters, we need a way to check that we really have the type definition at hand: recall that when the compiler does not find a .cmi, it can still handle a type as abstract, without a proper definition, and in particular without information about the constraints.
Original bug ID: 7374
Reporter: @lpw25
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-09-29T08:42:39Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.04.0 +dev / +beta1 / +beta2
Target version: 4.04.0 +dev / +beta1 / +beta2
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Child of: #5998
Monitored by: @gasche @yallop
Bug description
The contractiveness check ignores constraints, which makes it unsound. For example:
type ('a, 'b) eq = Refl : ('a, 'a) eq
let trans : type a b x . (a, x) eq -> (b, x) eq -> (a, b) eq =
fun Refl Refl -> Refl
let cast : type a b . (a, b) eq -> a -> b =
fun Refl x -> x
module type S = sig
type 'a t constraint 'a = [`Rec of 'b]
end
module Fix (X : S) : sig
type t
val uniq : ('a, [
Rec of 'a] X.t) eq -> ('a, t) eq end = struct type t = [
Rec of 'a] X.t as 'alet uniq : type a . (a, [`Rec of a] X.t) eq -> (a, t) eq =
fun Refl -> Refl
end
module Id = struct
type 'a t = 'b
constraint 'a = [ `Rec of 'b ]
end
module Bad = Fix(Id)
let segfault () =
print_endline
(cast (trans (Bad.uniq Refl) (Bad.uniq Refl)) 0)
;; segfault ()
I think the fix is to consider:
[`Rec of 'a] X.t
as non-contractive when X.t has a constraint of the form [`Rec of 'a].
The text was updated successfully, but these errors were encountered: