Type variable would escape its scope

Question

I'm trying to refactor my function by giving it a lens argument (from the xml-lens package). I'm missing something about type quantifiers. What is going on here?

*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’

What is interesting, this signature works.

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

Answer 1

The problem here isn't with lenses or xml-lens directly. It's a higher-rank type inference issue.

Simplified test case

First let's make a minimal-ish example using the problematic type from your question. In your code, you're passing l to the function (./), which expects a Traversable; I'm replacing (./) with g and leaving out the rest of the function.

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

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

Error:

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

Uncommenting the type signature fixes it, as with your problem.

Let's expand the type signature to see why.

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

The punchline here is simply that f has a higher-rank type, i.e. it contains a nested forall; you need RankNTypes to write either f or g.

Inferring higher-rank types

Type inference for higher-rank types is not always possible. Your problem boils down to "GHC can't infer this higher-rank type"; the answer to that is basically "GHC makes no promise that it can do so."

Specifically, the one documented assumption GHC makes regarding inference and higher-rank types is this, from the GHC 7.8.3 docs:

For a lambda-bound or case-bound variable, x, either the programmer provides an explicit polymorphic type for x, or GHC's type inference will assume that x's type has no foralls in it.

In our example, the variable l is lambda-bound, and it doesn't have an explicit polymorphic type. Therefore GHC assumes that its type (which the error message calls t) has no foralls. Trying to unify it with forall f. (a0 -> f b0) -> s0 -> f t0 violates that assumption.

The bit about type variable f escaping its scope indicates that f needs to have a forall on it.

By the way, the real minimal example is this:

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

f' = \x -> g' x