Why is higher order unification in Scala considered partial?

Question

SI-2712 Add support for partial unification of type constructors #5102 initially provided the feature under flag

-Yhigher-order-unification

but then renamed it to

-Ypartial-unification

because it seems not to be full higher order unification according to

comment

"partial type application inference" is probably a better term for what's happening here than "higher-order unification", which this most certainly is not

comment 2

rename it to -Ypartial-unification to reflect that fact it doesn't implement a general HOU algorithm.

How is partial unification different from higher order unification? In what sense does Scala not implement higher order unification? Could you demonstrate with a concrete code snippet when Scala is not able to perform HOU?

Answer 1

Broadly, the Scala implementation will only perform higher-order unification if the "missing" type is the right-most type.

Daniel Spiewak demonstrates this with a functor instance for a type that's basically Either, but left biased.