Fix #11648.
authorRichard Eisenberg <eir@cis.upenn.edu>
Sun, 13 Mar 2016 01:59:44 +0000 (20:59 -0500)
committerRichard Eisenberg <eir@cis.upenn.edu>
Tue, 15 Mar 2016 03:50:52 +0000 (23:50 -0400)
We now check that a CUSK is really a CUSK and issue an error if
it isn't. This also involves more solving and zonking in
kcHsTyVarBndrs, which was the outright bug reported in #11648.

Test cases: polykinds/T11648{,b}

This updates the haddock submodule.

[skip ci]

25 files changed:
compiler/deSugar/DsMeta.hs
compiler/hsSyn/Convert.hs
compiler/hsSyn/HsDecls.hs
compiler/hsSyn/HsTypes.hs
compiler/parser/RdrHsSyn.hs
compiler/rename/RnSource.hs
compiler/rename/RnTypes.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcValidity.hs
docs/users_guide/glasgow_exts.rst
testsuite/tests/dependent/should_compile/KindLevels.hs
testsuite/tests/dependent/should_fail/InferDependency.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/InferDependency.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/KindLevelsB.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/KindLevelsB.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/all.T
testsuite/tests/polykinds/T11648.hs [new file with mode: 0644]
testsuite/tests/polykinds/T11648b.hs [new file with mode: 0644]
testsuite/tests/polykinds/T11648b.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T6039.stderr [new file with mode: 0644]
testsuite/tests/polykinds/all.T
utils/haddock

index 4ed3431..833da59 100644 (file)
@@ -40,6 +40,7 @@ import Id
 import Name hiding( isVarOcc, isTcOcc, varName, tcName )
 import THNames
 import NameEnv
+import NameSet
 import TcType
 import TyCon
 import TysWiredIn
@@ -323,7 +324,8 @@ repFamilyDecl decl@(L loc (FamilyDecl { fdInfo      = info,
                                         fdInjectivityAnn = injectivity }))
   = do { tc1 <- lookupLOcc tc           -- See note [Binders and occurrences]
        ; let mkHsQTvs :: [LHsTyVarBndr Name] -> LHsQTyVars Name
-             mkHsQTvs tvs = HsQTvs { hsq_implicit = [], hsq_explicit = tvs }
+             mkHsQTvs tvs = HsQTvs { hsq_implicit = [], hsq_explicit = tvs
+                                   , hsq_dependent = emptyNameSet }
              resTyVar = case resultSig of
                      TyVarSig bndr -> mkHsQTvs [bndr]
                      _             -> mkHsQTvs []
@@ -471,7 +473,8 @@ repTyFamEqn (L _ (TyFamEqn { tfe_pats = HsIB { hsib_body = tys
                                              , hsib_vars = var_names }
                            , tfe_rhs = rhs }))
   = do { let hs_tvs = HsQTvs { hsq_implicit = var_names
-                             , hsq_explicit = [] }   -- Yuk
+                             , hsq_explicit = []
+                             , hsq_dependent = emptyNameSet }   -- Yuk
        ; addTyClTyVarBinds hs_tvs $ \ _ ->
          do { tys1 <- repLTys tys
             ; tys2 <- coreList typeQTyConName tys1
@@ -484,7 +487,8 @@ repDataFamInstD (DataFamInstDecl { dfid_tycon = tc_name
                                  , dfid_defn = defn })
   = do { tc <- lookupLOcc tc_name               -- See note [Binders and occurrences]
        ; let hs_tvs = HsQTvs { hsq_implicit = var_names
-                             , hsq_explicit = [] }   -- Yuk
+                             , hsq_explicit = []
+                             , hsq_dependent = emptyNameSet }   -- Yuk
        ; addTyClTyVarBinds hs_tvs $ \ bndrs ->
          do { tys1 <- repList typeQTyConName repLTy tys
             ; repDataDefn tc bndrs (Just tys1) defn } }
@@ -627,7 +631,8 @@ repC (L _ (ConDeclGADT { con_names = cons
   = do { let doc = text "In the constructor for " <+> ppr (head cons)
              con_tvs = HsQTvs { hsq_implicit = []
                               , hsq_explicit = (map (noLoc . UserTyVar . noLoc)
-                                                   con_vars) ++ tvs }
+                                                   con_vars) ++ tvs
+                              , hsq_dependent = emptyNameSet }
        ; addTyVarBinds con_tvs $ \ ex_bndrs -> do
        { (hs_details, gadt_res_ty) <-
            updateGadtResult failWithDs doc details res_ty'
@@ -875,7 +880,8 @@ repHsSigWcType (HsIB { hsib_vars = vars
   | (explicit_tvs, ctxt, ty) <- splitLHsSigmaTy (hswc_body sig1)
   = addTyVarBinds (HsQTvs { hsq_implicit = []
                           , hsq_explicit = map (noLoc . UserTyVar . noLoc) vars ++
-                                           explicit_tvs })
+                                           explicit_tvs
+                          , hsq_dependent = emptyNameSet })
                   $ \ th_tvs ->
     do { th_ctxt <- repLContext ctxt
        ; th_ty   <- repLTy ty
@@ -897,7 +903,8 @@ repForall :: HsType Name -> DsM (Core TH.TypeQ)
 -- Arg of repForall is always HsForAllTy or HsQualTy
 repForall ty
  | (tvs, ctxt, tau) <- splitLHsSigmaTy (noLoc ty)
- = addTyVarBinds (HsQTvs { hsq_implicit = [], hsq_explicit = tvs}) $ \bndrs ->
+ = addTyVarBinds (HsQTvs { hsq_implicit = [], hsq_explicit = tvs
+                         , hsq_dependent = emptyNameSet }) $ \bndrs ->
    do { ctxt1  <- repLContext ctxt
       ; ty1    <- repLTy tau
       ; repTForall bndrs ctxt1 ty1 }
index 213c4f5..90e3886 100644 (file)
@@ -210,6 +210,7 @@ cvtDec (DataD ctxt tc tvs ksig constrs derivs)
                                 , dd_cons = cons', dd_derivs = derivs' }
         ; returnJustL $ TyClD (DataDecl { tcdLName = tc', tcdTyVars = tvs'
                                         , tcdDataDefn = defn
+                                        , tcdDataCusk = PlaceHolder
                                         , tcdFVs = placeHolderNames }) }
 
 cvtDec (NewtypeD ctxt tc tvs ksig constr derivs)
@@ -224,6 +225,7 @@ cvtDec (NewtypeD ctxt tc tvs ksig constr derivs)
                                 , dd_derivs = derivs' }
         ; returnJustL $ TyClD (DataDecl { tcdLName = tc', tcdTyVars = tvs'
                                     , tcdDataDefn = defn
+                                    , tcdDataCusk = PlaceHolder
                                     , tcdFVs = placeHolderNames }) }
 
 cvtDec (ClassD ctxt cl tvs fds decs)
index 75544ab..2576871 100644 (file)
@@ -106,7 +106,7 @@ import Util
 import SrcLoc
 
 import Bag
-import Data.Maybe ( fromMaybe )
+import Maybes
 import Data.Data        hiding (TyCon,Fixity)
 
 {-
@@ -503,6 +503,7 @@ data TyClDecl name
                                                   -- Here the type decl for 'f' includes 'a'
                                                   -- in its tcdTyVars
              , tcdDataDefn :: HsDataDefn name
+             , tcdDataCusk :: PostRn name Bool    -- ^ does this have a CUSK?
              , tcdFVs      :: PostRn name NameSet }
 
   | ClassDecl { tcdCtxt    :: LHsContext name,          -- ^ Context...
@@ -632,7 +633,7 @@ countTyClDecls decls
 -- | Does this declaration have a complete, user-supplied kind signature?
 -- See Note [Complete user-supplied kind signatures]
 hsDeclHasCusk :: TyClDecl Name -> Bool
-hsDeclHasCusk (FamDecl { tcdFam = fam_decl }) = famDeclHasCusk fam_decl
+hsDeclHasCusk (FamDecl { tcdFam = fam_decl }) = famDeclHasCusk Nothing fam_decl
 hsDeclHasCusk (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs })
   = hsTvbAllKinded tyvars && rhs_annotated rhs
   where
@@ -640,7 +641,7 @@ hsDeclHasCusk (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs })
       HsParTy lty  -> rhs_annotated lty
       HsKindSig {} -> True
       _            -> False
-hsDeclHasCusk (DataDecl { tcdTyVars = tyvars })  = hsTvbAllKinded tyvars
+hsDeclHasCusk (DataDecl { tcdDataCusk = cusk }) = cusk
 hsDeclHasCusk (ClassDecl { tcdTyVars = tyvars }) = hsTvbAllKinded tyvars
 
 -- Pretty-printing TyClDecl
@@ -837,12 +838,15 @@ data FamilyInfo name
 deriving instance (DataId name) => Data (FamilyInfo name)
 
 -- | Does this family declaration have a complete, user-supplied kind signature?
-famDeclHasCusk :: FamilyDecl name -> Bool
-famDeclHasCusk (FamilyDecl { fdInfo      = ClosedTypeFamily _
-                           , fdTyVars    = tyvars
-                           , fdResultSig = L _ resultSig })
+famDeclHasCusk :: Maybe Bool
+                   -- ^ if associated, does the enclosing class have a CUSK?
+               -> FamilyDecl name -> Bool
+famDeclHasCusk _ (FamilyDecl { fdInfo      = ClosedTypeFamily _
+                             , fdTyVars    = tyvars
+                             , fdResultSig = L _ resultSig })
   = hsTvbAllKinded tyvars && hasReturnKindSignature resultSig
-famDeclHasCusk _ = True  -- all open families have CUSKs!
+famDeclHasCusk mb_class_cusk _ = mb_class_cusk `orElse` True
+        -- all un-associated open families have CUSKs!
 
 -- | Does this family declaration have user-supplied return kind signature?
 hasReturnKindSignature :: FamilyResultSig a -> Bool
@@ -879,6 +883,10 @@ variables and its return type are annotated.
 
  - An open type family always has a CUSK -- unannotated type variables (and
 return type) default to *.
+
+ - Additionally, if -XTypeInType is on, then a data definition with a top-level
+   :: must explicitly bind all kind variables to the right of the ::.
+   See test dependent/should_compile/KindLevels, which requires this case.
 -}
 
 instance (OutputableBndr name) => Outputable (FamilyDecl name) where
@@ -1133,7 +1141,7 @@ pprConDecl (ConDeclH98 { con_name = L _ con
                                  <+> pprConDeclFields (unLoc fields)
     tvs = case mtvs of
       Nothing -> []
-      Just (HsQTvs _ tvs) -> tvs
+      Just (HsQTvs { hsq_explicit = tvs }) -> tvs
 
     cxt = fromMaybe (noLoc []) mcxt
 
index a14c24d..04b0ae8 100644 (file)
@@ -74,6 +74,7 @@ import PlaceHolder ( PostTc,PostRn,DataId,PlaceHolder(..) )
 import Id ( Id )
 import Name( Name )
 import RdrName ( RdrName )
+import NameSet ( NameSet, emptyNameSet )
 import DataCon( HsSrcBang(..), HsImplBang(..),
                 SrcStrictness(..), SrcUnpackedness(..) )
 import TysPrim( funTyConName )
@@ -246,23 +247,27 @@ data LHsQTyVars name   -- See Note [HsType binders]
   = HsQTvs { hsq_implicit :: PostRn name [Name]      -- implicit (dependent) variables
            , hsq_explicit :: [LHsTyVarBndr name]     -- explicit variables
              -- See Note [HsForAllTy tyvar binders]
+           , hsq_dependent :: PostRn name NameSet
+               -- which explicit vars are dependent
+               -- See Note [Dependent LHsQTyVars] in TcHsType
     }
   deriving( Typeable )
 
 deriving instance (DataId name) => Data (LHsQTyVars name)
 
 mkHsQTvs :: [LHsTyVarBndr RdrName] -> LHsQTyVars RdrName
-mkHsQTvs tvs = HsQTvs { hsq_implicit = PlaceHolder, hsq_explicit = tvs }
+mkHsQTvs tvs = HsQTvs { hsq_implicit = PlaceHolder, hsq_explicit = tvs
+                      , hsq_dependent = PlaceHolder }
 
 hsQTvExplicit :: LHsQTyVars name -> [LHsTyVarBndr name]
 hsQTvExplicit = hsq_explicit
 
 emptyLHsQTvs :: LHsQTyVars Name
-emptyLHsQTvs = HsQTvs [] []
+emptyLHsQTvs = HsQTvs [] [] emptyNameSet
 
 isEmptyLHsQTvs :: LHsQTyVars Name -> Bool
-isEmptyLHsQTvs (HsQTvs [] []) = True
-isEmptyLHsQTvs _              = False
+isEmptyLHsQTvs (HsQTvs [] [] _) = True
+isEmptyLHsQTvs _                = False
 
 ------------------------------------------------
 --            HsImplicitBndrs
index 372874a..8aeeb9d 100644 (file)
@@ -176,6 +176,7 @@ mkTyData loc new_or_data cType (L _ (mcxt, tycl_hdr)) ksig data_cons maybe_deriv
        ; defn <- mkDataDefn new_or_data cType mcxt ksig data_cons maybe_deriv
        ; return (L loc (DataDecl { tcdLName = tc, tcdTyVars = tyvars,
                                    tcdDataDefn = defn,
+                                   tcdDataCusk = PlaceHolder,
                                    tcdFVs = placeHolderNames })) }
 
 mkDataDefn :: NewOrData
index df729dc..03d65ef 100644 (file)
@@ -816,7 +816,7 @@ rnDataFamInstDecl :: Maybe (Name, [Name])
 rnDataFamInstDecl mb_cls (DataFamInstDecl { dfid_tycon = tycon
                                           , dfid_pats  = pats
                                           , dfid_defn  = defn })
-  = do { (tycon', pats', defn', fvs) <-
+  = do { (tycon', pats', (defn', _), fvs) <-
            rnFamInstDecl (TyDataCtx tycon) mb_cls tycon pats defn rnDataDefn
        ; return (DataFamInstDecl { dfid_tycon = tycon'
                                  , dfid_pats  = pats'
@@ -1264,11 +1264,17 @@ rnTyClDecl (DataDecl { tcdLName = tycon, tcdTyVars = tyvars, tcdDataDefn = defn
        ; kvs <- extractDataDefnKindVars defn
        ; let doc = TyDataCtx tycon
        ; traceRn (text "rntycl-data" <+> ppr tycon <+> ppr kvs)
-       ; ((tyvars', defn'), fvs) <- bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' ->
-                                    do { (defn', fvs) <- rnDataDefn doc defn
-                                       ; return ((tyvars', defn'), fvs) }
+       ; ((tyvars', defn', no_kvs), fvs)
+           <- bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' ->
+              do { ((defn', no_kvs), fvs) <- rnDataDefn doc defn
+                 ; return ((tyvars', defn', no_kvs), fvs) }
+          -- See Note [Complete user-supplied kind signatures] in HsDecls
+       ; typeintype <- xoptM LangExt.TypeInType
+       ; let cusk = hsTvbAllKinded tyvars' &&
+                    (not typeintype || no_kvs)
        ; return (DataDecl { tcdLName = tycon', tcdTyVars = tyvars'
-                          , tcdDataDefn = defn', tcdFVs = fvs }, fvs) }
+                          , tcdDataDefn = defn', tcdDataCusk = cusk
+                          , tcdFVs = fvs }, fvs) }
 
 rnTyClDecl (ClassDecl { tcdCtxt = context, tcdLName = lcls,
                         tcdTyVars = tyvars, tcdFDs = fds, tcdSigs = sigs,
@@ -1391,14 +1397,23 @@ orphanRoleAnnotErr (L loc decl)
             quotes (ppr $ roleAnnotDeclName decl) <+>
             text "is declared.")
 
-rnDataDefn :: HsDocContext -> HsDataDefn RdrName -> RnM (HsDataDefn Name, FreeVars)
+rnDataDefn :: HsDocContext -> HsDataDefn RdrName
+           -> RnM ((HsDataDefn Name, Bool), FreeVars)
+                -- the Bool is True if the DataDefn is consistent with
+                -- having a CUSK. See Note [Complete user-supplied kind signatures]
+                -- in HsDecls
 rnDataDefn doc (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                            , dd_ctxt = context, dd_cons = condecls
-                           , dd_kindSig = sig, dd_derivs = derivs })
+                           , dd_kindSig = m_sig, dd_derivs = derivs })
   = do  { checkTc (h98_style || null (unLoc context))
                   (badGadtStupidTheta doc)
 
-        ; (sig', sig_fvs)  <- rnLHsMaybeKind doc sig
+        ; (m_sig', cusk, sig_fvs) <- case m_sig of
+             Just sig -> do { fkvs <- freeKiTyVarsAllVars <$>
+                                      extractHsTyRdrTyVars sig
+                            ; (sig', fvs) <- rnLHsKind doc sig
+                            ; return (Just sig', null fkvs, fvs) }
+             Nothing  -> return (Nothing, True, emptyFVs)
         ; (context', fvs1) <- rnContext doc context
         ; (derivs',  fvs3) <- rn_derivs derivs
 
@@ -1414,10 +1429,11 @@ rnDataDefn doc (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
 
         ; let all_fvs = fvs1 `plusFV` fvs3 `plusFV`
                         con_fvs `plusFV` sig_fvs
-        ; return ( HsDataDefn { dd_ND = new_or_data, dd_cType = cType
-                              , dd_ctxt = context', dd_kindSig = sig'
-                              , dd_cons = condecls'
-                              , dd_derivs = derivs' }
+        ; return (( HsDataDefn { dd_ND = new_or_data, dd_cType = cType
+                               , dd_ctxt = context', dd_kindSig = m_sig'
+                               , dd_cons = condecls'
+                               , dd_derivs = derivs' }
+                  , cusk )
                  , all_fvs )
         }
   where
@@ -1504,7 +1520,7 @@ rnFamResultSig doc kv_names (TyVarSig tvbndr)
                           (mkNameSet kv_names) emptyNameSet
                                        -- use of emptyNameSet here avoids
                                        -- redundant duplicate errors
-                          tvbndr $ \ _ tvbndr' ->
+                          tvbndr $ \ _ tvbndr' ->
          return (TyVarSig tvbndr', unitFV (hsLTyVarName tvbndr')) }
 
 -- Note [Renaming injectivity annotation]
index 7e82ddc..d14769e 100644 (file)
@@ -10,7 +10,7 @@
 module RnTypes (
         -- Type related stuff
         rnHsType, rnLHsType, rnLHsTypes, rnContext,
-        rnHsKind, rnLHsKind, rnLHsMaybeKind,
+        rnHsKind, rnLHsKind,
         rnHsSigType, rnHsWcType,
         rnHsSigWcType, rnHsSigWcTypeScoped,
         rnLHsInstType,
@@ -144,7 +144,7 @@ rnWcSigTy :: RnTyKiEnv -> LHsType RdrName
 -- wildcard.  Some code duplication, but no big deal.
 rnWcSigTy env (L loc hs_ty@(HsForAllTy { hst_bndrs = tvs, hst_body = hs_tau }))
   = bindLHsTyVarBndrs (rtke_ctxt env) (Just $ inTypeDoc hs_ty)
-                      Nothing [] tvs $ \ _ tvs' ->
+                      Nothing [] tvs $ \ _ tvs' ->
     do { (hs_tau', fvs) <- rnWcSigTy env hs_tau
        ; let hs_ty' = HsForAllTy { hst_bndrs = tvs', hst_body = hswc_body hs_tau' }
              awcs_bndrs = collectAnonWildCardsBndrs tvs'
@@ -426,14 +426,6 @@ rnLHsKind ctxt kind = rnLHsTyKi (mkTyKiEnv ctxt KindLevel RnTypeBody) kind
 rnHsKind  :: HsDocContext -> HsKind RdrName -> RnM (HsKind Name, FreeVars)
 rnHsKind ctxt kind = rnHsTyKi  (mkTyKiEnv ctxt KindLevel RnTypeBody) kind
 
-rnLHsMaybeKind  :: HsDocContext -> Maybe (LHsKind RdrName)
-                -> RnM (Maybe (LHsKind Name), FreeVars)
-rnLHsMaybeKind _ Nothing
-  = return (Nothing, emptyFVs)
-rnLHsMaybeKind doc (Just kind)
-  = do { (kind', fvs) <- rnLHsKind doc kind
-       ; return (Just kind', fvs) }
-
 --------------
 rnTyKiContext :: RnTyKiEnv -> LHsContext RdrName -> RnM (LHsContext Name, FreeVars)
 rnTyKiContext env (L loc cxt)
@@ -458,7 +450,7 @@ rnHsTyKi :: RnTyKiEnv -> HsType RdrName -> RnM (HsType Name, FreeVars)
 rnHsTyKi env ty@(HsForAllTy { hst_bndrs = tyvars, hst_body  = tau })
   = do { checkTypeInType env ty
        ; bindLHsTyVarBndrs (rtke_ctxt env) (Just $ inTypeDoc ty)
-                           Nothing [] tyvars $ \ _ tyvars' ->
+                           Nothing [] tyvars $ \ _ tyvars' ->
     do { (tau',  fvs) <- rnLHsTyKi env tau
        ; return ( HsForAllTy { hst_bndrs = tyvars', hst_body =  tau' }
                 , fvs) } }
@@ -853,9 +845,10 @@ bindHsQTyVars :: forall a b.
 bindHsQTyVars doc mb_in_doc mb_assoc kv_bndrs tv_bndrs thing_inside
   = do { bindLHsTyVarBndrs doc mb_in_doc
                            mb_assoc kv_bndrs (hsQTvExplicit tv_bndrs) $
-         \ rn_kvs rn_bndrs ->
+         \ rn_kvs rn_bndrs dep_var_set ->
          thing_inside (HsQTvs { hsq_implicit = rn_kvs
-                              , hsq_explicit = rn_bndrs }) }
+                              , hsq_explicit = rn_bndrs
+                              , hsq_dependent = dep_var_set }) }
 
 bindLHsTyVarBndrs :: forall a b.
                      HsDocContext
@@ -867,11 +860,14 @@ bindLHsTyVarBndrs :: forall a b.
                   -> [LHsTyVarBndr RdrName]  -- ... these user-written tyvars
                   -> (   [Name]  -- all kv names
                       -> [LHsTyVarBndr Name]
+                      -> NameSet -- which names, from the preceding list,
+                                 -- are used dependently within that list
+                                 -- See Note [Dependent LHsQTyVars] in TcHsType
                       -> RnM (b, FreeVars))
                   -> RnM (b, FreeVars)
 bindLHsTyVarBndrs doc mb_in_doc mb_assoc kv_bndrs tv_bndrs thing_inside
   = do { when (isNothing mb_assoc) (checkShadowedRdrNames tv_names_w_loc)
-       ; go [] [] emptyNameSet emptyNameSet tv_bndrs }
+       ; go [] [] emptyNameSet emptyNameSet emptyNameSet tv_bndrs }
   where
     tv_names_w_loc = map hsLTyVarLocName tv_bndrs
 
@@ -879,29 +875,38 @@ bindLHsTyVarBndrs doc mb_in_doc mb_assoc kv_bndrs tv_bndrs thing_inside
        -> [LHsTyVarBndr Name]    -- already renamed (in reverse order)
        -> NameSet                -- kind vars already in scope (for dup checking)
        -> NameSet                -- type vars already in scope (for dup checking)
+       -> NameSet                -- (all) variables used dependently
        -> [LHsTyVarBndr RdrName] -- still to be renamed, scoped
        -> RnM (b, FreeVars)
-    go rn_kvs rn_tvs kv_names tv_names (tv_bndr : tv_bndrs)
+    go rn_kvs rn_tvs kv_names tv_names dep_vars (tv_bndr : tv_bndrs)
       = bindLHsTyVarBndr doc mb_assoc kv_names tv_names tv_bndr $
-        \ kv_nms tv_bndr' ->
+        \ kv_nms used_dependently tv_bndr' ->
         do { (b, fvs) <- go (reverse kv_nms ++ rn_kvs)
                             (tv_bndr' : rn_tvs)
                             (kv_names `extendNameSetList` kv_nms)
                             (tv_names `extendNameSet` hsLTyVarName tv_bndr')
+                            (dep_vars `unionNameSet` used_dependently)
                             tv_bndrs
            ; warn_unused tv_bndr' fvs
            ; return (b, fvs) }
 
-    go rn_kvs rn_tvs _kv_names tv_names []
+    go rn_kvs rn_tvs _kv_names tv_names dep_vars []
       = -- still need to deal with the kv_bndrs passed in originally
-        bindImplicitKvs doc mb_assoc kv_bndrs tv_names $ \ kv_nms ->
+        bindImplicitKvs doc mb_assoc kv_bndrs tv_names $ \ kv_nms others ->
         do { let all_rn_kvs = reverse (reverse kv_nms ++ rn_kvs)
                  all_rn_tvs = reverse rn_tvs
            ; env <- getLocalRdrEnv
+           ; let all_dep_vars = dep_vars `unionNameSet` others
+                 exp_dep_vars -- variables in all_rn_tvs that are in dep_vars
+                   = mkNameSet [ name
+                               | v <- all_rn_tvs
+                               , let name = hsLTyVarName v
+                               , name `elemNameSet` all_dep_vars ]
            ; traceRn (text "bindHsTyVars" <+> (ppr env $$
                                                ppr all_rn_kvs $$
-                                               ppr all_rn_tvs))
-           ; thing_inside all_rn_kvs all_rn_tvs }
+                                               ppr all_rn_tvs $$
+                                               ppr exp_dep_vars))
+           ; thing_inside all_rn_kvs all_rn_tvs exp_dep_vars }
 
     warn_unused tv_bndr fvs = case mb_in_doc of
       Just in_doc -> warnUnusedForAll in_doc tv_bndr fvs
@@ -912,8 +917,9 @@ bindLHsTyVarBndr :: HsDocContext
                  -> NameSet   -- kind vars already in scope
                  -> NameSet   -- type vars already in scope
                  -> LHsTyVarBndr RdrName
-                 -> ([Name] -> LHsTyVarBndr Name -> RnM (b, FreeVars))
+                 -> ([Name] -> NameSet -> LHsTyVarBndr Name -> RnM (b, FreeVars))
                    -- passed the newly-bound implicitly-declared kind vars,
+                   -- any other names used in a kind
                    -- and the renamed LHsTyVarBndr
                  -> RnM (b, FreeVars)
 bindLHsTyVarBndr doc mb_assoc kv_names tv_names hs_tv_bndr thing_inside
@@ -922,7 +928,7 @@ bindLHsTyVarBndr doc mb_assoc kv_names tv_names hs_tv_bndr thing_inside
         do { check_dup loc rdr
            ; nm <- newTyVarNameRn mb_assoc lrdr
            ; bindLocalNamesFV [nm] $
-             thing_inside [] (L loc (UserTyVar (L lv nm))) }
+             thing_inside [] emptyNameSet (L loc (UserTyVar (L lv nm))) }
       L loc (KindedTyVar lrdr@(L lv rdr) kind) ->
         do { check_dup lv rdr
 
@@ -932,11 +938,12 @@ bindLHsTyVarBndr doc mb_assoc kv_names tv_names hs_tv_bndr thing_inside
 
              -- deal with kind vars in the user-written kind
            ; free_kvs <- freeKiTyVarsAllVars <$> extractHsTyRdrTyVars kind
-           ; bindImplicitKvs doc mb_assoc free_kvs tv_names $ \ kv_nms ->
+           ; bindImplicitKvs doc mb_assoc free_kvs tv_names $
+             \ new_kv_nms other_kv_nms ->
              do { (kind', fvs1) <- rnLHsKind doc kind
                 ; tv_nm  <- newTyVarNameRn mb_assoc lrdr
                 ; (b, fvs2) <- bindLocalNamesFV [tv_nm] $
-                               thing_inside kv_nms
+                               thing_inside new_kv_nms other_kv_nms
                                  (L loc (KindedTyVar (L lv tv_nm) kind'))
                 ; return (b, fvs1 `plusFV` fvs2) }}
   where
@@ -964,9 +971,11 @@ bindImplicitKvs :: HsDocContext
                                       -- intent to bind is inferred
                 -> NameSet            -- ^ *type* variables, for type/kind
                                       -- misuse check for -XNoTypeInType
-                -> ([Name] -> RnM (b, FreeVars)) -- ^ passed new kv_names
+                -> ([Name] -> NameSet -> RnM (b, FreeVars))
+                   -- ^ passed new kv_names, and any other names used in a kind
                 -> RnM (b, FreeVars)
-bindImplicitKvs _   _        []       _        thing_inside = thing_inside []
+bindImplicitKvs _   _        []       _        thing_inside
+  = thing_inside [] emptyNameSet
 bindImplicitKvs doc mb_assoc free_kvs tv_names thing_inside
   = do { rdr_env <- getLocalRdrEnv
        ; let part_kvs lrdr@(L loc kv_rdr)
@@ -987,7 +996,7 @@ bindImplicitKvs doc mb_assoc free_kvs tv_names thing_inside
           -- bind the vars and move on
        ; kv_nms <- mapM (newTyVarNameRn mb_assoc) new_kvs
        ; bindLocalNamesFV kv_nms $
-         thing_inside kv_nms }
+         thing_inside kv_nms (mkNameSet (map unLoc bound_kvs)) }
   where
       -- check to see if the variables free in a kind are bound as type
       -- variables. Assume -XNoTypeInType.
index 8c22c5c..f931073 100644 (file)
@@ -355,9 +355,12 @@ concern things that the renamer can't handle.
 
 -}
 
-data TcTyMode
+-- | Info about the context in which we're checking a type. Currently,
+-- differentiates only between types and kinds, but this will likely
+-- grow, at least to include the distinction between patterns and
+-- not-patterns.
+newtype TcTyMode
   = TcTyMode { mode_level :: TypeOrKind  -- True <=> type, False <=> kind
-                                         -- used only for -XNoTypeInType errors
              }
 
 typeLevelMode :: TcTyMode
@@ -370,6 +373,9 @@ kindLevelMode = TcTyMode { mode_level = KindLevel }
 kindLevel :: TcTyMode -> TcTyMode
 kindLevel mode = mode { mode_level = KindLevel }
 
+instance Outputable TcTyMode where
+  ppr = ppr . mode_level
+
 {-
 Note [Bidirectional type checking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -459,12 +465,17 @@ tc_lhs_type mode (L span ty) exp_kind
 
 ------------------------------------------
 tc_fun_type :: TcTyMode -> LHsType Name -> LHsType Name -> TcKind -> TcM TcType
-tc_fun_type mode ty1 ty2 exp_kind
-  = do { arg_rr <- newFlexiTyVarTy runtimeRepTy
+tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
+  TypeLevel ->
+    do { arg_rr <- newFlexiTyVarTy runtimeRepTy
        ; res_rr <- newFlexiTyVarTy runtimeRepTy
        ; ty1' <- tc_lhs_type mode ty1 (tYPE arg_rr)
        ; ty2' <- tc_lhs_type mode ty2 (tYPE res_rr)
        ; checkExpectedKind (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
+  KindLevel ->  -- no representation polymorphism in kinds. yet.
+    do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
+       ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
+       ; checkExpectedKind (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
 
 ------------------------------------------
 -- See also Note [Bidirectional type checking]
@@ -759,10 +770,8 @@ tc_infer_args mode orig_ty binders mb_kind_info orig_args n0
 
     go subst (binder:binders) (arg:args) n acc
       = ASSERT( isVisibleBinder binder )
-        do { let mode' | isNamedBinder binder = kindLevel mode
-                       | otherwise            = mode
-           ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
-                     tc_lhs_type mode' arg (substTyUnchecked subst $ binderType binder)
+        do { arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
+                     tc_lhs_type mode arg (substTyUnchecked subst $ binderType binder)
            ; let subst' = case binderVar_maybe binder of
                    Just tv -> extendTvSubst subst tv arg'
                    Nothing -> subst
@@ -1147,6 +1156,24 @@ we might be about to kindGeneralize.
 
 A little messy, but it works.
 
+Note [Dependent LHsQTyVars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We track (in the renamer) which explicitly bound variables in a
+LHsQTyVars are manifestly dependent; only precisely these variables
+may be used within the LHsQTyVars. We must do this so that kcHsTyVarBndrs
+can produce the right TcTyBinders, and tell Anon vs. Named. Earlier,
+I thought it would work simply to do a free-variable check during
+kcHsTyVarBndrs, but this is bogus, because there may be unsolved
+equalities about. And we don't want to eagerly solve the equalities,
+because we may get further information after kcHsTyVarBndrs is called.
+(Recall that kcHsTyVarBndrs is usually called from getInitialKind.
+The only other case is in kcConDecl.) This is what implements the rule
+that all variables intended to be dependent must be manifestly so.
+
+Sidenote: It's quite possible that later, we'll consider (t -> s)
+as a degenerate case of some (pi (x :: t) -> s) and then this will
+all get more permissive.
+
 -}
 
 tcWildCardBinders :: [Name]
@@ -1174,66 +1201,84 @@ tcWildCardBinders wcs thing_inside
 --
 -- This function does not do telescope checking.
 kcHsTyVarBndrs :: Bool    -- ^ True <=> the decl being checked has a CUSK
+               -> Bool    -- ^ True <=> the decl is an open type/data family
+               -> Bool    -- ^ True <=> all the hsq_implicit are *kind* vars
+                          -- (will give these kind * if -XNoTypeInType)
                -> LHsQTyVars Name
-               -> ([TyVar] -> [TyVar] -> TcM (Kind, r))
-                                  -- ^ the result kind, possibly with other info
-                                  -- ^ args are implicit vars, explicit vars
+               -> TcM (Kind, r)  -- ^ the result kind, possibly with other info
                -> TcM ([TcTyBinder], TcKind, r)
-                                  -- ^ The full kind of the thing being declared,
-                                  -- with the other info
-kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
-                            , hsq_explicit = hs_tvs }) thing_inside
-  = do { meta_kvs <- mapM (const newMetaKindVar) kv_ns
-       ; kvs <- if cusk
-                then return $ zipWith new_skolem_tv kv_ns meta_kvs
+                     -- ^ The bound variables in the kind, the result kind,
+                     -- with the other info.
+                     -- Always returns Named binders; sort out Named vs. Anon
+                     -- yourself.
+kcHsTyVarBndrs cusk open_fam all_kind_vars
+  (HsQTvs { hsq_implicit = kv_ns, hsq_explicit = hs_tvs
+          , hsq_dependent = dep_names }) thing_inside
+  | cusk
+  = do { kv_kinds <- mk_kv_kinds
+       ; let scoped_kvs = zipWith new_skolem_tv kv_ns kv_kinds
+       ; tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
+    do { (tvs, binders, res_kind, stuff) <- solveEqualities $
+                                            bind_telescope hs_tvs thing_inside
+
+           -- Now, because we're in a CUSK, quantify over the mentioned
+           -- kind vars, in dependency order.
+       ; binders  <- mapM zonkTcTyBinder binders
+       ; res_kind <- zonkTcType res_kind
+       ; let qkvs = tyCoVarsOfTypeWellScoped (mkForAllTys binders res_kind)
+                   -- the visibility of tvs doesn't matter here; we just
+                   -- want the free variables not to include the tvs
+
+          -- if there are any meta-tvs left, the user has lied about having
+          -- a CUSK. Error.
+       ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
+       ; when (not (null meta_tvs)) $
+         report_non_cusk_tvs (qkvs ++ tvs)
+
+       ; return ( map (mkNamedBinder Specified) good_tvs ++ binders
+                , res_kind, stuff ) }}
+
+  | otherwise
+  = do { kv_kinds <- mk_kv_kinds
+       ; scoped_kvs <- zipWithM newSigTyVar kv_ns kv_kinds
                      -- the names must line up in splitTelescopeTvs
-                else zipWithM newSigTyVar kv_ns meta_kvs
-       ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
-    do { (binders, res_kind, _, stuff) <- bind_telescope hs_tvs (thing_inside kvs)
-       ; let qkvs = filter (not . isMetaTyVar) $
-                    tyCoVarsOfTypeWellScoped (mkForAllTys binders res_kind)
-                      -- these have to be the vars made with new_skolem_tv
-                      -- above. Thus, they are known to the user and should
-                      -- be Specified, not Invisible, when kind-generalizing
-
-                -- the free non-meta variables in the returned kind will
-                -- contain both *mentioned* kind vars and *unmentioned* kind
-                -- vars (See case (1) under Note [Typechecking telescopes])
-             all_binders = if cusk
-                           then map (mkNamedBinder Specified) qkvs ++ binders
-                           else binders
-       ; return (all_binders, res_kind, stuff) } }
+       ; (_, binders, res_kind, stuff)
+           <- tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
+              bind_telescope hs_tvs thing_inside
+       ; return (binders, res_kind, stuff) }
   where
+      -- if -XNoTypeInType and we know all the implicits are kind vars,
+      -- just give the kind *. This prevents test
+      -- dependent/should_fail/KindLevelsB from compiling, as it should
+    mk_kv_kinds :: TcM [Kind]
+    mk_kv_kinds = do { typeintype <- xoptM LangExt.TypeInType
+                     ; if not typeintype && all_kind_vars
+                       then return (map (const liftedTypeKind) kv_ns)
+                       else mapM (const newMetaKindVar) kv_ns }
+
       -- there may be dependency between the explicit "ty" vars. So, we have
-      -- to handle them one at a time. We also produce the TyBinders here,
-      -- because this is the place we know whether to use Anon or Named.
-      -- We prefer using an anonymous binder over a trivial named
-      -- binder. If a user wants a trivial named one, use an explicit kind
-      -- signature.
+      -- to handle them one at a time.
     bind_telescope :: [LHsTyVarBndr Name]
-                   -> ([TyVar] -> TcM (Kind, r))
-                   -> TcM ([TcTyBinder], TcKind, VarSet, r)
+                   -> TcM (Kind, r)
+                   -> TcM ([TcTyVar], [TyBinder], TcKind, r)
     bind_telescope [] thing
-      = do { (res_kind, stuff) <- thing []
-           ; return ([], res_kind, tyCoVarsOfType res_kind, stuff) }
+      = do { (res_kind, stuff) <- thing
+           ; return ([], [], res_kind, stuff) }
     bind_telescope (L _ hs_tv : hs_tvs) thing
       = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
-           ; (binders, res_kind, fvs, stuff) <- bind_unless_scoped tv_pair $
-                                                bind_telescope hs_tvs $ \tvs ->
-                                                thing (tv:tvs)
-              -- we must be *lazy* in res_kind and fvs (assuming that the
-              -- caller of kcHsTyVarBndrs is, too), as sometimes these hold
-              -- panics. See kcConDecl.
-           ; k <- zonkTcType (tyVarKind tv)
-           ; let k_fvs = tyCoVarsOfType k
-                 (bndr, fvs')
-                   | tv `elemVarSet` fvs
-                   = ( mkNamedBinder Visible tv
-                     , fvs `delVarSet` tv `unionVarSet` k_fvs )
-                   | otherwise
-                   = (mkAnonBinder k, fvs `unionVarSet` k_fvs)
-
-           ; return (bndr : binders, res_kind, fvs', stuff ) }
+               -- NB: Bring all tvs into scope, even non-dependent ones,
+               -- as they're needed in type synonyms, data constructors, etc.
+           ; (tvs, binders, res_kind, stuff) <- bind_unless_scoped tv_pair $
+                                                bind_telescope hs_tvs $
+                                                thing
+                  -- See Note [Dependent LHsQTyVars]
+           ; let new_binder | hsTyVarName hs_tv `elemNameSet` dep_names
+                            = mkNamedBinder Visible tv
+                            | otherwise
+                            = mkAnonBinder (tyVarKind tv)
+           ; return ( tv : tvs
+                    , new_binder : binders
+                    , res_kind, stuff ) }
 
     -- | Bind the tyvar in the env't unless the bool is True
     bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
@@ -1242,21 +1287,41 @@ kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
       = tcExtendTyVarEnv [tv] thing_inside
 
     kc_hs_tv :: HsTyVarBndr Name -> TcM (TcTyVar, Bool)
-    kc_hs_tv hs_tvb
-      = do { (tv, scoped) <- tcHsTyVarBndr_Scoped hs_tvb
-
-              -- in the CUSK case, we want to default any un-kinded tyvars
-              -- See Note [Complete user-supplied kind signatures] in HsDecls
-           ; case hs_tvb of
-               UserTyVar {}
-                 | cusk
-                 , not scoped  -- don't default class tyvars
-                 -> discardResult $
-                    unifyKind (Just (mkTyVarTy tv)) liftedTypeKind
-                                                    (tyVarKind tv)
-               _ -> return ()
-
-           ; return (tv, scoped) }
+    kc_hs_tv (UserTyVar (L _ name))
+      = do { tv_pair@(tv, scoped) <- tcHsTyVarName name
+
+              -- Open type/data families default their variables to kind *.
+           ; when (open_fam && not scoped) $ -- (don't default class tyvars)
+             discardResult $ unifyKind (Just (mkTyVarTy tv)) liftedTypeKind
+                                                             (tyVarKind tv)
+
+           ; return tv_pair }
+
+    kc_hs_tv (KindedTyVar (L _ name) lhs_kind)
+      = do { tv_pair@(tv, _) <- tcHsTyVarName name
+           ; kind <- tcLHsKind lhs_kind
+               -- for a scoped variable: make sure annotation is consistent
+               -- for an unscoped variable: unify the meta-tyvar kind
+               -- either way: we can ignore the resulting coercion
+           ; discardResult $ unifyKind (Just (mkTyVarTy tv)) kind (tyVarKind tv)
+           ; return tv_pair }
+
+    report_non_cusk_tvs all_tvs
+      = do { all_tvs <- mapM zonkTyCoVarKind all_tvs
+           ; let (_, tidy_tvs)         = tidyOpenTyCoVars emptyTidyEnv all_tvs
+                 (meta_tvs, other_tvs) = partition isMetaTyVar tidy_tvs
+
+           ; addErr $
+             vcat [ text "You have written a *complete user-suppled kind signature*,"
+                  , hang (text "but the following variable" <> plural meta_tvs <+>
+                          isOrAre meta_tvs <+> text "undetermined:")
+                       2 (vcat (map pp_tv meta_tvs))
+                  , text "Perhaps add a kind signature."
+                  , hang (text "Inferred kinds of user-written variables:")
+                       2 (vcat (map pp_tv other_tvs)) ] }
+      where
+        pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+
 
 tcImplicitTKBndrs :: [Name]
                   -> TcM (a, TyVarSet)   -- vars are bound somewhere in the scope
@@ -1346,22 +1411,6 @@ tcHsTyVarBndr (KindedTyVar (L _ name) kind)
   = do { kind <- tcLHsKind kind
        ; return (mkTcTyVar name kind (SkolemTv False)) }
 
--- | Type-check a user-written TyVarBndr, which binds a variable
--- that might already be in scope (e.g., in an associated type declaration)
--- The second return value says whether the variable is in scope (True)
--- or not (False).
-tcHsTyVarBndr_Scoped :: HsTyVarBndr Name -> TcM (TcTyVar, Bool)
-tcHsTyVarBndr_Scoped (UserTyVar (L _ name))
-  = tcHsTyVarName name
-tcHsTyVarBndr_Scoped (KindedTyVar (L _ name) lhs_kind)
-  = do { tv_pair@(tv, _) <- tcHsTyVarName name
-       ; kind <- tcLHsKind lhs_kind
-               -- for a scoped variable: make sure annotation is consistent
-               -- for an unscoped variable: unify the meta-tyvar kind
-               -- either way: we can ignore the resulting coercion
-       ; discardResult $ unifyKind (Just (mkTyVarTy tv)) kind (tyVarKind tv)
-       ; return tv_pair }
-
 -- | Produce a tyvar of the given name (with a meta-tyvar kind). If
 -- the name is already in scope, return the scoped variable. The
 -- second return value says whether the variable is in scope (True)
@@ -1532,7 +1581,7 @@ processing necessary in the second pass.)
 Note [Tiresome kind matching]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Because of the use of SigTvs in kind inference (see #11203, for example)
-sometimes kind variables come into tcTClTyVars (the second, desugaring
+sometimes kind variables come into tcTyClTyVars (the second, desugaring
 pass in TcTyClDecls) with the wrong names. The best way to fix this up
 is just to unify the kinds, again. So we return HsKind/Kind pairs from
 splitTelescopeTvs that can get unified in tcTyClTyVars, but only if there
@@ -1714,7 +1763,8 @@ tcTyClTyVars tycon hs_tvs thing_inside
            (vcat [ text "Tycon:" <+> ppr tycon
                  , text "Binders:" <+> ppr binders
                  , text "res_kind:" <+> ppr res_kind
-                 , text "hs_tvs:" <+> ppr hs_tvs
+                 , text "hs_tvs.hsq_implicit:" <+> ppr (hsq_implicit hs_tvs)
+                 , text "hs_tvs.hsq_explicit:" <+> ppr (hsq_explicit hs_tvs)
                  , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs
                  , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs
                  , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs
index b905f53..58ff3c4 100644 (file)
@@ -1309,7 +1309,7 @@ zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
 -- unification variables.
 zonkTcTyCoVarBndr tyvar
     -- can't use isCoVar, because it looks at a TyCon. Argh.
-  = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), ppr tyvar ) do
+  = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTvBndr tyvar )
     updateTyVarKindM zonkTcType tyvar
 
 -- | Zonk a TyBinder
index 6a0daab..2b19b62 100644 (file)
@@ -285,7 +285,8 @@ kcTyClGroup (TyClGroup { group_tyclds = decls })
                -- Step 1: Bind kind variables for non-synonyms
                let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
              ; initial_kinds <- getInitialKinds non_syn_decls
-             ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
+             ; traceTc "kcTyClGroup: initial kinds" $
+               vcat (map pp_initial_kind initial_kinds)
 
              -- Step 2: Set initial envt, kind-check the synonyms
              ; lcl_env <- tcExtendKindEnv2 initial_kinds $
@@ -302,7 +303,7 @@ kcTyClGroup (TyClGroup { group_tyclds = decls })
              -- Now we have to kind generalize the flexis
         ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
 
-        ; traceTc "kcTyClGroup result" (ppr res)
+        ; traceTc "kcTyClGroup result" (vcat (map pp_res res))
         ; return res }
 
   where
@@ -316,14 +317,15 @@ kcTyClGroup (TyClGroup { group_tyclds = decls })
                  kc_res_kind = tyConResKind tc
            ; kvs <- kindGeneralize (mkForAllTys kc_binders kc_res_kind)
            ; (kc_binders', kc_res_kind') <- zonkTcKindToKind kc_binders kc_res_kind
+           ; let kc_binders'' = anonymiseTyBinders kc_binders' kc_res_kind'
 
                       -- Make sure kc_kind' has the final, zonked kind variables
            ; traceTc "Generalise kind" $
              vcat [ ppr name, ppr kc_binders, ppr kc_res_kind
-                  , ppr kvs, ppr kc_binders', ppr kc_res_kind' ]
+                  , ppr kvs, ppr kc_binders'', ppr kc_res_kind' ]
 
            ; return (mkTcTyCon name
-                               (map (mkNamedBinder Invisible) kvs ++ kc_binders')
+                               (map (mkNamedBinder Invisible) kvs ++ kc_binders'')
                                kc_res_kind'
                                (mightBeUnsaturatedTyCon tc)) }
 
@@ -348,6 +350,13 @@ kcTyClGroup (TyClGroup { group_tyclds = decls })
     generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
       = generalise kind_env name
 
+    pp_initial_kind (name, ATcTyCon tc)
+      = ppr name <+> dcolon <+> ppr (tyConKind tc)
+    pp_initial_kind pair
+      = ppr pair
+
+    pp_res tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)
+
 mkTcTyConPair :: TcTyCon -> (Name, TcTyThing)
 -- Makes a binding to put in the local envt, binding
 -- a name to a TcTyCon
@@ -393,20 +402,22 @@ getInitialKind :: TyClDecl Name
 
 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
   = do { (cl_binders, cl_kind, inner_prs) <-
-           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ ->
-           do { inner_prs <- getFamDeclInitialKinds ats
+           kcHsTyVarBndrs cusk False True ktvs $
+           do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
               ; return (constraintKind, inner_prs) }
        ; cl_binders <- mapM zonkTcTyBinder cl_binders
        ; cl_kind    <- zonkTcType cl_kind
        ; let main_pr = mkTcTyConPair (mkTcTyCon name cl_binders cl_kind True)
        ; return (main_pr : inner_prs) }
+  where
+    cusk = hsDeclHasCusk decl
 
 getInitialKind decl@(DataDecl { tcdLName = L _ name
                               , tcdTyVars = ktvs
                               , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                          , dd_cons = cons } })
   = do  { (decl_binders, decl_kind, _) <-
-           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ ->
+           kcHsTyVarBndrs (hsDeclHasCusk decl) False True ktvs $
            do { res_k <- case m_sig of
                            Just ksig -> tcLHsKind ksig
                            Nothing   -> return liftedTypeKind
@@ -419,31 +430,33 @@ getInitialKind decl@(DataDecl { tcdLName = L _ name
         ; return (main_pr : inner_prs) }
 
 getInitialKind (FamDecl { tcdFam = decl })
-  = getFamDeclInitialKind decl
+  = getFamDeclInitialKind Nothing decl
 
 getInitialKind decl@(SynDecl {})
   = pprPanic "getInitialKind" (ppr decl)
 
 ---------------------------------
-getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
-getFamDeclInitialKinds decls
+getFamDeclInitialKinds :: Maybe Bool  -- if assoc., CUSKness of assoc. class
+                       -> [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
+getFamDeclInitialKinds mb_cusk decls
   = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
                      | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
-    concatMapM (addLocM getFamDeclInitialKind) decls
+    concatMapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
 
-getFamDeclInitialKind :: FamilyDecl Name
+getFamDeclInitialKind :: Maybe Bool  -- if assoc., CUSKness of assoc. class
+                      -> FamilyDecl Name
                       -> TcM [(Name, TcTyThing)]
-getFamDeclInitialKind decl@(FamilyDecl { fdLName     = L _ name
-                                       , fdTyVars    = ktvs
-                                       , fdResultSig = L _ resultSig
-                                       , fdInfo      = info })
+getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
+                                               , fdTyVars    = ktvs
+                                               , fdResultSig = L _ resultSig
+                                               , fdInfo      = info })
   = do { (fam_binders, fam_kind, _) <-
-           kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $ \_ _ ->
+           kcHsTyVarBndrs cusk open True ktvs $
            do { res_k <- case resultSig of
                       KindSig ki                        -> tcLHsKind ki
                       TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKind ki
                       _ -- open type families have * return kind by default
-                        | famDeclHasCusk decl      -> return liftedTypeKind
+                        | open                     -> return liftedTypeKind
                         -- closed type families have their return kind inferred
                         -- by default
                         | otherwise                -> newMetaKindVar
@@ -452,10 +465,11 @@ getFamDeclInitialKind decl@(FamilyDecl { fdLName     = L _ name
        ; fam_kind    <- zonkTcType fam_kind
        ; return [ mkTcTyConPair (mkTcTyCon name fam_binders fam_kind unsat) ] }
   where
-    unsat = case info of
-      DataFamily         -> True
-      OpenTypeFamily     -> False
-      ClosedTypeFamily _ -> False
+    cusk  = famDeclHasCusk mb_cusk decl
+    (open, unsat) = case info of
+      DataFamily         -> (True,  True)
+      OpenTypeFamily     -> (True,  False)
+      ClosedTypeFamily _ -> (False, False)
 
 ----------------
 kcSynDecls :: [SCC (LTyClDecl Name)]
@@ -463,6 +477,7 @@ kcSynDecls :: [SCC (LTyClDecl Name)]
 kcSynDecls [] = getLclEnv
 kcSynDecls (group : groups)
   = do  { tc <- kcSynDecl1 group
+        ; traceTc "kcSynDecl" (ppr tc <+> dcolon <+> ppr (tyConKind tc))
         ; tcExtendKindEnv2 [ mkTcTyConPair tc ] $
           kcSynDecls groups }
 
@@ -479,7 +494,7 @@ kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
   -- Returns a possibly-unzonked kind
   = tcAddDeclCtxt decl $
     do { (syn_binders, syn_kind, _) <-
-           kcHsTyVarBndrs (hsDeclHasCusk decl) hs_tvs $ \_ _ ->
+           kcHsTyVarBndrs (hsDeclHasCusk decl) False True hs_tvs $
            do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
               ; (_, rhs_kind) <- tcLHsType rhs
               ; traceTc "kcd2" (ppr name)
@@ -548,8 +563,7 @@ kcConDecl (ConDeclH98 { con_name = name, con_qvars = 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 ((fromMaybe (HsQTvs mempty []) ex_tvs)) $
-              \ _ _ ->
+    do { _ <- kcHsTyVarBndrs False False False ((fromMaybe emptyLHsQTvs ex_tvs)) $
               do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt)
                  ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
                  ; return (panic "kcConDecl", ()) }
@@ -2075,11 +2089,28 @@ checkValidTyConTyVars tc
                    = text "NB: Implicitly declared kind variables are put first."
                    | otherwise
                    = empty
-       ; checkValidTelescope (pprTvBndrs vis_tvs) stripped_tvs extra }
+       ; checkValidTelescope (pprTvBndrs vis_tvs) stripped_tvs extra
+         `and_if_that_doesn't_error`
+           -- This triggers on test case dependent/should_fail/InferDependency
+           -- It reports errors around Note [Dependent LHsQTyVars] in TcHsType
+         addErr (vcat [ text "Invalid declaration for" <+>
+                        quotes (ppr tc) <> semi <+> text "you must explicitly"
+                      , text "declare which variables are dependent on which others."
+                      , hang (text "Inferred variable kinds:")
+                        2 (vcat (map pp_tv stripped_tvs)) ]) }
   where
     tvs = tyConTyVars tc
     duplicate_vars = sizeVarSet (mkVarSet tvs) < length tvs
 
+    pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+
+     -- only run try_second if the first reports no errors
+    and_if_that_doesn't_error :: TcM () -> TcM () -> TcM ()
+    try_first `and_if_that_doesn't_error` try_second
+      = recoverM (return ()) $
+        do { checkNoErrs try_first
+           ; try_second }
+
 -------------------------------
 checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
 checkValidDataCon dflags existential_ok tc con
index 40821e5..b3bd4ee 100644 (file)
@@ -87,6 +87,7 @@ module TcType (
   orphNamesOfTypes, orphNamesOfCoCon,
   getDFunTyKey,
   evVarPred_maybe, evVarPred,
+  anonymiseTyBinders,
 
   ---------------------------------
   -- Predicate types
@@ -222,6 +223,7 @@ import qualified GHC.LanguageExtensions as LangExt
 import Data.IORef
 import Control.Monad (liftM, ap)
 import Data.Functor.Identity
+import Data.List ( mapAccumR )
 
 {-
 ************************************************************************
@@ -2358,3 +2360,28 @@ sizeType = go
 
 sizeTypes :: [Type] -> TypeSize
 sizeTypes tys = sum (map sizeType tys)
+
+{-
+************************************************************************
+*                                                                      *
+       Binders
+*                                                                      *
+************************************************************************
+-}
+
+-- | Given a list of binders and a type they bind in, turn any
+-- superfluous Named binders into Anon ones.
+anonymiseTyBinders :: [TyBinder] -> Type -> [TyBinder]
+anonymiseTyBinders binders res_ty = binders'
+  where
+    (_, binders') = mapAccumR go (tyCoVarsOfTypeAcc res_ty) binders
+
+    go :: FV -> TyBinder -> (FV, TyBinder)
+    go fv (Named tv Visible)
+      | not (tv `elemVarSet` runFVSet fv)
+      = ( (tv `FV.delFV` fv) `unionFV` tyCoVarsOfTypeAcc kind
+        , Anon kind )
+      where
+        kind = tyVarKind tv
+
+    go fv binder = (tyCoVarsBndrAcc binder fv, binder)
index 99a9be3..868524f 100644 (file)
@@ -1712,7 +1712,7 @@ tcImplicitTKBndrs.
 checkValidTelescope :: SDoc        -- the original user-written telescope
                     -> [TyVar]     -- explicit vars (not necessarily zonked)
                     -> SDoc        -- note to put at bottom of message
-                    -> TcM ()      -- returns zonked tyvars
+                    -> TcM ()
 checkValidTelescope hs_tvs orig_tvs extra
   = discardResult $ checkZonkValidTelescope hs_tvs orig_tvs extra
 
index b42eb80..8295009 100644 (file)
@@ -7244,8 +7244,8 @@ kind-polymorphic, but not so ``D2``; and similarly ``F1``, ``F1``.
 
 .. _complete-kind-signatures:
 
-Polymorphic kind recursion and complete kind signatures
--------------------------------------------------------
+Complete user-supplied kind signatures and polymorphic recursion
+----------------------------------------------------------------
 
 Just as in type inference, kind inference for recursive types can only
 use *monomorphic* recursion. Consider this (contrived) example: ::
@@ -7294,6 +7294,18 @@ signature" for a type constructor? These are the forms:
        data T6 a b                         where ...
        -- No;  kind is inferred
 
+-  For a datatype with a top-level ``::`` when :ghc-flag:`-XTypeInType`
+   is in effect: all kind variables introduced after the ``::`` must
+   be explicitly quantified. ::
+
+     -- -XTypeInType is on
+     data T1 :: k -> *            -- No CUSK: `k` is not explicitly quantified
+     data T2 :: forall k. k -> *  -- CUSK: `k` is bound explicitly
+     data T3 :: forall (k :: *). k -> *   -- still a CUSK
+
+   Note that the first example would indeed have a CUSK without
+   :ghc-flag:`-XTypeInType`.
+
 -  For a class, every type variable must be annotated with a kind.
 
 -  For a type synonym, every type variable and the result type must all
@@ -7307,7 +7319,7 @@ signature" for a type constructor? These are the forms:
    rather apparent, but it is still not considered to have a complete
    signature -- no inference can be done before detecting the signature.
 
--  An open type or data family declaration *always* has a CUSK;
+-  An un-associated open type or data family declaration *always* has a CUSK;
    un-annotated type variables default to
    kind ``*``: ::
 
@@ -7316,13 +7328,14 @@ signature" for a type constructor? These are the forms:
        data family D3 (a :: k) :: *   -- D3 :: forall k. k -> *
        type family S1 a :: k -> *     -- S1 :: forall k. * -> k -> *
 
-       class C a where                -- C  :: k -> Constraint
-         type AT a b                  -- AT :: k -> * -> *
+-  An associated type or data family declaration has a CUSK precisely if
+   its enclosing class has a CUSK. ::
+       
+       class C a where                -- no CUSK
+         type AT a b                  -- no CUSK, b is defaulted
 
-   In the last example, the variable ``a`` has an implicit kind variable
-   annotation from the class declaration. It keeps its polymorphic kind
-   in the associated type declaration. The variable ``b``, however, gets
-   defaulted to ``*``.
+       class D (a :: k) where         -- yes CUSK
+         type AT2 a b                 -- yes CUSK, b is defaulted
 
 -  A closed type family has a complete signature when all of its type
    variables are annotated and a return kind (with a top-level ``::``)
@@ -7542,6 +7555,37 @@ If you like neither of these names, feel free to write your own synonym: ::
 All the affordances for ``*`` also apply to ``★``, the Unicode variant
 of ``*``.
 
+Inferring dependency in datatype declarations
+---------------------------------------------
+
+If a type variable ``a`` in a datatype, class, or type family declaration
+depends on another such variable ``k`` in the same declaration, two properties
+must hold:
+
+-  ``a`` must appear after ``k`` in the declaration, and
+
+-  ``k`` must appear explicitly in the kind of *some* type variable in that
+   declaration.
+
+The first bullet simply means that the dependency must be well-scoped. The
+second bullet concerns GHC's ability to infer dependency. Inferring this
+dependency is difficult, and GHC currently requires the dependency to be
+made explicit, meaning that ``k`` must appear in the kind of a type variable,
+making it obvious to GHC that dependency is intended. For example: ::
+
+  data Proxy k (a :: k)            -- OK: dependency is "obvious"
+  data Proxy2 k a = P (Proxy k a)  -- ERROR: dependency is unclear
+
+In the second declaration, GHC cannot immediately tell that ``k`` should
+be a dependent variable, and so the declaration is rejected.
+
+It is conceivable that this restriction will be relaxed in the future,
+but it is (at the time of writing) unclear if the difficulties around this
+scenario are theoretical (inferring this dependency would mean our type
+system does not have principal types) or merely practical (inferring this
+dependency is hard, given GHC's implementation). So, GHC takes the easy
+way out and requires a little help from the user.
+
 Kind defaulting without :ghc-flag:`-XPolyKinds`
 -----------------------------------------------
 
index 8076297..1aad299 100644 (file)
@@ -1,7 +1,9 @@
-{-# LANGUAGE DataKinds, PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
 
 module KindLevels where
 
+import Data.Kind
+
 data A
 data B :: A -> *
 data C :: B a -> *
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.hs b/testsuite/tests/dependent/should_fail/InferDependency.hs
new file mode 100644 (file)
index 0000000..47957d4
--- /dev/null
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeInType #-}
+
+module InferDependency where
+
+data Proxy k (a :: k)
+data Proxy2 k a = P (Proxy k a)
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.stderr b/testsuite/tests/dependent/should_fail/InferDependency.stderr
new file mode 100644 (file)
index 0000000..7fa900a
--- /dev/null
@@ -0,0 +1,8 @@
+
+InferDependency.hs:6:1: error:
+    • Invalid declaration for ‘Proxy2’; you must explicitly
+      declare which variables are dependent on which others.
+      Inferred variable kinds:
+        k :: *
+        a :: k
+    • In the data type declaration for ‘Proxy2’
diff --git a/testsuite/tests/dependent/should_fail/KindLevelsB.hs b/testsuite/tests/dependent/should_fail/KindLevelsB.hs
new file mode 100644 (file)
index 0000000..8076297
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds, PolyKinds #-}
+
+module KindLevels where
+
+data A
+data B :: A -> *
+data C :: B a -> *
+data D :: C b -> *
+data E :: D c -> *
diff --git a/testsuite/tests/dependent/should_fail/KindLevelsB.stderr b/testsuite/tests/dependent/should_fail/KindLevelsB.stderr
new file mode 100644 (file)
index 0000000..587eb97
--- /dev/null
@@ -0,0 +1,5 @@
+
+KindLevelsB.hs:7:13: error:
+    • Expected kind ‘A’, but ‘a’ has kind ‘*’
+    • In the first argument of ‘B’, namely ‘a’
+      In the kind ‘B a -> *’
index 63f08d2..a90b7bb 100644 (file)
@@ -10,3 +10,5 @@ test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334', normal, compile_fail, [''])
+test('InferDependency', normal, compile_fail, [''])
+test('KindLevelsB', normal, compile_fail, [''])
diff --git a/testsuite/tests/polykinds/T11648.hs b/testsuite/tests/polykinds/T11648.hs
new file mode 100644 (file)
index 0000000..15fcfa4
--- /dev/null
@@ -0,0 +1,8 @@
+{-# LANGUAGE PolyKinds, TypeOperators, TypeFamilies,
+             MultiParamTypeClasses #-}
+
+module T11648 where
+
+class Monoidy (to :: k0 -> k1 -> *) (m :: k1)  where
+  type MComp to m :: k1 -> k1 -> k0
+  mjoin :: MComp to m m m `to` m
diff --git a/testsuite/tests/polykinds/T11648b.hs b/testsuite/tests/polykinds/T11648b.hs
new file mode 100644 (file)
index 0000000..2ab27a6
--- /dev/null
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeInType #-}
+
+module T11648b where
+
+import Data.Proxy
+
+data X (a :: Proxy k)
diff --git a/testsuite/tests/polykinds/T11648b.stderr b/testsuite/tests/polykinds/T11648b.stderr
new file mode 100644 (file)
index 0000000..e709e00
--- /dev/null
@@ -0,0 +1,8 @@
+
+T11648b.hs:7:1: error:
+    You have written a *complete user-suppled kind signature*,
+    but the following variable is undetermined: k0 :: *
+    Perhaps add a kind signature.
+    Inferred kinds of user-written variables:
+      k :: k0
+      a :: Proxy k
diff --git a/testsuite/tests/polykinds/T6039.stderr b/testsuite/tests/polykinds/T6039.stderr
new file mode 100644 (file)
index 0000000..2ad2935
--- /dev/null
@@ -0,0 +1,5 @@
+
+T6039.hs:5:14: error:
+    • Expecting one fewer argument to ‘j’
+      Expected kind ‘* -> *’, but ‘j’ has kind ‘*’
+    • In the kind ‘j k’
index d48d108..45981e9 100644 (file)
@@ -37,7 +37,7 @@ test('T6035', normal, compile, [''])
 test('T6036', normal, compile, [''])
 test('T6025', normal, run_command, ['$MAKE -s --no-print-directory T6025'])
 test('T6002', normal, compile, [''])
-test('T6039', normal, compile, [''])
+test('T6039', normal, compile_fail, [''])
 test('T6021', normal, compile_fail, [''])
 test('T6020a', normal, compile, [''])
 test('T6044', normal, compile, [''])
@@ -143,3 +143,5 @@ test('T11362', normal, compile, ['-dunique-increment=-1'])
   # -dunique-increment=-1 doesn't work inside the file
 test('T11399', normal, compile_fail, [''])
 test('T11611', normal, compile_fail, [''])
+test('T11648', normal, compile, [''])
+test('T11648b', normal, compile_fail, [''])
index ab95426..bb994de 160000 (submodule)
@@ -1 +1 @@
-Subproject commit ab954263a793d8ced734459d6194a5d89214b66c
+Subproject commit bb994de1ab0c76d1aaf1e39c54158db2526d31f1