Haskell: Are type variables in "where" clauses in the same namespace with their parents?

Question

In the following snippet (I have abstracted all other trivial parts)

data T s = T (s -> s)

foo :: T s -> s -> s
foo (T f) x = bar x where
    bar :: s -> s
    bar a = f a

I got following error

Couldn't match expected type `s1' with actual type `s'
  `s1' is a rigid type variable bound by
       the type signature for bar :: s1 -> s1 at /tmp/test.hs:5:12
  `s' is a rigid type variable bound by
      the type signature for foo :: T s -> s -> s at /tmp/test.hs:3:8
In the return type of a call of `f'
In the expression: f a
In an equation for `bar': bar a = f a

my guess was that the type variables in bar's signature don't share the namespace with foo, so the compiler can't infer that the two s actually mean the same type.

Then I found this page Scoped type variables, which suggests that I can use {-# LANGUAGE ScopedTypeVariables #-}, which didn't help. I got the same error.

Answer 1

Are type variables in “where” clauses in the same namespace with their parents?

No*. This gets a little bit easier if you think of foo :: s -> s in terms of foo :: forall s. s -> s. After all, a type variable indicates that the function works for any type s. Let's add explicit quantifications to your code:

{-# LANGUAGE ExplicitForAll #-}

data T s = T (s -> s)

foo :: forall s. T s -> s -> s
foo (T f) x = bar x where
    bar :: forall s. s -> s
    bar a = f a

As you can see, there are two forall s. there. But the one in bar is wrong. After all, you cannot choose any s there, but the one already used in s. This can be done by enabling ScopedTypeVariables:

{-# LANGUAGE ScopedTypeVariables #-}

data T s = T (s -> s)

--     vvvvvvvv  explicit here
foo :: forall s. T s -> s -> s
foo (T f) x = bar x where
    --     vvvvvv  same as above here
    bar :: s -> s
    bar a = f a

However, there are some tricks to get rid of ScopedTypeVariables. For example the following in this case:

data T s = T (s -> s)

foo :: T s -> s -> s
foo (T f) x = (bar `asTypeOf` idType x) x where

    bar a = f a

    idType :: a -> a -> a
    idType a _ = a

-- For completion, definition and type of 'asTypeOf'
-- asTypeOf :: a -> a -> a
-- asTypeOf x _ = x

For any x :: s the term idType x has type s -> s, and asTypeOf enforces both to have the same type.

Depending on your actual code, something like this might be more or less feasible.

---

^{* Well, in this case, since it's possible to use ScopedTypeVariables, see later part of the answer.}

Answer 2

ScopedTypeVariables are indeed the solution, but there's an extra requirement to use them: You must put explicit foralls in the type signatures declaring the variables you want to scope, like this:

foo :: forall s. T s -> s -> s

This is so that the meaning of signatures in code doesn't depend on whether the extension is enabled or not.