Merge pull request #518 from Octachron/manual_polymorphic_locally_abstract_context

Manual: Add more context to the description of locally abstract types

manual/manual/refman/exten.etex

@@ -577,7 +577,9 @@ Here is another example:
             S.elements (List.fold_right S.add l S.empty)
 \end{verbatim}
 
-It is also extremely useful for first-class modules and GADTs.
+It is also extremely useful for first-class modules (see
+section~\ref{s-first-class-modules}) and generalized algebraic datatypes
+(GADTs: see section~\ref{s:gadts}).
 
 \paragraph{Polymorphic syntax} (Introduced in OCaml 4.00)
 
@@ -607,6 +609,8 @@ is automatically expanded into
         let rec f : 't1 't2. 't1 * 't2 list -> 't1 =
           fun (type t1) (type t2) -> (... : t1 * t2 list -> t1)
 \end{verbatim}
+This syntax can be very useful when defining recursive functions involving
+GADTs, see the section~\ref{s:gadts} for a more detailed explanation.
 
 The same feature is provided for method definitions.
 The @'method!'@ form combines this extension with the
@@ -1107,7 +1111,7 @@ intentional and should not trigger the warning.
 
 
 \section{Generalized algebraic datatypes} \ikwd{type\@\texttt{type}}
-\ikwd{match\@\texttt{match}}
+\ikwd{match\@\texttt{match}} \label{s:gadts}
 
 (Introduced in OCaml 4.00)
 
@@ -1148,6 +1152,8 @@ If a constructor has some existential variables, fresh locally
 abstract types are generated, and they must not escape the
 scope of this branch.
 
+\paragraph{Recursive functions}
+
 Here is a concrete example:
 \begin{verbatim}
         type _ term =
@@ -1164,6 +1170,36 @@ Here is a concrete example:
         let two = eval (App (App (Add, Int 1), Int 1))
         val two : int = 2
 \end{verbatim}
+It is important to remark that the function "eval" is using the
+polymorphic syntax for locally abstract types. When defining a recursive
+function that manipulates a GADT, explicit polymorphic recursion should
+generally be used. For instance, the following definition fails with a
+type error:
+\begin{verbatim}
+        let rec eval (type a): a term -> a = function
+          | Int n    -> n
+          | Add      -> (fun x y -> x+y)
+          | App(f,x) -> (eval f) (eval x)
+(*                            ^
+   Error: This expression has type ($App_'b -> a) term but an expression was
+   expected of type 'a
+   The type constructor $App_'b would escape its scope
+*)
+\end{verbatim}
+In absence of an explicit polymorphic annotation, a monomorphic type
+is inferred for the recursive function. If a recursive call occurs
+inside the function definition at a type that involves an existential
+GADT type variable, this variable flows to the type of the recursive
+function, and thus escapes its scope. In the above example, this happens
+in the branch "App(f,x)" when "eval" is called with "f" as an argument.
+In this branch, the type of "f" is "($App_ 'b-> a)". The prefix "$" in
+"$App_ 'b" denotes an existential type named by the compiler
+(see~\ref{p:existential-names}). Since the type of "eval" is
+"'a term -> 'a", the call "eval f" makes the existential type "$App_'b"
+flows to the type variable "'a" and escape its scope. This triggers the
+above error.
+
+\paragraph{Type inference}
 
 Type inference for GADTs is notoriously hard.
 This is due to the fact some types may become ambiguous when escaping
@@ -1320,7 +1356,8 @@ to implement dynamic types.
           | None -> None
           | Some Eq -> Some x
 \end{verbatim}
-\paragraph{Existential type names in error messages}
+\paragraph{Existential type names in error messages}%
+\label{p:existential-names}
 
 (Updated in OCaml 4.03.0)