Влияние ограничения мономорфизма на ограничения типа класса

Этот код прерывается, когда добавляется объявление типа для baz:

baz (x:y:_) = x == y
baz [_] = baz []
baz [] = False

Общее объяснение (см. Почему я не могу объявить тип вывода? для примера) заключается в том, что он из-за полиморфной рекурсии.

Но это объяснение не объясняет, почему эффект исчезает с другим полиморфно-рекурсивным примером:

foo f (x:y:_) = f x y
foo f [_] = foo f []
foo f [] = False

Он также не объясняет, почему GHC считает, что рекурсия мономорфна без объявления типа.

Может ли объяснение примера с reads в http://www.haskell.org/onlinereport/decls.html#sect4.5.5 применяться к моему случаю baz?

т.е. добавление подписи устраняет ограничение мономорфизма, и без ограничения возникает двусмысленность правой части [] с "неотъемлемо неоднозначным" типом forall a . Eq a => [a]?

Ответ 1

Уравнения для baz находятся в одной связывающей группе, обобщение выполняется после ввода всей группы. Без сигнатуры типа это означает, что baz предполагается иметь монотип, поэтому тип [] в рекурсивном вызове задается этим (посмотрите на вывод ghc -ddump-simple). С сигнатурой типа компилятор явно сообщает, что функция является полиморфной, поэтому он не может считать тип [] в рекурсивном вызове одинаковым, следовательно, он неоднозначен.

Как сказал Джон Л, в foo тип фиксируется появлением f - до тех пор, пока f имеет монотип. Вы можете создать ту же двусмысленность, указав f тот же тип, что и (==) (для которого требуется Rank2Types),

{-# LANGUAGE Rank2Types #-}
foo :: Eq b => (forall a. Eq a => a -> a -> Bool) -> [b] -> Bool
foo f (x:y:_) = f x y
foo f[_] = foo f []
foo _ [] = False

Это дает

Ambiguous type variable `b0' in the constraint:
  (Eq b0) arising from a use of `foo'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: foo f []
In an equation for `foo': foo f [_] = foo f []

Ответ 2

Второй пример не является полиморфно рекурсивным. Это связано с тем, что функция f появляется как на LHS, так и на RHS рекурсивного определения. Также рассмотрим тип foo, (a -> a -> Bool) -> [a] -> Bool. Это фиксирует тип элемента списка, который идентичен типу аргументов f. В результате GHC может определить, что пустой список в RHS должен иметь тот же тип, что и список ввода.

Я не думаю, что пример reads применим к случаю baz, потому что GHC может скомпилировать baz без сигнатуры типа, а ограничение мономорфизма отключено. Поэтому я ожидаю, что алгоритм типа GHC имеет другой механизм, с помощью которого он устраняет неоднозначность.