summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/typecheck/TcRnDriver.hs44
-rw-r--r--compiler/types/TypeRep.hs2
-rw-r--r--docs/users_guide/glasgow_exts.xml59
-rw-r--r--testsuite/tests/ghci/scripts/T10122.script5
-rw-r--r--testsuite/tests/ghci/scripts/T10122.stdout2
-rwxr-xr-xtestsuite/tests/ghci/scripts/all.T1
-rw-r--r--testsuite/tests/partial-sigs/should_run/GHCiWildcardKind.stdout2
7 files changed, 86 insertions, 29 deletions
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 2ac45fc224..1fb7662b59 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -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
diff --git a/compiler/types/TypeRep.hs b/compiler/types/TypeRep.hs
index 77e998d490..c78c9c5975 100644
--- a/compiler/types/TypeRep.hs
+++ b/compiler/types/TypeRep.hs
@@ -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) $
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index f38e0d7351..7bb2f68e95 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -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.
diff --git a/testsuite/tests/ghci/scripts/T10122.script b/testsuite/tests/ghci/scripts/T10122.script
new file mode 100644
index 0000000000..778f936ae9
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T10122.script
@@ -0,0 +1,5 @@
+:set -XPolyKinds
+data T m a = T (m a)
+:k T
+:set -fprint-explicit-foralls
+:k T
diff --git a/testsuite/tests/ghci/scripts/T10122.stdout b/testsuite/tests/ghci/scripts/T10122.stdout
new file mode 100644
index 0000000000..c79a8711f3
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T10122.stdout
@@ -0,0 +1,2 @@
+T :: (k -> *) -> k -> *
+T :: forall (k :: BOX). (k -> *) -> k -> *
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index 1decf78192..b576a6350f 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -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'])
diff --git a/testsuite/tests/partial-sigs/should_run/GHCiWildcardKind.stdout b/testsuite/tests/partial-sigs/should_run/GHCiWildcardKind.stdout
index e1b2bd37a6..49667f145e 100644
--- a/testsuite/tests/partial-sigs/should_run/GHCiWildcardKind.stdout
+++ b/testsuite/tests/partial-sigs/should_run/GHCiWildcardKind.stdout
@@ -1,2 +1,2 @@
-_ :: k0
+_ :: k
Maybe _ :: *
View Lorry Controller Status