Правило не срабатывает во многих случаях, потому что очень простая функция f
встроена до того, как у правила была возможность срабатывания. Если вы отложите врезку,
{-# INLINE [1] f #-}
правило
{-# RULES "f/f" forall a. f (f a) = 4*a #-}
должен срабатывать во всех этих случаях (работает здесь с 7.2.2 и 7.4.1).
Причина в том, что сопоставление правил не слишком сложное, оно сопоставляет только выражения, имеющие синтаксическую форму правила (не совсем верно, тело правила тоже подвергается некоторой нормализации). Выражения f $ f 3
или f . f $ 4
не соответствуют синтаксической форме правила. Чтобы соответствовать правилу, необходимо выполнить некоторое переписывание, ($)
и (.)
должны быть встроены, прежде чем правило будет соответствовать выражению. Но если вы не запретите встраивание f
в первую фазу упрощения, оно будет заменено своим телом в том же цикле, что и встроенные ($)
и (.)
, поэтому в следующей итерации упрощатель не больше не вижу * 1017, он видит только 2*(2*x)
, что не соответствует правилу.