What's wrong with my type signatures here?

Question

I'm playing around with corecursive data structures, and fairly early on in my code, I get a type error:

module Graph where
import Data.Map 

data Node a = Node { getLabel :: a, getInEdges :: [Edge a], getOutEdges :: [Edge a] }
data Edge a = Edge { getStart :: Node a, getEnd :: Node a }
data Graph a = Graph { getNodes :: [Node a], getEdges :: [Edge a] }

mkGraph :: (Ord a) => [(a,a)] -> Graph a
mkGraph pairs = Graph (elems nodes) edges
  where nodes :: Map a (Node a)
        edges :: [Edge a]
        (nodes, edges) = foldr addEdge (empty,[]) pairs
        addEdge :: (a,a) -> (Map a (Node a), [Edge a]) -> (Map a (Node a), [Edge a])
        addEdge (startLabel, endLabel) = undefined

When I try to load this in ghci, I get

graph.hs:13:25:
    Couldn't match expected type `forall a. Map a (Node a)'
           against inferred type `Map a (Node a)'
      Expected type: (forall a1. Map a1 (Node a1), forall a1. [Edge a1])
      Inferred type: (Map a (Node a), [Edge a])
    In the expression: foldr addEdge (empty, []) pairs
    In a pattern binding:
        (nodes, edges) = foldr addEdge (empty, []) pairs

If I delete the type signatures nodes :: Map a (Node a) and edges :: [Edge a], the error goes away.

What am I doing wrong here? I'm guessing that the type variable a isn't being bound by mkGraph's type signature, but shouldn't the definition of mkGraph compel the a in the signature of nodes and edges to be the same a?

Answer 1

What am I doing wrong here? I'm guessing that the type variable a isn't being bound by mkGraph's type signature, but shouldn't the definition of mkGraph compel the a in the signature of nodes and edges to be the same a?

You guess correctly; the other a is a fresh type variable. This means that, not only is it not the same a as in mkGraph's signature, it's a brand new universally quantified type variable, which is incorrect. The types called a in your inner signatures are thus neither polymorphic nor single known types. And no, it "shouldn't", as per the Haskell standard. In Haskell 98, it is in fact impossible to write a type signature for nodes and edges in your code. Yes, that's kind of silly.

However, GHC provides a ScopedTypeVariables extension that allows this, among other things. The relevant section of the GHC user guide also discusses the aforementioned "impossible type signature" problem.

Note that you'll also need to add an explicit forall in the type signature for mkGraph, i.e., forall a. (Ord a) => [(a,a)] -> Graph a to bring the type variable into scope. Enabling the extension and adding the forall lets your code type check for me.