A pathological annotation case? about primer HOT 1 OPEN

I think we could at the least have the rule: when checking T ∋ S : e, delete the annotation S if it is equal to T. This would fix this case - they are both ? here.

Potentially we could relax "equal" to "consistent -- up to holes", but I'd need to think more about that. The two key questions are

• soundness: if T ∋ S : e with T ~ S, do we also have T ∋ e. We have T ∋ S : e iff S ∋ e and S ~ T, so this reduces to whether consistent types always accept the same terms. My next point shows that this is not true, so any relaxation would have to be more subtle.
• usability: will it always/usually be a good idea (whatever that means). e.g.
  • How do consistent types act the same wrt smart holes for checking non-accepted terms: Bool ∋ 1 fails, but ? ∋ 1 succeeds. Removing the annotation from Bool ∋ ? : 1 would give Bool ∋ {? 1 ?} -- nb: this mostly shows that this transformation is not sound. If we did something smarter we may not have this weird Ann-transforms-into-Hole issue.
  • Will we remove information a human may find useful
  • Probably other concerns that slip my mind at the moment.

from primer.