diff options
Diffstat (limited to 'compiler/typecheck/TcHsType.hs')
| -rw-r--r-- | compiler/typecheck/TcHsType.hs | 2078 |
1 files changed, 1201 insertions, 877 deletions
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 2b671463cd..9fd74d1fa6 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -5,55 +5,55 @@ \section[TcMonoType]{Typechecking user-specified @MonoTypes@} -} -{-# LANGUAGE CPP #-} +{-# LANGUAGE CPP, TupleSections, MultiWayIf #-} module TcHsType ( -- Type signatures kcHsSigType, tcClassSigType, tcHsSigType, tcHsSigWcType, - zonkSigType, zonkAndCheckValidity, funsSigCtxt, addSigCtxt, tcHsClsInstType, tcHsDeriv, tcHsVectInst, UserTypeCtxt(..), - tcImplicitTKBndrs, tcHsTyVarBndrs, + tcImplicitTKBndrs, tcImplicitTKBndrsType, tcHsTyVarBndrs, - -- Type checking type and class decls + -- Type checking type and class decls kcLookupKind, kcTyClTyVars, tcTyClTyVars, tcHsConArgType, tcDataKindSig, -- Kind-checking types -- No kind generalisation, no checkValidType tcWildCardBinders, - kcHsTyVarBndrs, tcHsQTyVars, + kcHsTyVarBndrs, tcHsLiftedType, tcHsOpenType, tcHsLiftedTypeNC, tcHsOpenTypeNC, tcLHsType, tcCheckLHsType, - tcHsContext, tcLHsPredType, tcInferApps, tcHsArgTys, + tcHsContext, tcLHsPredType, tcInferApps, tcInferArgs, + solveEqualities, -- useful re-export - kindGeneralize, checkKind, + kindGeneralize, -- Sort-checking kinds tcLHsKind, -- Pattern type signatures - tcHsPatSigType, tcPatSig + tcHsPatSigType, tcPatSig, funAppCtxt ) where #include "HsVersions.h" import HsSyn import TcRnMonad -import TcEvidence( HsWrapper ) +import TcEvidence import TcEnv import TcMType import TcValidity import TcUnify import TcIface +import TcSimplify ( solveEqualities ) import TcType import Type -import TypeRep( Type(..) ) -- For the mkNakedXXX stuff import Kind import RdrName( lookupLocalRdrOcc ) import Var @@ -61,72 +61,51 @@ import VarSet import TyCon import ConLike import DataCon -import TysPrim ( liftedTypeKindTyConName, constraintKindTyConName ) +import TysPrim ( tYPE ) import Class import Name import NameEnv +import NameSet +import VarEnv import TysWiredIn import BasicTypes import SrcLoc -import DynFlags ( ExtensionFlag( Opt_DataKinds ), getDynFlags ) +import DynFlags ( ExtensionFlag( Opt_DataKinds, Opt_MonoLocalBinds + , Opt_TypeInType ) ) import Constants ( mAX_CTUPLE_SIZE ) import ErrUtils( MsgDoc ) import Unique +import Util import UniqSupply import Outputable import FastString -import Util +import PrelNames hiding ( wildCardName ) +import Pair -import Data.Maybe( isNothing ) -import Control.Monad ( unless, when, zipWithM, void ) -import PrelNames( funTyConKey, allNameStrings ) +import Data.Maybe +import Control.Monad {- ---------------------------- General notes ---------------------------- -Generally speaking we now type-check types in three phases - - 1. kcHsType: kind check the HsType - *includes* performing any TH type splices; - so it returns a translated, and kind-annotated, type - - 2. dsHsType: convert from HsType to Type: - perform zonking - expand type synonyms [mkGenTyApps] - hoist the foralls [tcHsType] - - 3. checkValidType: check the validity of the resulting type - -Often these steps are done one after the other (tcHsSigType). -But in mutually recursive groups of type and class decls we do - 1 kind-check the whole group - 2 build TyCons/Classes in a knot-tied way - 3 check the validity of types in the now-unknotted TyCons/Classes - -For example, when we find - (forall a m. m a -> m a) -we bind a,m to kind varibles and kind-check (m a -> m a). This makes -a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in -an environment that binds a and m suitably. +Unlike with expressions, type-checking types both does some checking and +desugars at the same time. This is necessary because we often want to perform +equality checks on the types right away, and it would be incredibly painful +to do this on un-desugared types. Luckily, desugared types are close enough +to HsTypes to make the error messages sane. -The kind checker passed to tcHsTyVars needs to look at enough to -establish the kind of the tyvar: - * For a group of type and class decls, it's just the group, not - the rest of the program - * For a tyvar bound in a pattern type signature, its the types - mentioned in the other type signatures in that bunch of patterns - * For a tyvar bound in a RULE, it's the type signatures on other - universally quantified variables in the rule - -Note that this may occasionally give surprising results. For example: - - data T a b = MkT (a b) - -Here we deduce a::*->*, b::* -But equally valid would be a::(*->*)-> *, b::*->* +During type-checking, we perform as little validity checking as possible. +This is because some type-checking is done in a mutually-recursive knot, and +if we look too closely at the tycons, we'll loop. This is why we always must +use mkNakedTyConApp and mkNakedAppTys, etc., which never look at a tycon. +The mkNamed... functions don't uphold Type invariants, but zonkTcTypeToType +will repair this for us. Note that zonkTcType *is* safe within a knot, and +can be done repeatedly with no ill effect: it just squeezes out metavariables. +Generally, after type-checking, you will want to do validity checking, say +with TcValidity.checkValidType. Validity checking ~~~~~~~~~~~~~~~~~ @@ -157,9 +136,8 @@ During step (1) we might fault in a TyCon defined in another module, and it migh knot around type declarations with ARecThing, so that the fault-in code can get the TyCon being defined. - -************************************************************************ -* * +%************************************************************************ +%* * Check types AND do validity checking * * ************************************************************************ @@ -185,48 +163,46 @@ tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty) kcHsSigType :: [Located Name] -> LHsSigType Name -> TcM () kcHsSigType names (HsIB { hsib_body = hs_ty - , hsib_kvs = sig_kvs - , hsib_tvs = sig_tvs }) + , hsib_vars = sig_vars }) = addSigCtxt (funsSigCtxt names) hs_ty $ - do { tcImplicitTKBndrs sig_kvs sig_tvs $ \ _ _ -> - void $ tc_check_lhs_type hs_ty liftedTypeKind } + discardResult $ + tcImplicitTKBndrsType sig_vars $ + tc_lhs_type typeLevelMode hs_ty liftedTypeKind tcClassSigType :: [Located Name] -> LHsSigType Name -> TcM Type -- Does not do validity checking; this must be done outside -- the recursive class declaration "knot" tcClassSigType names sig_ty = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $ - tc_hs_sig_type sig_ty liftedTypeKind + do { ty <- tc_hs_sig_type sig_ty liftedTypeKind + ; kindGeneralizeType ty } tcHsSigType :: UserTypeCtxt -> LHsSigType Name -> TcM Type -- Does validity checking tcHsSigType ctxt sig_ty = addSigCtxt ctxt (hsSigType sig_ty) $ do { kind <- case expectedKindInCtxt ctxt of - Nothing -> newMetaKindVar - Just k -> return k + AnythingKind -> newMetaKindVar + TheKind k -> return k + OpenKind -> do { lev <- newFlexiTyVarTy levityTy + ; return $ tYPE lev } -- The kind is checked by checkValidType, and isn't necessarily -- of kind * in a Template Haskell quote eg [t| Maybe |] ; ty <- tc_hs_sig_type sig_ty kind + -- Generalise here: see Note [Kind generalisation] + ; ty <- maybeKindGeneralizeType ty -- also zonks ; checkValidType ctxt ty ; return ty } tc_hs_sig_type :: LHsSigType Name -> Kind -> TcM Type --- Does not do validity checking +-- Does not do validity checking or zonking tc_hs_sig_type (HsIB { hsib_body = hs_ty - , hsib_kvs = sig_kvs - , hsib_tvs = sig_tvs }) kind - = do { ty <- tcImplicitTKBndrs sig_kvs sig_tvs $ \ kvs tvs -> - do { ty <- tc_check_lhs_type hs_ty kind - ; return (mkForAllTys kvs $ mkForAllTys tvs ty) } - - -- Generalise here: see Note [Kind generalisation] - ; ty <- kindGeneralizeType ty - - -- Zonk to expose kind information to checkValidType - ; zonkSigType ty } - + , hsib_vars = sig_vars }) kind + = do { (tkvs, ty) <- solveEqualities $ + tcImplicitTKBndrsType sig_vars $ + tc_lhs_type typeLevelMode hs_ty kind + ; return (mkInvForAllTys tkvs ty) } ----------------- tcHsDeriv :: LHsSigType Name -> TcM ([TyVar], Class, [Type], Kind) @@ -239,8 +215,13 @@ tcHsDeriv :: LHsSigType Name -> TcM ([TyVar], Class, [Type], Kind) -- if arg has a suitable kind tcHsDeriv hs_ty = do { arg_kind <- newMetaKindVar - ; ty <- tc_hs_sig_type hs_ty (mkArrowKind arg_kind constraintKind) - ; arg_kind <- zonkSigType arg_kind + -- always safe to kind-generalize, because there + -- can be no covars in an outer scope + ; ty <- checkNoErrs $ + -- avoid redundant error report with "illegal deriving", below + tc_hs_sig_type hs_ty (mkFunTy arg_kind constraintKind) + ; ty <- kindGeneralizeType ty -- also zonks + ; arg_kind <- zonkTcType arg_kind ; let (tvs, pred) = splitForAllTys ty ; case getClassPredTys_maybe pred of Just (cls, tys) -> return (tvs, cls, tys, arg_kind) @@ -252,30 +233,37 @@ tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt -- Like tcHsSigType, but for a class instance declaration -- The significant difference is that we expect a /constraint/ -- not a /type/ for the bit after the '=>'. -tcHsClsInstType user_ctxt hs_inst_ty@(HsIB { hsib_kvs = sig_kvs, hsib_tvs = sig_tvs +tcHsClsInstType user_ctxt hs_inst_ty@(HsIB { hsib_vars = sig_vars , hsib_body = hs_qual_ty }) - | (cxt, head_ty) <- splitLHsQualTy hs_qual_ty -- An explicit forall in an instance declaration isn't -- allowed, so there won't be any HsForAllTy here = setSrcSpan (getLoc hs_qual_ty) $ - do { inst_ty <- tcImplicitTKBndrs sig_kvs sig_tvs $ \ kvs tvs -> + do { (tkvs, phi_ty) <- solveEqualities $ + tcImplicitTKBndrsType sig_vars $ do { theta <- tcHsContext cxt - ; head_ty' <- tc_check_lhs_type head_ty constraintKind - ; return (mkForAllTys kvs $ mkForAllTys tvs $ - mkPhiTy theta head_ty') } + ; head_ty' <- tc_lhs_type typeLevelMode + head_ty constraintKind + ; return (mkPhiTy theta head_ty') } + ; let inst_ty = mkInvForAllTys tkvs phi_ty ; inst_ty <- kindGeneralizeType inst_ty - ; inst_ty <- zonkSigType inst_ty + ; inst_ty <- zonkTcType inst_ty ; checkValidInstance user_ctxt hs_inst_ty inst_ty } + where + (cxt, head_ty) = splitLHsQualTy hs_qual_ty -- Used for 'VECTORISE [SCALAR] instance' declarations -- tcHsVectInst :: LHsSigType Name -> TcM (Class, [Type]) tcHsVectInst ty - | Just (L _ cls_name, tys) <- splitLHsClassTy_maybe (hsSigType ty) + | Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe (hsSigType ty) -- Ignoring the binders looks pretty dodgy to me = do { (cls, cls_kind) <- tcClass cls_name - ; (arg_tys, _res_kind) <- tcInferApps cls_name cls_kind tys - ; return (cls, arg_tys) } + ; (applied_class, _res_kind) + <- tcInferApps typeLevelMode cls_name (mkClassPred cls []) cls_kind tys + ; case tcSplitTyConApp_maybe applied_class of + Just (_tc, args) -> ASSERT( _tc == classTyCon cls ) + return (cls, args) + _ -> failWithTc (text "Too many arguments passed to" <+> ppr cls_name) } | otherwise = failWithTc $ ptext (sLit "Malformed instance type") @@ -288,8 +276,8 @@ tcHsVectInst ty ************************************************************************ * * The main kind checker: no validity checks here -* * -************************************************************************ +%* * +%************************************************************************ First a couple of simple wrappers for kcHsType -} @@ -306,19 +294,6 @@ tcHsConArgType DataType bty = tcHsOpenType (getBangType bty) -- And newtypes can't be bang'd --------------------------- -tcHsArgTys :: SDoc -> [LHsType Name] -> [Kind] -> TcM [TcType] -tcHsArgTys what tys kinds - = sequence [ addTypeCtxt ty $ - tc_lhs_type ty (expArgKind what kind n) - | (ty,kind,n) <- zip3 tys kinds [1..] ] - -tc_hs_arg_tys :: SDoc -> [LHsType Name] -> [Kind] -> TcM [TcType] --- Just like tcHsArgTys but without the addTypeCtxt -tc_hs_arg_tys what tys kinds - = sequence [ tc_lhs_type ty (expArgKind what kind n) - | (ty,kind,n) <- zip3 tys kinds [1..] ] - ---------------------------- tcHsOpenType, tcHsLiftedType, tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType Name -> TcM TcType -- Used for type signatures @@ -326,153 +301,249 @@ tcHsOpenType, tcHsLiftedType, tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty -tcHsOpenTypeNC ty = tc_lhs_type ty ekOpen -tcHsLiftedTypeNC ty = tc_lhs_type ty ekLifted +tcHsOpenTypeNC ty = do { ek <- ekOpen + ; tc_lhs_type typeLevelMode ty ek } +tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind -- Like tcHsType, but takes an expected kind tcCheckLHsType :: LHsType Name -> Kind -> TcM Type tcCheckLHsType hs_ty exp_kind = addTypeCtxt hs_ty $ - tc_check_lhs_type hs_ty exp_kind - -tc_check_lhs_type :: LHsType Name -> Kind -> TcM Type -tc_check_lhs_type hs_ty exp_kind - = tc_lhs_type hs_ty (EK exp_kind expectedKindMsg) + tc_lhs_type typeLevelMode hs_ty exp_kind tcLHsType :: LHsType Name -> TcM (TcType, TcKind) -- Called from outside: set the context -tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type ty) +tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty) --------------------------- +-- | Should we generalise the kind of this type? +-- We *should* generalise if the type is mentions no scoped type variables +-- or if NoMonoLocalBinds is set. Otherwise, nope. +decideKindGeneralisationPlan :: Type -> TcM Bool +decideKindGeneralisationPlan ty + = do { mono_locals <- xoptM Opt_MonoLocalBinds + ; in_scope <- getInLocalScope + ; let fvs = tyCoVarsOfTypeList ty + should_gen = not mono_locals || all (not . in_scope . getName) fvs + ; traceTc "decideKindGeneralisationPlan" + (vcat [ text "type:" <+> ppr ty + , text "ftvs:" <+> ppr fvs + , text "should gen?" <+> ppr should_gen ]) + ; return should_gen } + +maybeKindGeneralizeType :: TcType -> TcM Type +maybeKindGeneralizeType ty + = do { should_gen <- decideKindGeneralisationPlan ty + ; if should_gen + then kindGeneralizeType ty + else zonkTcType ty } + {- -Like tcExpr, tc_hs_type takes an expected kind which it unifies with -the kind it figures out. When we don't know what kind to expect, we use -tc_lhs_type_fresh, to first create a new meta kind variable and use that as -the expected kind. +************************************************************************ +* * + Type-checking modes +* * +************************************************************************ + +The kind-checker is parameterised by a TcTyMode, which contains some +information about where we're checking a type. + +The renamer issues errors about what it can. All errors issued here must +concern things that the renamer can't handle. + -} -tc_infer_lhs_type :: LHsType Name -> TcM (TcType, TcKind) -tc_infer_lhs_type ty = - do { kv <- newMetaKindVar - ; r <- tc_lhs_type ty (EK kv expectedKindMsg) - ; return (r, kv) } +data TcTyMode + = TcTyMode { mode_level :: TypeOrKind -- True <=> type, False <=> kind + -- used only for -XNoTypeInType errors + } + +typeLevelMode :: TcTyMode +typeLevelMode = TcTyMode { mode_level = TypeLevel } + +kindLevelMode :: TcTyMode +kindLevelMode = TcTyMode { mode_level = KindLevel } + +-- switch to kind level +kindLevel :: TcTyMode -> TcTyMode +kindLevel mode = mode { mode_level = KindLevel } + +{- +Note [Bidirectional type checking] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In expressions, whenever we see a polymorphic identifier, say `id`, we are +free to instantiate it with metavariables, knowing that we can always +re-generalize with type-lambdas when necessary. For example: + + rank2 :: (forall a. a -> a) -> () + x = rank2 id + +When checking the body of `x`, we can instantiate `id` with a metavariable. +Then, when we're checking the application of `rank2`, we notice that we really +need a polymorphic `id`, and then re-generalize over the unconstrained +metavariable. + +In types, however, we're not so lucky, because *we cannot re-generalize*! +There is no lambda. So, we must be careful only to instantiate at the last +possible moment, when we're sure we're never going to want the lost polymorphism +again. This is done in calls to tcInstBinders and tcInstBindersX. + +To implement this behavior, we use bidirectional type checking, where we +explicitly think about whether we know the kind of the type we're checking +or not. Note that there is a difference between not knowing a kind and +knowing a metavariable kind: the metavariables are TauTvs, and cannot become +forall-quantified kinds. Previously (before dependent types), there were +no higher-rank kinds, and so we could instantiate early and be sure that +no types would have polymorphic kinds, and so we could always assume that +the kind of a type was a fresh metavariable. Not so anymore, thus the +need for two algorithms. + +For HsType forms that can never be kind-polymorphic, we implement only the +"down" direction, where we safely assume a metavariable kind. For HsType forms +that *can* be kind-polymorphic, we implement just the "up" (functions with +"infer" in their name) version, as we gain nothing by also implementing the +"down" version. + +Note [Future-proofing the type checker] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +As discussed in Note [Bidirectional type checking], each HsType form is +handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions +are mutually recursive, so that either one can work for any type former. +But, we want to make sure that our pattern-matches are complete. So, +we have a bunch of repetitive code just so that we get warnings if we're +missing any patterns. +-} -tc_lhs_type :: LHsType Name -> ExpKind -> TcM TcType -tc_lhs_type (L span ty) exp_kind +-- | Check and desugar a type, returning the core type and its +-- possibly-polymorphic kind. Much like 'tcInferRho' at the expression +-- level. +tc_infer_lhs_type :: TcTyMode -> LHsType Name -> TcM (TcType, TcKind) +tc_infer_lhs_type mode (L span ty) + = setSrcSpan span $ + do { traceTc "tc_infer_lhs_type:" (ppr ty) + ; tc_infer_hs_type mode ty } + +-- | Infer the kind of a type and desugar. This is the "up" type-checker, +-- as described in Note [Bidirectional type checking] +tc_infer_hs_type :: TcTyMode -> HsType Name -> TcM (TcType, TcKind) +tc_infer_hs_type mode (HsTyVar (L _ tv)) = tcTyVar mode tv +tc_infer_hs_type mode (HsAppTy ty1 ty2) + = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2] + ; (fun_ty', fun_kind) <- tc_infer_lhs_type mode fun_ty + ; fun_kind' <- zonkTcType fun_kind + ; tcInferApps mode fun_ty fun_ty' fun_kind' arg_tys } +tc_infer_hs_type mode (HsParTy t) = tc_infer_lhs_type mode t +tc_infer_hs_type mode (HsOpTy lhs (L _ op) rhs) + | not (op `hasKey` funTyConKey) + = do { (op', op_kind) <- tcTyVar mode op + ; op_kind' <- zonkTcType op_kind + ; tcInferApps mode op op' op_kind' [lhs, rhs] } +tc_infer_hs_type mode (HsKindSig ty sig) + = do { sig' <- tc_lhs_kind (kindLevel mode) sig + ; ty' <- tc_lhs_type mode ty sig' + ; return (ty', sig') } +tc_infer_hs_type mode (HsDocTy ty _) = tc_infer_lhs_type mode ty +tc_infer_hs_type _ (HsCoreTy ty) = return (ty, typeKind ty) +tc_infer_hs_type mode other_ty + = do { kv <- newMetaKindVar + ; ty' <- tc_hs_type mode other_ty kv + ; return (ty', kv) } + +tc_lhs_type :: TcTyMode -> LHsType Name -> TcKind -> TcM TcType +tc_lhs_type mode (L span ty) exp_kind = setSrcSpan span $ do { traceTc "tc_lhs_type:" (ppr ty $$ ppr exp_kind) - ; tc_hs_type ty exp_kind } - -tc_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [TcType] -tc_lhs_types tys_w_kinds = mapM (uncurry tc_lhs_type) tys_w_kinds + ; tc_hs_type mode ty exp_kind } ------------------------------------------ -tc_fun_type :: HsType Name -> LHsType Name -> LHsType Name -> ExpKind -> TcM TcType --- We need to recognise (->) so that we can construct a FunTy, --- *and* we need to do by looking at the Name, not the TyCon --- (see Note [Zonking inside the knot]). For example, --- consider f :: (->) Int Int (Trac #7312) -tc_fun_type ty ty1 ty2 exp_kind@(EK _ ctxt) - = do { ty1' <- tc_lhs_type ty1 (EK openTypeKind ctxt) - ; ty2' <- tc_lhs_type ty2 (EK openTypeKind ctxt) - ; checkExpectedKind ty liftedTypeKind exp_kind - ; return (mkFunTy ty1' ty2') } +tc_fun_type :: TcTyMode -> LHsType Name -> LHsType Name -> TcKind -> TcM TcType +tc_fun_type mode ty1 ty2 exp_kind + = do { arg_lev <- newFlexiTyVarTy levityTy + ; res_lev <- newFlexiTyVarTy levityTy + ; ty1' <- tc_lhs_type mode ty1 (tYPE arg_lev) + ; ty2' <- tc_lhs_type mode ty2 (tYPE res_lev) + ; checkExpectedKind (mkNakedFunTy ty1' ty2') liftedTypeKind exp_kind } ------------------------------------------ -tc_hs_type :: HsType Name -> ExpKind -> TcM TcType -tc_hs_type (HsParTy ty) exp_kind = tc_lhs_type ty exp_kind -tc_hs_type (HsDocTy ty _) exp_kind = tc_lhs_type ty exp_kind -tc_hs_type ty@(HsBangTy {}) _ +-- See also Note [Bidirectional type checking] +tc_hs_type :: TcTyMode -> HsType Name -> TcKind -> TcM TcType +tc_hs_type mode (HsParTy ty) exp_kind = tc_lhs_type mode ty exp_kind +tc_hs_type mode (HsDocTy ty _) exp_kind = tc_lhs_type mode ty exp_kind +tc_hs_type _ ty@(HsBangTy {}) _ -- While top-level bangs at this point are eliminated (eg !(Maybe Int)), -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of -- bangs are invalid, so fail. (#7210) = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty) -tc_hs_type ty@(HsRecTy _) _ +tc_hs_type _ ty@(HsRecTy _) _ -- Record types (which only show up temporarily in constructor -- signatures) should have been removed by now = failWithTc (ptext (sLit "Record syntax is illegal here:") <+> ppr ty) ----------- Functions and applications -tc_hs_type hs_ty@(HsTyVar (L _ name)) exp_kind - = do { (ty, k) <- tcTyVar name - ; checkExpectedKind hs_ty k exp_kind - ; return ty } +-- This should never happen; type splices are expanded by the renamer +tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind + = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty) -tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind - = tc_fun_type ty ty1 ty2 exp_kind +---------- Functions and applications +tc_hs_type mode (HsFunTy ty1 ty2) exp_kind + = tc_fun_type mode ty1 ty2 exp_kind -tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind +tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind | op `hasKey` funTyConKey - = tc_fun_type hs_ty ty1 ty2 exp_kind - | otherwise - = do { (op', op_kind) <- tcTyVar op - ; tys' <- tcCheckApps hs_ty l_op op_kind [ty1,ty2] exp_kind - ; return (mkNakedAppTys op' tys') } - -- mkNakedAppTys: see Note [Zonking inside the knot] - -tc_hs_type hs_ty@(HsAppTy ty1 ty2) exp_kind --- | L _ (HsTyVar fun) <- fun_ty --- , fun `hasKey` funTyConKey --- , [fty1,fty2] <- arg_tys --- = tc_fun_type hs_ty fty1 fty2 exp_kind --- | otherwise - = do { (fun_ty', fun_kind) <- tc_infer_lhs_type fun_ty - ; arg_tys' <- tcCheckApps hs_ty fun_ty fun_kind arg_tys exp_kind - ; return (mkNakedAppTys fun_ty' arg_tys') } - -- mkNakedAppTys: see Note [Zonking inside the knot] - -- This looks fragile; how do we *know* that fun_ty isn't - -- a TyConApp, say (which is never supposed to appear in the - -- function position of an AppTy)? - where - (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2] + = tc_fun_type mode ty1 ty2 exp_kind --------- Foralls -tc_hs_type hs_ty@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind@(EK exp_k _) - | isConstraintKind exp_k +tc_hs_type mode hs_ty@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind + -- Do not kind-generalise here. See Note [Kind generalisation] + | isConstraintKind exp_kind = failWithTc (hang (ptext (sLit "Illegal constraint:")) 2 (ppr hs_ty)) | otherwise - = tcHsTyVarBndrs hs_tvs $ \ tvs' -> + = fmap fst $ + tcHsTyVarBndrs hs_tvs $ \ tvs' -> -- Do not kind-generalise here! See Note [Kind generalisation] - do { ty' <- tc_lhs_type ty exp_kind - ; return (mkForAllTys tvs' ty') } + -- Why exp_kind? See Note [Body kind of forall] + do { ty' <- tc_lhs_type mode ty exp_kind + ; let bound_vars = allBoundVariables ty' + ; return (mkNakedInvSigmaTy tvs' [] ty', bound_vars) } -tc_hs_type hs_ty@(HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind - = do { ctxt' <- tcHsContext ctxt +tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind + = do { ctxt' <- tc_hs_context mode ctxt ; ty' <- if null (unLoc ctxt) then -- Plain forall, no context - tc_lhs_type ty exp_kind -- Why exp_kind? See Note [Body kind of forall] + tc_lhs_type mode ty exp_kind + -- Why exp_kind? See Note [Body kind of forall] else -- If there is a context, then this forall is really a -- _function_, so the kind of the result really is * -- The body kind (result of the function) can be * or #, hence ekOpen - do { checkExpectedKind hs_ty liftedTypeKind exp_kind - ; tc_lhs_type ty ekOpen } - ; return (mkPhiTy ctxt' ty') } - ---------- Lists, arraysp, and tuples -tc_hs_type hs_ty@(HsListTy elt_ty) exp_kind - = do { tau_ty <- tc_lhs_type elt_ty ekLifted - ; checkExpectedKind hs_ty liftedTypeKind exp_kind + do { ek <- ekOpen + ; ty <- tc_lhs_type mode ty ek + ; checkExpectedKind ty liftedTypeKind exp_kind } + + ; return (mkNakedPhiTy ctxt' ty') } + +--------- Lists, arrays, and tuples +tc_hs_type mode (HsListTy elt_ty) exp_kind + = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind ; checkWiredInTyCon listTyCon - ; return (mkListTy tau_ty) } + ; checkExpectedKind (mkListTy tau_ty) liftedTypeKind exp_kind } -tc_hs_type hs_ty@(HsPArrTy elt_ty) exp_kind - = do { tau_ty <- tc_lhs_type elt_ty ekLifted - ; checkExpectedKind hs_ty liftedTypeKind exp_kind +tc_hs_type mode (HsPArrTy elt_ty) exp_kind + = do { MASSERT( isTypeLevel (mode_level mode) ) + ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind ; checkWiredInTyCon parrTyCon - ; return (mkPArrTy tau_ty) } + ; checkExpectedKind (mkPArrTy tau_ty) liftedTypeKind exp_kind } -- See Note [Distinguishing tuple kinds] in HsTypes -- See Note [Inferring tuple kinds] -tc_hs_type hs_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind@(EK exp_k _ctxt) +tc_hs_type mode (HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind -- (NB: not zonking before looking at exp_k, to avoid left-right bias) - | Just tup_sort <- tupKindSort_maybe exp_k + | Just tup_sort <- tupKindSort_maybe exp_kind = traceTc "tc_hs_type tuple" (ppr hs_tys) >> - tc_tuple hs_ty tup_sort hs_tys exp_kind + tc_tuple mode tup_sort hs_tys exp_kind | otherwise = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys) - ; (tys, kinds) <- mapAndUnzipM tc_infer_lhs_type hs_tys - ; kinds <- mapM zonkTcKind kinds + ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys + ; kinds <- mapM zonkTcType kinds -- Infer each arg type separately, because errors can be -- confusing if we give them a shared kind. Eg Trac #7410 -- (Either Int, Int), we do not want to get an error saying @@ -485,16 +556,15 @@ tc_hs_type hs_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind@(EK exp_k [] -> (liftedTypeKind, BoxedTuple) -- In the [] case, it's not clear what the kind is, so guess * - ; sequence_ [ setSrcSpan loc $ - checkExpectedKind ty kind - (expArgKind (ptext (sLit "a tuple")) arg_kind n) - | (L loc ty, kind, n) <- zip3 hs_tys kinds [1..] ] + ; tys' <- sequence [ setSrcSpan loc $ + checkExpectedKind ty kind arg_kind + | ((L loc _),ty,kind) <- zip3 hs_tys tys kinds ] - ; finish_tuple hs_ty tup_sort tys exp_kind } + ; finish_tuple tup_sort tys' (map (const arg_kind) tys') exp_kind } -tc_hs_type hs_ty@(HsTupleTy hs_tup_sort tys) exp_kind - = tc_tuple hs_ty tup_sort tys exp_kind +tc_hs_type mode (HsTupleTy hs_tup_sort tys) exp_kind + = tc_tuple mode tup_sort tys exp_kind where tup_sort = case hs_tup_sort of -- Fourth case dealt with above HsUnboxedTuple -> UnboxedTuple @@ -504,106 +574,107 @@ tc_hs_type hs_ty@(HsTupleTy hs_tup_sort tys) exp_kind --------- Promoted lists and tuples -tc_hs_type hs_ty@(HsExplicitListTy _k hs_tys) exp_kind - = do { (taus, kinds) <- mapAndUnzipM tc_infer_lhs_type hs_tys - ; kind <- unifyKinds (ptext (sLit "In a promoted list")) hs_tys kinds - ; checkExpectedKind hs_ty (mkPromotedListTy kind) exp_kind - ; return (foldr (mk_cons kind) (mk_nil kind) taus) } +tc_hs_type mode (HsExplicitListTy _k tys) exp_kind + = do { tks <- mapM (tc_infer_lhs_type mode) tys + ; (taus', kind) <- unifyKinds tks + ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus') + ; checkExpectedKind ty (mkListTy kind) exp_kind } where mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b] mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k] -tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind - = do { tks <- mapM tc_infer_lhs_type tys +tc_hs_type mode (HsExplicitTupleTy _ tys) exp_kind + = do { tks <- mapM (tc_infer_lhs_type mode) tys ; let n = length tys - kind_con = promotedTupleTyCon Boxed n + kind_con = tupleTyCon Boxed n ty_con = promotedTupleDataCon Boxed n (taus, ks) = unzip tks tup_k = mkTyConApp kind_con ks - ; checkExpectedKind hs_ty tup_k exp_kind - ; return (mkTyConApp ty_con (ks ++ taus)) } + ; checkExpectedKind (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind } --------- Constraint types -tc_hs_type ipTy@(HsIParamTy n ty) exp_kind - = do { ty' <- tc_lhs_type ty ekLifted - ; checkExpectedKind ipTy constraintKind exp_kind +tc_hs_type mode (HsIParamTy n ty) exp_kind + = do { MASSERT( isTypeLevel (mode_level mode) ) + ; ty' <- tc_lhs_type mode ty liftedTypeKind ; let n' = mkStrLitTy $ hsIPNameFS n - ; return (mkClassPred ipClass [n',ty']) - } - -tc_hs_type ty@(HsEqTy ty1 ty2) exp_kind - = do { (ty1', kind1) <- tc_infer_lhs_type ty1 - ; (ty2', kind2) <- tc_infer_lhs_type ty2 - ; checkExpectedKind (unLoc ty2) kind2 - (EK kind1 msg_fn) - ; checkExpectedKind ty constraintKind exp_kind - ; return (mkNakedTyConApp eqTyCon [kind1, ty1', ty2']) } - where - msg_fn pkind = ptext (sLit "The left argument of the equality had kind") - <+> quotes (pprKind pkind) - ---------- Misc -tc_hs_type (HsKindSig ty sig_k) exp_kind - = do { sig_k' <- tcLHsKind sig_k - ; checkExpectedKind (unLoc ty) sig_k' exp_kind - ; tc_lhs_type ty (EK sig_k' msg_fn) } - where - msg_fn pkind = ptext (sLit "The signature specified kind") - <+> quotes (pprKind pkind) - -tc_hs_type hs_ty@(HsCoreTy ty) exp_kind - = do { checkExpectedKind hs_ty (typeKind ty) exp_kind - ; return ty } - - --- This should never happen; type splices are expanded by the renamer -tc_hs_type ty@(HsSpliceTy {}) _exp_kind - = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty) - -tc_hs_type (HsWrapTy {}) _exp_kind - = panic "tc_hs_type HsWrapTy" -- We kind checked something twice - -tc_hs_type hs_ty@(HsTyLit (HsNumTy _ n)) exp_kind - = do { checkExpectedKind hs_ty typeNatKind exp_kind - ; checkWiredInTyCon typeNatKindCon - ; return (mkNumLitTy n) } - -tc_hs_type hs_ty@(HsTyLit (HsStrTy _ s)) exp_kind - = do { checkExpectedKind hs_ty typeSymbolKind exp_kind - ; checkWiredInTyCon typeSymbolKindCon - ; return (mkStrLitTy s) } - -tc_hs_type hs_ty@(HsWildCardTy wc) exp_kind + ; checkExpectedKind (mkClassPred ipClass [n',ty']) + constraintKind exp_kind } + +tc_hs_type mode (HsEqTy ty1 ty2) exp_kind + = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1 + ; (ty2', kind2) <- tc_infer_lhs_type mode ty2 + ; ty2'' <- checkExpectedKind ty2' kind2 kind1 + ; eq_tc <- tcLookupTyCon eqTyConName + ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2''] + ; checkExpectedKind ty' constraintKind exp_kind } + +--------- Literals +tc_hs_type _ (HsTyLit (HsNumTy _ n)) exp_kind + = do { checkWiredInTyCon typeNatKindCon + ; checkExpectedKind (mkNumLitTy n) typeNatKind exp_kind } + +tc_hs_type _ (HsTyLit (HsStrTy _ s)) exp_kind + = do { checkWiredInTyCon typeSymbolKindCon + ; checkExpectedKind (mkStrLitTy s) typeSymbolKind exp_kind } + +--------- Potentially kind-polymorphic types: call the "up" checker +-- See Note [Future-proofing the type checker] +tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek +tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek +tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek +tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek +tc_hs_type mode ty@(HsCoreTy {}) ek = tc_infer_hs_type_ek mode ty ek + +tc_hs_type _ (HsWildCardTy wc) exp_kind = do { let name = wildCardName wc ; tv <- tcLookupTyVar name - ; checkExpectedKind hs_ty (tyVarKind tv) exp_kind - ; return (mkTyVarTy tv) } + ; checkExpectedKind (mkTyVarTy tv) (tyVarKind tv) exp_kind } + +-- disposed of by renamer +tc_hs_type _ ty@(HsAppsTy {}) _ + = pprPanic "tc_hs_tyep HsAppsTy" (ppr ty) + +--------------------------- +-- | Call 'tc_infer_hs_type' and check its result against an expected kind. +tc_infer_hs_type_ek :: TcTyMode -> HsType Name -> TcKind -> TcM TcType +tc_infer_hs_type_ek mode ty ek + = do { (ty', k) <- tc_infer_hs_type mode ty + ; checkExpectedKind ty' k ek } --------------------------- tupKindSort_maybe :: TcKind -> Maybe TupleSort tupKindSort_maybe k + | Just (k', _) <- tcSplitCastTy_maybe k = tupKindSort_maybe k' + | Just k' <- coreView k = tupKindSort_maybe k' | isConstraintKind k = Just ConstraintTuple | isLiftedTypeKind k = Just BoxedTuple | otherwise = Nothing -tc_tuple :: HsType Name -> TupleSort -> [LHsType Name] -> ExpKind -> TcM TcType -tc_tuple hs_ty tup_sort tys exp_kind - = do { tau_tys <- tc_hs_arg_tys cxt_doc tys (repeat arg_kind) - ; finish_tuple hs_ty tup_sort tau_tys exp_kind } +tc_tuple :: TcTyMode -> TupleSort -> [LHsType Name] -> TcKind -> TcM TcType +tc_tuple mode tup_sort tys exp_kind + = do { arg_kinds <- case tup_sort of + BoxedTuple -> return (nOfThem arity liftedTypeKind) + UnboxedTuple -> do { levs <- newFlexiTyVarTys arity levityTy + ; return $ map tYPE levs } + ConstraintTuple -> return (nOfThem arity constraintKind) + ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds + ; finish_tuple tup_sort tau_tys arg_kinds exp_kind } where - arg_kind = case tup_sort of - BoxedTuple -> liftedTypeKind - UnboxedTuple -> openTypeKind - ConstraintTuple -> constraintKind - cxt_doc = case tup_sort of - BoxedTuple -> ptext (sLit "a tuple") - UnboxedTuple -> ptext (sLit "an unboxed tuple") - ConstraintTuple -> ptext (sLit "a constraint tuple") - -finish_tuple :: HsType Name -> TupleSort -> [TcType] -> ExpKind -> TcM TcType -finish_tuple hs_ty tup_sort tau_tys exp_kind - = do { traceTc "finish_tuple" (ppr res_kind $$ ppr exp_kind $$ ppr exp_kind) - ; checkExpectedKind hs_ty res_kind exp_kind + arity = length tys + +finish_tuple :: TupleSort + -> [TcType] -- ^ argument types + -> [TcKind] -- ^ of these kinds + -> TcKind -- ^ expected kind of the whole tuple + -> TcM TcType +finish_tuple tup_sort tau_tys tau_kinds exp_kind + = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind) + ; let arg_tys = case tup_sort of + -- See also Note [Unboxed tuple levity vars] in TyCon + UnboxedTuple -> map (getLevityFromKind "finish_tuple") tau_kinds + ++ tau_tys + BoxedTuple -> tau_tys + ConstraintTuple -> tau_tys ; tycon <- case tup_sort of ConstraintTuple | arity > mAX_CTUPLE_SIZE @@ -613,7 +684,7 @@ finish_tuple hs_ty tup_sort tau_tys exp_kind ; checkWiredInTyCon tc ; return tc } UnboxedTuple -> return (tupleTyCon Unboxed arity) - ; return (mkTyConApp tycon tau_tys) } + ; checkExpectedKind (mkTyConApp tycon arg_tys) res_kind exp_kind } where arity = length tau_tys res_kind = case tup_sort of @@ -628,81 +699,324 @@ bigConstraintTuple arity 2 (ptext (sLit "Instead, use a nested tuple")) --------------------------- -tcInferApps :: Outputable a - => a - -> TcKind -- Function kind - -> [LHsType Name] -- Arg types - -> TcM ([TcType], TcKind) -- Kind-checked args -tcInferApps the_fun fun_kind args - = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) fun_kind args - ; args' <- tc_lhs_types args_w_kinds - ; return (args', res_kind) } - -tcCheckApps :: Outputable a - => HsType Name -- The type being checked (for err messages only) - -> a -- The function - -> TcKind -> [LHsType Name] -- Fun kind and arg types - -> ExpKind -- Expected kind - -> TcM [TcType] -tcCheckApps hs_ty the_fun fun_kind args exp_kind - = do { (arg_tys, res_kind) <- tcInferApps the_fun fun_kind args - ; checkExpectedKind hs_ty res_kind exp_kind - ; return arg_tys } +-- | Apply a type of a given kind to a list of arguments. This instantiates +-- invisible parameters as necessary. However, it does *not* necessarily +-- apply all the arguments, if the kind runs out of binders. +-- This takes an optional @VarEnv Kind@ which maps kind variables to kinds. +-- These kinds should be used to instantiate invisible kind variables; +-- they come from an enclosing class for an associated type/data family. +-- This version will instantiate all invisible arguments left over after +-- the visible ones. +tcInferArgs :: Outputable fun + => fun -- ^ the function + -> TcKind -- ^ function kind (zonked) + -> Maybe (VarEnv Kind) -- ^ possibly, kind info (see above) + -> [LHsType Name] -- ^ args + -> TcM (TcKind, [TcType], [LHsType Name], Int) + -- ^ (result kind, typechecked args, untypechecked args, n) +tcInferArgs fun fun_kind mb_kind_info args + = do { (res_kind, args', leftovers, n) + <- tc_infer_args typeLevelMode fun fun_kind mb_kind_info args 1 + -- now, we need to instantiate any remaining invisible arguments + ; let (invis_bndrs, really_res_kind) = splitPiTysInvisible res_kind + ; (subst, invis_args) + <- tcInstBindersX emptyTCvSubst mb_kind_info invis_bndrs + ; return ( substTy subst really_res_kind, args' `chkAppend` invis_args + , leftovers, n ) } + +-- | See comments for 'tcInferArgs'. But this version does not instantiate +-- any remaining invisible arguments. +tc_infer_args :: Outputable fun + => TcTyMode + -> fun -- ^ the function + -> TcKind -- ^ function kind (zonked) + -> Maybe (VarEnv Kind) -- ^ possibly, kind info (see above) + -> [LHsType Name] -- ^ args + -> Int -- ^ number to start arg counter at + -> TcM (TcKind, [TcType], [LHsType Name], Int) +tc_infer_args mode orig_ty ki mb_kind_info orig_args n0 + = do { traceTc "tcInferApps" (ppr ki $$ ppr orig_args) + ; go emptyTCvSubst ki orig_args n0 [] } + where + go subst fun_kind [] n acc + = return ( substTy subst fun_kind, reverse acc, [], n ) + -- when we call this when checking type family patterns, we really + -- do want to instantiate all invisible arguments. During other + -- typechecking, we don't. + + go subst fun_kind all_args n acc + | Just fun_kind' <- coreView fun_kind + = go subst fun_kind' all_args n acc + + | Just tv <- getTyVar_maybe fun_kind + , Just fun_kind' <- lookupTyVar subst tv + = go subst fun_kind' all_args n acc + + | (inv_bndrs, res_k) <- splitPiTysInvisible fun_kind + , not (null inv_bndrs) + = do { (subst', args') <- tcInstBindersX subst mb_kind_info inv_bndrs + ; go subst' res_k all_args n (reverse args' ++ acc) } + + | Just (bndr, res_k) <- splitPiTy_maybe fun_kind + , arg:args <- all_args -- this actually has to succeed + = ASSERT( isVisibleBinder bndr ) + do { let mode' | isNamedBinder bndr = kindLevel mode + | otherwise = mode + ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $ + tc_lhs_type mode' arg (substTy subst $ binderType bndr) + ; let subst' = case binderVar_maybe bndr of + Just tv -> extendTCvSubst subst tv arg' + Nothing -> subst + ; go subst' res_k args (n+1) (arg' : acc) } ---------------------------- -splitFunKind :: SDoc -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind) -splitFunKind the_fun fun_kind args - = go 1 fun_kind args + | otherwise + = return (substTy subst fun_kind, reverse acc, all_args, n) + +-- | Applies a type to a list of arguments. Always consumes all the +-- arguments. +tcInferApps :: Outputable fun + => TcTyMode + -> fun -- ^ Function (for printing only) + -> TcType -- ^ Function (could be knot-tied) + -> TcKind -- ^ Function kind (zonked) + -> [LHsType Name] -- ^ Args + -> TcM (TcType, TcKind) -- ^ (f args, result kind) +tcInferApps mode orig_ty ty ki args = go ty ki args 1 where - go _ fk [] = return ([], fk) - go arg_no fk (arg:args) - = do { mb_fk <- matchExpectedFunKind fk - ; case mb_fk of - Nothing -> failWithTc too_many_args - Just (ak,fk') -> do { (aks, rk) <- go (arg_no+1) fk' args - ; let exp_kind = expArgKind (quotes the_fun) ak arg_no - ; return ((arg, exp_kind) : aks, rk) } } + go fun fun_kind [] _ = return (fun, fun_kind) + go fun fun_kind args n + | Just fun_kind' <- coreView fun_kind + = go fun fun_kind' args n + + | isPiTy fun_kind + = do { (res_kind, args', leftover_args, n') + <- tc_infer_args mode orig_ty fun_kind Nothing args n + ; go (mkNakedAppTys fun args') res_kind leftover_args n' } + + go fun fun_kind all_args@(arg:args) n + = do { (co, arg_k, res_k) <- matchExpectedFunKind (length all_args) + fun fun_kind + ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $ + tc_lhs_type mode arg arg_k + ; go (mkNakedAppTy (fun `mkNakedCastTy` co) arg') + res_k args (n+1) } + +--------------------------- +-- | This is used to instantiate binders when type-checking *types* only. +-- Precondition: all binders are invisible. See also Note [Bidirectional type checking] +tcInstBinders :: [TyBinder] -> TcM (TCvSubst, [TcType]) +tcInstBinders = tcInstBindersX emptyTCvSubst Nothing + +-- | This is used to instantiate binders when type-checking *types* only. +-- Precondition: all binders are invisible. +-- The @VarEnv Kind@ gives some known instantiations. +-- See also Note [Bidirectional type checking] +tcInstBindersX :: TCvSubst -> Maybe (VarEnv Kind) + -> [TyBinder] -> TcM (TCvSubst, [TcType]) +tcInstBindersX subst mb_kind_info bndrs + = do { (subst, args) <- mapAccumLM (tcInstBinderX mb_kind_info) subst bndrs + ; traceTc "instantiating implicit dependent vars:" + (vcat $ zipWith (\bndr arg -> ppr bndr <+> text ":=" <+> ppr arg) + bndrs args) + ; return (subst, args) } + +-- | Used only in *types* +tcInstBinderX :: Maybe (VarEnv Kind) + -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType) +tcInstBinderX mb_kind_info subst binder + | Just tv <- binderVar_maybe binder + = case lookup_tv tv of + Just ki -> return (extendTCvSubst subst tv ki, ki) + Nothing -> do { (subst', tv') <- tcInstTyVarX subst tv + ; return (subst', mkTyVarTy tv') } + + -- This is the *only* constraint currently handled in types. + | Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty + = do { let origin = TypeEqOrigin { uo_actual = k1 + , uo_expected = k2 + , uo_thing = Nothing } + ; co <- case role of + Nominal -> unifyKind noThing k1 k2 + Representational -> emitWantedEq origin KindLevel role k1 k2 + Phantom -> pprPanic "tcInstBinderX Phantom" (ppr binder) + ; arg' <- mk co k1 k2 + ; return (subst, arg') } - too_many_args = quotes the_fun <+> - ptext (sLit "is applied to too many type arguments") + | otherwise + = do { let (env, tidy_ty) = tidyOpenType emptyTidyEnv substed_ty + ; addErrTcM (env, text "Illegal constraint in a type:" <+> ppr tidy_ty) + + -- just invent a new variable so that we can continue + ; u <- newUnique + ; let name = mkSysTvName u (fsLit "dict") + ; return (subst, mkTyVarTy $ mkTyVar name substed_ty) } + where + substed_ty = substTy subst (binderType binder) + + lookup_tv tv = do { env <- mb_kind_info -- `Maybe` monad + ; lookupVarEnv env tv } + + -- handle boxed equality constraints, because it's so easy + get_pred_tys_maybe ty + | Just (r, k1, k2) <- getEqPredTys_maybe ty + = Just (\co _ _ -> return $ mkCoercionTy co, r, k1, k2) + | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty + = if | tc `hasKey` heqTyConKey + -> Just (mkHEqBoxTy, Nominal, k1, k2) + | otherwise + -> Nothing + | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty + = if | tc `hasKey` eqTyConKey + -> Just (mkEqBoxTy, Nominal, k1, k2) + | tc `hasKey` coercibleTyConKey + -> Just (mkCoercibleBoxTy, Representational, k1, k2) + | otherwise + -> Nothing + | otherwise + = Nothing + +------------------------------- +-- | This takes @a ~# b@ and returns @a ~~ b@. +mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type +-- monadic just for convenience with mkEqBoxTy +mkHEqBoxTy co ty1 ty2 + = return $ + mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co] + where k1 = typeKind ty1 + k2 = typeKind ty2 + +-- | This takes @a ~# b@ and returns @a ~ b@. +mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type +mkEqBoxTy co ty1 ty2 + = do { eq_tc <- tcLookupTyCon eqTyConName + ; let [datacon] = tyConDataCons eq_tc + ; hetero <- mkHEqBoxTy co ty1 ty2 + ; return $ mkTyConApp (promoteDataCon datacon) [k, ty1, ty2, hetero] } + where k = typeKind ty1 + +-- | This takes @a ~R# b@ and returns @Coercible a b@. +mkCoercibleBoxTy :: TcCoercion -> Type -> Type -> TcM Type +-- monadic just for convenience with mkEqBoxTy +mkCoercibleBoxTy co ty1 ty2 + = do { return $ + mkTyConApp (promoteDataCon coercibleDataCon) + [k, ty1, ty2, mkCoercionTy co] } + where k = typeKind ty1 + + +-------------------------- +checkExpectedKind :: TcType -- the type whose kind we're checking + -> TcKind -- the known kind of that type, k + -> TcKind -- the expected kind, exp_kind + -> TcM TcType -- a possibly-inst'ed, casted type :: exp_kind +-- Instantiate a kind (if necessary) and then call unifyType +-- (checkExpectedKind ty act_kind exp_kind) +-- checks that the actual kind act_kind is compatible +-- with the expected kind exp_kind +checkExpectedKind ty act_kind exp_kind + = do { (ty', act_kind') <- instantiate ty act_kind exp_kind + ; let origin = TypeEqOrigin { uo_actual = act_kind' + , uo_expected = exp_kind + , uo_thing = Just $ mkTypeErrorThing ty' + } + ; co_k <- uType origin KindLevel act_kind' exp_kind + ; traceTc "checkExpectedKind" (vcat [ ppr act_kind + , ppr exp_kind + , ppr co_k ]) + ; let result_ty = ty' `mkNakedCastTy` co_k + ; return result_ty } + where + -- we need to make sure that both kinds have the same number of implicit + -- foralls out front. If the actual kind has more, instantiate accordingly. + -- Otherwise, just pass the type & kind through -- the errors are caught + -- in unifyType. + instantiate :: TcType -- the type + -> TcKind -- of this kind + -> TcKind -- but expected to be of this one + -> TcM ( TcType -- the inst'ed type + , TcKind ) -- its new kind + instantiate ty act_ki exp_ki + = let (exp_bndrs, _) = splitPiTysInvisible exp_ki in + instantiateTyN (length exp_bndrs) ty act_ki + +-- | Instantiate a type to have at most @n@ invisible arguments. +instantiateTyN :: Int -- ^ @n@ + -> TcType -- ^ the type + -> TcKind -- ^ its kind + -> TcM (TcType, TcKind) -- ^ The inst'ed type with kind +instantiateTyN n ty ki + = let (bndrs, inner_ki) = splitPiTysInvisible ki + num_to_inst = length bndrs - n + -- NB: splitAt is forgiving with invalid numbers + (inst_bndrs, leftover_bndrs) = splitAt num_to_inst bndrs + in + if num_to_inst <= 0 then return (ty, ki) else + do { (subst, inst_args) <- tcInstBinders inst_bndrs + ; let rebuilt_ki = mkForAllTys leftover_bndrs inner_ki + ki' = substTy subst rebuilt_ki + ; return (mkNakedAppTys ty inst_args, ki') } --------------------------- tcHsContext :: LHsContext Name -> TcM [PredType] -tcHsContext ctxt = mapM tcLHsPredType (unLoc ctxt) +tcHsContext = tc_hs_context typeLevelMode tcLHsPredType :: LHsType Name -> TcM PredType -tcLHsPredType pred = tc_lhs_type pred ekConstraint +tcLHsPredType = tc_lhs_pred typeLevelMode + +tc_hs_context :: TcTyMode -> LHsContext Name -> TcM [PredType] +tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt) + +tc_lhs_pred :: TcTyMode -> LHsType Name -> TcM PredType +tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind --------------------------- -tcTyVar :: Name -> TcM (TcType, TcKind) +tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind) -- See Note [Type checking recursive type and class declarations] -- in TcTyClsDecls -tcTyVar name -- Could be a tyvar, a tycon, or a datacon +tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon = do { traceTc "lk1" (ppr name) ; thing <- tcLookup name ; case thing of - ATyVar _ tv - | isKindVar tv - -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr tv) - <+> ptext (sLit "used as a type")) - | otherwise - -> return (mkTyVarTy tv, tyVarKind tv) - - AThing kind -> do { tc <- get_loopy_tc name - ; inst_tycon (mkNakedTyConApp tc) kind } - -- mkNakedTyConApp: see Note [Zonking inside the knot] + ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv) + + AThing kind -> do { data_kinds <- xoptM Opt_DataKinds + ; unless (isTypeLevel (mode_level mode) || + data_kinds) $ + promotionErr name NoDataKinds + ; tc <- get_loopy_tc name + ; return (mkNakedTyConApp tc [], kind) } + -- mkNakedTyConApp: see Note [Type-checking inside the knot] + -- NB: we really should check if we're at the kind level + -- and if the tycon is promotable if -XNoTypeInType is set. + -- But this is a terribly large amount of work! Not worth it. - AGlobal (ATyCon tc) -> inst_tycon (mkTyConApp tc) (tyConKind tc) + AGlobal (ATyCon tc) + -> do { type_in_type <- xoptM Opt_TypeInType + ; data_kinds <- xoptM Opt_DataKinds + ; unless (isTypeLevel (mode_level mode) || + data_kinds || + isKindTyCon tc) $ + promotionErr name NoDataKinds + ; unless (isTypeLevel (mode_level mode) || + type_in_type || + isLegacyPromotableTyCon tc) $ + promotionErr name NoTypeInTypeTC + ; return (mkTyConApp tc [], tyConKind tc) } AGlobal (AConLike (RealDataCon dc)) - | Promoted tc <- promoteDataCon_maybe dc -> do { data_kinds <- xoptM Opt_DataKinds - ; unless data_kinds $ promotionErr name NoDataKinds - ; inst_tycon (mkTyConApp tc) (tyConKind tc) } - | otherwise -> failWithTc (ptext (sLit "Data constructor") <+> quotes (ppr dc) - <+> ptext (sLit "comes from an un-promotable type") - <+> quotes (ppr (dataConTyCon dc))) + ; unless (data_kinds || specialPromotedDc dc) $ + promotionErr name NoDataKinds + ; type_in_type <- xoptM Opt_TypeInType + ; unless ( type_in_type || + ( isTypeLevel (mode_level mode) && + isLegacyPromotableDataCon dc ) || + ( isKindLevel (mode_level mode) && + specialPromotedDc dc ) ) $ + promotionErr name NoTypeInTypeDC + ; let tc = promoteDataCon dc + ; return (mkNakedTyConApp tc [], tyConKind tc) } APromotionErr err -> promotionErr name err @@ -714,19 +1028,6 @@ tcTyVar name -- Could be a tyvar, a tycon, or a datacon Just (ATyCon tc) -> return tc _ -> return (aThingErr "tcTyVar" name) } - inst_tycon :: ([Type] -> Type) -> Kind -> TcM (Type, Kind) - -- Instantiate the polymorphic kind - -- Lazy in the TyCon - inst_tycon mk_tc_app kind - | null kvs - = return (mk_tc_app [], ki_body) - | otherwise - = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind) - ; ks <- mapM (const newMetaKindVar) kvs - ; return (mk_tc_app ks, substKiWith kvs ks ki_body) } - where - (kvs, ki_body) = splitForAllTys kind - tcClass :: Name -> TcM (Class, TcKind) tcClass cls -- Must be a class = do { thing <- tcLookup cls @@ -745,7 +1046,7 @@ aThingErr :: String -> Name -> b aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x) {- -Note [Zonking inside the knot] +Note [Type-checking inside the knot] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we are checking the argument types of a data constructor. We must zonk the types before making the DataCon, because once built we @@ -757,81 +1058,22 @@ So we must be careful not to use "smart constructors" for types that look at the TyCon or Class involved. * Hence the use of mkNakedXXX functions. These do *not* enforce - the invariants (for example that we use (FunTy s t) rather + the invariants (for example that we use (ForAllTy (Anon s) t) rather than (TyConApp (->) [s,t])). - * Ditto in zonkTcType (which may be applied more than once, eg to - squeeze out kind meta-variables), we are careful not to look at - the TyCon. - - * We arrange to call zonkSigType *once* right at the end, and it - does establish the invariants. But in exchange we can't look - at the result (not even its structure) until we have emerged - from the "knot". + * The zonking functions establish invariants (even zonkTcType, a change from + previous behaviour). So we must never inspect the result of a + zonk that might mention a knot-tied TyCon. This is generally OK + because we zonk *kinds* while kind-checking types. And the TyCons + in kinds shouldn't be knot-tied, because they come from a previous + mutually recursive group. * TcHsSyn.zonkTcTypeToType also can safely check/establish invariants. This is horribly delicate. I hate it. A good example of how delicate it is can be seen in Trac #7903. --} - -mkNakedTyConApp :: TyCon -> [Type] -> Type --- Builds a TyConApp --- * without being strict in TyCon, --- * without satisfying the invariants of TyConApp --- A subsequent zonking will establish the invariants -mkNakedTyConApp tc tys = TyConApp tc tys - -mkNakedAppTys :: Type -> [Type] -> Type -mkNakedAppTys ty1 [] = ty1 -mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2) -mkNakedAppTys ty1 tys2 = foldl AppTy ty1 tys2 - -zonkAndCheckValidity :: UserTypeCtxt -> TcType -> TcM TcType --- Zonk a user-written type signature, and check it for validity -zonkAndCheckValidity ctxt ty - = do { ty <- zonkSigType ty - ; checkValidType ctxt ty - ; return ty } - -zonkSigType :: TcType -> TcM TcType --- Zonk the result of type-checking a user-written type signature --- It may have kind variables in it, but no meta type variables --- Because of knot-typing (see Note [Zonking inside the knot]) --- it may need to establish the Type invariants; --- hence the use of mkTyConApp and mkAppTy -zonkSigType ty - = go ty - where - go (TyConApp tc tys) = do tys' <- mapM go tys - return (mkTyConApp tc tys') - -- Key point: establish Type invariants! - -- See Note [Zonking inside the knot] - - go (LitTy n) = return (LitTy n) - - go (FunTy arg res) = do arg' <- go arg - res' <- go res - return (FunTy arg' res') - - go (AppTy fun arg) = do fun' <- go fun - arg' <- go arg - return (mkAppTy fun' arg') - -- NB the mkAppTy; we might have instantiated a - -- type variable to a type constructor, so we need - -- to pull the TyConApp to the top. - - -- The two interesting cases! - go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar - | otherwise = TyVarTy <$> updateTyVarKindM go tyvar - -- Ordinary (non Tc) tyvars occur inside quantified types - - go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv - ; ty' <- go ty - ; return (ForAllTy tv' ty') } -{- Note [Body kind of a forall] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The body of a forall is usually a type, but in principle @@ -867,17 +1109,23 @@ Then the dfun has type T :: * -> * MkT :: forall k. (Typeable ((k->*) -> k -> *) (Apply k)) -> T a - f :: (forall (k:BOX). forall (t:: k->*) (a:k). t a -> t a) -> Int + f :: (forall (k:*). forall (t:: k->*) (a:k). t a -> t a) -> Int f :: (forall a. a -> Typeable Apply) -> Int So we *must* keep the HsForAll on the instance type HsForAll Implicit [] [] (Typeable Apply) so that we do kind generalisation on it. -Really we should check that it's a type of value kind -{*, Constraint, #}, but I'm not doing that yet -Example that should be rejected: - f :: (forall (a:*->*). a) Int +It's tempting to check that the body kind is either * or #. But this is +wrong. For example: + + class C a b + newtype N = Mk Foo deriving (C a) + +We're doing newtype-deriving for C. But notice how `a` isn't in scope in +the predicate `C a`. So we quantify, yielding `forall a. C a` even though +`C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but +convenient. Bottom line: don't check for * or # here. Note [Inferring tuple kinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -907,7 +1155,7 @@ The type desugarer is phase 2 of dealing with HsTypes. Specifically: * It zonks any kinds. The returned type should have no mutable kind or type variables (hence returning Type not TcType): - - any unconstrained kind variables are defaulted to AnyK just + - any unconstrained kind variables are defaulted to (Any *) just as in TcHsSyn. - there are no mutable type variables because we are kind-checking a type @@ -918,7 +1166,7 @@ You might worry about nested scopes: ..a:kappa in scope.. let f :: forall b. T '[a,b] -> Int In this case, f's type could have a mutable kind variable kappa in it; -and we might then default it to AnyK when dealing with f's type +and we might then default it to (Any *) when dealing with f's type signature. But we don't expect this to happen because we can't get a lexically scoped type variable with a mutable kind variable in it. A delicate point, this. If it becomes an issue we might need to @@ -943,7 +1191,7 @@ as if $(..blah..) :: forall k. k. In the e1 example, the context of the splice fixes kappa to *. But in the e2 example, we'll desugar the type, zonking the kind unification variables as we go. When we encounter the unconstrained kappa, we -want to default it to '*', not to AnyK. +want to default it to '*', not to (Any *). Help functions for type applications @@ -962,14 +1210,33 @@ addTypeCtxt (L _ ty) thing ************************************************************************ * * Type-variable binders -* * -************************************************************************ +%* * +%************************************************************************ + +Note [Scope-check inferred kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + + data SameKind :: k -> k -> * + foo :: forall a (b :: Proxy a) (c :: Proxy d). SameKind b c + +d has no binding site. So it gets bound implicitly, at the top. The +problem is that d's kind mentions `a`. So it's all ill-scoped. + +The way we check for this is to gather all variables *bound* in a +type variable's scope. The type variable's kind should not mention +any of these variables. That is, d's kind can't mention a, b, or c. +We can't just check to make sure that d's kind is in scope, because +we might be about to kindGeneralize. + +A little messy, but it works. + -} tcWildCardBinders :: [Name] -> ([(Name, TcTyVar)] -> TcM a) -> TcM a --- Use the Unqique form the specified Name; don't clone it. There is +-- Use the Unique form the specified Name; don't clone it. There is -- no need to clone, and not doing so avoids the need to return a list -- of pairs to bring into scope. tcWildCardBinders wcs thing_inside @@ -982,122 +1249,176 @@ tcWildCardBinders wcs thing_inside ; tv <- newFlexiTyVar kind ; return (name, tv) } -mkKindSigVar :: Name -> TcM KindVar --- Use the specified Name; don't clone it. There is no need to --- clone, and not doing so avoids the need to return a list of --- pairs to bring into scope. -mkKindSigVar n - = do { mb_thing <- tcLookupLcl_maybe n - ; case mb_thing of - Just (AThing k) - | Just kvar <- getTyVar_maybe k - -> return kvar - _ -> return $ mkTcTyVar n superKind (SkolemTv False) } - -kcScopedKindVars :: [Name] -> TcM a -> TcM a --- Given some tyvar binders like [a (b :: k -> *) (c :: k)] --- bind each scoped kind variable (k in this case) to a fresh --- kind skolem variable -kcScopedKindVars kv_ns thing_inside - = do { kvs <- mapM newSigKindVar kv_ns - -- NB: use mutable signature variables - ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) thing_inside } - -- | Kind-check a 'LHsQTyVars'. 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 +-- user-supplied kind signature (CUSK), generalise the result. +-- Used in 'getInitialKind' (for tycon kinds and other kinds) +-- and in kind-checking (but not for tycon kinds, which are checked with +-- tcTyClDecls). See also Note [Complete user-supplied kind signatures] in -- HsDecls. +-- +-- This function does not do telescope checking. kcHsTyVarBndrs :: Bool -- ^ True <=> the decl being checked has a CUSK -> LHsQTyVars Name - -> TcM (Kind, r) -- ^ the result kind, possibly with other info + -> ([TyVar] -> [TyVar] -> TcM (Kind, r)) + -- ^ the result kind, possibly with other info + -- ^ args are implicit vars, explicit vars -> 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 newSigKindVar kv_ns +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 names must line up in splitTelescopeTvs + else zipWithM newSigTyVar kv_ns meta_kvs ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $ - do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs - ; (res_kind, stuff) <- tcExtendKindEnv nks thing_inside - ; let full_kind = mkArrowKinds (map snd nks) res_kind - kvs = filter (not . isMetaTyVar) $ - tyVarsOfTypeList full_kind + do { (full_kind, _, stuff) <- bind_telescope hs_tvs (thing_inside kvs) + ; let qkvs = filter (not . isMetaTyVar) $ + tyCoVarsOfTypeWellScoped full_kind + + -- 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]) gen_kind = if cusk - then mkForAllTys kvs full_kind + then mkInvForAllTys qkvs $ full_kind else full_kind ; return (gen_kind, stuff) } } where - kc_hs_tv :: HsTyVarBndr Name -> TcM (Name, TcKind) - kc_hs_tv (UserTyVar (L _ n)) - = do { mb_thing <- tcLookupLcl_maybe n - ; kind <- case mb_thing of - Just (AThing k) -> return k - _ | cusk -> return liftedTypeKind - | otherwise -> newMetaKindVar - ; return (n, kind) } - kc_hs_tv (KindedTyVar (L _ n) k) - = do { kind <- tcLHsKind k - -- In an associated type decl, the type variable may already - -- be in scope; in that case we want to make sure its kind - -- matches the one declared here - ; mb_thing <- tcLookupLcl_maybe n - ; case mb_thing of - Nothing -> return () - Just (AThing ks) -> checkKind kind ks - Just thing -> pprPanic "check_in_scope" (ppr thing) - ; return (n, kind) } - -tcImplicitTKBndrs :: [Name] -> [Name] -> ([TcTyVar] -> [TcTyVar] -> TcM a) -> TcM a + -- there may be dependency between the explicit "ty" vars. So, we have + -- to handle them one at a time. We also need to build up a full kind + -- here, because this is the place we know whether to use a FunTy or a + -- ForAllTy. We prefer using an anonymous binder over a trivial named + -- binder. If a user wants a trivial named one, use an explicit kind + -- signature. + bind_telescope :: [LHsTyVarBndr Name] + -> ([TyVar] -> TcM (Kind, r)) + -> TcM (Kind, VarSet, r) + bind_telescope [] thing + = do { (res_kind, stuff) <- thing [] + ; return (res_kind, tyCoVarsOfType res_kind, stuff) } + bind_telescope (L _ hs_tv : hs_tvs) thing + = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv + ; (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 tv Visible + , fvs `delVarSet` tv `unionVarSet` k_fvs ) + | otherwise + = (mkAnonBinder k, fvs `unionVarSet` k_fvs) + + ; return ( mkForAllTy bndr res_kind, fvs', stuff ) } + + -- | Bind the tyvar in the env't unless the bool is True + bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a + bind_unless_scoped (_, True) thing_inside = thing_inside + bind_unless_scoped (tv, False) thing_inside + = 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) } + +tcImplicitTKBndrs :: [Name] + -> TcM (a, TyVarSet) -- vars are bound somewhere in the scope + -- see Note [Scope-check inferred kinds] + -> TcM ([TcTyVar], a) +tcImplicitTKBndrs = tcImplicitTKBndrsX tcHsTyVarName + +-- | Convenient specialization +tcImplicitTKBndrsType :: [Name] + -> TcM Type + -> TcM ([TcTyVar], Type) +tcImplicitTKBndrsType var_ns thing_inside + = tcImplicitTKBndrs var_ns $ + do { res_ty <- thing_inside + ; return (res_ty, allBoundVariables res_ty) } + +-- this more general variant is needed in tcHsPatSigType. +-- See Note [Pattern signature binders] +tcImplicitTKBndrsX :: (Name -> TcM (TcTyVar, Bool)) -- new_tv function + -> [Name] + -> TcM (a, TyVarSet) + -> TcM ([TcTyVar], a) -- Returned TcTyVars have the supplied Names -- i.e. no cloning of fresh names -tcImplicitTKBndrs kv_ns tv_ns thing_inside - = do { kvs <- mapM mkKindSigVar kv_ns - ; tvs <- mapM tc_tv tv_ns - ; tcExtendTyVarEnv (kvs ++ tvs) (thing_inside kvs tvs) } - where - tc_tv name = do { kind <- newMetaKindVar - ; return (mkTcTyVar name kind (SkolemTv False)) } - -tcHsQTyVars :: LHsQTyVars Name - -> ([TcTyVar] -> TcM r) - -> TcM r --- Bind the kind variables to fresh skolem variables --- and type variables to skolems, each with a meta-kind variable kind -tcHsQTyVars (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside - = tcImplicitTKBndrs kv_ns [] $ \ kvs _ -> - do { tv_prs <- mapM tc_tv_bndr hs_tvs - ; tcExtendTyVarEnv [ tv | (tv, False) <- tv_prs ] $ - thing_inside (kvs ++ map fst tv_prs) } - where - -- If the variable is already in scope return it, instead of - -- introducing a new one. This can occur in - -- instance C (a,b) where - -- type F (a,b) c = ... - -- Here a,b will be in scope when processing the associated type instance for F. - -- See Note [Associated type tyvar names] in Class - tc_tv_bndr :: LHsTyVarBndr Name -> TcM (TcTyVar, Bool) - -- True <=> already in scope, do not extend envt - -- False <=> not already in scope - tc_tv_bndr (L _ hs_tv) - = do { let name = hsTyVarName hs_tv - ; mb_tv <- tcLookupLcl_maybe name - ; case mb_tv of - Just (ATyVar _ tv) -> return (tv, True) - _ -> do { tv <- tcHsTyVarBndr hs_tv - ; return (tv, False) } } - -tcHsTyVarBndrs :: [LHsTyVarBndr Name] -> ([TyVar] -> TcM a) -> TcM a +tcImplicitTKBndrsX new_tv var_ns thing_inside + = do { tkvs_pairs <- mapM new_tv var_ns + ; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ] + tkvs = map fst tkvs_pairs + ; (result, bound_tvs) <- tcExtendTyVarEnv must_scope_tkvs $ + thing_inside + + -- it's possible that we guessed the ordering of variables + -- wrongly. Adjust. + ; tkvs <- mapM zonkTyCoVarKind tkvs + ; let extra = text "NB: Implicitly-bound variables always come" <+> + text "before other ones." + ; checkValidInferredKinds tkvs bound_tvs extra + + ; let final_tvs = toposortTyVars tkvs + ; traceTc "tcImplicitTKBndrs" (ppr var_ns $$ ppr final_tvs) + + ; return (final_tvs, result) } + +tcHsTyVarBndrs :: [LHsTyVarBndr Name] + -> ([TyVar] -> TcM (a, TyVarSet)) + -- ^ Thing inside returns the set of variables bound + -- in the scope. See Note [Scope-check inferred kinds] + -> TcM (a, TyVarSet) -- ^ returns augmented bound vars -- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs -tcHsTyVarBndrs hs_tvs thing_inside - = do { tvs <- mapM (tcHsTyVarBndr . unLoc) hs_tvs - ; tcExtendTyVarEnv tvs (thing_inside tvs) } +tcHsTyVarBndrs orig_hs_tvs thing_inside + = go orig_hs_tvs $ \ tvs -> + do { (result, bound_tvs) <- thing_inside tvs + + -- Issue an error if the ordering is bogus. + -- See Note [Bad telescopes] in TcValidity. + ; tvs <- checkZonkValidTelescope (interppSP orig_hs_tvs) tvs empty + ; checkValidInferredKinds tvs bound_tvs empty + + ; traceTc "tcHsTyVarBndrs" $ + vcat [ text "Hs vars:" <+> ppr orig_hs_tvs + , text "tvs:" <+> sep (map pprTvBndr tvs) ] + + ; return (result, bound_tvs `unionVarSet` mkVarSet tvs) + } + where + go [] thing = thing [] + go (L _ hs_tv : hs_tvs) thing + = do { tv <- tcHsTyVarBndr hs_tv + ; tcExtendTyVarEnv [tv] $ + go hs_tvs $ \ tvs -> + thing (tv : tvs) } tcHsTyVarBndr :: HsTyVarBndr Name -> TcM TcTyVar -- Return a type variable initialised with a kind variable. -- Typically the Kind inside the HsTyVarBndr will be a tyvar -- with a mutable kind in it. +-- NB: These variables must not be in scope. This function +-- is not appropriate for use with associated types, for example. -- -- Returned TcTyVar has the same name; no cloning +-- +-- See also Note [Associated type tyvar names] in Class tcHsTyVarBndr (UserTyVar (L _ name)) = do { kind <- newMetaKindVar ; return (mkTcTyVar name kind (SkolemTv False)) } @@ -1105,27 +1426,49 @@ 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) +-- or not (False). (Use this for associated types, for example.) +tcHsTyVarName :: Name -> TcM (TcTyVar, Bool) +tcHsTyVarName name + = do { mb_tv <- tcLookupLcl_maybe name + ; case mb_tv of + Just (ATyVar _ tv) -> return (tv, True) + _ -> do { kind <- newMetaKindVar + ; return (mkTcTyVar name kind vanillaSkolemTv, False) }} + +-- makes a new skolem tv +new_skolem_tv :: Name -> Kind -> TcTyVar +new_skolem_tv n k = mkTcTyVar n k vanillaSkolemTv + ------------------ kindGeneralizeType :: Type -> TcM Type kindGeneralizeType ty - = do { kvs <- zonkTcTypeAndFV ty - ; kvs <- kindGeneralize kvs - ; return (mkForAllTys kvs ty) } - -kindGeneralize :: TyVarSet -> TcM [KindVar] -kindGeneralize tkvs - = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked - ; quantifyTyVars gbl_tvs (filterVarSet isKindVar tkvs) } - -- ToDo: remove the (filter isKindVar) - -- Any type variables in tkvs will be in scope, - -- and hence in gbl_tvs, so after removing gbl_tvs - -- we should only have kind variables left - -- - -- BUT there is a smelly case (to be fixed when TH is reorganised) - -- f t = [| e :: $t |] - -- When typechecking the body of the bracket, we typecheck $t to a - -- unification variable 'alpha', with no biding forall. We don't - -- want to kind-quantify it! + = do { kvs <- kindGeneralize ty + ; zonkTcType (mkInvForAllTys kvs ty) } + +kindGeneralize :: TcType -> TcM [KindVar] +kindGeneralize ty + = do { gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked + ; kvs <- zonkTcTypeAndFV ty + ; quantifyTyVars gbl_tvs (Pair kvs emptyVarSet) } {- Note [Kind generalisation] @@ -1144,6 +1487,11 @@ we want to infer the most general type. The f2 type signature would be *less applicable* than f1, because it requires a more polymorphic argument. +NB: There are no explicit kind variables written in f's signature. +When there are, the renamer adds these kind variables to the list of +variables bound by the forall, so you can indeed have a type that's +higher-rank in its kind. But only by explicit request. + Note [Kinds of quantified type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ tcTyVarBndrsGen quantifies over a specified list of type variables, @@ -1162,6 +1510,102 @@ which the type checker will then instantiate, and instantiate does not look through unification variables! Hence using zonked_kinds when forming tvs'. + +Note [Typechecking telescopes] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The function tcTyClTyVars has to bind the scoped type and kind +variables in a telescope. For example: + +class Foo k (t :: Proxy k -> k2) where ... + +By the time [kt]cTyClTyVars is called, we know *something* about the kind of Foo, +at least that it has the form + + Foo :: forall (k2 :: mk2). forall (k :: mk1) -> (Proxy mk1 k -> k2) -> Constraint + +if it has a CUSK (Foo does not, in point of fact) or + + Foo :: forall (k :: mk1) -> (Proxy mk1 k -> k2) -> Constraint + +if it does not, where mk1 and mk2 are meta-kind variables (mk1, mk2 :: *). + +When calling tcTyClTyVars, this kind is further generalized w.r.t. any +free variables appearing in mk1 or mk2. So, mk_tvs must handle +that possibility. Perhaps we discover that mk1 := Maybe k3 and mk2 := *, +so we have + +Foo :: forall (k3 :: *). forall (k2 :: *). forall (k :: Maybe k3) -> + (Proxy (Maybe k3) k -> k2) -> Constraint + +We now have several sorts of variables to think about: +1) The variable k3 is not mentioned in the source at all. It is neither + explicitly bound nor ever used. It is *not* a scoped kind variable, + and should not be bound when type-checking the scope of the telescope. + +2) The variable k2 is mentioned in the source, but it is not explicitly + bound. It *is* a scoped kind variable, and will appear in the + hsq_implicit field of a LHsTyVarBndrs. + + 2a) In the non-CUSK case, these variables won't have been generalized + yet and don't appear in the looked-up kind. So we just return these + in a NameSet. + +3) The variable k is mentioned in the source with an explicit binding. + It *is* a scoped type variable, and will appear in the + hsq_explicit field of a LHsTyVarBndrs. + +4) The variable t is bound in the source, but it is never mentioned later + in the kind. It *is* a scoped variable (it can appear in the telescope + scope, even though it is non-dependent), and will appear in the + hsq_explicit field of a LHsTyVarBndrs. + +splitTelescopeTvs walks through the output of a splitPiTys on the +telescope head's kind (Foo, in our example), creating a list of tyvars +to be bound within the telescope scope. It must simultaneously walk +through the hsq_implicit and hsq_explicit fields of a LHsTyVarBndrs. +Comments in the code refer back to the cases in this Note. + +Cases (1) and (2) can be mixed together, but these cases must appear before +cases (3) and (4) (the implicitly bound vars always precede the explicitly +bound ones). So, we handle the lists in two stages (mk_tvs and +mk_tvs2). + +As a further wrinkle, it's possible that the variables in case (2) have +been reordered. This is because hsq_implicit is ordered by the renamer, +but there may be dependency among the variables. Of course, the order in +the kind must take dependency into account. So we use a NameSet to keep +these straightened out. + +Note [Free-floating kind vars] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + + data T = MkT (forall (a :: k). Proxy a) + +This is not an existential datatype, but a higher-rank one. Note that +the forall to the right of MkT. Also consider + + data S a = MkS (Proxy (a :: k)) + +According to the rules around implicitly-bound kind variables, those +k's scope over the whole declarations. The renamer grabs it and adds it +to the hsq_implicits field of the HsQTyVars of the tycon. So it must +be in scope during type-checking, but we want to reject T while accepting +S. + +Why reject T? Because the kind variable isn't fixed by anything. For +a variable like k to be implicit, it needs to be mentioned in the kind +of a tycon tyvar. But it isn't. + +Why accept S? Because kind inference tells us that a has kind k, so it's +all OK. + +Here's the approach: in the first pass ("kind-checking") we just bring +k into scope. In the second pass, we certainly hope that k has been +integrated into the type's (generalized) kind, and so it should be found +by splitTelescopeTvs. If it's not, then we must have a definition like +T, and we reject. + -} -------------------- @@ -1178,76 +1622,168 @@ kcLookupKind nm AGlobal (ATyCon tc) -> return (tyConKind tc) _ -> pprPanic "kcLookupKind" (ppr tc_ty_thing) } -kcTyClTyVars :: Name -> LHsQTyVars Name -> TcM a -> TcM a --- Used for the type variables of a type or class decl, --- when doing the initial kind-check. -kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside - = kcScopedKindVars kvs $ - do { tc_kind <- kcLookupKind name - ; let (_, mono_kind) = splitForAllTys tc_kind - -- if we have a FullKindSignature, the tc_kind may already - -- be generalized. The kvs get matched up while kind-checking - -- the types in kc_tv, below - (arg_ks, _res_k) = splitKindFunTysN (length hs_tvs) mono_kind - -- There should be enough arrows, because - -- getInitialKinds used the tcdTyVars - ; name_ks <- zipWithM kc_tv hs_tvs arg_ks - ; tcExtendKindEnv name_ks thing_inside } +-- See Note [Typechecking telescopes] +splitTelescopeTvs :: Kind -- of the head of the telescope + -> LHsQTyVars Name + -> ( [TyVar] -- scoped type variables + , NameSet -- ungeneralized implicit variables (case 2a) + , [TyVar] -- implicit type variables (cases 1 & 2) + , [TyVar] -- explicit type variables (cases 3 & 4) + , Kind ) -- result kind +splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs + , hsq_explicit = hs_tvs }) + = let (bndrs, inner_ki) = splitPiTys kind + (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, mk_kind) + = mk_tvs [] [] bndrs (mkNameSet hs_kvs) hs_tvs + in + (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, mk_kind inner_ki) where - -- getInitialKind has already gotten the kinds of these type - -- variables, but tiresomely we need to check them *again* - -- to match the kind variables they mention against the ones - -- we've freshly brought into scope - kc_tv :: LHsTyVarBndr Name -> Kind -> TcM (Name, Kind) - kc_tv (L _ (UserTyVar (L _ n))) exp_k - = return (n, exp_k) - kc_tv (L _ (KindedTyVar (L _ n) hs_k)) exp_k - = do { k <- tcLHsKind hs_k - ; checkKind k exp_k - ; return (n, exp_k) } + mk_tvs :: [TyVar] -- scoped tv accum (reversed) + -> [TyVar] -- implicit tv accum (reversed) + -> [TyBinder] + -> NameSet -- implicit variables + -> [LHsTyVarBndr Name] -- explicit variables + -> ( [TyVar] -- the tyvars to be lexically bound + , NameSet -- Case 2a names + , [TyVar] -- implicit tyvars + , [TyVar] -- explicit tyvars + , Type -> Type ) -- a function to create the result k + mk_tvs scoped_tv_acc imp_tv_acc (bndr : bndrs) all_hs_kvs all_hs_tvs + | Just tv <- binderVar_maybe bndr + , isInvisibleBinder bndr + , let tv_name = getName tv + , tv_name `elemNameSet` all_hs_kvs + = mk_tvs (tv : scoped_tv_acc) (tv : imp_tv_acc) + bndrs (all_hs_kvs `delFromNameSet` tv_name) all_hs_tvs -- Case (2) + + | Just tv <- binderVar_maybe bndr + , isInvisibleBinder bndr + = mk_tvs scoped_tv_acc (tv : imp_tv_acc) + bndrs all_hs_kvs all_hs_tvs -- Case (1) + + -- there may actually still be some hs_kvs, if we're kind checking + -- a non-CUSK. The kinds *aren't* generalized, so we won't see them + -- here. + mk_tvs scoped_tv_acc imp_tv_acc all_bndrs all_hs_kvs all_hs_tvs + = let (scoped, exp_tvs, mk_kind) + = mk_tvs2 scoped_tv_acc [] all_bndrs all_hs_tvs in + (scoped, all_hs_kvs, reverse imp_tv_acc, exp_tvs, mk_kind) + -- no more Case (1) or (2) + + -- This can't handle Case (1) or Case (2) from [Typechecking telescopes] + mk_tvs2 :: [TyVar] + -> [TyVar] -- new parameter: explicit tv accum (reversed) + -> [TyBinder] + -> [LHsTyVarBndr Name] + -> ( [TyVar] + , [TyVar] -- explicit tvs only + , Type -> Type ) + mk_tvs2 scoped_tv_acc exp_tv_acc (bndr : bndrs) (hs_tv : hs_tvs) + | Just tv <- binderVar_maybe bndr + = ASSERT2( isVisibleBinder bndr, err_doc ) + ASSERT( getName tv == hsLTyVarName hs_tv ) + mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) bndrs hs_tvs -- Case (3) + + | otherwise + = ASSERT( isVisibleBinder bndr ) + let tv = mkTyVar (hsLTyVarName hs_tv) (binderType bndr) in + mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) bndrs hs_tvs -- Case (4) + where + err_doc = vcat [ ppr (bndr : bndrs) + , ppr (hs_tv : hs_tvs) + , ppr kind + , ppr tvbs ] + + mk_tvs2 scoped_tv_acc exp_tv_acc all_bndrs [] -- All done! + = ( reverse scoped_tv_acc + , reverse exp_tv_acc + , mkForAllTys all_bndrs ) + + mk_tvs2 _ _ all_bndrs all_hs_tvs + = pprPanic "splitTelescopeTvs 2" (vcat [ ppr all_bndrs + , ppr all_hs_tvs ]) + ----------------------- +-- used on first pass only ("kind checking") +kcTyClTyVars :: Name -> LHsQTyVars Name + -> TcM a -> TcM a +kcTyClTyVars tycon hs_tvs thing_inside + = tc_tycl_tyvars False tycon hs_tvs $ \_ _ _ _ -> thing_inside + +-- used on second pass only ("type checking", really desugaring) tcTyClTyVars :: Name -> LHsQTyVars Name -- LHS of the type or class decl - -> ([TyVar] -> Kind -> TcM a) -> TcM a --- Used for the type variables of a type or class decl, --- on the second pass when constructing the final result + -> ([TyVar] -> [TyVar] -> Kind -> Kind -> TcM a) -> TcM a +tcTyClTyVars = tc_tycl_tyvars True + +tc_tycl_tyvars :: Bool -- are we doing the second pass? + -> Name -> LHsQTyVars Name -- LHS of the type or class decl + -> ([TyVar] -> [TyVar] -> Kind -> Kind -> TcM a) -> TcM a +-- Used for the type variables of a type or class decl +-- on both the first and second full passes in TcTyClDecls. +-- *Not* used in the initial-kind run. +-- -- (tcTyClTyVars T [a,b] thing_inside) -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> * -- calls thing_inside with arguments --- [k1,k2,a,b] (k2 -> *) +-- [k1,k2] [a,b] (forall (k1:*) (k2:*) (a:k1 -> *) (b:k1). k2 -> *) (k2 -> *) -- having also extended the type environment with bindings -- for k1,k2,a,b -- -- No need to freshen the k's because they are just skolem -- constants here, and we are at top level anyway. -tcTyClTyVars tycon (HsQTvs { hsq_kvs = hs_kvs, hsq_tvs = hs_tvs }) thing_inside - = kcScopedKindVars hs_kvs $ -- Bind scoped kind vars to fresh kind univ vars - -- There may be fewer of these than the kvs of - -- the type constructor, of course - do { thing <- tcLookup tycon - ; let { kind = case thing of -- The kind of the tycon has been worked out - -- by the previous pass, and is fully zonked - AThing kind -> kind - _ -> panic "tcTyClTyVars" - -- We only call tcTyClTyVars during typechecking in - -- TcTyClDecls, where the local env is extended with - -- the generalized_env (mapping Names to AThings). - ; (kvs, body) = splitForAllTys kind - ; (kinds, res) = splitKindFunTysN (length hs_tvs) body } - ; tvs <- zipWithM tc_hs_tv hs_tvs kinds - ; tcExtendTyVarEnv tvs (thing_inside (kvs ++ tvs) res) } +-- +-- Never emits constraints. +-- +-- The LHsTyVarBndrs is always user-written, and the kind of the tycon +-- is available in the local env. +tc_tycl_tyvars second_pass tycon hs_tvs thing_inside + = do { kind <- kcLookupKind tycon + ; let (scoped_tvs, non_cusk_kv_name_set, all_kvs, all_tvs, res_k) + = splitTelescopeTvs kind hs_tvs + ; traceTc "tcTyClTyVars splitTelescopeTvs:" + (vcat [ text "Tycon:" <+> ppr tycon + , text "Kind:" <+> ppr kind + , text "hs_tvs:" <+> ppr hs_tvs + , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs + , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs + , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs + , text "non-CUSK kvs:" <+> ppr non_cusk_kv_name_set + , text "res_k:" <+> ppr res_k] ) + + -- need to look up the non-cusk kvs in order to get their + -- kinds right, in case the kinds were informed by + -- the getInitialKinds pass + ; let non_cusk_kv_names = nameSetElems non_cusk_kv_name_set + free_kvs = tyCoVarsOfTypes $ + map tyVarKind (all_kvs ++ all_tvs) + lookup nm = case lookupVarSetByName free_kvs nm of + Just tv -> Left tv + Nothing -> Right nm + (non_cusk_kvs, weirds) = partitionWith lookup non_cusk_kv_names + + -- See Note [Free-floating kind vars] TODO (RAE): Write note. + ; weird_kvs <- if second_pass + then do { checkNoErrs $ + mapM_ (report_floating_kv all_tvs) weirds + ; return [] } + else do { ks <- mapM (const newMetaKindVar) weirds + ; return (zipWith new_skolem_tv weirds ks) } + + ; tcExtendTyVarEnv (non_cusk_kvs ++ weird_kvs ++ scoped_tvs) $ + thing_inside (non_cusk_kvs ++ weird_kvs ++ all_kvs) all_tvs kind res_k } where - -- In the case of associated types, the renamer has - -- ensured that the names are in commmon - -- e.g. class C a_29 where - -- type T b_30 a_29 :: * - -- Here the a_29 is shared - tc_hs_tv (L _ (UserTyVar (L _ n))) kind - = return (mkTyVar n kind) - tc_hs_tv (L _ (KindedTyVar (L _ n) hs_k)) kind - = do { tc_kind <- tcLHsKind hs_k - ; checkKind kind tc_kind - ; return (mkTyVar n kind) } + report_floating_kv all_tvs kv_name + = addErr $ + vcat [ text "Kind variable" <+> quotes (ppr kv_name) <+> + text "is implicitly bound in datatype" + , quotes (ppr tycon) <> comma <+> + text "but does not appear as the kind of any" + , text "of its type variables. Perhaps you meant" + , text "to bind it (with TypeInType) explicitly somewhere?" + , if null all_tvs then empty else + hang (text "Type variables with inferred kinds:") + 2 (pprTvBndrs all_tvs) ] ----------------------------------- tcDataKindSig :: Kind -> TcM [TyVar] @@ -1256,6 +1792,7 @@ tcDataKindSig :: Kind -> TcM [TyVar] -- This function makes up suitable (kinded) type variables for -- the argument kinds, and checks that the result kind is indeed *. -- We use it also to make up argument type variables for for data instances. +-- Never emits constraints. tcDataKindSig kind = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind) ; span <- getSrcSpanM @@ -1270,7 +1807,8 @@ tcDataKindSig kind ; return [ mk_tv span uniq occ kind | ((kind, occ), uniq) <- arg_kinds `zip` occs `zip` uniqs ] } where - (arg_kinds, res_kind) = splitKindFunTys kind + (bndrs, res_kind) = splitPiTys kind + arg_kinds = map binderType bndrs mk_tv loc uniq occ kind = mkTyVar (mkInternalName uniq occ loc) kind @@ -1340,45 +1878,44 @@ Historical note: tcHsPatSigType :: UserTypeCtxt -> LHsSigWcType Name -- The type signature -> TcM ( Type -- The signature - , [(Name, TcTyVar)] -- The new bit of type environment, binding - -- the scoped type variables + , [TcTyVar] -- The new bit of type environment, binding + -- the scoped type variables , [(Name, TcTyVar)] ) -- The wildcards -- Used for type-checking type signatures in -- (a) patterns e.g f (x::Int) = e --- (b) result signatures e.g. g x :: Int = e --- (c) RULE forall bndrs e.g. forall (x::Int). f x = x +-- (b) RULE forall bndrs e.g. forall (x::Int). f x = x +-- +-- This may emit constraints tcHsPatSigType ctxt sig_ty - | HsIB { hsib_kvs = sig_kvs, hsib_tvs = sig_tvs, hsib_body = wc_ty } <- sig_ty - , HsWC { hswc_wcs = sig_wcs, hswc_ctx = extra, hswc_body = hs_ty } <- wc_ty + | HsIB { hsib_vars = sig_vars, hsib_body = wc_ty } <- sig_ty + , HsWC { hswc_wcs = sig_wcs, hswc_ctx = extra, hswc_body = hs_ty } <- wc_ty = ASSERT( isNothing extra ) -- No extra-constraint wildcard in pattern sigs addSigCtxt ctxt hs_ty $ tcWildCardBinders sig_wcs $ \ wcs -> do { emitWildCardHoleConstraints wcs - ; kvs <- mapM new_kv sig_kvs - ; tvs <- mapM new_tv sig_tvs - ; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` tvs) - ; sig_ty <- tcExtendTyVarEnv2 ktv_binds $ - tcHsLiftedType hs_ty - ; sig_ty <- zonkSigType sig_ty + ; (vars, sig_ty) <- tcImplicitTKBndrsX new_tkv sig_vars $ + do { ty <- tcHsLiftedType hs_ty + ; return (ty, allBoundVariables ty) } + ; sig_ty <- zonkTcType sig_ty + -- don't use zonkTcTypeToType; it mistreats wildcards ; checkValidType ctxt sig_ty - ; traceTc "tcHsPatSigType" (ppr sig_tvs $$ ppr ktv_binds) - ; return (sig_ty, ktv_binds, wcs) } + ; traceTc "tcHsPatSigType" (ppr sig_vars) + ; return (sig_ty, vars, wcs) } where - new_kv name = new_tkv name superKind - new_tv name = do { kind <- newMetaKindVar - ; new_tkv name kind } - - new_tkv name kind -- See Note [Pattern signature binders] - = case ctxt of - RuleSigCtxt {} -> return (mkTcTyVar name kind (SkolemTv False)) - _ -> newSigTyVar name kind -- See Note [Unifying SigTvs] + new_tkv name -- See Note [Pattern signature binders] + = (, False) <$> -- "False" means that these tyvars aren't yet in scope + do { kind <- newMetaKindVar + ; case ctxt of + RuleSigCtxt {} -> return $ new_skolem_tv name kind + _ -> newSigTyVar name kind } + -- See Note [Unifying SigTvs] tcPatSig :: Bool -- True <=> pattern binding -> LHsSigWcType Name -> TcSigmaType -> TcM (TcType, -- The type to use for "inside" the signature - [(Name, TcTyVar)], -- The new bit of type environment, binding + [TcTyVar], -- The new bit of type environment, binding -- the scoped type variables [(Name, TcTyVar)], -- The wildcards HsWrapper) -- Coercion due to unification with actual ty @@ -1409,8 +1946,8 @@ tcPatSig in_pat_bind sig res_ty -- f :: Int -> Int -- f (x :: T a) = ... -- Here 'a' doesn't get a binding. Sigh - ; let bad_tvs = [ tv | (_, tv) <- sig_tvs - , not (tv `elemVarSet` exactTyVarsOfType sig_ty) ] + ; let bad_tvs = [ tv | tv <- sig_tvs + , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ] ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs) -- Now do a subsumption check of the pattern signature against res_ty @@ -1430,10 +1967,10 @@ tcPatSig in_pat_bind sig res_ty 2 (ppr res_ty)) ] ; return (tidy_env, msg) } -patBindSigErr :: [(Name, TcTyVar)] -> SDoc +patBindSigErr :: [TcTyVar] -> SDoc patBindSigErr sig_tvs = hang (ptext (sLit "You cannot bind scoped type variable") <> plural sig_tvs - <+> pprQuotedList (map fst sig_tvs)) + <+> pprQuotedList sig_tvs) 2 (ptext (sLit "in a pattern binding signature")) {- @@ -1486,142 +2023,19 @@ in-scope variables that it should not unify with, but it's fiddly. * * ************************************************************************ -We would like to get a decent error message from - (a) Under-applied type constructors - f :: (Maybe, Maybe) - (b) Over-applied type constructors - f :: Int x -> Int x -} --- The ExpKind datatype means "expected kind" and contains --- some info about just why that kind is expected, to improve --- the error message on a mis-match -data ExpKind = EK TcKind (TcKind -> SDoc) - -- The second arg is function that takes a *tidied* version - -- of the first arg, and produces something like - -- "Expected kind k" - -- "Expected a constraint" - -- "The argument of Maybe should have kind k" - -instance Outputable ExpKind where - ppr (EK k f) = f k - -ekLifted, ekOpen, ekConstraint :: ExpKind -ekLifted = EK liftedTypeKind expectedKindMsg -ekOpen = EK openTypeKind expectedKindMsg -ekConstraint = EK constraintKind expectedKindMsg - -expectedKindMsg :: TcKind -> SDoc -expectedKindMsg pkind - | isConstraintKind pkind = ptext (sLit "Expected a constraint") - | isOpenTypeKind pkind = ptext (sLit "Expected a type") - | otherwise = ptext (sLit "Expected kind") <+> quotes (pprKind pkind) - --- Build an ExpKind for arguments -expArgKind :: SDoc -> TcKind -> Int -> ExpKind -expArgKind exp kind arg_no = EK kind msg_fn - where - msg_fn pkind - = sep [ ptext (sLit "The") <+> speakNth arg_no - <+> ptext (sLit "argument of") <+> exp - , nest 2 $ ptext (sLit "should have kind") - <+> quotes (pprKind pkind) ] - -unifyKinds :: SDoc -> [LHsType Name] -> [TcKind] -> TcM TcKind -unifyKinds fun hs_tys act_kinds +-- | Produce an 'TcKind' suitable for a checking a type that can be * or #. +ekOpen :: TcM TcKind +ekOpen = do { lev <- newFlexiTyVarTy levityTy + ; return (tYPE lev) } + +unifyKinds :: [(TcType, TcKind)] -> TcM ([TcType], TcKind) +unifyKinds act_kinds = do { kind <- newMetaKindVar - ; let check (arg_no, L _ hs_ty, act_kind) - = checkExpectedKind hs_ty act_kind (expArgKind (quotes fun) kind arg_no) - ; mapM_ check (zip3 [1..] hs_tys act_kinds) - ; return kind } - -checkKind :: TcKind -> TcKind -> TcM () -checkKind act_kind exp_kind - = do { mb_subk <- unifyKindX act_kind exp_kind - ; case mb_subk of - Just EQ -> return () - _ -> unifyKindMisMatch act_kind exp_kind } - -checkExpectedKind :: HsType Name -> TcKind -> ExpKind -> TcM () --- A fancy wrapper for 'unifyKindX', which tries --- to give decent error messages. --- (checkExpectedKind ty act_kind exp_kind) --- checks that the actual kind act_kind is compatible --- with the expected kind exp_kind --- The first argument, ty, is used only in the error message generation -checkExpectedKind ty act_kind (EK exp_kind ek_ctxt) - = do { mb_subk <- unifyKindX act_kind exp_kind - - -- Kind unification only generates definite errors - ; case mb_subk of { - Just LT -> return () ; -- act_kind is a sub-kind of exp_kind - Just EQ -> return () ; -- The two are equal - _other -> do - - { -- So there's an error - -- Now to find out what sort - exp_kind <- zonkTcKind exp_kind - ; act_kind <- zonkTcKind act_kind - ; traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr exp_kind) - ; env0 <- tcInitTidyEnv - ; dflags <- getDynFlags - ; let (exp_as, _) = splitKindFunTys exp_kind - (act_as, _) = splitKindFunTys act_kind - n_exp_as = length exp_as - n_act_as = length act_as - n_diff_as = n_act_as - n_exp_as - - (env1, tidy_exp_kind) = tidyOpenKind env0 exp_kind - (env2, tidy_act_kind) = tidyOpenKind env1 act_kind - - occurs_check - | Just act_tv <- tcGetTyVar_maybe act_kind - = check_occ act_tv exp_kind - | Just exp_tv <- tcGetTyVar_maybe exp_kind - = check_occ exp_tv act_kind - | otherwise - = False - - check_occ tv k = case occurCheckExpand dflags tv k of - OC_Occurs -> True - _bad -> False - - err | occurs_check -- Must precede the "more args expected" check - = ptext (sLit "Kind occurs check") $$ more_info - - | n_exp_as < n_act_as -- E.g. [Maybe] - = vcat [ ptext (sLit "Expecting") <+> - speakN n_diff_as <+> ptext (sLit "more argument") - <> (if n_diff_as > 1 then char 's' else empty) - <+> ptext (sLit "to") <+> quotes (ppr ty) - , more_info ] - - -- Now n_exp_as >= n_act_as. In the next two cases, - -- n_exp_as == 0, and hence so is n_act_as - | otherwise -- E.g. Monad [Int] - = more_info - - more_info - | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind - = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty) - <+> ptext (sLit "is unlifted") - - | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind - = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty) - <+> ptext (sLit "is lifted") - - | isSubOpenTypeKind exp_kind - , isConstraintKind act_kind - = ptext (sLit "Constraint") <+> quotes (ppr ty) - <+> ptext (sLit "used as a type") - - | otherwise - = sep [ ek_ctxt tidy_exp_kind <> comma - , nest 2 $ ptext (sLit "but") <+> quotes (ppr ty) - <+> ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind) ] - - ; traceTc "checkExpectedKind 1" (ppr ty $$ ppr tidy_act_kind $$ ppr tidy_exp_kind $$ ppr env1 $$ ppr env2) - ; failWithTcM (env2, err) } } } + ; let check (ty, act_kind) = checkExpectedKind ty act_kind kind + ; tys' <- mapM check act_kinds + ; return (tys', kind) } {- ************************************************************************ @@ -1632,113 +2046,15 @@ checkExpectedKind ty act_kind (EK exp_kind ek_ctxt) tcLHsKind converts a user-written kind to an internal, sort-checked kind. It does sort checking and desugaring at the same time, in one single pass. -It fails when the kinds are not well-formed (eg. data A :: * Int), or if there -are non-promotable or non-fully applied kinds. -} tcLHsKind :: LHsKind Name -> TcM Kind -tcLHsKind k = addErrCtxt (ptext (sLit "In the kind") <+> quotes (ppr k)) $ - tc_lhs_kind k +tcLHsKind = tc_lhs_kind kindLevelMode -tc_lhs_kind :: LHsKind Name -> TcM Kind -tc_lhs_kind (L span ki) = setSrcSpan span (tc_hs_kind ki) - --- The main worker -tc_hs_kind :: HsKind Name -> TcM Kind -tc_hs_kind (HsTyVar (L _ tc)) = tc_kind_var_app tc [] -tc_hs_kind k@(HsAppTy _ _) = tc_kind_app k [] - -tc_hs_kind (HsParTy ki) = tc_lhs_kind ki - -tc_hs_kind (HsFunTy ki1 ki2) = - do kappa_ki1 <- tc_lhs_kind ki1 - kappa_ki2 <- tc_lhs_kind ki2 - return (mkArrowKind kappa_ki1 kappa_ki2) - -tc_hs_kind (HsListTy ki) = - do kappa <- tc_lhs_kind ki - checkWiredInTyCon listTyCon - return $ mkPromotedListTy kappa - -tc_hs_kind (HsTupleTy _ kis) = - do kappas <- mapM tc_lhs_kind kis - checkWiredInTyCon tycon - return $ mkTyConApp tycon kappas - where - tycon = promotedTupleTyCon Boxed (length kis) - --- Argument not kind-shaped -tc_hs_kind k = pprPanic "tc_hs_kind" (ppr k) - --- Special case for kind application -tc_kind_app :: HsKind Name -> [LHsKind Name] -> TcM Kind -tc_kind_app (HsAppTy ki1 ki2) kis = tc_kind_app (unLoc ki1) (ki2:kis) -tc_kind_app (HsTyVar (L _ tc)) kis = do { arg_kis <- mapM tc_lhs_kind kis - ; tc_kind_var_app tc arg_kis } -tc_kind_app ki _ = failWithTc (quotes (ppr ki) <+> - ptext (sLit "is not a kind constructor")) - -tc_kind_var_app :: Name -> [Kind] -> TcM Kind --- Special case for * and Constraint kinds --- They are kinds already, so we don't need to promote them -tc_kind_var_app name arg_kis - | name == liftedTypeKindTyConName - || name == constraintKindTyConName - = do { unless (null arg_kis) - (failWithTc (text "Kind" <+> ppr name <+> text "cannot be applied")) - ; thing <- tcLookup name - ; case thing of - AGlobal (ATyCon tc) -> return (mkTyConApp tc []) - _ -> panic "tc_kind_var_app 1" } - --- General case -tc_kind_var_app name arg_kis - = do { thing <- tcLookup name - ; case thing of - AGlobal (ATyCon tc) - -> do { data_kinds <- xoptM Opt_DataKinds - ; unless data_kinds $ addErr (dataKindsErr name) - ; case promotableTyCon_maybe tc of - Promoted prom_tc | arg_kis `lengthIs` tyConArity prom_tc - -> return (mkTyConApp prom_tc arg_kis) - Promoted _ -> tycon_err tc "is not fully applied" - NotPromoted -> tycon_err tc "is not promotable" } - - -- A lexically scoped kind variable - ATyVar _ kind_var - | not (isKindVar kind_var) - -> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr kind_var) - <+> ptext (sLit "used as a kind")) - | not (null arg_kis) -- Kind variables always have kind BOX, - -- so cannot be applied to anything - -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr name) - <+> ptext (sLit "cannot appear in a function position")) - | otherwise - -> return (mkAppTys (mkTyVarTy kind_var) arg_kis) - - -- It is in scope, but not what we expected - AThing _ - | isTyVarName name - -> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr name) - <+> ptext (sLit "used in a kind")) - | otherwise - -> failWithTc (hang (ptext (sLit "Type constructor") <+> quotes (ppr name) - <+> ptext (sLit "used in a kind")) - 2 (ptext (sLit "inside its own recursive group"))) - - APromotionErr err -> promotionErr name err - - _ -> wrongThingErr "promoted type" thing name - -- This really should not happen - } - where - tycon_err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind") - <+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg)) - -dataKindsErr :: Name -> SDoc -dataKindsErr name - = hang (ptext (sLit "Illegal kind:") <+> quotes (ppr name)) - 2 (ptext (sLit "Perhaps you intended to use DataKinds")) +tc_lhs_kind :: TcTyMode -> LHsKind Name -> TcM Kind +tc_lhs_kind mode k + = addErrCtxt (ptext (sLit "In the kind") <+> quotes (ppr k)) $ + tc_lhs_type (kindLevel mode) k liftedTypeKind promotionErr :: Name -> PromotionErr -> TcM a promotionErr name err @@ -1746,9 +2062,11 @@ promotionErr name err 2 (parens reason)) where reason = case err of - FamDataConPE -> ptext (sLit "it comes from a data family instance") - NoDataKinds -> ptext (sLit "Perhaps you intended to use DataKinds") - _ -> ptext (sLit "it is defined and used in the same recursive group") + FamDataConPE -> text "it comes from a data family instance" + NoDataKinds -> text "Perhaps you intended to use DataKinds" + NoTypeInTypeTC -> text "Perhaps you intended to use TypeInType" + NoTypeInTypeDC -> text "Perhaps you intended to use TypeInType" + _ -> text "it is defined and used in the same recursive group" {- ************************************************************************ @@ -1767,12 +2085,18 @@ badPatSigTvs sig_ty bad_tvs , ptext (sLit "To fix this, expand the type synonym") , ptext (sLit "[Note: I hope to lift this restriction in due course]") ] -unifyKindMisMatch :: TcKind -> TcKind -> TcM a -unifyKindMisMatch ki1 ki2 = do - ki1' <- zonkTcKind ki1 - ki2' <- zonkTcKind ki2 - let msg = hang (ptext (sLit "Couldn't match kind")) - 2 (sep [quotes (ppr ki1'), - ptext (sLit "against"), - quotes (ppr ki2')]) - failWithTc msg +{- +************************************************************************ +* * + Error messages and such +* * +************************************************************************ +-} + +-- | Make an appropriate message for an error in a function argument. +-- Used for both expressions and types. +funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc +funAppCtxt fun arg arg_no + = hang (hsep [ ptext (sLit "In the"), speakNth arg_no, ptext (sLit "argument of"), + quotes (ppr fun) <> text ", namely"]) + 2 (quotes (ppr arg)) |