type X = & C (| D E) type Y = { member x : X type Z = & X { type T = C assert C <: D } member r : (box forall S. (=> S Y)) member s : C[X, Y, z] member f : -> A B }