X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=492cbf9edaf8754121e3f9d8658ac2b61b7c2446;hb=0884a2cb09cd5f609b6163a225ca3b8cce942250;hp=865c749131e159d59e6cd818e795e8053b0f2558;hpb=0f5e104c36b1dc3d8deeec5fef3d65e7b3a1b5ad;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 865c749..492cbf9 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -33,18 +33,19 @@ module TcMType ( -------------------------------- -- Instantiation tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, - tcInstSigTyVars, - tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, - tcSkolSigType, tcSkolSigTyVars, occurCheckErr, + tcInstSigType, + tcInstSkolTyVars, tcInstSkolType, + 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 @@ -69,7 +70,8 @@ import TyCon import Var -- others: -import TcRnMonad -- TcType, amongst others +import HsSyn -- HsType +import TcRnMonad -- TcType, amongst others import FunDeps import Name import VarEnv @@ -77,6 +79,7 @@ import VarSet import ErrUtils import DynFlags import Util +import Bag import Maybes import ListSetOps import UniqSupply @@ -179,7 +182,7 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) -- (checkTauTvUpdate tv ty) -- We are about to update the TauTv tv with ty. -- Check (a) that tv doesn't occur in ty (occurs check) --- (b) that ty is a monotype +-- (b) that ty is a monotype -- Furthermore, in the interest of (b), if you find an -- empty box (BoxTv that is Flexi), fill it in with a TauTv -- @@ -218,7 +221,7 @@ checkTauTvUpdate orig_tv orig_ty | isSynTyCon tc = go_syn tc tys | otherwise = do { tys' <- mapM go tys ; return $ occurs (TyConApp tc) tys' } - go (PredTy p) = do { p' <- go_pred p + go (PredTy p) = do { p' <- go_pred p ; return $ occurs1 PredTy p' } go (FunTy arg res) = do { arg' <- go arg ; res' <- go res @@ -336,6 +339,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} @@ -392,7 +416,7 @@ occurCheckErr ty containingTy newCoVars :: [(TcType,TcType)] -> TcM [CoVar] newCoVars spec = do { us <- newUniqueSupply - ; return [ mkCoVar (mkSysTvName uniq (fsLit "co")) + ; return [ mkCoVar (mkSysTvName uniq (fsLit "co_kv")) (mkCoKind ty1 ty2) | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] } @@ -430,17 +454,17 @@ tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info | tv <- tyvars ] -tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar +tcInstSkolTyVar :: SkolemInfo -> (Name -> SrcSpan) -> TyVar -> TcM TcTyVar -- Instantiate the tyvar, using -- * the occ-name and kind of the supplied tyvar, -- * the unique from the monad, -- * the location either from the tyvar (mb_loc = Nothing) -- or from mb_loc (Just loc) -tcInstSkolTyVar info mb_loc tyvar +tcInstSkolTyVar info get_loc tyvar = do { uniq <- newUnique ; let old_name = tyVarName tyvar kind = tyVarKind tyvar - loc = mb_loc `orElse` getSrcSpan old_name + loc = get_loc old_name new_name = mkInternalName uniq (nameOccName old_name) loc ; return (mkSkolTyVar new_name kind info) } @@ -448,12 +472,21 @@ tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] -- Get the location from the monad tcInstSkolTyVars info tyvars = do { span <- getSrcSpanM - ; mapM (tcInstSkolTyVar info (Just span)) tyvars } + ; mapM (tcInstSkolTyVar info (const span)) tyvars } tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) -- Instantiate a type with fresh skolem constants -- Binding location comes from the monad tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty + +tcInstSigType :: Bool -> SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType) +-- Instantiate with skolems or meta SigTvs; depending on use_skols +-- Always take location info from the supplied tyvars +tcInstSigType use_skols skol_info ty + = tcInstType (mapM inst_tyvar) ty + where + inst_tyvar | use_skols = tcInstSkolTyVar skol_info getSrcSpan + | otherwise = instMetaTyVar (SigTv skol_info) \end{code} @@ -512,13 +545,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} @@ -563,16 +600,6 @@ tcInstTyVars tyvars %************************************************************************ \begin{code} -tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar] --- Instantiate with skolems or meta SigTvs; depending on use_skols --- Always take location info from the supplied tyvars -tcInstSigTyVars use_skols skol_info tyvars - | use_skols - = mapM (tcInstSkolTyVar skol_info Nothing) tyvars - - | otherwise - = mapM (instMetaTyVar (SigTv skol_info)) tyvars - zonkSigTyVar :: TcTyVar -> TcM TcTyVar zonkSigTyVar sig_tv | isSkolemTyVar sig_tv @@ -763,8 +790,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 @@ -811,7 +841,7 @@ Consider this: * Now abstract over the 'a', but float out the Num (C d a) constraint because it does not 'really' mention a. (see exactTyVarsOfType) The arg to foo becomes - /\a -> \t -> t+t + \/\a -> \t -> t+t * So we get a dict binding for Num (C d a), which is zonked to give a = () @@ -820,10 +850,10 @@ Consider this: quantification, so the floated dict will still have type (C d a). Which renders this whole note moot; happily!] -* Then the /\a abstraction has a zonked 'a' in it. +* Then the \/\a abstraction has a zonked 'a' in it. All very silly. I think its harmless to ignore the problem. We'll end up with -a /\a in the final result but all the occurrences of a will be zonked to () +a \/\a in the final result but all the occurrences of a will be zonked to () Note [Zonking to Skolem] ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -896,12 +926,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') @@ -911,7 +943,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 @@ -922,6 +954,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} @@ -993,30 +1037,36 @@ checkValidType ctxt ty = do rankn <- doptM Opt_RankNTypes polycomp <- doptM Opt_PolymorphicComponents let - rank | rankn = Arbitrary - | rank2 = Rank 2 - | otherwise - = case ctxt of -- Haskell 98 - GenPatCtxt -> Rank 0 - LamPatSigCtxt -> Rank 0 - BindPatSigCtxt -> Rank 0 - DefaultDeclCtxt-> Rank 0 - ResSigCtxt -> Rank 0 - TySynCtxt _ -> Rank 0 - ExprSigCtxt -> Rank 1 - FunSigCtxt _ -> Rank 1 - ConArgCtxt _ -> if polycomp - then Rank 2 + gen_rank n | rankn = ArbitraryRank + | rank2 = Rank 2 + | otherwise = Rank n + rank + = case ctxt of + 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 - else Rank 1 - ForSigCtxt _ -> Rank 1 - SpecInstCtxt -> 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 @@ -1026,45 +1076,54 @@ 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 - checkTc kind_ok (kindErr actual_kind) - -- Check the internal validity of the type itself check_type rank ubx_tup ty + -- Check that the thing has kind Type, and is lifted if necessary + -- Do this second, becuase we can't usefully take the kind of an + -- ill-formed type such as (a~Int) + checkTc kind_ok (kindErr actual_kind) + traceTc (text "checkValidType done" <+> ppr ty) checkValidMonoType :: Type -> TcM () -checkValidMonoType ty = check_mono_type ty +checkValidMonoType ty = check_mono_type MustBeMonoType ty \end{code} \begin{code} -data Rank = Rank Int | Arbitrary +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 -decRank Arbitrary = Arbitrary -decRank (Rank n) = Rank (n-1) +decRank :: Rank -> Rank -- Function arguments +decRank (Rank 0) = Rank 0 +decRank (Rank n) = Rank (n-1) +decRank other_rank = other_rank nonZeroRank :: Rank -> Bool -nonZeroRank (Rank 0) = False -nonZeroRank _ = True +nonZeroRank ArbitraryRank = True +nonZeroRank (Rank n) = n>0 +nonZeroRank _ = False ---------------------------------------- data UbxTupFlag = UT_Ok | UT_NotOk - -- The "Ok" version means "ok if -fglasgow-exts is on" + -- The "Ok" version means "ok if UnboxedTuples is on" ---------------------------------------- -check_mono_type :: Type -> TcM () -- No foralls anywhere - -- No unlifted types of any kind -check_mono_type ty - = do { check_type (Rank 0) UT_NotOk ty +check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere + -- No unlifted types of any kind +check_mono_type rank ty + = do { check_type rank UT_NotOk ty ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } check_type :: Rank -> UbxTupFlag -> Type -> TcM () --- The args say what the *type* context requires, independent +-- The args say what the *type context* requires, independent -- of *flag* settings. You test the flag settings at usage sites. -- -- Rank is allowed rank for function args @@ -1072,7 +1131,7 @@ check_type :: Rank -> UbxTupFlag -> Type -> TcM () check_type rank ubx_tup ty | not (null tvs && null theta) - = do { checkTc (nonZeroRank rank) (forAllTyErr ty) + = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty) -- Reject e.g. (Maybe (?x::Int => Int)), -- with a decent error message ; check_valid_theta SigmaCtxt theta @@ -1082,15 +1141,12 @@ check_type rank ubx_tup ty where (tvs, theta, tau) = tcSplitSigmaTy ty --- Naked PredTys don't usually show up, but they can as a result of --- {-# SPECIALISE instance Ord Char #-} --- The Right Thing would be to fix the way that SPECIALISE instance pragmas --- are handled, but the quick thing is just to permit PredTys here. -check_type _ _ (PredTy sty) - = do { dflags <- getDOpts - ; check_pred_ty dflags TypeCtxt sty } +-- Naked PredTys should, I think, have been rejected before now +check_type _ _ ty@(PredTy {}) + = failWithTc (text "Predicate used as a type:" <+> ppr ty) check_type _ _ (TyVarTy _) = return () + check_type rank _ (FunTy arg_ty res_ty) = do { check_type (decRank rank) UT_NotOk arg_ty ; check_type rank UT_Ok res_ty } @@ -1113,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 tys + mapM_ (check_mono_type SynArgMonoType) tys else -- In the liberal case (only for closed syns), expand then check case tcView ty of @@ -1126,7 +1182,7 @@ check_type rank ubx_tup ty@(TyConApp tc tys) ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg ; impred <- doptM Opt_ImpredicativeTypes - ; let rank' = if impred then rank else Rank 0 + ; let rank' = if impred then ArbitraryRank else TyConArgMonoType -- c.f. check_arg_type -- However, args are allowed to be unlifted, or -- more unboxed tuples, so can't use check_arg_ty @@ -1170,13 +1226,31 @@ check_arg_type :: Rank -> Type -> TcM () check_arg_type rank ty = do { impred <- doptM Opt_ImpredicativeTypes - ; let rank' = if impred then rank else Rank 0 -- Monotype unless impredicative + ; 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) } ---------------------------------------- -forAllTyErr, unliftedArgErr, ubxArgTyErr :: Type -> SDoc -forAllTyErr ty = sep [ptext (sLit "Illegal polymorphic or qualified type:"), ppr ty] +forAllTyErr :: Rank -> Type -> SDoc +forAllTyErr rank ty + = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty) + , suggestion ] + where + 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 unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty] ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty] @@ -1269,7 +1343,7 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) ; checkTc (arity == n_tys) arity_err -- Check the form of the argument types - ; mapM_ check_mono_type tys + ; mapM_ checkValidMonoType tys ; checkTc (check_class_pred_tys dflags ctxt tys) (predTyVarErr pred $$ how_to_allow) } @@ -1280,17 +1354,25 @@ 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 ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred) -- Check the form of the argument types - ; check_mono_type ty1 - ; check_mono_type ty2 + ; checkValidMonoType ty1 + ; checkValidMonoType ty2 } -check_pred_ty _ SigmaCtxt (IParam _ ty) = check_mono_type ty +check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty -- Implicit parameters only allowed in type -- signatures; not in instance decls, superclasses etc -- The reason for not allowing implicit params in instances is a bit @@ -1364,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 && @@ -1378,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 @@ -1479,29 +1583,32 @@ checkValidInstHead ty -- Should be a source type Just (clas,tys) -> do dflags <- getDOpts - mapM_ check_mono_type tys check_inst_head dflags clas tys return (clas, tys) }} check_inst_head :: DynFlags -> Class -> [Type] -> TcM () check_inst_head dflags clas tys - -- If GlasgowExts then check at least one isn't a type variable - = do checkTc (dopt Opt_TypeSynonymInstances dflags || - all tcInstHeadTyNotSynonym tys) - (instTypeErr (pprClassPred clas tys) head_type_synonym_msg) - checkTc (dopt Opt_FlexibleInstances dflags || - all tcInstHeadTyAppAllTyVars tys) - (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg) - checkTc (dopt Opt_MultiParamTypeClasses dflags || - isSingleton tys) - (instTypeErr (pprClassPred clas tys) head_one_type_msg) - mapM_ check_mono_type tys + = do { -- If GlasgowExts then check at least one isn't a type variable + ; checkTc (dopt Opt_TypeSynonymInstances dflags || + all tcInstHeadTyNotSynonym tys) + (instTypeErr (pprClassPred clas tys) head_type_synonym_msg) + ; checkTc (dopt Opt_FlexibleInstances dflags || + all tcInstHeadTyAppAllTyVars tys) + (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg) + ; checkTc (dopt Opt_MultiParamTypeClasses dflags || + isSingleton tys) + (instTypeErr (pprClassPred clas tys) head_one_type_msg) + -- May not contain type family applications + ; mapM_ checkTyFamFreeness tys + + ; mapM_ checkValidMonoType tys -- For now, I only allow tau-types (not polytypes) in -- the head of an instance decl. -- E.g. instance C (forall a. a->a) is rejected -- One could imagine generalising that, but I'm not sure -- what all the consequences might be + } where head_type_synonym_msg = parens ( @@ -1532,11 +1639,15 @@ instTypeErr pp_ty msg %* * %************************************************************************ - \begin{code} -checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM () -checkValidInstance tyvars theta clas inst_tys - = do { undecidable_ok <- doptM Opt_UndecidableInstances +checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type + -> TcM (Class, [TcType]) +checkValidInstance hs_type tyvars theta tau + = setSrcSpan (getLoc hs_type) $ + do { (clas, inst_tys) <- setSrcSpan head_loc $ + checkValidInstHead tau + + ; undecidable_ok <- doptM Opt_UndecidableInstances ; checkValidTheta InstThetaCtxt theta ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys) @@ -1550,10 +1661,17 @@ checkValidInstance tyvars theta clas inst_tys -- The Coverage Condition ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) (instTypeErr (pprClassPred clas inst_tys) msg) + + ; return (clas, inst_tys) } where msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"), undecidableMsg]) + + -- The location of the "head" of the instance + head_loc = case hs_type of + L _ (HsForAllTy _ _ _ (L loc _)) -> loc + L loc _ -> loc \end{code} Termination test: the so-called "Paterson conditions" (see Section 5 of @@ -1621,7 +1739,6 @@ Notice that this instance (just) satisfies the Paterson termination conditions. Then we *could* derive an instance decl like this: instance (C Int a, Eq b, Eq c) => Eq (T a b c) - even though there is no instance for (C Int a), because there just *might* be an instance for, say, (C Int Bool) at a site where we need the equality instance for T's. @@ -1681,8 +1798,7 @@ checkValidTypeInst typats rhs ; mapM_ checkTyFamFreeness typats -- the right-hand side is a tau type - ; checkTc (isTauTy rhs) $ - polyTyErr rhs + ; checkValidMonoType rhs -- we have a decidable instance unless otherwise permitted ; undecidable_ok <- doptM Opt_UndecidableInstances @@ -1720,7 +1836,7 @@ checkFamInst lhsTys famInsts checkTyFamFreeness :: Type -> TcM () checkTyFamFreeness ty = checkTc (isTyFamFree ty) $ - tyFamInstInIndexErr ty + tyFamInstIllegalErr ty -- Check that a type does not contain any type family applications. -- @@ -1729,17 +1845,12 @@ isTyFamFree = null . tyFamInsts -- Error messages -tyFamInstInIndexErr :: Type -> SDoc -tyFamInstInIndexErr ty - = hang (ptext (sLit "Illegal type family application in type instance") <> +tyFamInstIllegalErr :: Type -> SDoc +tyFamInstIllegalErr ty + = hang (ptext (sLit "Illegal type synonym family application in instance") <> colon) 4 $ ppr ty -polyTyErr :: Type -> SDoc -polyTyErr ty - = hang (ptext (sLit "Illegal polymorphic type in type instance") <> colon) 4 $ - ppr ty - famInstUndecErr :: Type -> SDoc -> SDoc famInstUndecErr ty msg = sep [msg, @@ -1791,8 +1902,16 @@ sizeType (ForAllTy _ ty) = sizeType ty sizeTypes :: [Type] -> Int sizeTypes xs = sum (map sizeType xs) +-- Size of a predicate +-- +-- Equalities are a special case. The equality itself doesn't contribute to the +-- size and as we do not count class predicates, we have to start with one less. +-- This is easy to see considering that, given +-- class C a b | a -> b +-- type family F a +-- constraints (C a b) and (F a ~ b) are equivalent in size. sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' sizePred (IParam _ ty) = sizeType ty -sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 +sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 - 1 \end{code}