4
votes

I'm working on a complicated function in yesod. It has a lot of functions in the where portion that are untyped, but typecheck properly. I decided to try and add a few type signatures so that I could figure out what was going on one piece at a time, but adding the type signatures caused type errors.

So I pared down the function to a simple case to post here, which still gives a similar error that I don't understand.

helper :: [(String, a)] -> [(Int, a)]
helper xs = blah
  where
    blah :: [(Int, a)]
    blah = zip [1..10] (map snd xs)

If I remove the type signature from blah, it compiles just fine, but if I add that type signature it gives me the error:

Couldn't match type `a' with `a1'
  `a' is a rigid type variable bound by
      the type signature for helper :: [(String, a)] -> [(Int, a)]
      at Blah.hs:4:1
  `a1' is a rigid type variable bound by
       the type signature for blah :: [(Int, a1)] at Blah.hs:7:5
Expected type: [(String, a1)]
  Actual type: [(String, a)]
In the second argument of `map', namely `xs'
In the second argument of `zip', namely `(map snd xs)'
  1. I also have no idea why the "a" in helper is interpretted as a different "a" than helper when typechecking goes forth.
  2. Why it even cares if the a's are different in the first place
  3. I have no idea how to figure out what type blah actually is, because I can't move it to the toplevel while still using its argument.

Edit:

Okay, I have one more edit before I mark this answered. In the code I'm using there are some constraints (Eq a, Monad monad) => etc, etc, etc. and so the solution I have doesn't quite work. So I'm modifying my sample code to be more close to the real code:

helper :: (Eq a, Num b) => b -> [(String, a)] -> (b, [(Int, a)])
helper b xs = (b+b, blah)
  where
    blah :: [(Int, a)]
    blah = filter (\y -> fst y == 11) $ zip [1..10] (map snd xs)

If I put

helper :: forall a. (Eq a, Num b) => b -> [(String, a)] -> (b, [(Int, a)])

this doesn't work because (I assume because b is not in scope, but I can't figure out the syntax to get forall b into this type. (forall a, forall b doesn't work, forall a,b doesn't work).

1

1 Answers

13
votes

The a in the type of blah is not the same as the a in the type of helper, unless you use the ScopedTypeVariables extension. So your type signatures are saying that they are independent, but they are clearly not. Your code is equivalent to this:

helper :: forall a. [(String, a)] -> [(Int, a)]
helper xs = blah
  where
    blah :: forall b. [(Int, b)]
    blah = zip [1..10] (map snd xs)

Here you are saying that for any given a, we can choose any b, but that's not true. Since xs has type [(String, a)], map snd xs has type [a]. So a and b must be the same type, i.e. a ~ b. Thus the compiler complains that blah isn't as polymorphic as you said it was in the type signature.

You have three options:

  • Remove the type signature. The compiler will infer the correct type for blah.

  • Enable ScopedTypeVariables. The compiler will then realise that you wanted the a in the type of blah to be the same as the a in the signature of helper. In this case, you need to add an explicit forall a. to the type signature of helper:

    {-# LANGUAGE ScopedTypeVariables #-}
    helper :: forall a. [(String, a)] -> [(Int, a)]
    helper xs = blah
      where
        blah :: [(Int, a)]
        blah = zip [1..10] (map snd xs)
    
  • Make the type of blah independent:

    helper :: [(String, a)] -> [(Int, a)]
    helper xs = blah xs
      where
        blah :: [(String, b)] -> [(Int, b)] -- Or 'a'. Doesn't matter.
        blah ys = zip [1..10] (map snd ys)
    

    Now blah will work on any b. The fact that you only use it with b ~ a is perfectly fine.

Answer to edit:

Use a space between the type variables in the forall, e.g.

helper :: forall a b. (Eq a, Num b) => ...