Tidy up the handling of kind generalisation

In particular in forall abc. <blah> we should
kind generalise over <blah> as well as over the
kinds of a,b,c.

This fixes bug (in Trac #5862, caught by Lint) in the handling of
  data SMaybe a where
     SNothing :: SMaybe 'Nothing
where I didn't get a sufficiently general kind. And it's simpler.

3 files changed, 34 insertions, 58 deletions

diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index 7394f4f3cd..78c8cbe655 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -30,7 +30,7 @@ module TcHsType (
         tcHsContext, tcInferApps, tcHsArgTys,
 
         ExpKind(..), ekConstraint, expArgKind, checkExpectedKind,
-        kindGeneralizeKind, kindGeneralizeKinds,
+        kindGeneralize,
 
 		-- Sort-checking kinds
 	tcLHsKind, 
@@ -823,53 +823,26 @@ tcHsTyVarBndr (L _ hs_tv)
 
 ------------------
 tcHsTyVarBndrsGen :: [LHsTyVarBndr Name] 
-	          -> TcM r 
-	          -> TcM ([TyVar], r)
+	          -> TcM (TcTyVarSet, r)  -- Result + free tyvars of thing inside
+	          -> TcM ([TyVar], r)     -- Generalised kind variables 
+                                          -- + zonked tyvars + result result
 -- tcHsTyVarBndrsGen [(f :: ?k -> *), (a :: ?k)] thing_inside
 -- Returns with tyvars [(k :: BOX), (f :: k -> *), (a :: k)]
 tcHsTyVarBndrsGen hs_tvs thing_inside
   = do { traceTc "tcHsTyVarBndrsGen" (ppr hs_tvs) 
-       ; (tvs, res) <- tcHsTyVarBndrs hs_tvs $ \ tvs ->
+       ; (tvs, (ftvs, res)) <- tcHsTyVarBndrs hs_tvs $ \ tvs ->
                        do { res <- thing_inside
                           ; return (tvs, res) }
        ; let kinds = map tyVarKind tvs
-       ; (kvs', zonked_kinds) <- kindGeneralizeKinds kinds
+       ; kvs' <- kindGeneralize (tyVarsOfTypes kinds `unionVarSet` 
+                                        (ftvs `delVarSetList` tvs))
+       ; zonked_kinds <- mapM zonkTcKind kinds
        ; let tvs' = zipWith setTyVarKind tvs zonked_kinds
                      -- See Note [Kinds of quantified type variables]
        ; traceTc "tcTyVarBndrsGen" (ppr (hs_tvs, kvs', tvs))
        ; return (kvs' ++ tvs', res) }
 
-------------------
--- Used when generalizing binders and type family patterns
--- It takes a kind from the type checker (like `k0 -> *`), and returns the 
--- final, kind-generalized kind (`forall k::BOX. k -> *`)
-kindGeneralizeKinds :: [TcKind] -> TcM ([KindVar], [Kind])
--- INVARIANT: the returned kinds are zonked, and
---            mention the returned kind variables
-kindGeneralizeKinds kinds 
-  = do { -- Quantify over kind variables free in
-         -- the kinds, and *not* in the environment
-       ; traceTc "kindGeneralizeKinds 1" (ppr kinds)
-
-       ; kvs <- kindGeneralize (tyVarsOfTypes kinds)
-
-         -- Zonk the kinds again, to pick up either the kind 
-         -- variables we quantify over, or *, depending on whether
-         -- zonkQuantifiedTyVars decided to generalise (which in
-         -- turn depends on PolyKinds)
-       ; final_kinds <- mapM zonkTcKind kinds
-
-       ; traceTc "kindGeneralizeKinds 2" (vcat [ ppr kinds, ppr kvs, ppr final_kinds ])
-       ; return (kvs, final_kinds) }
-
-
-kindGeneralizeKind :: TcKind -> TcM ([KindVar], Kind)    
--- Unary version of kindGeneralizeKinds
-kindGeneralizeKind kind
-  = do { kvs   <- kindGeneralize (tyVarsOfType kind)
-       ; kind' <- zonkTcKind kind
-       ; return (kvs, kind') }
-
+-------------------
 kindGeneralize :: TyVarSet -> TcM [KindVar]
 kindGeneralize tkvs
   = do { gbl_tvs  <- tcGetGlobalTyVars -- Already zonked
diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index f237b67301..7b759d100e 100644
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -251,12 +251,14 @@ newNoSigLetBndr (LetGblBndr prags) name ty
 ----------
 addInlinePrags :: TcId -> [LSig Name] -> TcM TcId
 addInlinePrags poly_id prags
-  = tc_inl inl_sigs
+  = do { traceTc "addInlinePrags" (ppr poly_id $$ ppr prags) 
+       ; tc_inl inl_sigs }
   where
     inl_sigs = filter isInlineLSig prags
     tc_inl [] = return poly_id
     tc_inl (L loc (InlineSig _ prag) : other_inls)
        = do { unless (null other_inls) (setSrcSpan loc warn_dup_inline)
+            ; traceTc "addInlinePrag" (ppr poly_id $$ ppr prag) 
             ; return (poly_id `setInlinePragma` prag) }
     tc_inl _ = panic "tc_inl"
 
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index b04f4156aa..c166e6210e 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -294,7 +294,8 @@ kcTyClGroup decls
            ; let kc_kind = case thing of
                                AThing k -> k
                                _ -> pprPanic "kcTyClGroup" (ppr thing)
-           ; (kvs, kc_kind') <- kindGeneralizeKind kc_kind
+           ; kvs <- kindGeneralize (tyVarsOfType kc_kind)
+           ; kc_kind' <- zonkTcKind kc_kind
            ; return (name, mkForAllTys kvs kc_kind') }
 
 getInitialKinds :: LTyClDecl Name -> TcM [(Name, TcTyThing)]
@@ -433,6 +434,8 @@ kcFamilyDecl d = pprPanic "kcFamilyDecl" (ppr d)
 kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM ()
 kcResultKind Nothing res_k
   = discardResult (unifyKind res_k liftedTypeKind)
+      --             type family F a 
+      -- defaults to type family F a :: *
 kcResultKind (Just k) res_k
   = do { k' <- tcLHsKind k
        ; discardResult (unifyKind k' res_k) }
@@ -749,24 +752,18 @@ tcFamTyPats fam_tc tyvars arg_pats kind_checker thing_inside
                  = splitKindFunTysN fam_arity $
                    substKiWith fam_kvs fam_arg_kinds fam_body
 
-         -- Kind-check
-       ; (tvs, typats) <- tcHsTyVarBndrs tyvars $ \tvs -> do
+         -- Kind-check and quantify
+         -- See Note [Quantifying over family patterns]
+       ; (tkvs, typats) <- tcHsTyVarBndrsGen tyvars $ do
                 { typats <- tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds
                 ; kind_checker res_kind
-                ; return (tvs, typats) }
+                ; return (tyVarsOfTypes typats, typats) }
 
-         -- Quantify
-         -- See Note [Quantifying over family patterns]
-       ; let tv_kinds = map tyVarKind tvs
-       ; (kvs, kinds') <- kindGeneralizeKinds (tv_kinds ++ fam_arg_kinds)
-       ; typats'   <- zonkTcTypeToTypes emptyZonkEnv typats
+       ; all_args' <- zonkTcTypeToTypes emptyZonkEnv (fam_arg_kinds ++ typats)
        ; res_kind' <- zonkTcTypeToType emptyZonkEnv res_kind
-       ; let (tv_kinds', fam_arg_kinds') = splitAtList tv_kinds kinds'
-             tvs' = zipWith setTyVarKind tvs tv_kinds'
-             tkvs = kvs ++ tvs'   -- Kind and type variables
-       ; traceTc "tcFamPats" (ppr tvs' $$ ppr kvs $$ ppr kinds')
+       ; traceTc "tcFamPats" (ppr tkvs $$ ppr all_args' $$ ppr res_kind')
        ; tcExtendTyVarEnv tkvs $
-         thing_inside tkvs (fam_arg_kinds' ++ typats') res_kind' }
+         thing_inside tkvs all_args' res_kind' }
 \end{code}
 
 Note [Quantifying over family patterns]
@@ -876,21 +873,25 @@ tcConDecl new_or_data existential_ok rep_tycon res_tmpl 	-- Data types
                        , con_details = details, con_res = res_ty })
   = addErrCtxt (dataConCtxt name) $
     do { traceTc "tcConDecl 1" (ppr name)
-       ; (tvs', stuff) <- tcHsTyVarBndrsGen tvs $ 
+       ; (tvs', (ctxt', arg_tys', res_ty', is_infix, field_lbls, stricts)) 
+           <- tcHsTyVarBndrsGen tvs $ 
               do { ctxt'    <- tcHsContext ctxt
                  ; details' <- tcConArgs new_or_data details
                  ; res_ty'  <- tcConRes res_ty
-                 ; return (ctxt', details', res_ty') }
+                 ; let (is_infix, field_lbls, btys') = details'
+                       (arg_tys', stricts)           = unzip btys'
+                       ftvs = tyVarsOfTypes ctxt'     `unionVarSet`
+                              tyVarsOfTypes arg_tys'  `unionVarSet`
+                              case res_ty' of
+                                 ResTyH98     -> emptyVarSet
+                                 ResTyGADT ty -> tyVarsOfType ty
+                 ; return (ftvs, (ctxt', arg_tys', res_ty', is_infix, field_lbls, stricts)) }
 
-       ; let (ctxt', details', res_ty')    = stuff
-             (is_infix, field_lbls, btys') = details'
-             (arg_tys', stricts)           = unzip btys'
 
              -- Substitute, to account for the kind 
              -- unifications done by tcHsTyVarBndrsGen
-             ze = mkTyVarZonkEnv tvs'
-       
        ; traceTc "tcConDecl 2" (ppr name)
+       ; let ze = mkTyVarZonkEnv tvs'
        ; arg_tys' <- zonkTcTypeToTypes ze arg_tys'
        ; ctxt'    <- zonkTcTypeToTypes ze ctxt'
        ; res_ty'  <- case res_ty' of