What should delegates with qualifiers mean?

[Timon Gehr]

On 24.03.21 22:56, Paul Backus wrote:
> struct S
> {
>      int n;
>      int* getPtr() { return &n; }
> }
> 
> void main() @safe
> {
>      immutable S s = { 123 };
>      // implicitly convert from `delegate() immutable` to `delegate()`
>      int* delegate() dg = &s.getPtr;
>      // undefined behavior
>      *dg() = 456;
> }


This is not what was explained in the OP. Removing context qualifiers 
from delegates is sound. You are calling a mutable method on an 
immutable object. Not the same thing, and obviously unsound.

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

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

Therefore,

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

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