Переменная типа исчезла бы

Я пытаюсь реорганизовать свою функцию, предоставив ей аргумент объектива (из пакета xml-lens). Я пропускаю что-то о квантификаторах типа. Что здесь происходит?

*Main> let z name = listToMaybe $ pom ^.. root ./ ell name . text
*Main> :t z
z :: Text -> Maybe Text
*Main> let z name l = listToMaybe $ pom ^.. l ./ ell name . text

<interactive>:13:38:
    Couldn't match expected type ‘(Element -> f Element)
                                  -> Document -> f Document’
                with actual type ‘t’
      because type variable ‘f’ would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context:
        Applicative f => (Element -> f Element) -> Document -> f Document
      at <interactive>:13:38-57
    Relevant bindings include
      l :: t (bound at <interactive>:13:12)
      z :: Text -> t -> Maybe Text (bound at <interactive>:13:5)
    In the first argument of ‘(./)’, namely ‘l’
    In the second argument of ‘(^..)’, namely ‘l ./ ell name . text’

Что интересно, эта подпись работает.

textFrom :: Text -> Document -> Lens' Document Element -> Maybe Text
textFrom name pom ln = listToMaybe $ pom ^.. ln ./ ell name . text

Ответы

Ответ 1

Проблема здесь не в объективах или xml-lens. Это проблема вывода типа более высокого ранга.

Упрощенный тестовый пример

Сначала дайте пример минимального иеша, используя проблемный тип из вашего вопроса. В коде вы передаете l функции (./), которая ожидает Traversable; Я заменяю (./) на g и оставляю остальную часть функции.

g :: Traversal s t a b -> String
g = undefined

-- f :: Traversal s t a b -> String
f l = g l

Ошибка:

Couldn't match expected type `(a0 -> f b0) -> s0 -> f t0'
            with actual type `t'
  because type variable `f' would escape its scope
This (rigid, skolem) type variable is bound by
  a type expected by the context:
    Control.Applicative.Applicative f => (a0 -> f b0) -> s0 -> f t0
  at SO27247620.hs:14:7-9
Relevant bindings include
  l :: t (bound at SO27247620.hs:14:3)
  f :: t -> String (bound at SO27247620.hs:14:1)
In the first argument of `g', namely `l'
In the expression: g l

Раскомментирование сигнатуры типа исправляет ее, как и с вашей проблемой.

Разложим сигнатуру типа, чтобы понять, почему.

type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

f :: (forall f. Applicative f => (a-> f b) -> s -> f t) -> String

Пунктир здесь просто состоит в том, что f имеет тип более высокого ранга, т.е. содержит вложенный forall; вам нужно RankNTypes написать либо f, либо g.

Вывод типов более высокого ранга

Тип вывода для типов более высокого ранга не всегда возможен. Ваша проблема сводится к тому, что "GHC не может вывести этот тип более высокого ранга"; ответ на это в основном "GHC не дает никаких обещаний, что он может это сделать".

В частности, одно задокументированное допущение GHC делает вывод о выводах и типах более высокого ранга именно из GHC 7.8.3 docs:

Для связанной с lambda или связанной с регистром переменной x либо программист предоставляет явный полиморфный тип для x, либо вывод типа GHC будет предполагать, что в нем нет никаких фоллонов.

В нашем примере переменная l является lambda-bound, и она не имеет явного полиморфного типа. Поэтому GHC предполагает, что его тип (который вызывает сообщение об ошибке t) не имеет фокусов. Попытка унифицировать его с помощью forall f. (a0 -> f b0) -> s0 -> f t0 нарушает это предположение.

Бит о переменной типа f, выходящей из области видимости, указывает, что f должен иметь forall на нем.

Кстати, реальный минимальный пример:

g' :: (forall a. a) -> b
g' = undefined

f' = \x -> g' x