Re-add missing kind generalisation

When splitting H98/GADT syntax in ConDecl we lost a key
kind-generalisation step.

I also renamed tcHsTyVarBndrs to tcExplicitTKBnders, by analogy
with tcImplicitTkBndrs.

This fixes Trac #11459.

Merge to 8.0.

compiler/typecheck/TcBinds.hs

@@ -1826,7 +1826,7 @@ tcUserTypeSig hs_sig_ty mb_name
                   -- so that they can be unified under the forall
               tcImplicitTKBndrs vars $
               tcWildCardBinders wcs  $ \ wcs ->
-              tcHsTyVarBndrs hs_tvs  $ \ tvs2 ->
+              tcExplicitTKBndrs hs_tvs  $ \ tvs2 ->
          do { -- Instantiate the type-class context; but if there
               -- is an extra-constraints wildcard, just discard it here
               traceTc "tcPartial" (ppr name $$ ppr vars $$ ppr wcs)

compiler/typecheck/TcHsType.hs

@@ -17,7 +17,7 @@ module TcHsType (
         tcHsDeriv, tcHsVectInst,
         tcHsTypeApp,
         UserTypeCtxt(..),
-        tcImplicitTKBndrs, tcImplicitTKBndrsType, tcHsTyVarBndrs,
+        tcImplicitTKBndrs, tcImplicitTKBndrsType, tcExplicitTKBndrs,
 
                 -- Type checking type and class decls
         kcLookupKind, kcTyClTyVars, tcTyClTyVars,
@@ -515,7 +515,7 @@ tc_hs_type mode hs_ty@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kin
 
   | otherwise
   = fmap fst $
-    tcHsTyVarBndrs hs_tvs $ \ tvs' ->
+    tcExplicitTKBndrs hs_tvs $ \ tvs' ->
     -- Do not kind-generalise here!  See Note [Kind generalisation]
     -- Why exp_kind?  See Note [Body kind of forall]
     do { ty' <- tc_lhs_type mode ty exp_kind
@@ -1410,13 +1410,13 @@ tcImplicitTKBndrsX new_tv var_ns thing_inside
 
        ; return (final_tvs, result) }
 
-tcHsTyVarBndrs :: [LHsTyVarBndr Name]
-               -> ([TyVar] -> TcM (a, TyVarSet))
-                  -- ^ Thing inside returns the set of variables bound
-                  -- in the scope. See Note [Scope-check inferred kinds]
-               -> TcM (a, TyVarSet)  -- ^ returns augmented bound vars
+tcExplicitTKBndrs :: [LHsTyVarBndr Name]
+                  -> ([TyVar] -> TcM (a, TyVarSet))
+                        -- ^ Thing inside returns the set of variables bound
+                        -- in the scope. See Note [Scope-check inferred kinds]
+                  -> TcM (a, TyVarSet)  -- ^ returns augmented bound vars
 -- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
-tcHsTyVarBndrs orig_hs_tvs thing_inside
+tcExplicitTKBndrs orig_hs_tvs thing_inside
   = go orig_hs_tvs $ \ tvs ->
     do { (result, bound_tvs) <- thing_inside tvs
 
@@ -1425,7 +1425,7 @@ tcHsTyVarBndrs orig_hs_tvs thing_inside
        ; tvs <- checkZonkValidTelescope (interppSP orig_hs_tvs) tvs empty
        ; checkValidInferredKinds tvs bound_tvs empty
 
-       ; traceTc "tcHsTyVarBndrs" $
+       ; traceTc "tcExplicitTKBndrs" $
            vcat [ text "Hs vars:" <+> ppr orig_hs_tvs
                 , text "tvs:" <+> sep (map pprTvBndr tvs) ]
 

compiler/typecheck/TcPatSyn.hs

@@ -13,7 +13,7 @@ module TcPatSyn ( tcPatSynSig, tcInferPatSynDecl, tcCheckPatSynDecl
 
 import HsSyn
 import TcPat
-import TcHsType( tcImplicitTKBndrs, tcHsTyVarBndrs
+import TcHsType( tcImplicitTKBndrs, tcExplicitTKBndrs
                , tcHsContext, tcHsLiftedType, tcHsOpenType )
 import TcRnMonad
 import TcEnv
@@ -105,8 +105,8 @@ tcPatSynSig name sig_ty
   = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty))
            <- solveEqualities $
               tcImplicitTKBndrs implicit_hs_tvs $
-              tcHsTyVarBndrs univ_hs_tvs  $ \ univ_tvs ->
-              tcHsTyVarBndrs ex_hs_tvs    $ \ ex_tvs   ->
+              tcExplicitTKBndrs univ_hs_tvs  $ \ univ_tvs ->
+              tcExplicitTKBndrs ex_hs_tvs    $ \ ex_tvs   ->
               do { req     <- tcHsContext hs_req
                  ; prov    <- tcHsContext hs_prov
                  ; arg_tys <- mapM tcHsOpenType (hs_arg_tys :: [LHsType Name])

compiler/typecheck/TcTyClsDecls.hs

@@ -1368,10 +1368,10 @@ tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl
                Nothing -> ([], [])
                Just (HsQTvs { hsq_implicit = kvs, hsq_explicit = tvs })
                        -> (kvs, tvs)
-       ; (kvs, (ctxt, arg_tys, field_lbls, stricts, tvs))
+       ; (_, (ctxt, arg_tys, field_lbls, stricts))
            <- solveEqualities $
               tcImplicitTKBndrs hs_kvs $
-              tcHsTyVarBndrs hs_tvs $ \tvs ->
+              tcExplicitTKBndrs hs_tvs $ \ _ ->
               do { traceTc "tcConDecl" (ppr name <+> text "tvs:" <+> ppr hs_tvs)
                  ; ctxt <- tcHsContext (fromMaybe (noLoc []) hs_ctxt)
                  ; btys <- tcConArgs new_or_data hs_details
@@ -1379,13 +1379,17 @@ tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl
                  ; let (arg_tys, stricts) = unzip btys
                        bound_vars = allBoundVariabless ctxt `unionVarSet`
                                     allBoundVariabless arg_tys
-                 ; return ((ctxt, arg_tys, field_lbls, stricts, tvs), bound_vars)
+                 ; return ((ctxt, arg_tys, field_lbls, stricts), bound_vars)
                  }
 
+             -- Kind generalisation
+       ; tkvs <- quantifyTyVars (mkVarSet tmpl_tvs)
+                                (splitDepVarsOfTypes (ctxt++arg_tys))
+
              -- Zonk to Types
-       ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (kvs ++ tvs)
-       ; arg_tys <- zonkTcTypeToTypes ze arg_tys
-       ; ctxt    <- zonkTcTypeToTypes ze ctxt
+       ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
+       ; arg_tys     <- zonkTcTypeToTypes ze arg_tys
+       ; ctxt        <- zonkTcTypeToTypes ze ctxt
 
        ; fam_envs <- tcGetFamInstEnvs
 
@@ -1461,12 +1465,11 @@ tcGadtSigType :: SDoc -> Name -> LHsSigType Name
                                     (Located [LConDeclField Name]) )
 tcGadtSigType doc name ty@(HsIB { hsib_vars = vars })
   = do { let (hs_details', res_ty', cxt, gtvs) = gadtDeclDetails ty
-       ; (hs_details, res_ty) <-
-           updateGadtResult failWithTc doc hs_details' res_ty'
+       ; (hs_details, res_ty) <- updateGadtResult failWithTc doc hs_details' res_ty'
        ; (_, (ctxt, arg_tys, res_ty, field_lbls, stricts))
            <- solveEqualities $
               tcImplicitTKBndrs vars $
-              tcHsTyVarBndrs gtvs $ \ _ ->
+              tcExplicitTKBndrs gtvs $ \ _ ->
               do { ctxt <- tcHsContext cxt
                  ; btys <- tcConArgs DataType hs_details
                  ; ty' <- tcHsLiftedType res_ty
@@ -1477,7 +1480,7 @@ tcGadtSigType doc name ty@(HsIB { hsib_vars = vars })
 
                  ; return ((ctxt, arg_tys, ty', field_lbls, stricts), bound_vars)
                  }
-       ; return (ctxt,stricts,field_lbls,arg_tys,res_ty,hs_details)
+       ; return (ctxt, stricts, field_lbls, arg_tys, res_ty, hs_details)
        }
 
 tcConIsInfixH98 :: Name
@@ -2076,10 +2079,6 @@ checkValidDataCon dflags existential_ok tc con
 
         ; traceTc "checkValidDataCon 2" (ppr (dataConUserType con))
 
-          -- Check that existentials are allowed if they are used
-        ; checkTc (existential_ok || isVanillaDataCon con)
-                  (badExistential con)
-
           -- Check that the result type is a *monotype*
           --  e.g. reject this:   MkT :: T (forall a. a->a)
           -- Reason: it's really the argument of an equality constraint
@@ -2091,6 +2090,10 @@ checkValidDataCon dflags existential_ok tc con
           -- Extra checks for newtype data constructors
         ; when (isNewTyCon tc) (checkNewDataCon con)
 
+          -- Check that existentials are allowed if they are used
+        ; checkTc (existential_ok || isVanillaDataCon con)
+                  (badExistential con)
+
           -- Check that UNPACK pragmas and bangs work out
           -- E.g.  reject   data T = MkT {-# UNPACK #-} Int     -- No "!"
           --                data T = MkT {-# UNPACK #-} !a      -- Can't unpack

compiler/typecheck/TcValidity.hs

@@ -1553,7 +1553,7 @@ If there is a bad telescope, the kind-generalization will end up generalizing
 over a variable bound later in the telescope.
 
 For non-tycons, we do scope checking when we bring tyvars into scope,
-in tcImplicitTKBndrs and tcHsTyVarBndrs. Note that we also have to
+in tcImplicitTKBndrs and tcExplicitTKBndrs. Note that we also have to
 sort implicit binders into a well-scoped order whenever we have implicit
 binders to worry about. This is done in quantifyTyVars and in
 tcImplicitTKBndrs.

testsuite/tests/ghci/scripts/T7873.stdout

-data D2
-  = MkD2 (forall (p :: GHC.Prim.Any -> *) (a :: GHC.Prim.Any).
-          p a -> Int)
+data D2 where
+  MkD2 :: (forall (p :: k -> *) (a :: k). p a -> Int) -> D2
   	-- Defined at <interactive>:3:1
-data D3 = MkD3 (forall k (p :: k -> *) (a :: k). p a -> Int)
+data D3 where
+  MkD3 :: (forall k1 (p :: k1 -> *) (a :: k1). p a -> Int) -> D3
   	-- Defined at <interactive>:4:1

testsuite/tests/polykinds/T11459.hs

+{-# LANGUAGE  PolyKinds, RankNTypes #-}
+
+module T11459 where
+
+
+type Failure f r   = String -> f r
+type Success a f r = a -> f r
+
+newtype Parser a = Parser {
+      unParser :: forall f r.
+                  Failure f r
+               -> Success a f r
+               -> f r
+    }

testsuite/tests/polykinds/T11459.stderr

+
+T11459.hs:9:20: error:
+    • A newtype constructor cannot have existential type variables
+      Parser :: forall a k.
+                (forall (f :: k -> *) (r :: k).
+                 Failure f r -> Success a f r -> f r)
+                -> Parser a
+    • In the definition of data constructor ‘Parser’
+      In the newtype declaration for ‘Parser’

testsuite/tests/polykinds/all.T

@@ -132,3 +132,4 @@ test('T11249', normal, compile, [''])
 test('T11248', normal, compile, [''])
 test('T11278', normal, compile, [''])
 test('T11255', normal, compile, [''])
+test('T11459', normal, compile_fail, [''])
\ No newline at end of file

testsuite/tests/rename/should_fail/rnfail055.stderr

@@ -73,8 +73,7 @@ RnFail055.hs-boot:25:1: error:
     Main module: type role T7 phantom
                  data T7 a where
                    T7 :: a1 -> T7 a
-    Boot file:   data T7 a where
-                   T7 :: a -> T7 a
+    Boot file:   data T7 a = T7 a
     The roles do not match.
     Roles on abstract types default to ‘representational’ in boot files.
     The constructors do not match: The types for ‘T7’ differ