optimization: Elaborate ascriptions to casts only when needed

[ontomaquia]

Ascriptions that elaborate into an identity cast should be removed. For example, □0 : □1 should elaborate to □0 instead of ⟨□1 ⇐ □1⟩ □0.