Dynamic binding constraints behave just like other type class constraints in that they are automatically propagated. Thus, when a function is used, its implicit parameters are inherited by the function that called it. For example, our sort function might be used to pick out the least value in a list:

  least   :: (?cmp :: a -> a -> Bool) => [a] -> a
  least xs = head (sort xs)

Without lifting a finger, the ?cmp parameter is propagated to become a parameter of least as well. With explicit parameters, the default is that parameters must always be explicit propagated. With implicit parameters, the default is to always propagate them.

An implicit-parameter type constraint differs from other type class constraints in the following way: All uses of a particular implicit parameter must have the same type. This means that the type of (?x, ?x) is (?x::a) => (a,a), and not (?x::a, ?x::b) => (a, b), as would be the case for type class constraints.

You can't have an implicit parameter in the context of a class or instance declaration. For example, both these declarations are illegal:

  class (?x::Int) => C a where ...
  instance (?x::a) => Foo [a] where ...

Reason: exactly which implicit parameter you pick up depends on exactly where you invoke a function. But the ``invocation'' of instance declarations is done behind the scenes by the compiler, so it's hard to figure out exactly where it is done. Easiest thing is to outlaw the offending types.

Implicit-parameter constraints do not cause ambiguity. For example, consider:

   f :: (?x :: [a]) => Int -> Int
   f n = n + length ?x

   g :: (Read a, Show a) => String -> String
   g s = show (read s)

Here, g has an ambiguous type, and is rejected, but f is fine. The binding for ?x at f's call site is quite unambiguous, and fixes the type a.

An implicit parameter is bound using the standard let or where binding forms. For example, we define the min function by binding cmp.

  min :: [a] -> a
  min  = let ?cmp = (<=) in least

A group of implicit-parameter bindings may occur anywhere a normal group of Haskell bindings can occur, except at top level. That is, they can occur in a let (including in a list comprehension, or do-notation, or pattern guards), or a where clause. Note the following points:

Consider these two definitions:

  len1 :: [a] -> Int
  len1 xs = let ?acc = 0 in len_acc1 xs

  len_acc1 [] = ?acc
  len_acc1 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs

  ------------

  len2 :: [a] -> Int
  len2 xs = let ?acc = 0 in len_acc2 xs

  len_acc2 :: (?acc :: Int) => [a] -> Int
  len_acc2 [] = ?acc
  len_acc2 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs

The only difference between the two groups is that in the second group len_acc is given a type signature. In the former case, len_acc1 is monomorphic in its own right-hand side, so the implicit parameter ?acc is not passed to the recursive call. In the latter case, because len_acc2 has a type signature, the recursive call is made to the polymorphic version, which takes ?acc as an implicit parameter. So we get the following results in GHCi:

  Prog> len1 "hello"
  0
  Prog> len2 "hello"
  5

Adding a type signature dramatically changes the result! This is a rather counter-intuitive phenomenon, worth watching out for.

GHC applies the dreaded Monomorphism Restriction (section 4.5.5 of the Haskell Report) to implicit parameters. For example, consider:

 f :: Int -> Int
  f v = let ?x = 0     in
        let y = ?x + v in
        let ?x = 5     in
        y

Since the binding for y falls under the Monomorphism Restriction it is not generalised, so the type of y is simply Int, not (?x::Int) => Int. Hence, (f 9) returns result 9. If you add a type signature for y, then y will get type (?x::Int) => Int, so the occurrence of y in the body of the let will see the inner binding of ?x, so (f 9) will return 14.

In a data or newtype declaration one can quantify the types of the constructor arguments. Here are several examples:

data T a = T1 (forall b. b -> b -> b) a

data MonadT m = MkMonad { return :: forall a. a -> m a,
                          bind   :: forall a b. m a -> (a -> m b) -> m b
                        }

newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])

The constructors have rank-2 types:

T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
MkMonad :: forall m. (forall a. a -> m a)
                  -> (forall a b. m a -> (a -> m b) -> m b)
                  -> MonadT m
MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle

Notice that you don't need to use a forall if there's an explicit context. For example in the first argument of the constructor MkSwizzle, an implicit "forall a." is prefixed to the argument type. The implicit forall quantifies all type variables that are not already in scope, and are mentioned in the type quantified over. (Arguably, it would be better to require explicit quantification on constructor arguments where that is what is wanted. See Trac #4426.)

As for type signatures, implicit quantification happens for non-overloaded types too. So if you write this:

  f :: (a -> a) -> a

it's just as if you had written this:

  f :: forall a. (a -> a) -> a

That is, since the type variable a isn't in scope, it's implicitly universally quantified.

You construct values of types T1, MonadT, Swizzle by applying the constructor to suitable values, just as usual. For example,

    a1 :: T Int
    a1 = T1 (\xy->x) 3

    a2, a3 :: Swizzle
    a2 = MkSwizzle sort
    a3 = MkSwizzle reverse

    a4 :: MonadT Maybe
    a4 = let r x = Just x
	     b m k = case m of
		       Just y -> k y
		       Nothing -> Nothing
         in
         MkMonad r b

    mkTs :: (forall b. b -> b -> b) -> a -> [T a]
    mkTs f x y = [T1 f x, T1 f y]

The type of the argument can, as usual, be more general than the type required, as (MkSwizzle reverse) shows. (reverse does not need the Ord constraint.)

When you use pattern matching, the bound variables may now have polymorphic types. For example:

    f :: T a -> a -> (a, Char)
    f (T1 w k) x = (w k x, w 'c' 'd')

    g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b]
    g (MkSwizzle s) xs f = s (map f (s xs))

    h :: MonadT m -> [m a] -> m [a]
    h m [] = return m []
    h m (x:xs) = bind m x          $ \y ->
                 bind m (h m xs)   $ \ys ->
                 return m (y:ys)

In the function h we use the record selectors return and bind to extract the polymorphic bind and return functions from the MonadT data structure, rather than using pattern matching.

In general, type inference for arbitrary-rank types is undecidable. GHC uses an algorithm proposed by Odersky and Laufer ("Putting type annotations to work", POPL'96) to get a decidable algorithm by requiring some help from the programmer. We do not yet have a formal specification of "some help" but the rule is this:

For a lambda-bound or case-bound variable, x, either the programmer provides an explicit polymorphic type for x, or GHC's type inference will assume that x's type has no foralls in it.

What does it mean to "provide" an explicit type for x? You can do that by giving a type signature for x directly, using a pattern type signature (Section 7.12.8, “Lexically scoped type variables ”), thus:

     \ f :: (forall a. a->a) -> (f True, f 'c')

Alternatively, you can give a type signature to the enclosing context, which GHC can "push down" to find the type for the variable:

     (\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)

Here the type signature on the expression can be pushed inwards to give a type signature for f. Similarly, and more commonly, one can give a type signature for the function itself:

     h :: (forall a. a->a) -> (Bool,Char)
     h f = (f True, f 'c')

You don't need to give a type signature if the lambda bound variable is a constructor argument. Here is an example we saw earlier:

    f :: T a -> a -> (a, Char)
    f (T1 w k) x = (w k x, w 'c' 'd')

Here we do not need to give a type signature to w, because it is an argument of constructor T1 and that tells GHC all it needs to know.

GHC performs implicit quantification as follows. At the top level (only) of user-written types, if and only if there is no explicit forall, GHC finds all the type variables mentioned in the type that are not already in scope, and universally quantifies them. For example, the following pairs are equivalent:

  f :: a -> a
  f :: forall a. a -> a

  g (x::a) = let
                h :: a -> b -> b
                h x y = y
             in ...
  g (x::a) = let
                h :: forall b. a -> b -> b
                h x y = y
             in ...

Notice that GHC does not find the innermost possible quantification point. For example:

  f :: (a -> a) -> Int
           -- MEANS
  f :: forall a. (a -> a) -> Int
           -- NOT
  f :: (forall a. a -> a) -> Int


  g :: (Ord a => a -> a) -> Int
           -- MEANS the illegal type
  g :: forall a. (Ord a => a -> a) -> Int
           -- NOT
  g :: (forall a. Ord a => a -> a) -> Int

The latter produces an illegal type, which you might think is silly, but at least the rule is simple. If you want the latter type, you can write your for-alls explicitly. Indeed, doing so is strongly advised for rank-2 types.

The design follows the following principles

A lexically scoped type variable can be bound by:

In Haskell, a programmer-written type signature is implicitly quantified over its free type variables (Section 4.1.2 of the Haskell Report). Lexically scoped type variables affect this implicit quantification rules as follows: any type variable that is in scope is not universally quantified. For example, if type variable a is in scope, then

  (e :: a -> a)     means     (e :: a -> a)
  (e :: b -> b)     means     (e :: forall b. b->b)
  (e :: a -> b)     means     (e :: forall b. a->b)

A declaration type signature that has explicit quantification (using forall) brings into scope the explicitly-quantified type variables, in the definition of the named function. For example:

  f :: forall a. [a] -> [a]
  f (x:xs) = xs ++ [ x :: a ]

The "forall a" brings "a" into scope in the definition of "f".

This only happens if:

An expression type signature that has explicit quantification (using forall) brings into scope the explicitly-quantified type variables, in the annotated expression. For example:

  f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )

Here, the type signature forall s. ST s Bool brings the type variable s into scope, in the annotated expression (op >>= \(x :: STRef s Int) -> g x).

A type signature may occur in any pattern; this is a pattern type signature. For example:

  -- f and g assume that 'a' is already in scope
  f = \(x::Int, y::a) -> x
  g (x::a) = x
  h ((x,y) :: (Int,Bool)) = (y,x)

In the case where all the type variables in the pattern type signature are already in scope (i.e. bound by the enclosing context), matters are simple: the signature simply constrains the type of the pattern in the obvious way.

Unlike expression and declaration type signatures, pattern type signatures are not implicitly generalised. The pattern in a pattern binding may only mention type variables that are already in scope. For example:

  f :: forall a. [a] -> (Int, [a])
  f xs = (n, zs)
    where
      (ys::[a], n) = (reverse xs, length xs) -- OK
      zs::[a] = xs ++ ys                     -- OK

      Just (v::b) = ...  -- Not OK; b is not in scope

Here, the pattern signatures for ys and zs are fine, but the one for v is not because b is not in scope.

However, in all patterns other than pattern bindings, a pattern type signature may mention a type variable that is not in scope; in this case, the signature brings that type variable into scope. This is particularly important for existential data constructors. For example:

  data T = forall a. MkT [a]

  k :: T -> T
  k (MkT [t::a]) = MkT t3
                 where
                   t3::[a] = [t,t,t]

Here, the pattern type signature (t::a) mentions a lexical type variable that is not already in scope. Indeed, it cannot already be in scope, because it is bound by the pattern match. GHC's rule is that in this situation (and only then), a pattern type signature can mention a type variable that is not already in scope; the effect is to bring it into scope, standing for the existentially-bound type variable.

When a pattern type signature binds a type variable in this way, GHC insists that the type variable is bound to a rigid, or fully-known, type variable. This means that any user-written type signature always stands for a completely known type.

If all this seems a little odd, we think so too. But we must have some way to bring such type variables into scope, else we could not name existentially-bound type variables in subsequent type signatures.

This is (now) the only situation in which a pattern type signature is allowed to mention a lexical variable that is not already in scope. For example, both f and g would be illegal if a was not already in scope.

The type variables in the head of a class or instance declaration scope over the methods defined in the where part. For example:

  class C a where
    op :: [a] -> a

    op xs = let ys::[a]
                ys = reverse xs
            in
            head ys

Haskell's monomorphism restriction (see Section 4.5.5 of the Haskell Report) can be completely switched off by -XNoMonomorphismRestriction.

The Haskell Report specifies that a group of bindings (at top level, or in a let or where) should be sorted into strongly-connected components, and then type-checked in dependency order (Haskell Report, Section 4.5.1). As each group is type-checked, any binders of the group that have an explicit type signature are put in the type environment with the specified polymorphic type, and all others are monomorphic until the group is generalised (Haskell Report, Section 4.5.2).

Following a suggestion of Mark Jones, in his paper Typing Haskell in Haskell, GHC implements a more general scheme. If -XRelaxedPolyRec is specified: the dependency analysis ignores references to variables that have an explicit type signature. As a result of this refined dependency analysis, the dependency groups are smaller, and more bindings will typecheck. For example, consider:

  f :: Eq a => a -> Bool
  f x = (x == x) || g True || g "Yes"

  g y = (y <= y) || f True

This is rejected by Haskell 98, but under Jones's scheme the definition for g is typechecked first, separately from that for f, because the reference to f in g's right hand side is ignored by the dependency analysis. Then g's type is generalised, to get

  g :: Ord a => a -> Bool

Now, the definition for f is typechecked, with this type for g in the type environment.

The same refined dependency analysis also allows the type signatures of mutually-recursive functions to have different contexts, something that is illegal in Haskell 98 (Section 4.5.2, last sentence). With -XRelaxedPolyRec GHC only insists that the type signatures of a refined group have identical type signatures; in practice this means that only variables bound by the same pattern binding must have the same context. For example, this is fine:

  f :: Eq a => a -> Bool
  f x = (x == x) || g True

  g :: Ord a => a -> Bool
  g y = (y <= y) || f True

An ML-style language usually generalises the type of any let-bound or where-bound variable, so that it is as polymorphic as possible. With the flag -XMonoLocalBinds GHC implements a slightly more conservative policy: it generalises only "closed" bindings. A binding is considered "closed" if either

For example, consider

f x = x + 1
g x = let h y = f y * 2
          k z = z+x
      in  h x + k x

Here f and g are closed because they are bound at top level. Also h is closed because its only free variable f is closed. But k is not closed because it mentions x which is locally bound. Another way to think of it is this: all closed bindings could be defined at top level. (In the example, we could move h to top level.)

All of this applies only to bindings that lack an explicit type signature, so that GHC has to infer its type. If you supply a type signature, then that fixes type of the binding, end of story.

The rationale for this more conservative strategy is given in the papers "Let should not be generalised" and "Modular type inference with local assumptions", and a related blog post.

The flag -XMonoLocalBinds is implied by -XTypeFamilies and -XGADTs. You can switch it off again with -XNoMonoLocalBinds but type inference becomes less predicatable if you do so. (Read the papers!)