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

Question

In the next snippet (I dropped 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 = fa 

I got the 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: fa In an equation for `bar': bar a = fa 

My assumption was that type variables in the bar signature do not share the namespace with foo , so the compiler cannot conclude that the two s actually mean the same type.

Then I found Scope type variables on this page, which suggests that I can use {-# LANGUAGE ScopedTypeVariables #-} , which did not help. I got the same error.

Answer 1

Are type variables in "where" sentences in the same namespace with parents?

No *. It gets a little easier if you think of foo :: s -> s in terms of foo :: forall s. s -> s foo :: forall s. s -> s . After all, a type variable indicates that the function works for any type s . Let me add explicit quantitative values ​​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 = fa 

As you can see, there are two forall s. . But one in bar is wrong. In the end, you cannot select s there, but one that is 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 = fa 

However, there are some tricks to get rid of ScopedTypeVariables . For example, 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 = fa 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 term idType x is of type s -> s , and asTypeOf forces both to be of the same type.

Depending on your actual code, something like this may be more or less doable.

---

^{* Well, in this case, since you can use ScopedTypeVariables , see the later part of the answer.}

Answer 2

ScopedTypeVariables are indeed a solution, but there is an additional requirement to use them: you must specify explicit forall in the type of signatures declaring the variables that you want to use, for example:

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

This is so that the value of the signatures in the code does not depend on whether the extension is enabled or not.