Two kind-polymorphism fixes (Trac #10122)
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 2 Mar 2015 16:29:39 +0000 (16:29 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 2 Mar 2015 16:31:10 +0000 (16:31 +0000)
* 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.

compiler/typecheck/TcRnDriver.hs
compiler/types/TypeRep.hs
docs/users_guide/glasgow_exts.xml
testsuite/tests/ghci/scripts/T10122.script [new file with mode: 0644]
testsuite/tests/ghci/scripts/T10122.stdout [new file with mode: 0644]
testsuite/tests/ghci/scripts/all.T
testsuite/tests/partial-sigs/should_run/GHCiWildcardKind.stdout

index 2ac45fc..1fb7662 100644 (file)
@@ -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
index 77e998d..c78c9c5 100644 (file)
@@ -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) $
index f38e0d7..7bb2f68 100644 (file)
@@ -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 (file)
index 0000000..778f936
--- /dev/null
@@ -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 (file)
index 0000000..c79a871
--- /dev/null
@@ -0,0 +1,2 @@
+T :: (k -> *) -> k -> *
+T :: forall (k :: BOX). (k -> *) -> k -> *
index 1decf78..b576a63 100755 (executable)
@@ -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'])