Commit f630eb51 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by
Browse files

Document promotion of existential data types

Thanks to Richard Eisenberg for writing this.
parent e3dc71de
......@@ -5500,8 +5500,9 @@ The following restrictions apply to promotion:
higher-kinded datatypes such as <literal>data Fix f = In (f (Fix f))</literal>,
or datatypes whose kinds involve promoted types such as
<literal>Vec :: * -> Nat -> *</literal>.</para></listitem>
<listitem><para>We do not promote datatypes whose constructors are kind
polymorphic, involve constraints, or use existential quantification.
<listitem><para>We do not promote data constructors that are kind
polymorphic, involve constraints, mention type or data families, or involve types that
are not promotable.
<listitem><para>We do not promote data family instances (<xref linkend="data-families"/>).
......@@ -5556,7 +5557,7 @@ Note that this requires <option>-XTypeOperators</option>.
<sect2 id="promoted-literals">
<title>Promoted Literals</title>
Numeric and string literals are prmoted to the type level, giving convenient
Numeric and string literals are promoted to the type level, giving convenient
access to a large number of predefined type-level constants. Numeric literals
are of kind <literal>Nat</literal>, while string literals are of kind
<literal>Symbol</literal>. These kinds are defined in the module
......@@ -5597,6 +5598,46 @@ example = from (Point 1 2) (Get :: Label "x")
<sect2 id="promotion-existentials">
<title>Promoting existential data constructors</title>
Note that we do promote existential data constructors that are otherwise suitable.
For example, consider the following:
data Ex :: * where
MkEx :: forall a. a -> Ex
Both the type <literal>Ex</literal> and the data constructor <literal>MkEx</literal>
get promoted, with the polymorphic kind <literal>'MkEx :: forall k. k -> Ex</literal>.
Somewhat surprisingly, you can write a type family to extract the member
of a type-level existential:
type family UnEx (ex :: Ex) :: k
type instance UnEx (MkEx x) = x
At first blush, <literal>UnEx</literal> seems poorly-kinded. The return kind
<literal>k</literal> is not mentioned in the arguments, and thus it would seem
that an instance would have to return a member of <literal>k</literal>
<emphasis>for any</emphasis> <literal>k</literal>. However, this is not the
case. The type family <literal>UnEx</literal> is a kind-indexed type family.
The return kind <literal>k</literal> is an implicit parameter to <literal>UnEx</literal>.
The elaborated definitions are as follows:
type family UnEx (k :: BOX) (ex :: Ex) :: k
type instance UnEx k (MkEx k x) = x
Thus, the instance triggers only when the implicit parameter to <literal>UnEx</literal>
matches the implicit parameter to <literal>MkEx</literal>. Because <literal>k</literal>
is actually a parameter to <literal>UnEx</literal>, the kind is not escaping the
existential, and the above code is valid.
See also <ulink url="">Trac #7347</ulink>.
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