#type synonym の部分適用が出来ないのは higher order unification が決定不能だから。
#higher order unificationとは? by 教えて君 > @masahiro_sakai
#higher-order unification は項の構文にラムダ抽象があるような場合の単一化。例えば一階だと x A と B C は A≠C なので単一化できないけど、高階だと x = λ_ -> B C とおいて単一化できる。
#で、型シノニムの部分適用を許すのは、型式にラムダ抽象を導入するのとほぼ同じなので、型推論に高階単一化が必要になってしまうはず。