Weird error when using scoped type variables and the y combinator in haskell

Question

So I'm playing around with the y-combinator and anonymous functions, and I ran into this weird error:

Couldn't match expected type `t0 -> t1 -> t2'
            with actual type `forall b. b -> [b] -> [b]'
The lambda expression `\ (n :: Int) newVal xs -> ...'
has three arguments,
but its type `Int -> forall b. b -> [b] -> [b]' has only one

(source code that creates the error, and version that I eventually got working)

If I modify the types slightly to avoid Rank N polymorphism (use forall b. Int -> b -> [b] -> [b]), the error is similar:

Couldn't match expected type `t0 -> t1 -> t2 -> t3'
            with actual type `forall b. Int -> b -> [b] -> [b]'
The lambda expression `\ (n :: Int) newVal xs -> ...'
has three arguments,
but its type `forall b. Int -> b -> [b] -> [b]' has none

Could someone explain to me why forall b. b -> [b] -> [b] has no arguments?

Answer 1

Since you're using GHC 7, this appears to have the same root cause as the bug reported in http://hackage.haskell.org/trac/ghc/ticket/4347 . While that bug report talks about impredicative polymorphism, it seems like it's most likely in a unification problem in higher-rank polymorphism. In your case, it's being triggered by your placement of the forall, which makes the type syntactically rank-2.

Note that this isn't really a bug. The further clarification provided makes it clear this is intended behavior, in that polymorphic instantiations of types, including rank-N types and impredicative types, are not inferred. Careful addition of type signatures can make it work.

But since the type wasn't intended to be higher-rank, at all, in your case, it's best to just get rid of that.

Answer 2

Do you rather want

forall b. Int -> b -> [b] -> [b]

or really

Int -> forall b . b -> [b] -> [b]

I would read the latter: A function that takes an Int and returns SOMETHING OPAQUE THAT IS MOST LIKELY NOT WHAT YOU THINK IT IS.

Answer 3

My guess was that you've written the wrong types down.

Removing the type annotations helps somewhat, leading to less confusing errors:

A.hs:7:76:
    Occurs check: cannot construct the infinite type: a0 = [a0]
    In the third argument of `replaceNth', namely `arg'
    In the expression: replaceNth m (replaceNth n v (arg !! m)) arg

so

 \m n v arg -> replaceNth m (replaceNth n v (arg !! m)) arg

has already got problems.

---

Rank N types and lexically scoped type variables

By using a forall not in an outermost position, you have stumbled into rank N types. The forall on your inner b says that it must be opaque, polymorphic, and unrelated to your other uses of the b type. This is likely not what you intended to do.

This is subtly distinct from lexically scoped type variables, which can also be introduced by a forall in the outermost position, as described here.

By removing the (I think) mistaken foralls in the non-outermost position, you will get much simpler type errors.