X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=f8162bc2bf0e29c9247c3098664577d2acd25c29;hb=d759c7231dde979ed2824bd39b2fdff24357d355;hp=90268e442015f064a13c3feced4677641c746508;hpb=cdd7fdacaafc36de12e8d703904667aada6bbe31;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 90268e4..f8162bc 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_GHC -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/WorkingConventions#Warnings +-- for details + module TcMType ( TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet, @@ -41,7 +48,7 @@ module TcMType ( Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, checkValidInstance, checkAmbiguity, - checkInstTermination, + checkInstTermination, checkValidTypeInst, checkTyFamFreeness, arityErr, -------------------------------- @@ -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,8 +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_ExpressionSignaturesUnboxedTuples `thenM` \ exp_sigs_unboxed -> - doptM Opt_TypeSynonymUnboxedTuples `thenM` \ type_synonym_unboxed -> + doptM Opt_UnboxedTuples `thenM` \ unboxed -> doptM Opt_Rank2Types `thenM` \ rank2 -> doptM Opt_RankNTypes `thenM` \ rankn -> doptM Opt_PolymorphicComponents `thenM` \ polycomp -> @@ -731,9 +737,9 @@ checkValidType ctxt ty other -> isSubArgTypeKind actual_kind ubx_tup = case ctxt of - TySynCtxt _ | type_synonym_unboxed -> UT_Ok - ExprSigCtxt | exp_sigs_unboxed -> UT_Ok - _ -> UT_NotOk + 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_` @@ -981,7 +987,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 @@ -1176,14 +1182,14 @@ instTypeErr pp_ty msg \begin{code} checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM () checkValidInstance tyvars theta clas inst_tys - = do { 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 this will already have been done by checkValidTheta, - -- but as we may be using other extensions we need to check. + -- but as we may be using other extensions we need to check. ; unless undecidable_ok $ mapM_ addErrTc (checkInstTermination inst_tys theta) @@ -1234,7 +1240,101 @@ 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} + + +%************************************************************************ +%* * +\subsection{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 @@ -1272,4 +1372,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}