A type constructor or class can be an operator, beginning with a colon; e.g. :*:. The lexical syntax is the same as that for data constructors.

Data type and type-synonym declarations can be written infix, parenthesised if you want further arguments. E.g.

  data a :*: b = Foo a b
  type a :+: b = Either a b
  class a :=: b where ...

  data (a :**: b) x = Baz a b x
  type (a :++: b) y = Either (a,b) y

Types, and class constraints, can be written infix. For example

	x :: Int :*: Bool
        f :: (a :=: b) => a -> b
  

A type variable can be an (unqualified) operator e.g. +. The lexical syntax is the same as that for variable operators, excluding "(.)", "(!)", and "(*)". In a binding position, the operator must be parenthesised. For example:

   type T (+) = Int + Int
   f :: T Either
   f = Left 3

   liftA2 :: Arrow (~>)
	  => (a -> b -> c) -> (e ~> a) -> (e ~> b) -> (e ~> c)
   liftA2 = ...

Back-quotes work as for expressions, both for type constructors and type variables; e.g. Int `Either` Bool, or Int `a` Bool. Similarly, parentheses work the same; e.g. (:*:) Int Bool.

Fixities may be declared for type constructors, or classes, just as for data constructors. However, one cannot distinguish between the two in a fixity declaration; a fixity declaration sets the fixity for a data constructor and the corresponding type constructor. For example:

  infixl 7 T, :*:

sets the fixity for both type constructor T and data constructor T, and similarly for :*:. Int `a` Bool.

Function arrow is infixr with fixity 0. (This might change; I'm not sure what it should be.)

You can write a forall (including overloading) in a type synonym, thus:

  type Discard a = forall b. Show b => a -> b -> (a, String)

  f :: Discard a
  f x y = (x, show y)

  g :: Discard Int -> (Int,String)    -- A rank-2 type
  g f = f 3 True

If you also use -XUnboxedTuples, you can write an unboxed tuple in a type synonym:

  type Pr = (# Int, Int #)

  h :: Int -> Pr
  h x = (# x, x #)

You can apply a type synonym to a forall type:

  type Foo a = a -> a -> Bool

  f :: Foo (forall b. b->b)

After expanding the synonym, f has the legal (in GHC) type:

  f :: (forall b. b->b) -> (forall b. b->b) -> Bool

You can apply a type synonym to a partially applied type synonym:

  type Generic i o = forall x. i x -> o x
  type Id x = x

  foo :: Generic Id []

After expanding the synonym, foo has the legal (in GHC) type:

  foo :: forall x. x -> [x]

Type constructor applied to a type involving for-alls.

Unboxed tuple on left of an arrow.

Partially-applied type synonym.

The result type of each data constructor must begin with the type constructor being defined. If the result type of all constructors has the form T a1 ... an, where a1 ... an are distinct type variables, then the data type is ordinary; otherwise is a generalised data type (Section 7.4.7, “Generalised Algebraic Data Types (GADTs)”).

As with other type signatures, you can give a single signature for several data constructors. In this example we give a single signature for T1 and T2:

  data T a where
    T1,T2 :: a -> T a
    T3 :: T a

The type signature of each constructor is independent, and is implicitly universally quantified as usual. In particular, the type variable(s) in the "data T a where" header have no scope, and different constructors may have different universally-quantified type variables:

  data T a where        -- The 'a' has no scope
    T1,T2 :: b -> T b   -- Means forall b. b -> T b
    T3 :: T a           -- Means forall a. T a

A constructor signature may mention type class constraints, which can differ for different constructors. For example, this is fine:

  data T a where
    T1 :: Eq b => b -> b -> T b
    T2 :: (Show c, Ix c) => c -> [c] -> T c

When pattern matching, these constraints are made available to discharge constraints in the body of the match. For example:

  f :: T a -> String
  f (T1 x y) | x==y      = "yes"
             | otherwise = "no"
  f (T2 a b)             = show a

Note that f is not overloaded; the Eq constraint arising from the use of == is discharged by the pattern match on T1 and similarly the Show constraint arising from the use of show.

Unlike a Haskell-98-style data type declaration, the type variable(s) in the "data Set a where" header have no scope. Indeed, one can write a kind signature instead:

  data Set :: * -> * where ...

or even a mixture of the two:

  data Bar a :: (* -> *) -> * where ...

The type variables (if given) may be explicitly kinded, so we could also write the header for Foo like this:

  data Bar a (b :: * -> *) where ...

You can use strictness annotations, in the obvious places in the constructor type:

  data Term a where
      Lit    :: !Int -> Term Int
      If     :: Term Bool -> !(Term a) -> !(Term a) -> Term a
      Pair   :: Term a -> Term b -> Term (a,b)

You can use a deriving clause on a GADT-style data type declaration. For example, these two declarations are equivalent

  data Maybe1 a where {
      Nothing1 :: Maybe1 a ;
      Just1    :: a -> Maybe1 a
    } deriving( Eq, Ord )

  data Maybe2 a = Nothing2 | Just2 a
       deriving( Eq, Ord )

The type signature may have quantified type variables that do not appear in the result type:

  data Foo where
     MkFoo :: a -> (a->Bool) -> Foo
     Nil   :: Foo

Here the type variable a does not appear in the result type of either constructor. Although it is universally quantified in the type of the constructor, such a type variable is often called "existential". Indeed, the above declaration declares precisely the same type as the data Foo in Section 7.4.5, “Existentially quantified data constructors ”.

The type may contain a class context too, of course:

  data Showable where
    MkShowable :: Show a => a -> Showable

You can use record syntax on a GADT-style data type declaration:

  data Person where
      Adult :: { name :: String, children :: [Person] } -> Person
      Child :: Show a => { name :: !String, funny :: a } -> Person

As usual, for every constructor that has a field f, the type of field f must be the same (modulo alpha conversion). The Child constructor above shows that the signature may have a context, existentially-quantified variables, and strictness annotations, just as in the non-record case. (NB: the "type" that follows the double-colon is not really a type, because of the record syntax and strictness annotations. A "type" of this form can appear only in a constructor signature.)

Record updates are allowed with GADT-style declarations, only fields that have the following property: the type of the field mentions no existential type variables.

As in the case of existentials declared using the Haskell-98-like record syntax (Section 7.4.5.3, “Record Constructors”), record-selector functions are generated only for those fields that have well-typed selectors. Here is the example of that section, in GADT-style syntax:

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

As before, only one selector function is generated here, that for tag. Nevertheless, you can still use all the field names in pattern matching and record construction.

In a GADT-style data type declaration there is no obvious way to specify that a data constructor should be infix, which makes a difference if you derive Show for the type. (Data constructors declared infix are displayed infix by the derived show.) So GHC implements the following design: a data constructor declared in a GADT-style data type declaration is displayed infix by Show iff (a) it is an operator symbol, (b) it has two arguments, (c) it has a programmer-supplied fixity declaration. For example

   infix 6 (:--:) 
   data T a where
     (:--:) :: Int -> Bool -> T Int

A GADT can only be declared using GADT-style syntax (Section 7.4.6, “Declaring data types with explicit constructor signatures”); the old Haskell-98 syntax for data declarations always declares an ordinary data type. The result type of each constructor must begin with the type constructor being defined, but for a GADT the arguments to the type constructor can be arbitrary monotypes. For example, in the Term data type above, the type of each constructor must end with Term ty, but the ty need not be a type variable (e.g. the Lit constructor).

It is permitted to declare an ordinary algebraic data type using GADT-style syntax. What makes a GADT into a GADT is not the syntax, but rather the presence of data constructors whose result type is not just T a b.

You cannot use a deriving clause for a GADT; only for an ordinary data type.

As mentioned in Section 7.4.6, “Declaring data types with explicit constructor signatures”, record syntax is supported. For example:

  data Term a where
      Lit    { val  :: Int }      :: Term Int
      Succ   { num  :: Term Int } :: Term Int
      Pred   { num  :: Term Int } :: Term Int
      IsZero { arg  :: Term Int } :: Term Bool
      Pair   { arg1 :: Term a
             , arg2 :: Term b
             }                    :: Term (a,b)
      If     { cnd  :: Term Bool
             , tru  :: Term a
             , fls  :: Term a
             }                    :: Term a

However, for GADTs there is the following additional constraint: every constructor that has a field f must have the same result type (modulo alpha conversion) Hence, in the above example, we cannot merge the num and arg fields above into a single name. Although their field types are both Term Int, their selector functions actually have different types:

  num :: Term Int -> Term Int
  arg :: Term Bool -> Term Int

When pattern-matching against data constructors drawn from a GADT, for example in a case expression, the following rules apply:

A type is "rigid" if it is completely known to the compiler at its binding site. The easiest way to ensure that a variable a rigid type is to give it a type signature. For more precise details see Simple unification-based type inference for GADTs . The criteria implemented by GHC are given in the Appendix.