Skip to content

Commit

Permalink
add entry in manual, just after existential type names in error messages
Browse files Browse the repository at this point in the history
  • Loading branch information
garrigue committed Jan 25, 2021
1 parent 7fe5d64 commit 9f6cf10
Showing 1 changed file with 22 additions and 0 deletions.
22 changes: 22 additions & 0 deletions manual/manual/refman/exten.etex
Original file line number Diff line number Diff line change
Expand Up @@ -1259,6 +1259,28 @@ which could not be named using one of the previous schemes.
As shown by the last item, the current behavior is imperfect
and may be improved in future versions.

\lparagraph{p:explicit-existential-name}{Explicit naming of
existentials} (Introduced in OCaml 4.13.0)

As explained above, pattern-matching on a GADT constructor may
introduce existential types. The following syntax allows to name them
explicitly.

\begin{syntax}
pattern:
...
| constr '(' "type" {{typeconstr-name}} ')' '(' pattern ':' typexpr ')'
;
\end{syntax}

For instance, the following code names the type of the argument of f
and uses this name.

\begin{caml_example*}{verbatim}
type _ closure = Closure : ('a -> 'b) * 'a -> 'b closure
let eval = fun (Closure (type a) (f, x : (a -> _) * _)) -> f (x : a)
\end{caml_example*}

\lparagraph{p:gadt-equation-nonlocal-abstract}{Equations on non-local abstract types} (Introduced in OCaml
4.04)

Expand Down

0 comments on commit 9f6cf10

Please sign in to comment.