Generally speaking, GHC’s error messages are fairly helpful and intelligible (so long as you don’t go wild with typelevel programming). But there are definitely a few common but relatively less clear ones. Some of the GHC type error messages that can potentially lead to bewilderment are discussed in this post. The GHC version I used is 8.10.2.
🤔 ‘a’ is a rigid type variable bound by…
If you’ve written Haskell for any amount of time, you’ve probably seen this error message, and it is hardly a confusing one. However, the word “rigid” may seem counterintuitive, and one might wonder what it actually means. Consider the following function definition:
f :: a > a
f x = not x
This definition does not compile and the error message is
• Couldn't match expected type ‘Bool’ with actual type ‘a’
‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a. a > a
at Example.hs:11:111
• In the first argument of ‘not’, namely ‘x’
In the expression: not x
In an equation for ‘f’: f x = not x
• Relevant bindings include
x :: a (bound at Example.hs:12:3)
f :: a > a (bound at Example.hs:12:1)
It should be obvious why f
doesn’t type check, but a potential point of confusion for some, including myself when I first
encountered an error message like this is: why does it say a
is “rigid”? a
can represent any type, so shouldn’t it be “flexible”?
a
is flexible indeed, but only from the perspective of the caller of f
. From the perspective of the definition of f
, it is not
at all flexible. The definition of f
must treat a
as some unknown but fixed type, and must do the exact same thing
for all possible a
.
Haskell has several sorts of type variables, including:
 Type variables written by programmers, such as those bound by
forall
s in type signatures, and those appearing in type applications and type annotations.  Type variables used internally by the compiler. These include
 Unification type variables (or flexible type variables, meta type variables, unification variables). They are fresh variables allocated
to stand for unknown types that need to be determined. One of the tasks of the type inference engine is to determine their actual types by
finding a substitution for each unification variable. Unification variables are flexible in the sense that
they can unify with any type or type variable that does not contain
forall
s^{1} (except when they are untouchable, which will be explained later).  Rigid type variables (or skolem type variables, skolem constants, skolems). They are fresh variables allocated to stand for unknown but fixed types. Their actual types do not need to be, and cannot be determined. They are rigid in the sense that they cannot unify with anything other than themselves or unification variables. In particular, a rigid type variable cannot unify with a concrete type or type constructor, or another rigid type variable.
 Unification type variables (or flexible type variables, meta type variables, unification variables). They are fresh variables allocated
to stand for unknown types that need to be determined. One of the tasks of the type inference engine is to determine their actual types by
finding a substitution for each unification variable. Unification variables are flexible in the sense that
they can unify with any type or type variable that does not contain
Unification type variables and rigid type variables are freshly allocated by the type checker. In an error message like
Couldn't match expected type <expected> with actual type <actual>
<expected>
and <actual>
often contain type variables not written by the programmer, because they are compilerallocated.
When type checking the above f
function, where a
is a programmerwritten, universally quantified type variable, GHC first allocates
a rigid type variable for it (a process called skolemization), because from f
’s point of view, a
is unknown and fixed (or existential). The body
of f
requests that this rigid type variable be unified with Bool
, which the type checker outright refuses, hence the above error message.
🤔 …type variable ‘a’ would escape its scope. This (rigid, skolem) type variable…
A rigid/skolem type variable cannot escape, via a unification variable, the scope where it is introduced. In other words, a rigid type variable can unify with a unification variable, but not when that unification variable has a bigger scope. This can happen in two cases.
1. Type checking a polymorphic function argument:
fun :: (forall a. [a] > b) > Bool
fun _ = True
arg :: c > c
arg c = c
x :: Bool
x = fun arg
This leads to the following error:
• Couldn't match type ‘b0’ with ‘[a]’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall a. [a] > b0
at Example.hs:18:911
Expected type: [a] > b0
Actual type: b0 > b0
• In the first argument of ‘fun’, namely ‘arg’
In the expression: fun arg
In an equation for ‘x’: x = fun arg
In order for x = fun arg
to be well typed, arg
’s type must subsume (i.e., be more general than or equal
to) the type required by fun
. This is not the case here. fun
requires that its argument be able to convert a list of a
s for any
arbitrary a
, into a fixed b
. b
can be flexibly chosen, for instance fun (length :: [a] > Int)
would be legal, but it is
chosen before a
, and must be fixed (i.e., does not depend on a
) once chosen. arg
does not satisfy this requirement, because it maps an
arbitrary a
to itself. Therefore, this program is rejected.
When type checking x = fun arg
, the type checker allocates a rigid type variable for a
, and allocates unification
variables for b
and c
. It then determines that the type of both b
and c
is [a]
. But sadly, b
is not allowed to
unify with [a]
, because b
is bound by an (implicit) toplevel forall
, while a
is bound by an inner forall
. If they were
allowed to unify, the rigid/skolem type variable a
would escape its scope via unification variable b
.
By the way, this is how the ST monad works.
2. Opening existential types:
data A = forall a. A a
f (A x) = Just x
This leads to a similar skolem escape error:
• Couldn't match expected type ‘p’ with actual type ‘Maybe a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a pattern with constructor: A :: forall a. a > A,
in an equation for ‘f’
at Example.hs:12:46
• In the expression: Just x
In an equation for ‘f’: f (A x) = Just x
• Relevant bindings include
x :: a (bound at Example.hs:12:6)
f :: A > p (bound at Example.hs:12:1)
The type of the value encapsulated in an existential type (x
in this example) is considered private.
When an existential type is opened via pattern matching^{2}, a rigid type variable is allocated to denote the (unknown but fixed)
private type, i.e., x
’s type, and a unification variable (p
in this example) is allocated to denote the type of
the pattern matching branch. This rigid type variable must not escape the scope of the branch via the unification variable.
In other words, Let a
denote x
’s type in case A of (A x) > ...
. The types of local bindings within ...
(declared
in let
or where
clauses) may refer to a
(but you can’t write explicit type signatures for such bindings), but the type of
the entire ...
may not. Therefore the above f
is illtyped because the right hand side has type Maybe a
which of course
mentions a
.
If Haskell allowed the exists
keyword for existential quantification, f
would be welltyped because it would be possible
to assign the following type to f
:
f :: A > exists a. Maybe a
But Haskell doesn’t have the exists
keyword, because exists
can be expressed in terms of forall
and >
:
exists a. Maybe a ≅ forall r. (forall a. Maybe a > r) > r
Intuitively, saying “I have a Maybe a
for some a
, but I won’t tell you what a
is” is equivalent to saying “If you give me
a function that maps an arbitrary Maybe a
to r
, then I’ll give you an r
back, by applying your function to my secret Maybe a
”.
But note that the LHS and RHS above are only isomorphic; they are not identical. So f
in the above example
doesn’t have a valid haskell type, but the following function g
, which is isomorphic to f
, does have a valid type:
g :: A > (forall a. Maybe a > r) > r
g (A x) h = h (Just x)
Incidentally, in intuitionistic secondorder propositional logic^{3}, not only the existential quantifier, but also
negation, conjunction, disjunction and absurdity, can all be expressed in terms of the universal quantifier and >
. For example,
absurdity (corresponding to Haskell’s Void
type) is forall a. a
, and a \/ b
(corresponding to Haskell’s sum type)
is forall r. (a > r) > (b > r) > r
. But this is off topic so I digress.
🤔 ‘p’ is untouchable
The “untouchable” error can happen when you pattern match against a GADT without supplying a type signature. Consider this example:
data A a where
A :: A Bool
f = \case A > True
This seemingly trivial and unproblematic code does not type check:
• Couldn't match expected type ‘p’ with actual type ‘Bool’
‘p’ is untouchable
inside the constraints: a ~ Bool
bound by a pattern with constructor: A :: A Bool,
in a case alternative
at Example.hs:15:11
‘p’ is a rigid type variable bound by
the inferred type of f :: A a > p
at Example.hs:15:119
Possible fix: add a type signature for ‘f’
• In the expression: True
In a case alternative: A > True
In the expression: \case A > True
• Relevant bindings include
f :: A a > p (bound at Example.hs:15:1)
This is because f
has more than one valid type:
f :: forall a. A a > a
f :: forall a. A a > Bool
Note that neither of the above two types is more general than the other. They are just two different and incomparable types. In other words,
f
lacks a principal type (a unique most general type)^{4}. The fix is to add a type signature for f
, which is clearly indicated in the error message.
The word “untouchable” refers to the fact that the return type of the pattern matching, although a unification
variable, is considered unavailable for unification in this particular branch. Therefore it can’t actually be unified with Bool
.
If data type A
had other data constructors, and the pattern match in f
had more branches, then another branch may end up successfully
unifying the result of the pattern match with Bool. For instance if A
and f
are defined as
data A a where
A :: A Bool
B :: A a
f = \case A > True; B > True
then it would be well typed and accepted by GHC. The reason is that B
here is a regular, nonGADT data constructor (although
it is written in GADT syntax), because it returns A a
rather than A <something that is not a>
. So when type checking f
, in the
B
branch, nothing is untouchable, hence the result of the pattern match is successfully inferred to be Bool
.
It is worth mentioning that this approach is conservative, and may fail to type check a definition with a unique, most general correct type. For instance
g = \case A > 'a'
GHC can’t infer g
’s type, and fails with the same “untouchable” error. This can be confusing since g
does have a
unique, most general type, namely g :: forall a. A a > Char
.
The conservativity turns out to be unavoidable, since when GADTs are involved, the problem of determining whether a term has a principal type is undecidable. Besides, if there happens to be a type family like this:
type family F a where
F Bool = Char
Then one can argue that g
no longer has a principal type, because both of the following types are now valid:
g :: forall a. A a > F a
g :: forall a. A a > F Bool
🤔 Overloaded signature conflicts with monomorphism restriction
Consider this code in which a polymorphic constant x
is defined:
x :: Num a => a
y :: ()
(x, y) = (42, ())
Perhaps surprisingly, this definition doesn’t type check, unless monomorphism restriction is
turned off by enabling NoMonomorphismRestriction
. The error message says
Overloaded signature conflicts with monomorphism restriction
x :: forall a. Num a => a
To understand why this happens requires some knowledge about how the monomorphism restriction works. The monomorphism restriction reduces polymorphism of a definition in certain cases. It comes in two flavors:
 Some monomorphism restrictions can be resolved by adding a type signature to a binding.
 Some monomorphism restrictions cannot be resolved by adding type signatures. The above example obviously
belongs to this case, since both
x
andy
already have type signatures.
The first case is applicable to simple pattern bindings, i.e., the pattern consists of only a single variable. For instance, all of these are simple pattern bindings:
x = 42
f = show
g = \a > show a
Without type signatures, they either don’t type check, or are assigned types that are monomorphic, e.g., the
inferred type for x
is Integer
rather than Num a => a
. The fix is to add type signatures to these bindings.
On the other hand, h a = show a
is fine. It type checks and is assigned a polymorphic type. This is because h
is a function binding as opposed to a pattern binding, and the monomorphism restriction only applies to
pattern bindings.
The second case is applicable to nonsimple pattern bindings. The above example is a nonsimple pattern binding since
the lefthand side is a pair. In this case, adding a polymorphic type signature does not work, and if you want x
to have type Num a => a
, you must define it separately.
More information about monomorphism restrictions can be found in Section 4.5.5 of the Haskell 2010 report.
Final Words
Besides type error messages, there are some other aspects of GHC that can potentially be confusing to inexperienced haskell programmers, for instance when you try to do some seemingly simple and unharmful things but GHC wouldn’t let you do them. Here are some of the things off the top of my mind that I’d love to discuss in another blog post, if time permits:
 why you sometimes can’t rewrite
f (g x)
intof . g
 why you can’t partially apply type synonyms
 why sometimes you can’t
deriving Show
but you canderiving instance Show
using standalone deriving
Until then, have fun wrestling with the type checker, and stay safe and well!

Once impredicativity is supported, they will, in effect, be able to unify with types that do contain
forall
s. ↩ 
Existential types can only be opened by pattern matching. Use of record selectors is not allowed. ↩

Under the curryhoward isomorphism, intuitionistic secondorder propositional logic corresponds to polymorphic lambda calculus, a.k.a. System F, which greatly overlaps with Haskell’s type system. ↩

Another valid type of
f
isf :: A Bool > Bool
, but it is less general than both previous types, so this is not the cause of the problem. ↩