optimization: Elaborate ascriptions to casts only when needed #23
Description
Ascriptions that elaborate into an identity cast should be removed. For example, □0 : □1 should elaborate to □0 instead of ⟨□1 ⇐ □1⟩ □0.
{{ message }}
Ascriptions that elaborate into an identity cast should be removed. For example, □0 : □1 should elaborate to □0 instead of ⟨□1 ⇐ □1⟩ □0.