proved preservation with appropriate modification for compability on types.
Especially, the compability of function types now demands that the annotations
can be joined in the 'correct' way after a cast has occured.