Commit 55577a91 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix #11648.

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]
parent e7a8cb14
......@@ -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 }
......
......@@ -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)
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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]
......
......@@ -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.
......
......@@ -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 }