From e8d4ca746464db8c15e935bc8f799536d7400ed8 Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Tue, 29 Jul 2008 14:53:13 +0000 Subject: [PATCH] Improve docs for GADTs --- docs/users_guide/glasgow_exts.xml | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 0f55b9b..63c5dbd 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -2436,11 +2436,17 @@ 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 Term data type above, the type of each constructor must end with Term ty, but -the ty may not be a type variable (e.g. the Lit +the ty need not be a type variable (e.g. the Lit constructor). +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 T a b. + + + You cannot use a deriving 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 case expression, the following rules apply: + +The type of the scrutinee must be rigid. +The type of the result of the case expression must be rigid. +The type of any free variable mentioned in any of +the case alternatives must be rigid. + +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. + + -- 1.7.10.4