Observations

Я знаю, что если c поменять на a, то сойдется. Но я наивно полагал, что функция типа a->b->a - это частный случай функции типа a->b->c.

Вот, например, скала:

scala> type F2[A,B,C] = A => B => C
defined type alias F2

scala> type P1[A,B] = F2[A,B,A]
defined type alias P1

scala> def p1[A,B]: P1[A,B] = (a:A) => (b:B) => a
p1: [A, B]=> A => (B => A)

Уж не в том ли проблема, что типы Черча в некотором смысле не столь, э, сильны, как типы Карри?