Looks correct to me. This const annotation does not prevent you
from deleting memory or free'ing external resources - but it does
ensure no transitive mutations for data reachable from struct
fields. If it allowed destroying with mutable destructor, type
system hole like this would be legal: