With the -fglasgow-exts flag, GHC lets you declare a data type with no constructors. For example:

  data S      -- S :: *
  data T a    -- T :: * -> *

Syntactically, the declaration lacks the "= constrs" part. The type can be parameterised over types of any kind, but if the kind is not * then an explicit kind annotation must be used (see Section 7.4.7, “Explicitly-kinded quantification”).

Such data types have only one value, namely bottom. Nevertheless, they can be useful when defining "phantom types".

GHC allows type constructors, classes, and type variables to be operators, and to be written infix, very much like expressions. More specifically:

Type synonyms are like macros at the type level, and GHC does validity checking on types only after expanding type synonyms. That means that GHC can be very much more liberal about type synonyms than Haskell 98:

GHC currently does kind checking before expanding synonyms (though even that could be changed.)

After expanding type synonyms, GHC does validity checking on types, looking for the following mal-formedness which isn't detected simply by kind checking:

So, for example, this will be rejected:

  type Pr = (# Int, Int #)

  h :: Pr -> Int
  h x = ...

because GHC does not allow unboxed tuples on the left of a function arrow.

The idea of using existential quantification in data type declarations was suggested by Perry, and implemented in Hope+ (Nigel Perry, The Implementation of Practical Functional Programming Languages, PhD Thesis, University of London, 1991). It was later formalised by Laufer and Odersky (Polymorphic type inference and abstract data types, TOPLAS, 16(5), pp1411-1430, 1994). It's been in Lennart Augustsson's hbc Haskell compiler for several years, and proved very useful. Here's the idea. Consider the declaration:

  data Foo = forall a. MkFoo a (a -> Bool)
           | Nil

The data type Foo has two constructors with types:

  MkFoo :: forall a. a -> (a -> Bool) -> Foo
  Nil   :: Foo

Notice that the type variable a in the type of MkFoo does not appear in the data type itself, which is plain Foo. For example, the following expression is fine:

  [MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]

Here, (MkFoo 3 even) packages an integer with a function even that maps an integer to Bool; and MkFoo 'c' isUpper packages a character with a compatible function. These two things are each of type Foo and can be put in a list.

What can we do with a value of type Foo?. In particular, what happens when we pattern-match on MkFoo?

  f (MkFoo val fn) = ???

Since all we know about val and fn is that they are compatible, the only (useful) thing we can do with them is to apply fn to val to get a boolean. For example:

  f :: Foo -> Bool
  f (MkFoo val fn) = fn val

What this allows us to do is to package heterogenous values together with a bunch of functions that manipulate them, and then treat that collection of packages in a uniform manner. You can express quite a bit of object-oriented-like programming this way.

  MkFoo :: (exists a . (a, a -> Bool)) -> Foo

data Baz = forall a. Eq a => Baz1 a a
         | forall b. Show b => Baz2 b (b -> b)

Baz1 :: forall a. Eq a => a -> a -> Baz
Baz2 :: forall b. Show b => b -> (b -> b) -> Baz

  f :: Baz -> String
  f (Baz1 p q) | p == q    = "Yes"
               | otherwise = "No"
  f (Baz2 v fn)            = show (fn v)

data Counter a = forall self. NewCounter
    { _this    :: self
    , _inc     :: self -> self
    , _display :: self -> IO ()
    , tag      :: a
    }

inc :: Counter a -> Counter a
inc (NewCounter x i d t) = NewCounter
    { _this = i x, _inc = i, _display = d, tag = t } 

display :: Counter a -> IO ()
display NewCounter{ _this = x, _display = d } = d x

counterA :: Counter String 
counterA = NewCounter
    { _this = 0, _inc = (1+), _display = print, tag = "A" }

counterB :: Counter String 
counterB = NewCounter
    { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }

main = do
    display (inc counterA)         -- prints "1"
    display (inc (inc counterB))   -- prints "##"

data Counter a where
    NewCounter { _this    :: self
               , _inc     :: self -> self
               , _display :: self -> IO ()
               , tag      :: a
               }
        :: Counter a

-- This is invalid; use explicit NewCounter instead for now
setTag :: Counter a -> a -> Counter a
setTag obj t = obj{ tag = t }

Multi-parameter type classes are permitted. For example:

  class Collection c a where
    union :: c a -> c a -> c a
    ...etc.

There are no restrictions on the context in a class declaration (which introduces superclasses), except that the class hierarchy must be acyclic. So these class declarations are OK:

  class Functor (m k) => FiniteMap m k where
    ...

  class (Monad m, Monad (t m)) => Transform t m where
    lift :: m a -> (t m) a

As in Haskell 98, The class hierarchy must be acyclic. However, the definition of "acyclic" involves only the superclass relationships. For example, this is OK:

  class C a where {
    op :: D b => a -> b -> b
  }

  class C a => D a where { ... }

Here, C is a superclass of D, but it's OK for a class operation op of C to mention D. (It would not be OK for D to be a superclass of C.)

Haskell 98 prohibits class method types to mention constraints on the class type variable, thus:

  class Seq s a where
    fromList :: [a] -> s a
    elem     :: Eq a => a -> s a -> Bool

The type of elem is illegal in Haskell 98, because it contains the constraint Eq a, constrains only the class type variable (in this case a). GHC lifts this restriction.

In a class declaration, all of the class type variables must be reachable (in the sense mentioned in Section 7.4.5, “Type signatures”) from the free variables of each method type. For example:

  class Coll s a where
    empty  :: s
    insert :: s -> a -> s

is not OK, because the type of empty doesn't mention a. Functional dependencies can make the type variable reachable:

  class Coll s a | s -> a where
    empty  :: s
    insert :: s -> a -> s

Alternatively Coll might be rewritten

  class Coll s a where
    empty  :: s a
    insert :: s a -> a -> s a

which makes the connection between the type of a collection of a's (namely (s a)) and the element type a. Occasionally this really doesn't work, in which case you can split the class like this:

  class CollE s where
    empty  :: s

  class CollE s => Coll s a where
    insert :: s -> a -> s

The following description of the motivation and use of functional dependencies is taken from the Hugs user manual, reproduced here (with minor changes) by kind permission of Mark Jones.

Consider the following class, intended as part of a library for collection types:

   class Collects e ce where
       empty  :: ce
       insert :: e -> ce -> ce
       member :: e -> ce -> Bool

The type variable e used here represents the element type, while ce is the type of the container itself. Within this framework, we might want to define instances of this class for lists or characteristic functions (both of which can be used to represent collections of any equality type), bit sets (which can be used to represent collections of characters), or hash tables (which can be used to represent any collection whose elements have a hash function). Omitting standard implementation details, this would lead to the following declarations:

   instance Eq e => Collects e [e] where ...
   instance Eq e => Collects e (e -> Bool) where ...
   instance Collects Char BitSet where ...
   instance (Hashable e, Collects a ce)
              => Collects e (Array Int ce) where ...

All this looks quite promising; we have a class and a range of interesting implementations. Unfortunately, there are some serious problems with the class declaration. First, the empty function has an ambiguous type:

   empty :: Collects e ce => ce

By "ambiguous" we mean that there is a type variable e that appears on the left of the => symbol, but not on the right. The problem with this is that, according to the theoretical foundations of Haskell overloading, we cannot guarantee a well-defined semantics for any term with an ambiguous type.

We can sidestep this specific problem by removing the empty member from the class declaration. However, although the remaining members, insert and member, do not have ambiguous types, we still run into problems when we try to use them. For example, consider the following two functions:

   f x y = insert x . insert y
   g     = f True 'a'

for which GHC infers the following types:

   f :: (Collects a c, Collects b c) => a -> b -> c -> c
   g :: (Collects Bool c, Collects Char c) => c -> c

Notice that the type for f allows the two parameters x and y to be assigned different types, even though it attempts to insert each of the two values, one after the other, into the same collection. If we're trying to model collections that contain only one type of value, then this is clearly an inaccurate type. Worse still, the definition for g is accepted, without causing a type error. As a result, the error in this code will not be flagged at the point where it appears. Instead, it will show up only when we try to use g, which might even be in a different module.

   class Collects e c where
      empty  :: c e
      insert :: e -> c e -> c e
      member :: e -> c e -> Bool

   f :: (Collects e c) => e -> e -> c e -> c e

   class C a b where ...

   class D a b | a -> b where ...
   class E a b | a -> b, b -> a where ...

   instance D Bool Int where ...
   instance D Bool Char where ...

   instance D [a] b where ...

   instance D t s where ...

   class Collects e ce | ce -> e where
      empty  :: ce
      insert :: e -> ce -> ce
      member :: e -> ce -> Bool

   f x y = insert x y = insert x . insert y

   f :: (Collects a c, Collects b c) => a -> b -> c -> c

   f :: (Collects a c) => a -> a -> c -> c

An instance declaration has the form

  instance ( assertion1, ..., assertionn) => class type1 ... typem where ...

The part before the "=>" is the context, while the part after the "=>" is the head of the instance declaration.

In Haskell 98 the head of an instance declaration must be of the form C (T a1 ... an), where C is the class, T is a type constructor, and the a1 ... an are distinct type variables. Furthermore, the assertions in the context of the instance declaration must be of the form C a where a is a type variable that occurs in the head.

The -fglasgow-exts flag loosens these restrictions considerably. Firstly, multi-parameter type classes are permitted. Secondly, the context and head of the instance declaration can each consist of arbitrary (well-kinded) assertions (C t1 ... tn) subject only to the following rules:

These restrictions ensure that context reduction terminates: each reduction step makes the problem smaller by at least one constructor. For example, the following would make the type checker loop if it wasn't excluded:

  instance C a => C a where ...

For example, these are OK:

  instance C Int [a]          -- Multiple parameters
  instance Eq (S [a])         -- Structured type in head

      -- Repeated type variable in head
  instance C4 a a => C4 [a] [a] 
  instance Stateful (ST s) (MutVar s)

      -- Head can consist of type variables only
  instance C a
  instance (Eq a, Show b) => C2 a b

      -- Non-type variables in context
  instance Show (s a) => Show (Sized s a)
  instance C2 Int a => C3 Bool [a]
  instance C2 Int a => C3 [a] b

But these are not:

      -- Context assertion no smaller than head
  instance C a => C a where ...
      -- (C b b) has more more occurrences of b than the head
  instance C b b => Foo [b] where ...

The same restrictions apply to instances generated by deriving clauses. Thus the following is accepted:

  data MinHeap h a = H a (h a)
    deriving (Show)

because the derived instance

  instance (Show a, Show (h a)) => Show (MinHeap h a)

conforms to the above rules.

A useful idiom permitted by the above rules is as follows. If one allows overlapping instance declarations then it's quite convenient to have a "default instance" declaration that applies if something more specific does not:

  instance C a where
    op = ... -- Default

You can find lots of background material about the reason for these restrictions in the paper Understanding functional dependencies via Constraint Handling Rules.

Sometimes even the rules of Section 7.4.4.1, “Relaxed rules for instance declarations” are too onerous. For example, sometimes you might want to use the following to get the effect of a "class synonym":

  class (C1 a, C2 a, C3 a) => C a where { }

  instance (C1 a, C2 a, C3 a) => C a where { }

This allows you to write shorter signatures:

  f :: C a => ...

instead of

  f :: (C1 a, C2 a, C3 a) => ...

The restrictions on functional dependencies (Section 7.4.3, “Functional dependencies ”) are particularly troublesome. It is tempting to introduce type variables in the context that do not appear in the head, something that is excluded by the normal rules. For example:

  class HasConverter a b | a -> b where
     convert :: a -> b
   
  data Foo a = MkFoo a

  instance (HasConverter a b,Show b) => Show (Foo a) where
     show (MkFoo value) = show (convert value)

This is dangerous territory, however. Here, for example, is a program that would make the typechecker loop:

  class D a
  class F a b | a->b
  instance F [a] [[a]]
  instance (D c, F a c) => D [a]   -- 'c' is not mentioned in the head

Similarly, it can be tempting to lift the coverage condition:

  class Mul a b c | a b -> c where
  	(.*.) :: a -> b -> c

  instance Mul Int Int Int where (.*.) = (*)
  instance Mul Int Float Float where x .*. y = fromIntegral x * y
  instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v

The third instance declaration does not obey the coverage condition; and indeed the (somewhat strange) definition:

  f = \ b x y -> if b then x .*. [y] else y

makes instance inference go into a loop, because it requires the constraint (Mul a [b] b).

Nevertheless, GHC allows you to experiment with more liberal rules. If you use the experimental flag -fallow-undecidable-instances , you can use arbitrary types in both an instance context and instance head. Termination is ensured by having a fixed-depth recursion stack. If you exceed the stack depth you get a sort of backtrace, and the opportunity to increase the stack depth with -fcontext-stack=N.

In general, GHC requires that that it be unambiguous which instance declaration should be used to resolve a type-class constraint. This behaviour can be modified by two flags: -fallow-overlapping-instances and -fallow-incoherent-instances , as this section discusses. Both these flags are dynamic flags, and can be set on a per-module basis, using an OPTIONS_GHC pragma if desired (Section 4.1.2, “command line options in source files”).

When GHC tries to resolve, say, the constraint C Int Bool, it tries to match every instance declaration against the constraint, by instantiating the head of the instance declaration. For example, consider these declarations:

  instance context1 => C Int a     where ...  -- (A)
  instance context2 => C a   Bool  where ...  -- (B)
  instance context3 => C Int [a]   where ...  -- (C)
  instance context4 => C Int [Int] where ...  -- (D)

The instances (A) and (B) match the constraint C Int Bool, but (C) and (D) do not. When matching, GHC takes no account of the context of the instance declaration (context1 etc). GHC's default behaviour is that exactly one instance must match the constraint it is trying to resolve. It is fine for there to be a potential of overlap (by including both declarations (A) and (B), say); an error is only reported if a particular constraint matches more than one.

The -fallow-overlapping-instances flag instructs GHC to allow more than one instance to match, provided there is a most specific one. For example, the constraint C Int [Int] matches instances (A), (C) and (D), but the last is more specific, and hence is chosen. If there is no most-specific match, the program is rejected.

However, GHC is conservative about committing to an overlapping instance. For example:

  f :: [b] -> [b]
  f x = ...

Suppose that from the RHS of f we get the constraint C Int [b]. But GHC does not commit to instance (C), because in a particular call of f, b might be instantiate to Int, in which case instance (D) would be more specific still. So GHC rejects the program. If you add the flag -fallow-incoherent-instances, GHC will instead pick (C), without complaining about the problem of subsequent instantiations.

The willingness to be overlapped or incoherent is a property of the instance declaration itself, controlled by the presence or otherwise of the -fallow-overlapping-instances and -fallow-incoherent-instances flags when that mdodule is being defined. Neither flag is required in a module that imports and uses the instance declaration. Specifically, during the lookup process:

These rules make it possible for a library author to design a library that relies on overlapping instances without the library client having to know.

If an instance declaration is compiled without -fallow-overlapping-instances, then that instance can never be overlapped. This could perhaps be inconvenient. Perhaps the rule should instead say that the overlapping instance declaration should be compiled in this way, rather than the overlapped one. Perhaps overlap at a usage site should be permitted regardless of how the instance declarations are compiled, if the -fallow-overlapping-instances flag is used at the usage site. (Mind you, the exact usage site can occasionally be hard to pin down.) We are interested to receive feedback on these points.

The -fallow-incoherent-instances flag implies the -fallow-overlapping-instances flag, but not vice versa.

Unlike Haskell 98, instance heads may use type synonyms. (The instance "head" is the bit after the "=>" in an instance decl.) As always, using a type synonym is just shorthand for writing the RHS of the type synonym definition. For example:

  type Point = (Int,Int)
  instance C Point   where ...
  instance C [Point] where ...

is legal. However, if you added

  instance C (Int,Int) where ...

as well, then the compiler will complain about the overlapping (actually, identical) instance declarations. As always, type synonyms must be fully applied. You cannot, for example, write:

  type P a = [[a]]
  instance Monad P where ...

This design decision is independent of all the others, and easily reversed, but it makes sense to me.

Unlike Haskell 98, constraints in types do not have to be of the form (class type-variable) or (class (type-variable type-variable ...)). Thus, these type signatures are perfectly OK

  g :: Eq [a] => ...
  g :: Ord (T a ()) => ...

GHC imposes the following restrictions on the constraints in a type signature. Consider the type:

  forall tv1..tvn (c1, ...,cn) => type

(Here, we write the "foralls" explicitly, although the Haskell source language omits them; in Haskell 98, all the free type variables of an explicit source-language type signature are universally quantified, except for the class type variables in a class declaration. However, in GHC, you can give the foralls if you want. See Section 7.4.8, “Arbitrary-rank polymorphism ”).

It is often convenient to use generalised type synonyms (see Section 7.4.1.3, “Liberalised type synonyms”) at the right hand end of an arrow, thus:

  type Discard a = forall b. a -> b -> a

  g :: Int -> Discard Int
  g x y z = x+y

Simply expanding the type synonym would give

  g :: Int -> (forall b. Int -> b -> Int)

but GHC "hoists" the forall to give the isomorphic type

  g :: forall b. Int -> Int -> b -> Int

In general, the rule is this: to determine the type specified by any explicit user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly performs the transformation:

  type1 -> forall a1..an. context2 => type2
==>
  forall a1..an. context2 => type1 -> type2

(In fact, GHC tries to retain as much synonym information as possible for use in error messages, but that is a usability issue.) This rule applies, of course, whether or not the forall comes from a synonym. For example, here is another valid way to write g's type signature:

  g :: Int -> Int -> forall b. b -> Int

When doing this hoisting operation, GHC eliminates duplicate constraints. For example:

  type Foo a = (?x::Int) => Bool -> a
  g :: Foo (Foo Int)

means

  g :: (?x::Int) => Bool -> Bool -> Int

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 polymoprhic 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.

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

  data T a = MkT (Either a b) (b -> b)

it's just as if you had written this:

  data T a = MkT (forall b. Either a b) (forall b. b -> b)

That is, since the type variable b isn't in scope, it's implicitly universally quantified. (Arguably, it would be better to require explicit quantification on constructor arguments where that is what is wanted. Feedback welcomed.)

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.4.10, “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 quantifed over its free type variables (Section 4.1.2 of the Haskel 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(s). 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 the quantification in f's type signature is explicit. For example:

  g :: [a] -> [a]
  g (x:xs) = xs ++ [ x :: a ]

This program will be rejected, because "a" does not scope over the definition of "f", so "x::a" means "x::forall a. a" by Haskell's usual implicit quantification rules.

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 a. 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 sigature 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.

There is only one situation in which you can write a pattern type signature that mentions a type variable that is not already in scope, namely in pattern match of an existential data constructor. 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.

If 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 subequent 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

GHC now permits such instances to be derived instead, so one can write

 
  newtype Dollars = Dollars Int deriving (Eq,Show,Num)

and the implementation uses the same Num dictionary for Dollars as for Int. Notionally, the compiler derives an instance declaration of the form

 
  instance Num Int => Num Dollars

which just adds or removes the newtype constructor according to the type.

We can also derive instances of constructor classes in a similar way. For example, suppose we have implemented state and failure monad transformers, such that

 
  instance Monad m => Monad (State s m) 
  instance Monad m => Monad (Failure m)

In Haskell 98, we can define a parsing monad by

 
  type Parser tok m a = State [tok] (Failure m) a

which is automatically a monad thanks to the instance declarations above. With the extension, we can make the parser type abstract, without needing to write an instance of class Monad, via

 
  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
                         deriving Monad

In this case the derived instance declaration is of the form

 
  instance Monad (State [tok] (Failure m)) => Monad (Parser tok m) 

Notice that, since Monad is a constructor class, the instance is a partial application of the new type, not the entire left hand side. We can imagine that the type declaration is ``eta-converted'' to generate the context of the instance declaration.

We can even derive instances of multi-parameter classes, provided the newtype is the last class parameter. In this case, a ``partial application'' of the class appears in the deriving clause. For example, given the class

 
  class StateMonad s m | m -> s where ... 
  instance Monad m => StateMonad s (State s m) where ... 

then we can derive an instance of StateMonad for Parsers by

 
  newtype Parser tok m a = Parser (State [tok] (Failure m) a)
                         deriving (Monad, StateMonad [tok])

The derived instance is obtained by completing the application of the class to the new type:

 
  instance StateMonad [tok] (State [tok] (Failure m)) =>
           StateMonad [tok] (Parser tok m)

As a result of this extension, all derived instances in newtype declarations are treated uniformly (and implemented just by reusing the dictionary for the representation type), except Show and Read, which really behave differently for the newtype and its representation.

Derived instance declarations are constructed as follows. Consider the declaration (after expansion of any type synonyms)

 
  newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm) 

where

Then, for each ci, the derived instance declaration is:

 
  instance ci (t vk+1...v) => ci (T v1...vp)

where p is chosen so that T v1...vp is of the right kind for the last parameter of class Ci.

As an example which does not work, consider

 
  newtype NonMonad m s = NonMonad (State s m s) deriving Monad 

Here we cannot derive the instance

 
  instance Monad (State s m) => Monad (NonMonad m) 

because the type variable s occurs in State s m, and so cannot be "eta-converted" away. It is a good thing that this deriving clause is rejected, because NonMonad m is not, in fact, a monad --- for the same reason. Try defining >>= with the correct type: you won't be able to.

Notice also that the order of class parameters becomes important, since we can only derive instances for the last one. If the StateMonad class above were instead defined as

 
  class StateMonad m s | m -> s where ... 

then we would not have been able to derive an instance for the Parser type above. We hypothesise that multi-parameter classes usually have one "main" parameter for which deriving new instances is most interesting.

Lastly, all of this applies only for classes other than Read, Show, Typeable, and Data, for which the built-in derivation applies (section 4.3.3. of the Haskell Report). (For the standard classes Eq, Ord, Ix, and Bounded it is immaterial whether the standard method is used or the one described here.)