6.4.6. Type variable defaulting

During type-checking, the typechecker will create metavariables that stand for as-yet unknown types. If the typechecker cannot infer a specific type for a metavariable (nor quantify over it), it will default the type variable to a specific type, such as Int or String.

The main principle of defaulting is that it is used as a best guess for type variables that remain undetermined at the very end of type inference.

For example:

-- Ambiguity:
u :: String
u = show 4.12
  -- The type of 4.12 is ambiguous; default it to Double

-- Monomorphism restriction:
k = 6
  -- Due to the monomorphism restriction, we must infer a monomorphic type, not:
  --
  --   k :: forall a. Num a => a
  --
  -- GHC defaults the type of k to Integer.

-- NoPolyKinds:
f Proxy = ()
  -- With -XNoPolyKinds, we cannot infer the poly-kinded type
  --
  --   forall {k} (a :: k). Proxy a -> ()
  --
  -- GHC defaults (k := Type), thus inferring
  --
  --   f :: forall (a :: Type). Proxy a -> ()

-- Representation polymorphism:
g x = x
  -- Should not quantify over the representation, as we cannot infer
  -- a representation-polymorphic type for 'x':
  --
  --   forall {r} (a :: TYPE r). a -> a
  --
  -- Default r := LiftedRep, thus inferring
  --
  --   g :: forall (a :: Type). a -> a

-- Multiplicity polymorphism
{-# LANGUAGE LinearTypes #-}
h x = x
  -- Do not infer multiplicity polymorphism:
  --
  -- h :: forall {m} a. a %m -> a
  --
  -- GHC defaults (m := Many), thus inferring
  --
  --   h :: forall (a :: Type). a %Many -> a

The rest of this section will explain how defaulting assignment choices are made by GHC.

6.4.6.1. Type class defaulting

The principal defaulting mechanism is type class defaulting. It is used in situations such as:

u :: String
u = show 4.12
  -- (4.12 :: a), with constraints (Fractional a, Show a).

v :: [Int] -> [Char] -> Bool
v xs ys = genericLength xs > genericLength ys
  -- Recall that (genericLength :: Num i => [x] -> i). Here, the return type
  -- of the two calls to genericLength are ambiguous; we get
  -- (genericLength xs :: a) with constraints (Num a, Ord a).

The idea is that, because the type variable a appears as the argument to an unsolved numeric constraint such as Num a or Fractional a, it is natural to default a to a numeric type such as Double or Integer, respectively.

The original rules from the (Haskell Report, Section 4.3.4) for defaulting an unfilled metavariable a are as follows:

  1. The type variable a appears only in constraints of the form C v for a class C. (Small asterisk: ignoring invisible type parameters, e.g. the kind parameter for Typeable.)

  2. All the classes that a appears in are standard (i.e. they are defined in the Prelude or a standard library).

  3. At least one of the classes is numeric (e.g. is Num, or implies Num).

In such a situation, GHC will attempt to default a by looking at which default declarations are in scope in the module, e.g.:

default (Int, Integer, Double)

means: first try to default a to Int. If that fails, try Integer instead, and if that fails try Double. The Haskell report requires that all the types listed in the default declaration must be instances of Num.

If the module contains no default declaration, then GHC behaves as if the following fallback default declaration is present:

default (Integer, Double)

6.4.6.2. Extensions to type class defaulting

Several extensions to the rules are available. The basic mechanism described above dictates that the only defaultable classes are the numeric classes, with the extra constraint that all classes must be standard.

6.4.6.2.1. Overloaded strings

OverloadedStrings extends both the defaultable and standard classes to include IsString. It allows types that are instances of IsString in default declarations, and adds String to the fallback default declaration when no default declaration is provided.

6.4.6.2.2. Named defaults

NamedDefaults allows per-class default declarations, e.g. default Show (Int, Bool), with the requirement that the types are instances of the class. The sets of defaultable and standard classes are both extended to include any class with a named default declaration.

6.4.6.2.3. Extended default rules

ExtendedDefaultRules, which is enabled by default in the GHCi prompt, extends the rules more significantly:

  1. It extends the set of defautable classes to include interactive classes, adding Show, Eq, Ord, Foldable, Traversable. Types that are instances of any of these classes are then allowed in default declarations.

  2. It adds the unit type () and the list type [] to the start of the fallback default declaration.

  3. The rules for defaulting are changed to the following:

  1. Find the constraints that are of form C a where a is a type variable, and partition those constraints into groups that share a common type variable a.

  2. Keep only the groups in which at least one of the classes is a defaultable class. (As explained above, these include the interactive classes, IsString with OverloadedStrings, and any class with a named default declaration with NamedDefaults.)

  3. For each remaining group G, try each type ty from the default-type list in turn. If setting a = ty would allow the constraints in G to be completely solved, default a to ty; otherwise try the next type in the list.

To rephrase, (3) means that we filter out all the constraints that are not of the form C a for a defaultable class C. Such constraints thus do not participate in the process (either to help or to hinder); but they must of course be soluble once the defaulting process is complete. In particular, this includes all multi-parameter constraints such as D a b or E [a] Int.

6.4.6.3. Other defaulting mechanisms

Besides the main type-class defaulting mechanism described in Type class defaulting, GHC also contains a several other (more specialised) mechanisms for defaulting.

6.4.6.3.1. Kind-based defaulting

For type variables of kind RuntimeRep or Levity, GHC will default them to LiftedRep and Lifted, respectively. This is explained in Inference and defaulting.

For type variables of kind Multiplicity, GHC will default to Many, as explained in Linear types: linear and multiplicity-polymorphic arrows are always declared, never inferred.

For kind variables (of kind Type), GHC will default to Type when PolyKinds is not enabled; see Kind defaulting without PolyKinds.

6.4.6.3.2. Callstack defaulting

To implement the HasCallStack and ExceptionContext mechanisms, GHC will default any unsolved HasCallStack constraints to EmptyCallStack, and any unsolved ExceptionContext constraints to emptyExceptionContext, respectively.

6.4.6.3.3. Equality defaulting

Usually, when GHC encounters an equality constraint alpha ~ ty in which alpha is an unfilled metavariable, GHC will immediately unify alpha with ty. However, in certain circumstances, GHC will hold off from eagerly unifying alpha := ty in order to preserve the ability to infer principal types. For example:

{-# LANGUAGE GADTs #-}
data T a where
  MkT :: T Bool
h x = case x of { MkT -> True }

Within the case match, GHC creates a fresh metavariable beta for the return type, but this metavariable is “stuck” inside the equality constraint introduced by the GADT pattern match:

forall a. a ~ Bool => beta ~ Bool

Here GHC could either unify beta := a or beta := Bool, which would result in the following type signatures for h, respectively:

forall a. T a -> a
T Bool -> Bool

Neither of these is more general than the other, so GHC holds off from unifying beta := Bool – even though there is an unsolved equality constraint beta ~ Bool. Because we are not at the top-level (we are inside a GADT pattern match), this will cause GHC to reject this program (fix: add a type signature to h).

However, in cases where typechecking does manage to proceed to the top-level, it makes sense to default unfilled metavariables that appear in unsolved nominal equality constraints. For example:

f :: forall a. (forall t. (F t ~ Int) => a -> Int) -> Int

g :: Int
g = f id

In this case, when instantiating f in the body of g, GHC will create a fresh metavariable alpha for the outer forall of f, which again appears in an implication below another equality constraint:

forall t. (F t ~ Int) => alpha ~ Int

However, unlike in the previous GADT example, here we are at the top-level and we can’t quantify over alpha. So GHC goes ahead and defaults alpha to Int; this does not threaten principal types.