GADTs extension is enabled, besides regular data declarations, you can also declare generalized algebraic datatypes as follows:
data DataType a where Constr1 :: Int -> a -> Foo a -> DataType a Constr2 :: Show a => a -> DataType a Constr3 :: DataType Int
A GADT declaration lists the types of all constructors a datatype has, explicitly. Unlike regular datatype declarations, the type of a constructor can be any N-ary (including nullary) function that ultimately results in the datatype applied to some arguments.
In this case we've declared that the type
DataType has three constructors:
Constr1 constructor is no different from one declared using a regular data declaration:
data DataType a = Constr1 Int a (Foo a) | ...
Constr2 however requires that
a has an instance of
Show, and so when using the constructor the instance would need to exist. On the other hand, when pattern-matching on it, the fact that
a is an instance of
Show comes into scope, so you can write:
foo :: DataType a -> String foo val = case val of Constr2 x -> show x ...
Note that the
Show a constraint doesn't appear in the type of the function, and is only visible in the code to the right of
Constr3 has type
DataType Int, which means that whenever a value of type
DataType a is a
Constr3, it is known that
a ~ Int. This information, too, can be recovered with a pattern match.