X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=c5748203a7c45bab13182dceaca9700b2306302f;hp=e5ccbd0a34ce08fe48900d94873a7479b4e27d84;hb=25f84fa7e4b84c3db5ba745a7881c009b778e0b1;hpb=9eb79d53316804b4c384b5084825112c48f1bbc4 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index e5ccbd0..c574820 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, @@ -41,8 +48,8 @@ module TcMType ( Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, checkValidInstance, checkAmbiguity, - checkInstTermination, - arityErr, + checkInstTermination, checkValidTypeInst, checkTyFamFreeness, + validDerivPred, arityErr, -------------------------------- -- Zonking @@ -53,7 +60,6 @@ module TcMType ( zonkTcKindToKind, zonkTcKind, zonkTopTyVar, readKindVar, writeKindVar - ) where #include "HsVersions.h" @@ -199,7 +205,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") @@ -216,7 +222,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)) } @@ -236,7 +242,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 @@ -331,7 +338,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 @@ -365,7 +372,7 @@ lookupTcTyVar tyvar 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 @@ -694,7 +701,7 @@ 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 -> @@ -729,14 +736,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_` @@ -857,8 +860,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 @@ -867,7 +870,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 @@ -932,6 +935,7 @@ 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) = do { -- Class predicates are valid in all contexts ; checkTc (arity == n_tys) arity_err @@ -975,6 +979,7 @@ 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 @@ -984,7 +989,7 @@ check_class_pred_tys dflags ctxt tys other -> flexible_contexts || all tyvar_head tys where flexible_contexts = dopt Opt_FlexibleContexts dflags - undecidable_ok = dopt Opt_AllowUndecidableInstances dflags + undecidable_ok = dopt Opt_UndecidableInstances dflags ------------------------- tyvar_head ty -- Haskell 98 allows predicates of form @@ -1179,15 +1184,15 @@ 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) $ + -- 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 @@ -1237,7 +1242,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 @@ -1275,4 +1439,16 @@ sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' sizePred (IParam _ ty) = sizeType ty sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 + +-- Type family instances occuring in a type after expanding synonyms +tyFamInsts :: Type -> [(TyCon, [Type])] +tyFamInsts ty + | Just exp_ty <- tcView ty = tyFamInsts exp_ty +tyFamInsts (TyVarTy _) = [] +tyFamInsts (TyConApp tc tys) + | isOpenSynTyCon tc = [(tc, tys)] + | otherwise = concat (map tyFamInsts tys) +tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 +tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 +tyFamInsts (ForAllTy _ ty) = tyFamInsts ty \end{code}