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.

5 files changed, 31 insertions, 28 deletions

diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index dacdafdff1..8adfa357db 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/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)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 76c2977e2d..1b6d5cf8ec 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/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) ]
 
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 0c6d713c3a..03cbf6762f 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/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])
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 95f773ea0b..e1152ab76e 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/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
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 4833684828..49cbb42449 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/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.