X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcHsType.lhs;h=2174be39206ccea4fd5d633d266b70984f6b8735;hp=64da3c0f6e5e06bf54109d73caa64da3101eb26a;hb=b2524b3960999fffdb3767900f58825903f6560f;hpb=6f8ff0bbad3b9fa389c960ad1b5a267a1ae502f1 diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index 64da3c0..2174be3 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -16,7 +16,7 @@ module TcHsType ( -- Typechecking kinded types tcHsKindedContext, tcHsKindedType, tcHsBangType, - tcTyVarBndrs, dsHsType, tcLHsConResTy, + tcTyVarBndrs, dsHsType, kcHsLPred, dsHsLPred, tcDataKindSig, ExpKind(..), EkCtxt(..), -- Pattern type signatures @@ -37,15 +37,14 @@ import TcMType import TcUnify import TcIface import TcType +import TypeRep ( ecKind ) import {- Kind parts of -} Type import Var import VarSet -import Coercion import TyCon import Class import Name import NameSet -import PrelNames import TysWiredIn import BasicTypes import SrcLoc @@ -156,29 +155,36 @@ tcHsSigTypeNC ctxt hs_ty ; checkValidType ctxt ty ; return ty } -tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Type) +tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type]) -- Typecheck an instance head. We can't use -- tcHsSigType, because it's not a valid user type. -tcHsInstHead (L loc ty) +tcHsInstHead (L loc hs_ty) = setSrcSpan loc $ -- No need for an "In the type..." context - tc_inst_head ty -- because that comes from the caller + -- because that comes from the caller + do { kinded_ty <- kc_inst_head hs_ty + ; ds_inst_head kinded_ty } where - -- tc_inst_head expects HsPredTy, which isn't usually even allowed - tc_inst_head (HsPredTy pred) - = do { pred' <- kcHsPred pred - ; pred'' <- dsHsPred pred' - ; return ([], [], mkPredTy pred'') } - - tc_inst_head (HsForAllTy _ tvs ctxt (L _ (HsPredTy pred))) - = kcHsTyVars tvs $ \ tvs' -> - do { ctxt' <- kcHsContext ctxt - ; pred' <- kcHsPred pred - ; tcTyVarBndrs tvs' $ \ tvs'' -> - do { ctxt'' <- mapM dsHsLPred (unLoc ctxt') - ; pred'' <- dsHsPred pred' - ; return (tvs'', ctxt'', mkPredTy pred'') } } - - tc_inst_head _ = failWithTc (ptext (sLit "Malformed instance type")) + kc_inst_head ty@(HsPredTy pred@(HsClassP {})) + = do { (pred', kind) <- kc_pred pred + ; checkExpectedKind ty kind ekLifted + ; return (HsPredTy pred') } + kc_inst_head (HsForAllTy exp tv_names context (L loc ty)) + = kcHsTyVars tv_names $ \ tv_names' -> + do { ctxt' <- kcHsContext context + ; ty' <- kc_inst_head ty + ; return (HsForAllTy exp tv_names' ctxt' (L loc ty')) } + kc_inst_head _ = failWithTc (ptext (sLit "Malformed instance type")) + + ds_inst_head (HsPredTy (HsClassP cls_name tys)) + = do { clas <- tcLookupClass cls_name + ; arg_tys <- dsHsTypes tys + ; return ([], [], clas, arg_tys) } + ds_inst_head (HsForAllTy _ tvs ctxt (L _ tau)) + = tcTyVarBndrs tvs $ \ tvs' -> + do { ctxt' <- mapM dsHsLPred (unLoc ctxt) + ; (tvs_r, ctxt_r, cls, tys) <- ds_inst_head tau + ; return (tvs' ++ tvs_r, ctxt' ++ ctxt_r , cls, tys) } + ds_inst_head _ = panic "ds_inst_head" tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type) -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty), @@ -359,8 +365,10 @@ kc_hs_type (HsPArrTy ty) = do ty' <- kcLiftedType ty return (HsPArrTy ty', liftedTypeKind) -kc_hs_type (HsNumTy n) - = return (HsNumTy n, liftedTypeKind) +kc_hs_type (HsModalBoxType ecn ty) = do + kc_check_hs_type (HsTyVar ecn) (EK ecKind EkUnk) + ty' <- kcLiftedType ty + return (HsModalBoxType ecn ty', liftedTypeKind) kc_hs_type (HsKindSig ty k) = do ty' <- kc_check_lhs_type ty (EK k EkKindSig) @@ -394,6 +402,9 @@ kc_hs_type (HsAppTy ty1 ty2) = do kc_hs_type (HsPredTy pred) = wrongPredErr pred +kc_hs_type (HsCoreTy ty) + = return (HsCoreTy ty, typeKind ty) + kc_hs_type (HsForAllTy exp tv_names context ty) = kcHsTyVars tv_names $ \ tv_names' -> do { ctxt' <- kcHsContext context @@ -419,12 +430,11 @@ kc_hs_type ty@(HsRecTy _) -- should have been removed by now #ifdef GHCI /* Only if bootstrapped */ -kc_hs_type (HsSpliceTy sp) = kcSpliceType sp +kc_hs_type (HsSpliceTy sp fvs _) = kcSpliceType sp fvs #else kc_hs_type ty@(HsSpliceTy {}) = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty) #endif -kc_hs_type (HsSpliceTyOut {}) = panic "kc_hs_type" -- Should not happen at all kc_hs_type (HsQuasiQuoteTy {}) = panic "kc_hs_type" -- Eliminated by renamer -- remove the doc nodes here, no need to worry about the location since @@ -473,7 +483,7 @@ mkHsAppTys fun_ty (arg_ty:arg_tys) splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind) splitFunKind _ _ fk [] = return ([], fk) splitFunKind the_fun arg_no fk (arg:args) - = do { mb_fk <- unifyFunKind fk + = do { mb_fk <- matchExpectedFunKind fk ; case mb_fk of Nothing -> failWithTc too_many_args Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args @@ -490,9 +500,9 @@ kcHsLPred :: LHsPred Name -> TcM (LHsPred Name) kcHsLPred = wrapLocM kcHsPred kcHsPred :: HsPred Name -> TcM (HsPred Name) -kcHsPred pred = do -- Checks that the result is of kind liftedType +kcHsPred pred = do -- Checks that the result is a type kind (pred', kind) <- kc_pred pred - checkExpectedKind pred kind ekLifted + checkExpectedKind pred kind ekOpen return pred' --------------------------- @@ -501,28 +511,23 @@ kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind) -- application (reason: used from TcDeriv) kc_pred (HsIParam name ty) = do { (ty', kind) <- kc_lhs_type ty - ; return (HsIParam name ty', kind) - } + ; return (HsIParam name ty', kind) } kc_pred (HsClassP cls tys) = do { kind <- kcClass cls ; (tys', res_kind) <- kcApps cls kind tys - ; return (HsClassP cls tys', res_kind) - } + ; return (HsClassP cls tys', res_kind) } kc_pred (HsEqualP ty1 ty2) = do { (ty1', kind1) <- kc_lhs_type ty1 --- ; checkExpectedKind ty1 kind1 liftedTypeKind ; (ty2', kind2) <- kc_lhs_type ty2 --- ; checkExpectedKind ty2 kind2 liftedTypeKind ; checkExpectedKind ty2 kind2 (EK kind1 EkEqPred) - ; return (HsEqualP ty1' ty2', liftedTypeKind) - } + ; return (HsEqualP ty1' ty2', unliftedTypeKind) } --------------------------- kcTyVar :: Name -> TcM TcKind kcTyVar name = do -- Could be a tyvar or a tycon - traceTc (text "lk1" <+> ppr name) + traceTc "lk1" (ppr name) thing <- tcLookup name - traceTc (text "lk2" <+> ppr name <+> ppr thing) + traceTc "lk2" (ppr name <+> ppr thing) case thing of ATyVar _ ty -> return (typeKind ty) AThing kind -> return kind @@ -586,6 +591,11 @@ ds_type (HsPArrTy ty) = do checkWiredInTyCon parrTyCon return (mkPArrTy tau_ty) +ds_type (HsModalBoxType ecn ty) = do + tau_ty <- dsHsType ty + checkWiredInTyCon hetMetCodeTypeTyCon + return (mkHetMetCodeTypeTy (mkTyVar ecn ecKind) tau_ty) + ds_type (HsTupleTy boxity tys) = do tau_tys <- dsHsTypes tys checkWiredInTyCon tycon @@ -603,11 +613,6 @@ ds_type (HsOpTy ty1 (L span op) ty2) = do tau_ty2 <- dsHsType ty2 setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2]) -ds_type (HsNumTy n) - = ASSERT(n==1) do - tc <- tcLookupTyCon genUnitTyConName - return (mkTyConApp tc []) - ds_type ty@(HsAppTy _ _) = ds_app ty [] @@ -624,12 +629,12 @@ ds_type (HsForAllTy _ tv_names ctxt ty) ds_type (HsDocTy ty _) -- Remove the doc comment = dsHsType ty -ds_type (HsSpliceTyOut kind) +ds_type (HsSpliceTy _ _ kind) = do { kind' <- zonkTcKindToKind kind ; newFlexiTyVarTy kind' } -ds_type (HsSpliceTy {}) = panic "ds_type" ds_type (HsQuasiQuoteTy {}) = panic "ds_type" -- Eliminated by renamer +ds_type (HsCoreTy ty) = return ty dsHsTypes :: [LHsType Name] -> TcM [Type] dsHsTypes arg_tys = mapM dsHsType arg_tys @@ -684,35 +689,7 @@ dsHsPred (HsIParam name ty) } \end{code} -GADT constructor signatures - \begin{code} -tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType]) -tcLHsConResTy (L span res_ty) - = setSrcSpan span $ - case get_args res_ty [] of - (HsTyVar tc_name, args) - -> do { args' <- mapM dsHsType args - ; thing <- tcLookup tc_name - ; case thing of - AGlobal (ATyCon tc) -> return (tc, args') - _ -> failWithTc (badGadtDecl res_ty) } - _ -> failWithTc (badGadtDecl res_ty) - where - -- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe - -- because that causes a black hole, and for good reason. Building - -- the type means expanding type synonyms, and we can't do that - -- inside the "knot". So we have to work by steam. - get_args (HsAppTy (L _ fun) arg) args = get_args fun (arg:args) - get_args (HsParTy (L _ ty)) args = get_args ty args - get_args (HsOpTy ty1 (L _ tc) ty2) args = (HsTyVar tc, ty1:ty2:args) - get_args ty args = (ty, args) - -badGadtDecl :: HsType Name -> SDoc -badGadtDecl ty - = hang (ptext (sLit "Malformed constructor result type:")) - 2 (ppr ty) - addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a -- Wrap a context around only if we want to show that contexts. addKcTypeCtxt (L _ (HsPredTy _)) thing = thing @@ -735,14 +712,14 @@ kcHsTyVars :: [LHsTyVarBndr Name] -> ([LHsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated -- They scope over the thing inside -> TcM r -kcHsTyVars tvs thing_inside = do - bndrs <- mapM (wrapLocM kcHsTyVar) tvs - tcExtendKindEnvTvs bndrs (thing_inside bndrs) +kcHsTyVars tvs thing_inside + = do { kinded_tvs <- mapM (wrapLocM kcHsTyVar) tvs + ; tcExtendKindEnvTvs kinded_tvs thing_inside } kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name) -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it -kcHsTyVar (UserTyVar name) = KindedTyVar name <$> newKindVar -kcHsTyVar (KindedTyVar name kind) = return (KindedTyVar name kind) +kcHsTyVar (UserTyVar name _) = UserTyVar name <$> newKindVar +kcHsTyVar tv@(KindedTyVar {}) = return tv ------------------ tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking @@ -754,10 +731,9 @@ tcTyVarBndrs bndrs thing_inside = do tyvars <- mapM (zonk . unLoc) bndrs tcExtendTyVarEnv tyvars (thing_inside tyvars) where - zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind - ; return (mkTyVar name kind') } - zonk (UserTyVar name) = WARN( True, ptext (sLit "Un-kinded tyvar") <+> ppr name ) - return (mkTyVar name liftedTypeKind) + zonk (UserTyVar name kind) = do { kind' <- zonkTcKindToKind kind + ; return (mkTyVar name kind') } + zonk (KindedTyVar name kind) = return (mkTyVar name kind) ----------------------------------- tcDataKindSig :: Maybe Kind -> TcM [TyVar] @@ -867,9 +843,9 @@ tcHsPatSigType ctxt hs_ty -- should be bound by the pattern signature in_scope <- getInLocalScope ; let span = getLoc hs_ty - sig_tvs = [ L span (UserTyVar n) - | n <- nameSetToList (extractHsTyVars hs_ty), - not (in_scope n) ] + sig_tvs = userHsTyVarBndrs $ map (L span) $ + filterOut in_scope $ + nameSetToList (extractHsTyVars hs_ty) ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty ; checkValidType ctxt sig_ty @@ -878,21 +854,24 @@ tcHsPatSigType ctxt hs_ty tcPatSig :: UserTypeCtxt -> LHsType Name - -> BoxySigmaType + -> TcSigmaType -> TcM (TcType, -- The type to use for "inside" the signature [(Name, TcType)], -- The new bit of type environment, binding -- the scoped type variables - CoercionI) -- Coercion due to unification with actual ty + HsWrapper) -- Coercion due to unification with actual ty + -- Of shape: res_ty ~ sig_ty tcPatSig ctxt sig res_ty = do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig + -- sig_tvs are the type variables free in 'sig', + -- and not already in scope. These are the ones + -- that should be brought into scope ; if null sig_tvs then do { -- The type signature binds no type variables, -- and hence is rigid, so use it to zap the res_ty - coi <- boxyUnify sig_ty res_ty - ; return (sig_ty, [], coi) - - } else do { + wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty + ; return (sig_ty, [], wrap) + } else do { -- Type signature binds at least one scoped type variable -- A pattern binding cannot bind scoped type variables @@ -904,9 +883,6 @@ tcPatSig ctxt sig res_ty _ -> False ; ASSERT( not in_pat_bind || null sig_tvs ) return () - -- Check that pat_ty is rigid - ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs) - -- Check that all newly-in-scope tyvars are in fact -- constrained by the pattern. This catches tiresome -- cases like @@ -917,41 +893,32 @@ tcPatSig ctxt sig res_ty ; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs) - -- Now match the pattern signature against res_ty - -- For convenience, and uniform-looking error messages - -- we do the matching by allocating meta type variables, - -- unifying, and reading out the results. - -- This is a strictly local operation. - ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs - ; coi <- boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) - res_ty - ; sig_tv_tys <- mapM readFilledBox box_tvs - - -- Check that each is bound to a distinct type variable, - -- and one that is not already in scope - ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys - ; binds_in_scope <- getScopedTyVarBinds + -- Now do a subsumption check of the pattern signature against res_ty + ; sig_tvs' <- tcInstSigTyVars sig_tvs + ; let sig_ty' = substTyWith sig_tvs sig_tv_tys' sig_ty + sig_tv_tys' = mkTyVarTys sig_tvs' + ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty' + + -- Check that each is bound to a distinct type variable, + -- and one that is not already in scope + ; binds_in_scope <- getScopedTyVarBinds + ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys' ; check binds_in_scope tv_binds - -- Phew! - ; return (res_ty, tv_binds, coi) - } } + -- Phew! + ; return (sig_ty', tv_binds, wrap) + } } where check _ [] = return () check in_scope ((n,ty):rest) = do { check_one in_scope n ty ; check ((n,ty):in_scope) rest } check_one in_scope n ty - = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty) - -- Must bind to a type variable - - ; checkTc (null dups) (dupInScope n (head dups) ty) + = checkTc (null dups) (dupInScope n (head dups) ty) -- Must not bind to the same type variable -- as some other in-scope type variable - - ; return () } where - dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty] + dups = [n' | (n',ty') <- in_scope, eqType ty' ty] \end{code} @@ -1061,12 +1028,6 @@ pprHsSigCtxt ctxt hs_ty = sep [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> co pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty) -wobblyPatSig :: [Var] -> SDoc -wobblyPatSig sig_tvs - = hang (ptext (sLit "A pattern type signature cannot bind scoped type variables") - <+> pprQuotedList sig_tvs) - 2 (ptext (sLit "unless the pattern has a rigid type context")) - badPatSigTvs :: TcType -> [TyVar] -> SDoc badPatSigTvs sig_ty bad_tvs = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs, @@ -1076,12 +1037,6 @@ 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]") ] -scopedNonVar :: Name -> Type -> SDoc -scopedNonVar n ty - = vcat [sep [ptext (sLit "The scoped type variable") <+> quotes (ppr n), - nest 2 (ptext (sLit "is bound to the type") <+> quotes (ppr ty))], - nest 2 (ptext (sLit "You can only bind scoped type variables to type variables"))] - dupInScope :: Name -> Name -> Type -> SDoc dupInScope n n' _ = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))