X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=13fbf557d100728e4da90085e83f3b448ea4918c;hp=0845853f1375288ae3b070306bcf76bc4a873c20;hb=6d2b0ae3ae3296cb6cdd496cbf85b897c7ce150b;hpb=2423c249f5ca7785d0ec89eb33e72662da7561c1 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 0845853..13fbf55 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -9,6 +9,13 @@ This module contains monadic operations over types that contain mutable type variables \begin{code} +{-# OPTIONS -w #-} +-- The above warning supression flag is a temporary kludge. +-- While working on this module you are encouraged to remove it and fix +-- any warnings in the module. See +-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings +-- for details + module TcMType ( TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet, @@ -27,22 +34,23 @@ module TcMType ( -------------------------------- -- Creating new coercion variables - newCoVars, + newCoVars, newMetaCoVar, -------------------------------- -- Instantiation tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, tcInstSigTyVars, zonkSigTyVar, tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, - tcSkolSigType, tcSkolSigTyVars, + tcSkolSigType, tcSkolSigTyVars, occurCheckErr, -------------------------------- -- Checking type validity Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, - checkValidInstHead, checkValidInstance, checkAmbiguity, - checkInstTermination, - arityErr, + checkValidInstHead, checkValidInstance, + checkInstTermination, checkValidTypeInst, checkTyFamFreeness, + checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt, + unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs, -------------------------------- -- Zonking @@ -53,7 +61,6 @@ module TcMType ( zonkTcKindToKind, zonkTcKind, zonkTopTyVar, readKindVar, writeKindVar - ) where #include "HsVersions.h" @@ -62,7 +69,6 @@ module TcMType ( import TypeRep import TcType import Type -import Type import Coercion import Class import TyCon @@ -82,7 +88,7 @@ import UniqSupply import SrcLoc import Outputable -import Control.Monad ( when ) +import Control.Monad ( when, unless ) import Data.List ( (\\) ) \end{code} @@ -119,6 +125,186 @@ tcInstType inst_tyvars ty %************************************************************************ %* * + Updating tau types +%* * +%************************************************************************ + +Can't be in TcUnify, as we also need it in TcTyFuns. + +\begin{code} +type SwapFlag = Bool + -- False <=> the two args are (actual, expected) respectively + -- True <=> the two args are (expected, actual) respectively + +checkUpdateMeta :: SwapFlag + -> TcTyVar -> IORef MetaDetails -> TcType -> TcM () +-- Update tv1, which is flexi; occurs check is alrady done +-- The 'check' version does a kind check too +-- We do a sub-kind check here: we might unify (a b) with (c d) +-- where b::*->* and d::*; this should fail + +checkUpdateMeta swapped tv1 ref1 ty2 + = do { checkKinds swapped tv1 ty2 + ; updateMeta tv1 ref1 ty2 } + +updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM () +updateMeta tv1 ref1 ty2 + = ASSERT( isMetaTyVar tv1 ) + ASSERT( isBoxyTyVar tv1 || isTauTy ty2 ) + do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 ) + ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2) + ; writeMutVar ref1 (Indirect ty2) + } + +---------------- +checkKinds swapped tv1 ty2 +-- We're about to unify a type variable tv1 with a non-tyvar-type ty2. +-- ty2 has been zonked at this stage, which ensures that +-- its kind has as much boxity information visible as possible. + | tk2 `isSubKind` tk1 = returnM () + + | otherwise + -- Either the kinds aren't compatible + -- (can happen if we unify (a b) with (c d)) + -- or we are unifying a lifted type variable with an + -- unlifted type: e.g. (id 3#) is illegal + = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $ + unifyKindMisMatch k1 k2 + where + (k1,k2) | swapped = (tk2,tk1) + | otherwise = (tk1,tk2) + tk1 = tyVarKind tv1 + tk2 = typeKind ty2 + +---------------- +checkTauTvUpdate :: TcTyVar -> TcType -> TcM 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 +-- Furthermore, in the interest of (b), if you find an +-- empty box (BoxTv that is Flexi), fill it in with a TauTv +-- +-- Returns the (non-boxy) type to update the type variable with, or fails + +checkTauTvUpdate orig_tv orig_ty + = go orig_ty + where + go (TyConApp tc tys) + | isSynTyCon tc = go_syn tc tys + | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') } + go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations + go (PredTy p) = do { p' <- go_pred p; return (PredTy p') } + 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. + go (ForAllTy tv ty) = notMonoType orig_ty -- (b) + + go (TyVarTy tv) + | orig_tv == tv = occurCheck tv -- (a) + | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv) + | otherwise = return (TyVarTy tv) + -- Ordinary (non Tc) tyvars + -- occur inside quantified types + + go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') } + go_pred (IParam n ty) = do { ty' <- go ty; return (IParam n ty') } + go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') } + + go_tyvar tv (SkolemTv _) = return (TyVarTy tv) + go_tyvar tv (MetaTv box ref) + = do { cts <- readMutVar ref + ; case cts of + Indirect ty -> go ty + Flexi -> case box of + BoxTv -> fillBoxWithTau tv ref + other -> return (TyVarTy tv) + } + + -- go_syn is called for synonyms only + -- See Note [Type synonyms and the occur check] + go_syn tc tys + | not (isTauTyCon tc) + = notMonoType orig_ty -- (b) again + | otherwise + = do { (msgs, mb_tys') <- tryTc (mapM go tys) + ; case mb_tys' of + Just tys' -> return (TyConApp tc tys') + -- Retain the synonym (the common case) + Nothing | isOpenTyCon tc + -> notMonoArgs (TyConApp tc tys) + -- Synonym families must have monotype args + | otherwise + -> go (expectJust "checkTauTvUpdate" + (tcView (TyConApp tc tys))) + -- Try again, expanding the synonym + } + + occurCheck tv = occurCheckErr (mkTyVarTy tv) orig_ty + +fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType +-- (fillBoxWithTau tv ref) fills ref with a freshly allocated +-- tau-type meta-variable, whose print-name is the same as tv +-- Choosing the same name is good: when we instantiate a function +-- we allocate boxy tyvars with the same print-name as the quantified +-- tyvar; and then we often fill the box with a tau-tyvar, and again +-- we want to choose the same name. +fillBoxWithTau tv ref + = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget + ; let tau = mkTyVarTy tv' -- name of the type variable + ; writeMutVar ref (Indirect tau) + ; return tau } +\end{code} + +Error mesages in case of kind mismatch. + +\begin{code} +unifyKindMisMatch ty1 ty2 + = zonkTcKind ty1 `thenM` \ ty1' -> + zonkTcKind ty2 `thenM` \ ty2' -> + let + msg = hang (ptext SLIT("Couldn't match kind")) + 2 (sep [quotes (ppr ty1'), + ptext SLIT("against"), + quotes (ppr ty2')]) + in + failWithTc msg + +unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred + -- tv1 and ty2 are zonked already + = returnM msg + where + msg = (env2, ptext SLIT("When matching the kinds of") <+> + sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual]) + + (pp_expected, pp_actual) | swapped = (pp2, pp1) + | otherwise = (pp1, pp2) + (env1, tv1') = tidyOpenTyVar tidy_env tv1 + (env2, ty2') = tidyOpenType env1 ty2 + pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1) + pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2) +\end{code} + +Error message for failure due to an occurs check. + +\begin{code} +occurCheckErr :: TcType -> TcType -> TcM a +occurCheckErr ty containingTy + = do { env0 <- tcInitTidyEnv + ; ty' <- zonkTcType ty + ; containingTy' <- zonkTcType containingTy + ; let (env1, tidy_ty1) = tidyOpenType env0 ty' + (env2, tidy_ty2) = tidyOpenType env1 containingTy' + extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2] + ; failWithTcM (env2, hang msg 2 extra) } + where + msg = ptext SLIT("Occurs check: cannot construct the infinite type:") +\end{code} + +%************************************************************************ +%* * Kind variables %* * %************************************************************************ @@ -131,6 +317,9 @@ newCoVars spec (mkCoKind ty1 ty2) | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] } +newMetaCoVar :: TcType -> TcType -> TcM TcTyVar +newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2) + newKindVar :: TcM TcKind newKindVar = do { uniq <- newUnique ; ref <- newMutVar Flexi @@ -162,7 +351,7 @@ tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info | tv <- tyvars ] -tcInstSkolTyVar :: SkolemInfo -> Maybe SrcLoc -> TyVar -> TcM TcTyVar +tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar -- Instantiate the tyvar, using -- * the occ-name and kind of the supplied tyvar, -- * the unique from the monad, @@ -172,7 +361,7 @@ tcInstSkolTyVar info mb_loc tyvar = do { uniq <- newUnique ; let old_name = tyVarName tyvar kind = tyVarKind tyvar - loc = mb_loc `orElse` getSrcLoc old_name + loc = mb_loc `orElse` getSrcSpan old_name new_name = mkInternalName uniq (nameOccName old_name) loc ; return (mkSkolTyVar new_name kind info) } @@ -180,7 +369,7 @@ tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] -- Get the location from the monad tcInstSkolTyVars info tyvars = do { span <- getSrcSpanM - ; mapM (tcInstSkolTyVar info (Just (srcSpanStart span))) tyvars } + ; mapM (tcInstSkolTyVar info (Just span)) tyvars } tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) -- Instantiate a type with fresh skolem constants @@ -200,7 +389,7 @@ newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar -- Make a new meta tyvar out of thin air newMetaTyVar box_info kind = do { uniq <- newUnique - ; ref <- newMutVar Flexi ; + ; ref <- newMutVar Flexi ; let name = mkSysTvName uniq fs fs = case box_info of BoxTv -> FSLIT("t") @@ -217,7 +406,7 @@ instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar -- come from an existing TyVar instMetaTyVar box_info tyvar = do { uniq <- newUnique - ; ref <- newMutVar Flexi ; + ; ref <- newMutVar Flexi ; let name = setNameUnique (tyVarName tyvar) uniq kind = tyVarKind tyvar ; return (mkTcTyVar name kind (MetaTv box_info ref)) } @@ -237,7 +426,8 @@ writeMetaTyVar tyvar ty | otherwise = ASSERT( isMetaTyVar tyvar ) - ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) ) + -- 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 ) ; writeMutVar (metaTvRef tyvar) (Indirect ty) } where @@ -332,7 +522,7 @@ readFilledBox :: BoxyTyVar -> TcM TcType readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv ) do { cts <- readMetaTyVar box_tv ; case cts of - Flexi -> pprPanic "readFilledBox" (ppr box_tv) + Flexi -> pprPanic "readFilledBox" (ppr box_tv) Indirect ty -> return ty } tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar @@ -360,13 +550,13 @@ data LookupTyVarResult -- The result of a lookupTcTyVar call lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult lookupTcTyVar tyvar - = ASSERT( isTcTyVar tyvar ) + = ASSERT2( isTcTyVar tyvar, ppr tyvar ) case details of SkolemTv _ -> return (DoneTv details) MetaTv _ ref -> do { meta_details <- readMutVar ref ; case meta_details of Indirect ty -> return (IndirectTv ty) - Flexi -> return (DoneTv details) } + Flexi -> return (DoneTv details) } where details = tcTyVarDetails tyvar @@ -423,7 +613,7 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> returnM (tyVarsOfTypes tys) zonkTcTyVar :: TcTyVar -> TcM TcType -zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar ) +zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar) zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar \end{code} @@ -695,9 +885,13 @@ checkValidType :: UserTypeCtxt -> Type -> TcM () -- Checks that the type is valid for the given context checkValidType ctxt ty = traceTc (text "checkValidType" <+> ppr ty) `thenM_` - doptM Opt_GlasgowExts `thenM` \ gla_exts -> + doptM Opt_UnboxedTuples `thenM` \ unboxed -> + doptM Opt_Rank2Types `thenM` \ rank2 -> + doptM Opt_RankNTypes `thenM` \ rankn -> + doptM Opt_PolymorphicComponents `thenM` \ polycomp -> let - rank | gla_exts = Arbitrary + rank | rankn = Arbitrary + | rank2 = Rank 2 | otherwise = case ctxt of -- Haskell 98 GenPatCtxt -> Rank 0 @@ -708,8 +902,11 @@ checkValidType ctxt ty TySynCtxt _ -> Rank 0 ExprSigCtxt -> Rank 1 FunSigCtxt _ -> Rank 1 - ConArgCtxt _ -> Rank 1 -- We are given the type of the entire - -- constructor, hence rank 1 + ConArgCtxt _ -> if polycomp + then Rank 2 + -- We are given the type of the entire + -- constructor, hence rank 1 + else Rank 1 ForSigCtxt _ -> Rank 1 SpecInstCtxt -> Rank 1 @@ -723,14 +920,10 @@ checkValidType ctxt ty ForSigCtxt _ -> isLiftedTypeKind actual_kind other -> isSubArgTypeKind actual_kind - ubx_tup | not gla_exts = UT_NotOk - | otherwise = case ctxt of - TySynCtxt _ -> UT_Ok - ExprSigCtxt -> UT_Ok - other -> UT_NotOk - -- Unboxed tuples ok in function results, - -- but for type synonyms we allow them even at - -- top level + ubx_tup = case ctxt of + TySynCtxt _ | unboxed -> UT_Ok + ExprSigCtxt | unboxed -> UT_Ok + _ -> UT_NotOk in -- Check that the thing has kind Type, and is lifted if necessary checkTc kind_ok (kindErr actual_kind) `thenM_` @@ -827,12 +1020,14 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) -- type Foo a = Tree [a] -- f :: Foo a b -> ... ; case tcView ty of - Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion - Nothing -> failWithTc arity_msg - - ; gla_exts <- doptM Opt_GlasgowExts - ; if gla_exts then - -- If -fglasgow-exts then don't check the type arguments + Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion + Nothing -> unless (isOpenTyCon tc -- No expansion if open + && tyConArity tc <= length tys) $ + failWithTc arity_msg + + ; ok <- doptM Opt_PartiallyAppliedClosedTypeSynonyms + ; if ok && not (isOpenTyCon tc) then + -- Don't check the type arguments of *closed* synonyms. -- This allows us to instantiate a synonym defn with a -- for-all type, or with a partially-applied type synonym. -- e.g. type T a b = a @@ -849,8 +1044,8 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) } | isUnboxedTupleTyCon tc - = doptM Opt_GlasgowExts `thenM` \ gla_exts -> - checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_` + = doptM Opt_UnboxedTuples `thenM` \ ub_tuples_allowed -> + checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg `thenM_` mappM_ (check_tau_type (Rank 0) UT_Ok) tys -- Args are allowed to be unlifted, or -- more unboxed tuples, so can't use check_arg_ty @@ -859,7 +1054,7 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) = mappM_ check_arg_type tys where - ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False } + ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False } n_args = length tys tc_arity = tyConArity tc @@ -875,7 +1070,6 @@ kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of \end{code} - %************************************************************************ %* * \subsection{Checking a theta or source type} @@ -924,26 +1118,40 @@ check_valid_theta ctxt theta (_,dups) = removeDups tcCmpPred theta ------------------------- +check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM () check_pred_ty dflags ctxt pred@(ClassP cls tys) - = -- Class predicates are valid in all contexts - checkTc (arity == n_tys) arity_err `thenM_` - - -- Check the form of the argument types - mappM_ check_arg_type tys `thenM_` - checkTc (check_class_pred_tys dflags ctxt tys) - (predTyVarErr pred $$ how_to_allow) - + = do { -- Class predicates are valid in all contexts + ; checkTc (arity == n_tys) arity_err + + -- Check the form of the argument types + ; mappM_ check_arg_type tys + ; checkTc (check_class_pred_tys dflags ctxt tys) + (predTyVarErr pred $$ how_to_allow) + } where class_name = className cls arity = classArity cls n_tys = length tys arity_err = arityErr "Class" class_name arity n_tys - how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this")) + how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this")) + +check_pred_ty dflags ctxt 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_eq_arg_type ty1 + ; check_eq_arg_type ty2 + } + where + check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty - -- Implicit parameters only allows in type + -- 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 subtle + -- The reason for not allowing implicit params in instances is a bit + -- subtle. -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ... -- then when we saw (e :: (?x::Int) => t) it would be unclear how to -- discharge all the potential usas of the ?x in e. For example, a @@ -954,16 +1162,17 @@ check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty) ------------------------- +check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool check_class_pred_tys dflags ctxt tys = case ctxt of TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine - InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys + InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys -- Further checks on head and theta in -- checkInstTermination - other -> gla_exts || all tyvar_head tys + other -> flexible_contexts || all tyvar_head tys where - gla_exts = dopt Opt_GlasgowExts dflags - undecidable_ok = dopt Opt_AllowUndecidableInstances dflags + flexible_contexts = dopt Opt_FlexibleContexts dflags + undecidable_ok = dopt Opt_UndecidableInstances dflags ------------------------- tyvar_head ty -- Haskell 98 allows predicates of form @@ -1004,6 +1213,7 @@ If the list of tv_names is empty, we have a monotype, and then we don't need to check for ambiguity either, because the test can't fail (see is_ambig). + \begin{code} checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM () checkAmbiguity forall_tyvars theta tau_tyvars @@ -1012,11 +1222,7 @@ checkAmbiguity forall_tyvars theta tau_tyvars complain pred = addErrTc (ambigErr pred) extended_tau_vars = grow theta tau_tyvars - -- Only a *class* predicate can give rise to ambiguity - -- An *implicit parameter* cannot. For example: - -- foo :: (?x :: [a]) => Int - -- foo = length ?x - -- is fine. The call site will suppply a particular 'x' + -- See Note [Implicit parameters and ambiguity] in TcSimplify is_ambig pred = isClassPred pred && any ambig_var (varSetElems (tyVarsOfPred pred)) @@ -1036,9 +1242,8 @@ even in a scope where b is in scope. \begin{code} checkFreeness forall_tyvars theta - = do { gla_exts <- doptM Opt_GlasgowExts - ; if gla_exts then return () -- New! Oct06 - else mappM_ complain (filter is_free theta) } + = do { flexible_contexts <- doptM Opt_FlexibleContexts + ; unless flexible_contexts $ mappM_ complain (filter is_free theta) } where is_free pred = not (isIPPred pred) && not (any bound_var (varSetElems (tyVarsOfPred pred))) @@ -1046,10 +1251,13 @@ checkFreeness forall_tyvars theta complain pred = addErrTc (freeErr pred) freeErr pred - = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+> - ptext SLIT("are already in scope"), - nest 4 (ptext SLIT("(at least one must be universally quantified here)")) - ] + = sep [ ptext SLIT("All of the type variables in the constraint") <+> + quotes (pprPred pred) + , ptext SLIT("are already in scope") <+> + ptext SLIT("(at least one must be universally quantified here)") + , nest 4 $ + ptext SLIT("(Use -XFlexibleContexts to lift this restriction)") + ] \end{code} \begin{code} @@ -1058,6 +1266,9 @@ checkThetaCtxt ctxt theta ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty +eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty + $$ + parens (ptext SLIT("Use -XTypeFamilies to permit this")) predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"), nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)] dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) @@ -1069,6 +1280,21 @@ arityErr kind name n m n_arguments | n == 0 = ptext SLIT("no arguments") | n == 1 = ptext SLIT("1 argument") | True = hsep [int n, ptext SLIT("arguments")] + +----------------- +notMonoType ty + = do { ty' <- zonkTcType ty + ; env0 <- tcInitTidyEnv + ; let (env1, tidy_ty) = tidyOpenType env0 ty' + msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty) + ; failWithTcM (env1, msg) } + +notMonoArgs ty + = do { ty' <- zonkTcType ty + ; env0 <- tcInitTidyEnv + ; let (env1, tidy_ty) = tidyOpenType env0 ty' + msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty) + ; failWithTcM (env1, msg) } \end{code} @@ -1107,19 +1333,30 @@ checkValidInstHead ty -- Should be a source type check_inst_head dflags clas tys -- If GlasgowExts then check at least one isn't a type variable - | dopt Opt_GlasgowExts dflags - = mapM_ check_one tys - - -- WITH HASKELL 98, MUST HAVE C (T a b c) - | otherwise - = checkTc (isSingleton tys && tcValidInstHeadTy first_ty) - (instTypeErr (pprClassPred clas tys) head_shape_msg) - + = 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_one tys where - (first_ty : _) = tys + head_type_synonym_msg = parens ( + text "All instance types must be of the form (T t1 ... tn)" $$ + text "where T is not a synonym." $$ + text "Use -XTypeSynonymInstances if you want to disable this.") - head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$ - text "where T is not a synonym, and a,b,c are distinct type variables") + head_type_args_tyvars_msg = parens ( + text "All instance types must be of the form (T a1 ... an)" $$ + text "where a1 ... an are distinct type *variables*" $$ + text "Use -XFlexibleInstances if you want to disable this.") + + head_one_type_msg = parens ( + text "Only one type can be given in an instance head." $$ + text "Use -XMultiParamTypeClasses if you want to allow more.") -- For now, I only allow tau-types (not polytypes) in -- the head of an instance decl. @@ -1145,16 +1382,16 @@ instTypeErr pp_ty msg \begin{code} checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM () checkValidInstance tyvars theta clas inst_tys - = do { gla_exts <- doptM Opt_GlasgowExts - ; undecidable_ok <- doptM Opt_AllowUndecidableInstances + = do { undecidable_ok <- doptM Opt_UndecidableInstances ; checkValidTheta InstThetaCtxt theta ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys) -- Check that instance inference will terminate (if we care) - -- For Haskell 98, checkValidTheta has already done that - ; when (gla_exts && not undecidable_ok) $ - mapM_ failWithTc (checkInstTermination inst_tys theta) + -- For Haskell 98 this will already have been done by checkValidTheta, + -- but as we may be using other extensions we need to check. + ; unless undecidable_ok $ + mapM_ addErrTc (checkInstTermination inst_tys theta) -- The Coverage Condition ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) @@ -1165,7 +1402,11 @@ checkValidInstance tyvars theta clas inst_tys undecidableMsg]) \end{code} -Termination test: each assertion in the context satisfies +Termination test: the so-called "Paterson conditions" (see Section 5 of +"Understanding functionsl dependencies via Constraint Handling Rules, +JFP Jan 2007). + +We check that each assertion in the context satisfies: (1) no variable has more occurrences in the assertion than in the head, and (2) the assertion has fewer constructors and variables (taken together and counting repetitions) than the head. @@ -1199,7 +1440,166 @@ predUndecErr pred msg = sep [msg, nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head") smallerMsg = ptext SLIT("Constraint is no smaller than the instance head") undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this") +\end{code} + + +%************************************************************************ +%* * + Checking the context of a derived instance declaration +%* * +%************************************************************************ +Note [Exotic derived instance contexts] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In a 'derived' instance declaration, we *infer* the context. It's a +bit unclear what rules we should apply for this; the Haskell report is +silent. Obviously, constraints like (Eq a) are fine, but what about + data T f a = MkT (f a) deriving( Eq ) +where we'd get an Eq (f a) constraint. That's probably fine too. + +One could go further: consider + data T a b c = MkT (Foo a b c) deriving( Eq ) + instance (C Int a, Eq b, Eq c) => Eq (Foo a b c) + +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. + +However, this seems pretty exotic, and it's quite tricky to allow +this, and yet give sensible error messages in the (much more common) +case where we really want that instance decl for C. + +So for now we simply require that the derived instance context +should have only type-variable constraints. + +Here is another example: + data Fix f = In (f (Fix f)) deriving( Eq ) +Here, if we are prepared to allow -fallow-undecidable-instances we +could derive the instance + instance Eq (f (Fix f)) => Eq (Fix f) +but this is so delicate that I don't think it should happen inside +'deriving'. If you want this, write it yourself! + +NB: if you want to lift this condition, make sure you still meet the +termination conditions! If not, the deriving mechanism generates +larger and larger constraints. Example: + data Succ a = S a + data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show + +Note the lack of a Show instance for Succ. First we'll generate + instance (Show (Succ a), Show a) => Show (Seq a) +and then + instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a) +and so on. Instead we want to complain of no instance for (Show (Succ a)). + +The bottom line +~~~~~~~~~~~~~~~ +Allow constraints which consist only of type variables, with no repeats. + +\begin{code} +validDerivPred :: PredType -> Bool +validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs + where fvs = fvTypes tys +validDerivPred otehr = False +\end{code} + +%************************************************************************ +%* * + Checking type instance well-formedness and termination +%* * +%************************************************************************ + +\begin{code} +-- Check that a "type instance" is well-formed (which includes decidability +-- unless -fallow-undecidable-instances is given). +-- +checkValidTypeInst :: [Type] -> Type -> TcM () +checkValidTypeInst typats rhs + = do { -- left-hand side contains no type family applications + -- (vanilla synonyms are fine, though) + ; mappM_ checkTyFamFreeness typats + + -- the right-hand side is a tau type + ; checkTc (isTauTy rhs) $ + polyTyErr rhs + + -- we have a decidable instance unless otherwise permitted + ; undecidable_ok <- doptM Opt_UndecidableInstances + ; unless undecidable_ok $ + mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs)) + } + +-- Make sure that each type family instance is +-- (1) strictly smaller than the lhs, +-- (2) mentions no type variable more often than the lhs, and +-- (3) does not contain any further type family instances. +-- +checkFamInst :: [Type] -- lhs + -> [(TyCon, [Type])] -- type family instances + -> [Message] +checkFamInst lhsTys famInsts + = mapCatMaybes check famInsts + where + size = sizeTypes lhsTys + fvs = fvTypes lhsTys + check (tc, tys) + | not (all isTyFamFree tys) + = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg) + | not (null (fvTypes tys \\ fvs)) + = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg) + | size <= sizeTypes tys + = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg) + | otherwise + = Nothing + where + famInst = TyConApp tc tys + +-- Ensure that no type family instances occur in a type. +-- +checkTyFamFreeness :: Type -> TcM () +checkTyFamFreeness ty + = checkTc (isTyFamFree ty) $ + tyFamInstInIndexErr ty + +-- Check that a type does not contain any type family applications. +-- +isTyFamFree :: Type -> Bool +isTyFamFree = null . tyFamInsts + +-- Error messages + +tyFamInstInIndexErr ty + = hang (ptext SLIT("Illegal type family application in type instance") <> + colon) 4 $ + ppr ty + +polyTyErr ty + = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $ + ppr ty + +famInstUndecErr ty msg + = sep [msg, + nest 2 (ptext SLIT("in the type family application:") <+> + pprType ty)] + +nestedMsg = ptext SLIT("Nested type family application") +nomoreVarMsg = ptext SLIT("Variable occurs more often than in instance head") +smallerAppMsg = ptext SLIT("Application is no smaller than the instance head") +\end{code} + + +%************************************************************************ +%* * +\subsection{Auxiliary functions} +%* * +%************************************************************************ + +\begin{code} -- Free variables of a type, retaining repetitions, and expanding synonyms fvType :: Type -> [TyVar] fvType ty | Just exp_ty <- tcView ty = fvType exp_ty