How does GHCi pick names for type variables?

Question

When using the interactive GHC interpreter, it's possible to ask for the inferred type of an expression:

Prelude> :t map
map :: (a -> b) -> [a] -> [b]

It seems that it takes the names of the type variables from the signature since map is defined as

map :: (a -> b) -> [a] -> [b]
map _ []     = []
map f (x:xs) = f x : map f xs

in the Prelude. That makes a lot of sense! My question is: how are type variable names picked when there is no signature given?

An example would be

Prelude> :t map fst
map fst :: [(b, b1)] -> [b]

where it picked names b and b1. It's clear that renaming must take place, but simply starting with a, b, ... would have given

map fst :: [(a, b)] -> [a]

instead, which I find slightly more readable.

Answer 1

As I understand it, ghci chooses names in the same order that it infers the types. It uses the naming scheme as you mentioned to decide the type name of the result, which is [b] because that is the type name specified in the definition of map. It then decides that the function that is the first parameter to map should return something of type b also.

The remaining type variable to be named is thus the type variable for the second element in the argument tuple to fst, and again, it looks at the definition of fst to decide which name to use. The definition of fst :: (a, b) -> a, so b would be the preferred name here, but since b is already taken, it appends a 1 so that it becomes b1.

I think that this system has advantages in situations where you don't deal with arbitrary types as is the case here. If the resulting type looks something like this, for example:

castAdd :: (Num n, Num n1, Num n2) => n -> n1 -> n2

... it is arguably more readable than:

castAdd :: (Num a, Num b, Num c) => a -> b -> c

... because you can mostly rely on that n# signifies a numeric type, since the class definition for Num is class Num n where ....

EDIT: Yes, I know that castAdd is impossible to implement, but it's just a type example.