X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=08a3cbd6ee79fed2654b87f13126d27208ddac8e;hb=2da37f4f15790377900fa6c38ff8fdcd394dfaa2;hp=1addfe4f1be1ef04013beb04787c57f1bd0eec52;hpb=f16dbbbe59cf3aa19c5fd384560a1b89076d7bc8;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 1addfe4..08a3cbd 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -35,16 +35,17 @@ module TcMType ( tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, tcInstSigType, tcInstSkolTyVars, tcInstSkolType, - tcSkolSigType, tcSkolSigTyVars, occurCheckErr, + tcSkolSigType, tcSkolSigTyVars, occurCheckErr, execTcTyVarBinds, -------------------------------- -- Checking type validity Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, checkValidInstance, - checkInstTermination, checkValidTypeInst, checkTyFamFreeness, + checkInstTermination, checkValidTypeInst, checkTyFamFreeness, checkKinds, checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt, unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs, + growPredTyVars, growTyVars, growThetaTyVars, -------------------------------- -- Zonking @@ -77,6 +78,7 @@ import VarSet import ErrUtils import DynFlags import Util +import Bag import Maybes import ListSetOps import UniqSupply @@ -336,6 +338,27 @@ Rather, we should bind t to () (= non_var_ty2). -------------- +Execute a bag of type variable bindings. + +\begin{code} +execTcTyVarBinds :: TcTyVarBinds -> TcM () +execTcTyVarBinds = mapM_ execTcTyVarBind . bagToList + where + execTcTyVarBind (TcTyVarBind tv ty) + = do { ASSERTM2( do { details <- readMetaTyVar tv + ; return (isFlexi details) }, ppr tv ) + ; ty' <- if isCoVar tv + then return ty + else do { maybe_ty <- checkTauTvUpdate tv ty + ; case maybe_ty of + Nothing -> pprPanic "TcRnMonad.execTcTyBind" + (ppr tv <+> text ":=" <+> ppr ty) + Just ty' -> return ty' + } + ; writeMetaTyVar tv ty' + } +\end{code} + Error mesages in case of kind mismatch. \begin{code} @@ -521,13 +544,17 @@ writeMetaTyVar tyvar ty return () | otherwise = ASSERT( isMetaTyVar tyvar ) - -- TOM: It should also work for coercions - -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) ) - do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar ) + ASSERT2( isCoVar tyvar || typeKind ty `isSubKind` tyVarKind tyvar, + (ppr tyvar <+> ppr (tyVarKind tyvar)) + $$ (ppr ty <+> ppr (typeKind ty)) ) + do { if debugIsOn then do { details <- readMetaTyVar tyvar; +-- FIXME ; ASSERT2( not (isFlexi details), ppr tyvar ) + ; WARN( not (isFlexi details), ppr tyvar ) + return () } + else return () + + ; traceTc (text "writeMetaTyVar" <+> ppr tyvar <+> text ":=" <+> ppr ty) ; writeMutVar (metaTvRef tyvar) (Indirect ty) } - where - _k1 = tyVarKind tyvar - _k2 = typeKind ty \end{code} @@ -762,8 +789,11 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- -- We leave skolem TyVars alone; they are immutable. zonkQuantifiedTyVar tv - | ASSERT( isTcTyVar tv ) - isSkolemTyVar tv = return tv + | ASSERT2( isTcTyVar tv, ppr tv ) + isSkolemTyVar tv + = do { kind <- zonkTcType (tyVarKind tv) + ; return $ setTyVarKind tv kind + } -- It might be a skolem type variable, -- for example from a user type signature @@ -895,12 +925,14 @@ zonkType unbound_var_fn ty -- The two interesting cases! go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar - | otherwise = return (TyVarTy tyvar) + | otherwise = liftM TyVarTy $ + zonkTyVar unbound_var_fn tyvar -- Ordinary (non Tc) tyvars occur inside quantified types go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do ty' <- go ty - return (ForAllTy tyvar ty') + tyvar' <- zonkTyVar unbound_var_fn tyvar + return (ForAllTy tyvar' ty') go_pred (ClassP c tys) = do tys' <- mapM go tys return (ClassP c tys') @@ -910,7 +942,7 @@ zonkType unbound_var_fn ty ty2' <- go ty2 return (EqPred ty1' ty2') -zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable +zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var -> TcTyVar -> TcM TcType zonk_tc_tyvar unbound_var_fn tyvar | not (isMetaTyVar tyvar) -- Skolems @@ -921,6 +953,18 @@ zonk_tc_tyvar unbound_var_fn tyvar ; case cts of Flexi -> unbound_var_fn tyvar -- Unbound meta type variable Indirect ty -> zonkType unbound_var_fn ty } + +-- Zonk the kind of a non-TC tyvar in case it is a coercion variable (their +-- kind contains types). +-- +zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var + -> TyVar -> TcM TyVar +zonkTyVar unbound_var_fn tv + | isCoVar tv + = do { kind <- zonkType unbound_var_fn (tyVarKind tv) + ; return $ setTyVarKind tv kind + } + | otherwise = return tv \end{code} @@ -997,25 +1041,31 @@ checkValidType ctxt ty = do | otherwise = Rank n rank = case ctxt of - GenPatCtxt -> MustBeMonoType DefaultDeclCtxt-> MustBeMonoType ResSigCtxt -> MustBeMonoType LamPatSigCtxt -> gen_rank 0 BindPatSigCtxt -> gen_rank 0 TySynCtxt _ -> gen_rank 0 + GenPatCtxt -> gen_rank 1 + -- This one is a bit of a hack + -- See the forall-wrapping in TcClassDcl.mkGenericInstance + ExprSigCtxt -> gen_rank 1 FunSigCtxt _ -> gen_rank 1 ConArgCtxt _ | polycomp -> gen_rank 2 -- We are given the type of the entire -- constructor, hence rank 1 | otherwise -> gen_rank 1 + ForSigCtxt _ -> gen_rank 1 SpecInstCtxt -> gen_rank 1 + ThBrackCtxt -> gen_rank 1 actual_kind = typeKind ty kind_ok = case ctxt of TySynCtxt _ -> True -- Any kind will do + ThBrackCtxt -> True -- Any kind will do ResSigCtxt -> isSubOpenTypeKind actual_kind ExprSigCtxt -> isSubOpenTypeKind actual_kind GenPatCtxt -> isLiftedTypeKind actual_kind @@ -1025,6 +1075,7 @@ checkValidType ctxt ty = do ubx_tup = case ctxt of TySynCtxt _ | unboxed -> UT_Ok ExprSigCtxt | unboxed -> UT_Ok + ThBrackCtxt | unboxed -> UT_Ok _ -> UT_NotOk -- Check that the thing has kind Type, and is lifted if necessary @@ -1044,6 +1095,7 @@ checkValidMonoType ty = check_mono_type MustBeMonoType ty data Rank = ArbitraryRank -- Any rank ok | MustBeMonoType -- Monotype regardless of flags | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes + | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms | Rank Int -- Rank n, but could be more with -XRankNTypes decRank :: Rank -> Rank -- Function arguments @@ -1117,7 +1169,7 @@ check_type rank ubx_tup ty@(TyConApp tc tys) ; liberal <- doptM Opt_LiberalTypeSynonyms ; if not liberal || isOpenSynTyCon tc then -- For H98 and synonym families, do check the type args - mapM_ (check_mono_type TyConArgMonoType) tys + mapM_ (check_mono_type SynArgMonoType) tys else -- In the liberal case (only for closed syns), expand then check case tcView ty of @@ -1174,13 +1226,14 @@ check_arg_type :: Rank -> Type -> TcM () check_arg_type rank ty = do { impred <- doptM Opt_ImpredicativeTypes - ; let rank' = if impred then ArbitraryRank -- Arg of tycon can have arby rank, regardless - else case rank of -- Predictive => must be monotype - MustBeMonoType -> MustBeMonoType - _ -> TyConArgMonoType + ; let rank' = case rank of -- Predictive => must be monotype + MustBeMonoType -> MustBeMonoType -- Monotype, regardless + _other | impred -> ArbitraryRank + | otherwise -> TyConArgMonoType -- Make sure that MustBeMonoType is propagated, -- so that we don't suggest -XImpredicativeTypes in -- (Ord (forall a.a)) => a -> a + -- and so that if it Must be a monotype, we check that it is! ; check_type rank' UT_NotOk ty ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } @@ -1194,6 +1247,7 @@ forAllTyErr rank ty suggestion = case rank of Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types") TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes") + SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms") _ -> empty -- Polytype is always illegal unliftedArgErr, ubxArgTyErr :: Type -> SDoc @@ -1300,6 +1354,14 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) arity_err = arityErr "Class" class_name arity n_tys how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this")) +check_pred_ty _ (ClassSCCtxt _) (EqPred _ _) + = -- We do not yet support superclass equalities. + failWithTc $ + sep [ ptext (sLit "The current implementation of type families does not") + , ptext (sLit "support equality constraints in superclass contexts.") + , ptext (sLit "They are planned for a future release.") + ] + check_pred_ty dflags _ pred@(EqPred ty1 ty2) = do { -- Equational constraints are valid in all contexts if type -- families are permitted @@ -1384,7 +1446,7 @@ checkAmbiguity forall_tyvars theta tau_tyvars = mapM_ complain (filter is_ambig theta) where complain pred = addErrTc (ambigErr pred) - extended_tau_vars = grow theta tau_tyvars + extended_tau_vars = growThetaTyVars theta tau_tyvars -- See Note [Implicit parameters and ambiguity] in TcSimplify is_ambig pred = isClassPred pred && @@ -1398,6 +1460,28 @@ ambigErr pred = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred), nest 4 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$ ptext (sLit "must be reachable from the type after the '=>'"))] + +-------------------------- +-- For this 'grow' stuff see Note [Growing the tau-tvs using constraints] in Inst + +growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet +-- Finds a fixpoint +growThetaTyVars theta tvs + | null theta = tvs + | otherwise = fixVarSet mk_next tvs + where + mk_next tvs = foldr growPredTyVars tvs theta + + +growPredTyVars :: TcPredType -> TyVarSet -> TyVarSet +-- Here is where the special case for inplicit parameters happens +growPredTyVars (IParam _ ty) tvs = tvs `unionVarSet` tyVarsOfType ty +growPredTyVars pred tvs = growTyVars (tyVarsOfPred pred) tvs + +growTyVars :: TyVarSet -> TyVarSet -> TyVarSet +growTyVars new_tvs tvs + | new_tvs `intersectsVarSet` tvs = tvs `unionVarSet` new_tvs + | otherwise = tvs \end{code} In addition, GHC insists that at least one type variable