This would make definitions like contextual equivalence easier. For example, if We could write $C[s] \Downarrow r \iff C[t] \Downarrow r$. Where $r$ would be either a unit value, or an error. But since error carries a type annotation, the errors may be syntactically different, when the type annotations were instantiated differently.
This would make definitions like contextual equivalence easier. For example, if We could write $C[s] \Downarrow r \iff C[t] \Downarrow r$. Where $r$ would be either a unit value, or an error. But since error carries a type annotation, the errors may be syntactically different, when the type annotations were instantiated differently.