> Скобки можно переставлять и раскрывать? По статье - можно.
Раскрывать можно - ассоциация левая, а вот переставлять нельзя:

Есть composition rule:

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

Но мне не удалось свести к нему.

Насчёт вывода типов, я им активно пользовался в доказательстве, в посте я просто перевод с него сделал :-)

Насчёт доказательства:

1. Ни в одном из законов нет вывода аргумента из под pure, значит трюк с гомоморфизмом не применишь (всё равно вытаскивать придётся a и b)
2. Ни в одном из законов, кроме interchange нельзя обернуть параметры (флип), а interchange использует pure, из под которого уже не выведешь аргмент

Это меня убеждает в том, что с помощью законов и определений участвующих в уравнении функций, нельзя построить доказательство.

Т.е. можно построить доказательство, что

liftA2 (flip ($)) (pure a) (pure b) = pure b <*> pure a

Но вот с a и b никак - их с трубы не снимешь :-(