Commit cabe1748 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Two kind-polymorphism fixes (Trac #10122)

* The original fix was to improve the documentation, in
  line with the suggestions on Trac #10122

* But in doing so I realised that the kind generalisation in
  TcRnDriver.tcRnType was completely wrong.  So I fixed that
  and updated Note [Kind-generalise in tcRnType] to explain.
parent 52dfa616
......@@ -1743,7 +1743,7 @@ tcRnExpr hsc_env rdr_expr
(rn_expr, _fvs) <- rnLExpr rdr_expr ;
failIfErrsM ;
-- Now typecheck the expression;
-- Now typecheck the expression, and generalise its type
-- it might have a rank-2 type (e.g. :t runST)
uniq <- newUnique ;
let { fresh_it = itName uniq (getLoc rdr_expr) } ;
......@@ -1755,7 +1755,7 @@ tcRnExpr hsc_env rdr_expr
False {- No MR for now -}
[(fresh_it, res_ty)]
lie ;
-- wanted constraints from static forms
-- Wanted constraints from static forms
stWC <- tcg_static_wc <$> getGblEnv >>= readTcRef ;
-- Ignore the dictionary bindings
......@@ -1797,7 +1797,13 @@ tcRnType hsc_env normalise rdr_type
-- Now kind-check the type
-- It can have any rank or kind
; nwc_tvs <- mapM newWildcardVarMetaKind wcs
; ty <- tcExtendTyVarEnv nwc_tvs $ tcHsSigType GhciCtxt rn_type
; (ty, kind) <- tcExtendTyVarEnv nwc_tvs $
tcLHsType rn_type
-- Do kind generalisation; see Note [Kind-generalise in tcRnType]
; kvs <- zonkTcTypeAndFV kind
; kvs <- kindGeneralize kvs
; ty <- zonkTcTypeToType emptyZonkEnv ty
; ty' <- if normalise
then do { fam_envs <- tcGetFamInstEnvs
......@@ -1806,20 +1812,32 @@ tcRnType hsc_env normalise rdr_type
-- which we discard, so the Role is irrelevant
else return ty ;
; return (ty', typeKind ty) }
; return (ty', mkForAllTys kvs (typeKind ty')) }
{-
Note [Kind-generalise in tcRnType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
{- Note [Kind-generalise in tcRnType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We switch on PolyKinds when kind-checking a user type, so that we will
kind-generalise the type. This gives the right default behaviour at
the GHCi prompt, where if you say ":k T", and T has a polymorphic
kind, you'd like to see that polymorphism. Of course. If T isn't
kind-polymorphic you won't get anything unexpected, but the apparent
*loss* of polymorphism, for types that you know are polymorphic, is
quite surprising. See Trac #7688 for a discussion.
kind-generalise the type, even when PolyKinds is not otherwise on.
This gives the right default behaviour at the GHCi prompt, where if
you say ":k T", and T has a polymorphic kind, you'd like to see that
polymorphism. Of course. If T isn't kind-polymorphic you won't get
anything unexpected, but the apparent *loss* of polymorphism, for
types that you know are polymorphic, is quite surprising. See Trac
#7688 for a discussion.
Note that the goal is to generalise the *kind of the type*, not
the type itself! Example:
ghci> data T m a = MkT (m a) -- T :: forall . (k -> *) -> k -> *
ghci> :k T
We instantiate T to get (T kappa). We do not want to kind-generalise
that to forall k. T k! Rather we want to take its kind
T kappa :: (kappa -> *) -> kappa -> *
and now kind-generalise that kind, to forall k. (k->*) -> k -> *
(It was Trac #10122 that made me realise how wrong the previous
approach was.) -}
{-
************************************************************************
* *
tcRnDeclsi
......
......@@ -639,7 +639,7 @@ pprSigmaTypeExtraCts :: Bool -> Type -> SDoc
pprSigmaTypeExtraCts = ppr_sigma_type False
pprUserForAll :: [TyVar] -> SDoc
-- Print a user-level forall; see Note [WHen to print foralls]
-- Print a user-level forall; see Note [When to print foralls]
pprUserForAll tvs
= sdocWithDynFlags $ \dflags ->
ppWhen (any tv_has_kind_var tvs || gopt Opt_PrintExplicitForalls dflags) $
......
......@@ -6608,50 +6608,81 @@ Note that the datatype <literal>Proxy</literal> has kind
<literal>Typeable</literal> class has kind
<literal>forall k. k -> Constraint</literal>.
</para>
</sect2>
<sect2> <title>Overview</title>
<para>
Note the following specific points:
<itemizedlist>
<listitem><para>
Generally speaking, with <option>-XPolyKinds</option>, GHC will infer a polymorphic
kind for un-decorated declarations, whenever possible. For example:
kind for un-decorated declarations, whenever possible. For example, in GHCi
<programlisting>
ghci> :set -XPolyKinds
ghci> data T m a = MkT (m a)
ghci> :k T
T :: (k -> *) -> k -> *
</programlisting>
</para></listitem>
<listitem><para>
GHC does not usually print explicit <literal>forall</literal>s, including kind <literal>forall</literal>s.
You can make GHC show them explicitly with <option>-fprint-explicit-foralls</option>
(see <xref linkend="options-help"/>):
<programlisting>
data T m a = MkT (m a)
-- GHC infers kind T :: forall k. (k -> *) -> k -> *
ghci> :set -XPolyKinds
ghci> :set -fprint-explicit-foralls
ghci> data T m a = MkT (m a)
ghci> :k T
T :: forall (k :: BOX). (k -> *) -> k -> *
</programlisting>
Here the kind variable <literal>k</literal> itself has a
kind annotation "<literal>BOX</literal>". This is just GHC's way of
saying "<literal>k</literal> is a kind variable".
</para></listitem>
<listitem><para>
Just as in the world of terms, you can restrict polymorphism using a
kind signature (sometimes called a kind annotation)
(<option>-XPolyKinds</option> implies <option>-XKindSignatures</option>):
<programlisting>
data T m (a :: *) = MkT (m a)
-- GHC now infers kind T :: (* -> *) -> * -> *
</programlisting>
There is no "forall" for kind variables. Instead, when binding a type variable,
NB: <option>-XPolyKinds</option> implies <option>-XKindSignatures</option> (see <xref linkend="kinding"/>).
</para></listitem>
<listitem><para>
The source language does not support an explicit <literal>forall</literal> for kind variables. Instead, when binding a type variable,
you can simply mention a kind
variable in a kind annotation for that type-variable binding, thus:
<programlisting>
data T (m :: k -> *) a = MkT (m a)
-- GHC now infers kind T :: forall k. (k -> *) -> k -> *
</programlisting>
The kind "forall" is placed
</para></listitem>
<listitem><para>
The (implicit) kind "forall" is placed
just outside the outermost type-variable binding whose kind annotation mentions
the kind variable. For example
<programlisting>
f1 :: (forall a m. m a -> Int) -> Int
-- f1 :: forall (k:BOX).
-- (forall (a:k) (m:k->*). m a -> Int)
-- f1 :: forall (k::BOX).
-- (forall (a::k) (m::k->*). m a -> Int)
-- -> Int
f2 :: (forall (a::k) m. m a -> Int) -> Int
-- f2 :: (forall (k:BOX) (a:k) (m:k->*). m a -> Int)
-- f2 :: (forall (k::BOX) (a::k) (m::k->*). m a -> Int)
-- -> Int
</programlisting>
Here in <literal>f1</literal> there is no kind annotation mentioning the polymorphic
kind variable, so <literal>k</literal> is generalised at the top
level of the signature for <literal>f1</literal>,
making the signature for <literal>f1</literal> is as polymorphic as possible.
level of the signature for <literal>f1</literal>.
But in the case of of <literal>f2</literal> we give a kind annotation in the <literal>forall (a:k)</literal>
binding, and GHC therefore puts the kind <literal>forall</literal> right there too.
This design decision makes default case (<literal>f1</literal>)
as polymorphic as possible; remember that a <emphasis>more</emphasis> polymorhic argument type (as in <literal>f2</literal>
makes the overall function <emphasis>less</emphasis> polymorphic, because there are fewer accepable arguments.
</para></listitem>
</itemizedlist>
</para>
<para>
(Note: These rules are a bit indirect and clumsy. Perhaps GHC should allow explicit kind quantification.
......
:set -XPolyKinds
data T m a = T (m a)
:k T
:set -fprint-explicit-foralls
:k T
T :: (k -> *) -> k -> *
T :: forall (k :: BOX). (k -> *) -> k -> *
......@@ -206,3 +206,4 @@ test('T9878b',
[ extra_run_opts('-fobject-code'),
extra_clean(['T9878b.hi','T9878b.o'])],
ghci_script, ['T9878b.script'])
test('T10122', normal, ghci_script, ['T10122.script'])
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