Remove NonParametricKinds (#9200)

This commit also removes 'KindCheckingStrategy' and related gubbins,
instead including the notion of a CUSK into HsDecls.

4 files changed, 77 insertions, 226 deletions

diff --git a/compiler/hsSyn/HsDecls.lhs b/compiler/hsSyn/HsDecls.lhs
index 313dccccd5..9680c89e9b 100644
--- a/compiler/hsSyn/HsDecls.lhs
+++ b/compiler/hsSyn/HsDecls.lhs
@@ -23,6 +23,7 @@ module HsDecls (
   tyFamInstDeclName, tyFamInstDeclLName,
   countTyClDecls, pprTyClDeclFlavour,
   tyClDeclLName, tyClDeclTyVars,
+  hsDeclHasCusk, famDeclHasCusk,
   FamilyDecl(..), LFamilyDecl,
 
   -- ** Instance declarations
@@ -93,6 +94,7 @@ import Bag
 import Data.Data        hiding (TyCon)
 import Data.Foldable (Foldable)
 import Data.Traversable
+import Data.Maybe
 \end{code}
 
 %************************************************************************
@@ -604,8 +606,54 @@ countTyClDecls decls
    
    isNewTy DataDecl{ tcdDataDefn = HsDataDefn { dd_ND = NewType } } = True
    isNewTy _                                                      = False
+
+-- | Does this declaration have a complete, user-supplied kind signature?
+-- See Note [Complete user-supplied kind signatures]
+hsDeclHasCusk :: TyClDecl name -> Bool
+hsDeclHasCusk (ForeignType {}) = True
+hsDeclHasCusk (FamDecl { tcdFam = fam_decl }) = famDeclHasCusk fam_decl
+hsDeclHasCusk (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs })
+  = hsTvbAllKinded tyvars && rhs_annotated rhs
+  where
+    rhs_annotated (L _ ty) = case ty of
+      HsParTy lty  -> rhs_annotated lty
+      HsKindSig {} -> True
+      _            -> False
+hsDeclHasCusk (DataDecl { tcdTyVars = tyvars })  = hsTvbAllKinded tyvars
+hsDeclHasCusk (ClassDecl { tcdTyVars = tyvars }) = hsTvbAllKinded tyvars
+
+-- | Does this family declaration have a complete, user-supplied kind signature?
+famDeclHasCusk :: FamilyDecl name -> Bool
+famDeclHasCusk (FamilyDecl { fdInfo = ClosedTypeFamily _
+                           , fdTyVars = tyvars
+                           , fdKindSig = m_sig })
+  = hsTvbAllKinded tyvars && isJust m_sig
+famDeclHasCusk _ = True  -- all open families have CUSKs!
 \end{code}
 
+Note [Complete user-supplied kind signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We kind-check declarations differently if they have a complete, user-supplied
+kind signature (CUSK). This is because we can safely generalise a CUSKed
+declaration before checking all of the others, supporting polymorphic recursion.
+See https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference#Proposednewstrategy
+and #9200 for lots of discussion of how we got here.
+
+A declaration has a CUSK if we can know its complete kind without doing any inference,
+at all. Here are the rules:
+
+ - A class or datatype is said to have a CUSK if and only if all of its type
+variables are annotated. Its result kind is, by construction, Constraint or *
+respectively.
+
+ - A type synonym has a CUSK if and only if all of its type variables and its
+RHS are annotated with kinds.
+
+ - A closed type family is said to have a CUSK if and only if all of its type
+variables and its return type are annotated.
+
+ - An open type family always has a CUSK -- unannotated type variables (and return type) default to *.
+
 \begin{code}
 instance OutputableBndr name
               => Outputable (TyClDecl name) where
diff --git a/compiler/hsSyn/HsTypes.lhs b/compiler/hsSyn/HsTypes.lhs
index eada762738..0cf8455bad 100644
--- a/compiler/hsSyn/HsTypes.lhs
+++ b/compiler/hsSyn/HsTypes.lhs
@@ -25,7 +25,7 @@ module HsTypes (
 
         ConDeclField(..), pprConDeclFields,
         
-        mkHsQTvs, hsQTvBndrs, isHsKindedTyVar,
+        mkHsQTvs, hsQTvBndrs, isHsKindedTyVar, hsTvbAllKinded,
         mkExplicitHsForAllTy, mkImplicitHsForAllTy, hsExplicitTvs,
         hsTyVarName, mkHsWithBndrs, hsLKiTyVarNames,
         hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsLTyVarLocNames,
@@ -193,6 +193,10 @@ isHsKindedTyVar :: HsTyVarBndr name -> Bool
 isHsKindedTyVar (UserTyVar {})   = False
 isHsKindedTyVar (KindedTyVar {}) = True
 
+-- | Do all type variables in this 'LHsTyVarBndr' come with kind annotations?
+hsTvbAllKinded :: LHsTyVarBndrs name -> Bool
+hsTvbAllKinded = all (isHsKindedTyVar . unLoc) . hsQTvBndrs
+
 data HsType name
   = HsForAllTy  HsExplicitFlag          -- Renamer leaves this flag unchanged, to record the way
                                         -- the user wrote it originally, so that the printer can
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index d075cbcfbf..39c0acf2a6 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -25,7 +25,6 @@ module TcHsType (
 
 		-- Kind-checking types
                 -- No kind generalisation, no checkValidType
-	KindCheckingStrategy(..), kcStrategy, kcStrategyFamDecl,
         kcHsTyVarBndrs, tcHsTyVarBndrs, 
         tcHsLiftedType, tcHsOpenType,
 	tcLHsType, tcCheckLHsType, 
@@ -902,205 +901,7 @@ addTypeCtxt (L _ ty) thing
 %*									*
 %************************************************************************
 
-Note [Kind-checking strategies]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-There are three main declarations that we have to kind check carefully in the
-presence of -XPolyKinds: classes, datatypes, and data/type families. They each
-have a different kind-checking strategy (labeled in the parentheses above each
-section). This should potentially be cleaned up in the future, but this is how
-it stands now (June 2013).
-
-Classes (ParametricKinds):
-  - kind-polymorphic by default
-  - each un-annotated type variable is given a fresh meta kind variable
-  - every explicit kind variable becomes a SigTv during inference
-  - no generalisation is done while kind-checking the recursive group
-
-  Taken together, this means that classes cannot participate in polymorphic
-  recursion. Thus, the following is not definable:
-
-  class Fugly (a :: k) where
-    foo :: forall (b :: k -> *). Fugly b => b a
-
-  But, because explicit kind variables are SigTvs, it is OK for the kind to
-  be forced to be the same kind that is used in a separate declaration. See
-  test case polykinds/T7020.hs.
-
-Datatypes:
-  Here we have two cases, whether or not a Full Kind Signature is provided.
-  A Full Kind Signature means that there is a top-level :: in the definition
-  of the datatype. For example:
-
-  data T1 :: k -> Bool -> * where ...         -- YES
-  data T2 (a :: k) :: Bool -> * where ...     -- YES
-  data T3 (a :: k) (b :: Bool) :: * where ... -- YES
-  data T4 (a :: k) (b :: Bool) where ...      -- NO
-
-  Kind signatures are not allowed on datatypes declared in the H98 style,
-  so those always have no Full Kind Signature.
-
-  Full Kind Signature (FullKindSignature):
-    - each un-annotated type variable defaults to *
-    - every explicit kind variable becomes a skolem during type inference
-    - these kind variables are generalised *before* kind-checking the group
-
-    With these rules, polymorphic recursion is possible. This is essentially
-    because of the generalisation step before kind-checking the group -- it
-    gives the kind-checker enough flexibility to supply the right kind arguments
-    to support polymorphic recursion.
-
-  no Full Kind Signature (ParametricKinds):
-    - kind-polymorphic by default
-    - each un-annotated type variable is given a fresh meta kind variable
-    - every explicit kind variable becomes a SigTv during inference
-    - no generalisation is done while kind-checking the recursive group
-
-    Thus, no polymorphic recursion in this case. See also Trac #6093 & #6049.
-
-Type families:
-  Here we have three cases: open top-level families, closed top-level families,
-  and open associated types. (There are no closed associated types, for good
-  reason.)
-
-  Open top-level families (FullKindSignature):
-    - All open top-level families are considered to have a Full Kind Signature
-    - All arguments and the result default to *
-    - All kind variables are skolems
-    - All kind variables are generalised before kind-checking the group
-
-    This behaviour supports kind-indexed type and data families, because we
-    need to have generalised before kind-checking for this to work. For example:
-
-    type family F (a :: k)
-    type instance F Int = Bool
-    type instance F Maybe = Char
-    type instance F (x :: * -> * -> *) = Double
-
-  Closed top-level families (NonParametricKinds):
-    - kind-monomorphic by default
-    - each un-annotated type variable is given a fresh meta kind variable
-    - every explicit kind variable becomes a skolem during inference
-    - all such skolems are generalised before kind-checking; other kind
-      variables are not generalised
-    - all unconstrained meta kind variables are defaulted to * at the
-      end of kind checking
-
-    This behaviour is to allow kind inference to occur in closed families, but
-    without becoming too polymorphic. For example:
-
-    type family F a where
-      F Int = Bool
-      F Bool = Char
-
-    We would want F to have kind * -> * from this definition, although something
-    like k1 -> k2 would be perfectly sound. The reason we want this restriction is
-    that it is better to have (F Maybe) be a kind error than simply stuck.
-
-    The kind inference gives us also
-
-    type family Not b where
-      Not False = True
-      Not True  = False
-
-    With an open family, the above would need kind annotations in its header.
-
-    The tricky case is
-
-    type family G a (b :: k) where
-      G Int Int    = False
-      G Bool Maybe = True
-
-    We want this to work. But, we also want (G Maybe Maybe) to be a kind error
-    (in the first argument). So, we need to generalise the skolem "k" but not
-    the meta kind variable associated with "a".
-
-  Associated families (FullKindSignature):
-    - Kind-monomorphic by default
-    - Result kind defaults to *
-    - Each type variable is either in the class header or not:
-      - Type variables in the class header are given the kind inherited from
-        the class header (and checked against an annotation, if any)
-      - Un-annotated type variables default to *
-    - Each kind variable mentioned in the class header becomes a SigTv during
-      kind inference.
-    - Each kind variable not mentioned in the class header becomes a skolem during
-      kind inference.
-    - Only the skolem kind variables are generalised before kind checking.
-
-    Here are some examples:
-    
-    class Foo1 a b where
-      type Bar1 (a :: k) (b :: k)
-
-    The kind of Foo1 will be k -> k -> Constraint. Kind annotations on associated
-    type declarations propagate to the header because the type variables in Bar1's
-    declaration inherit the (meta) kinds of the class header.
-
-    class Foo2 a where
-      type Bar2 a
-
-    The kind of Bar2 will be k -> *.
-
-    class Foo3 a where
-      type Bar3 a (b :: k)
-      meth :: Bar3 a Maybe -> ()
-
-    The kind of Bar3 will be k1 -> k2 -> *. This only kind-checks because the kind
-    of b is generalised before kind-checking.
-
-    class Foo4 a where
-      type Bar4 a b
-
-    Here, the kind of Bar4 will be k -> * -> *, because b is not mentioned in the
-    class header, so it defaults to *.
-
 \begin{code}
-data KindCheckingStrategy   -- See Note [Kind-checking strategies]
-  = ParametricKinds
-  | NonParametricKinds
-  | FullKindSignature
-  deriving (Eq)
-
--- determine the appropriate strategy for a decl
-kcStrategy :: TyClDecl Name -> KindCheckingStrategy
-kcStrategy d@(ForeignType {}) = pprPanic "kcStrategy" (ppr d)
-kcStrategy (FamDecl fam_decl)
-  = kcStrategyFamDecl fam_decl
-kcStrategy (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs })
-  | all_tyvars_annotated tyvars
-  , rhs_annotated rhs
-  = FullKindSignature
-  | otherwise
-  = ParametricKinds
-  where
-    rhs_annotated (L _ ty) = case ty of
-      HsParTy lty  -> rhs_annotated lty
-      HsKindSig {} -> True
-      _            -> False
-kcStrategy decl@(DataDecl {})  = kcStrategyAlgDecl decl
-kcStrategy decl@(ClassDecl {}) = kcStrategyAlgDecl decl
-
-kcStrategyAlgDecl :: TyClDecl Name -> KindCheckingStrategy
-kcStrategyAlgDecl decl
-  | all_tyvars_annotated $ tcdTyVars decl
-  = FullKindSignature
-  | otherwise
-  = ParametricKinds
-
-kcStrategyFamDecl :: FamilyDecl Name -> KindCheckingStrategy
-kcStrategyFamDecl (FamilyDecl { fdInfo = ClosedTypeFamily _
-                              , fdTyVars = tyvars
-                              , fdKindSig = Just _ })
-  | all (isHsKindedTyVar . unLoc) (hsQTvBndrs tyvars)
-  = FullKindSignature
--- if the ClosedTypeFamily has no equations, do the defaulting to *, etc.
-kcStrategyFamDecl (FamilyDecl { fdInfo = ClosedTypeFamily (_:_) }) = ParametricKinds
-kcStrategyFamDecl _                                                = FullKindSignature
-
--- | Are all the type variables given with a kind annotation?
-all_tyvars_annotated :: LHsTyVarBndrs name -> Bool
-all_tyvars_annotated = all (isHsKindedTyVar . unLoc) . hsQTvBndrs
 
 mkKindSigVar :: Name -> TcM KindVar
 -- Use the specified name; don't clone it
@@ -1121,13 +922,17 @@ kcScopedKindVars kv_ns thing_inside
                      -- NB: use mutable signature variables
        ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) thing_inside } 
 
-kcHsTyVarBndrs :: KindCheckingStrategy
+-- | Kind-check a 'LHsTyVarBndrs'. If the decl under consideration has a complete,
+-- user-supplied kind signature (CUSK), generalise the result. Used in 'getInitialKind'
+-- and in kind-checking. See also Note [Complete user-supplied kind signatures] in
+-- HsDecls.
+kcHsTyVarBndrs :: Bool    -- ^ True <=> the decl being checked has a CUSK
                -> LHsTyVarBndrs Name 
-	       -> TcM (Kind, r)   -- the result kind, possibly with other info
-	       -> TcM (Kind, r)
--- Used in getInitialKind
-kcHsTyVarBndrs strat (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
-  = do { kvs <- if skolem_kvs
+	       -> TcM (Kind, r)   -- ^ the result kind, possibly with other info
+	       -> TcM (Kind, r)   -- ^ The full kind of the thing being declared,
+                                  -- with the other info
+kcHsTyVarBndrs cusk (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
+  = do { kvs <- if cusk
                 then mapM mkKindSigVar kv_ns
                 else mapM (\n -> newSigTyVar n superKind) kv_ns
        ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
@@ -1136,24 +941,18 @@ kcHsTyVarBndrs strat (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
        ; let full_kind = mkArrowKinds (map snd nks) res_kind
              kvs       = filter (not . isMetaTyVar) $
                          varSetElems $ tyVarsOfType full_kind
-             gen_kind  = if generalise
+             gen_kind  = if cusk
                          then mkForAllTys kvs full_kind
                          else full_kind
        ; return (gen_kind, stuff) } }
   where
-    -- See Note [Kind-checking strategies]
-    (skolem_kvs, default_to_star, generalise) = case strat of
-          ParametricKinds    -> (False, False, False)
-          NonParametricKinds -> (True,  False, True)
-          FullKindSignature  -> (True,  True,  True)
-
     kc_hs_tv :: HsTyVarBndr Name -> TcM (Name, TcKind)
     kc_hs_tv (UserTyVar n)
       = do { mb_thing <- tcLookupLcl_maybe n
            ; kind <- case mb_thing of
-               	       Just (AThing k)     -> return k
-               	       _ | default_to_star -> return liftedTypeKind
-               	         | otherwise       -> newMetaKindVar
+               	       Just (AThing k) -> return k
+               	       _ | cusk        -> return liftedTypeKind
+               	         | otherwise   -> newMetaKindVar
            ; return (n, kind) }
     kc_hs_tv (KindedTyVar n k) 
       = do { kind <- tcLHsKind k
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 2db31e33e4..6dcbaffef8 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -354,7 +354,6 @@ getInitialKinds decls
     do { pairss <- mapM (addLocM getInitialKind) decls
        ; return (concat pairss) }
 
--- See Note [Kind-checking strategies] in TcHsType
 getInitialKind :: TyClDecl Name -> TcM [(Name, TcTyThing)]
 -- Allocate a fresh kind variable for each TyCon and Class
 -- For each tycon, return   (tc, AThing k)
@@ -375,7 +374,7 @@ getInitialKind :: TyClDecl Name -> TcM [(Name, TcTyThing)]
 
 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
   = do { (cl_kind, inner_prs) <-
-           kcHsTyVarBndrs (kcStrategy decl) ktvs $
+           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
            do { inner_prs <- getFamDeclInitialKinds ats
               ; return (constraintKind, inner_prs) }
        ; let main_pr = (name, AThing cl_kind)
@@ -386,7 +385,7 @@ getInitialKind decl@(DataDecl { tcdLName = L _ name
                                 , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                            , dd_cons = cons } })
   = do { (decl_kind, _) <-
-           kcHsTyVarBndrs (kcStrategy decl) ktvs $
+           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
            do { res_k <- case m_sig of
                            Just ksig -> tcLHsKind ksig
                            Nothing   -> return liftedTypeKind
@@ -418,16 +417,14 @@ getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name
                                        , fdTyVars = ktvs
                                        , fdKindSig = ksig })
   = do { (fam_kind, _) <-
-           kcHsTyVarBndrs (kcStrategyFamDecl decl) ktvs $
+           kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $
            do { res_k <- case ksig of
                            Just k  -> tcLHsKind k
                            Nothing
-                             | defaultResToStar -> return liftedTypeKind
-                             | otherwise        -> newMetaKindVar
+                             | famDeclHasCusk decl -> return liftedTypeKind
+                             | otherwise           -> newMetaKindVar
               ; return (res_k, ()) }
        ; return [ (name, AThing fam_kind) ] }
-  where
-    defaultResToStar = (kcStrategyFamDecl decl == FullKindSignature)
 
 ----------------
 kcSynDecls :: [SCC (LTyClDecl Name)]
@@ -451,7 +448,7 @@ kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
   -- Returns a possibly-unzonked kind
   = tcAddDeclCtxt decl $
     do { (syn_kind, _) <-
-           kcHsTyVarBndrs (kcStrategy decl) hs_tvs $
+           kcHsTyVarBndrs (hsDeclHasCusk decl) hs_tvs $
            do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
               ; (_, rhs_kind) <- tcLHsType rhs
               ; traceTc "kcd2" (ppr name)
@@ -516,7 +513,10 @@ kcConDecl (ConDecl { con_name = name, con_qvars = ex_tvs
                    , con_cxt = ex_ctxt, con_details = details
                    , con_res = res })
   = addErrCtxt (dataConCtxt name) $
-    do { _ <- kcHsTyVarBndrs ParametricKinds ex_tvs $
+         -- the 'False' says that the existentials don't have a CUSK, as the
+         -- concept doesn't really apply here. We just need to bring the variables
+         -- into scope!
+    do { _ <- kcHsTyVarBndrs False ex_tvs $
               do { _ <- tcHsContext ex_ctxt
                  ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
                  ; _ <- tcConRes res