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

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].