Generally speaking, GHC’s error messages are fairly helpful and intelligible (so long as you don’t go wild with type-level 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 counter-intuitive, 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:1-11 • 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
Haskell has several sorts of type variables, including:
- Type variables written by programmers, such as those bound by
foralls 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
foralls1 (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>
<actual> often contain type variables not written by the programmer, because they are compiler-allocated.
When type checking the above
f function, where
a is a programmer-written, 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
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:9-11 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
as for any
a, into a fixed
b can be flexibly chosen, for instance
fun (length :: [a] -> Int) would be legal, but it is
a, and must be fixed (i.e., does not depend on
a) once chosen.
arg does not satisfy this requirement, because it maps an
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
c. It then determines that the type of both
[a]. But sadly,
b is not allowed to
b is bound by an (implicit) top-level
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
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:4-6 • 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 matching2, 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
x’s type in
case A of (A x) -> .... The types of local bindings within
where clauses) may refer to
a (but you can’t write explicit type signatures for such bindings), but the type of
... may not. Therefore the above
f is ill-typed because the right hand side has type
Maybe a which of course
If Haskell allowed the
exists keyword for existential quantification,
f would be well-typed because it would be possible
to assign the following type to
f :: A -> exists a. Maybe a
But Haskell doesn’t have the
exists keyword, because
exists can be expressed in terms of
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
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 second-order propositional logic3, 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)
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:1-19 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
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
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, non-GADT 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
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
yalready 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
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
is a function binding as opposed to a pattern binding, and the monomorphism restriction only applies to
The second case is applicable to non-simple pattern bindings. The above example is a non-simple pattern binding since
the left-hand side is a pair. In this case, adding a polymorphic type signature does not work, and if you want
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.
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)into
f . g
- why you can’t partially apply type synonyms
- why sometimes you can’t
deriving Showbut you can
deriving instance Showusing standalone deriving
Until then, have fun wrestling with the type checker, and stay safe and well!
Existential types can only be opened by pattern matching. Use of record selectors is not allowed. ↩
Under the curry-howard isomorphism, intuitionistic second-order 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 :: A Bool -> Bool, but it is less general than both previous types, so this is not the cause of the problem. ↩