Commit e8d4ca74 authored by's avatar

Improve docs for GADTs

parent 8f0ebee0
......@@ -2436,10 +2436,16 @@ The result type of each constructor must begin with the type constructor being d
but for a GADT the arguments to the type constructor can be arbitrary monotypes.
For example, in the <literal>Term</literal> data
type above, the type of each constructor must end with <literal>Term ty</literal>, but
the <literal>ty</literal> may not be a type variable (e.g. the <literal>Lit</literal>
the <literal>ty</literal> need not be a type variable (e.g. the <literal>Lit</literal>
It's 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 <literal>T a b</literal>.
You cannot use a <literal>deriving</literal> clause for a GADT; only for
an ordinary data type.
......@@ -2476,6 +2482,19 @@ their selector functions actually have different types:
When pattern-matching against data constructors drawn from a GADT,
for example in a <literal>case</literal> expression, the following rules apply:
<listitem><para>The type of the scrutinee must be rigid.</para></listitem>
<listitem><para>The type of the result of the <literal>case</literal> expression must be rigid.</para></listitem>
<listitem><para>The type of any free variable mentioned in any of
the <literal>case</literal> alternatives must be rigid.</para></listitem>
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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment