Disentangling unification and implicit coercion (subtyping interaction problem) (opens in new tab)

It’s well known that unification and subtyping don’t play well together, even in the setting of bidirectional elaboration; the problem, as Amélia Liao very helpfully outlined is scheduling. The problem is essentially that we cannot resolve a coercion problem \(\gamma \colon \alpha \lhd A\) by solving \(\alpha :\equiv A, \gamma :\equiv 1_A\) because this is not the most general solution: it is in fact the least general solution, considering that \((A,1_A)\) is the terminal object of \(\...