What should delegates with qualifiers mean?

[Timon Gehr]

On 24.03.21 23:18, Timon Gehr wrote:
> 
> Why is removing qualifiers sound? delegate is an existential type:
> 
> B delegate(A)q ≡ ∃C. (A×q(C)*)→B

Oops. Typo. This should of course have been:

Why is removing qualifiers sound? delegate is an existential type:

B delegate(A)q ≡ ∃C. (A×q(C)*)×q(C)*→B

Therefore,

B delegate(A)immutable ≡ ∃C. (A×immutable(C)*)×immutable(C)*→B ⊆ ∃C'. 
(A×C'*)×C'*→B,

where we have chosen C' as immutable(C).