X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMType.lhs;h=fa129d3927fd04c2a6beb0372160927c648cca42;hb=3d8ae1e7ba9f238959ca5395b17c485eda5d70e9;hp=88aa75362f48f3ba33bb8eb578e42e2bbe728a1f;hpb=ac10f8408520a30e8437496d320b8b86afda2e8f;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index 88aa753..fa129d3 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -20,7 +20,7 @@ module TcMType ( -------------------------------- -- Boxy type variables - newBoxyTyVar, newBoxyTyVars, readFilledBox, + newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, -------------------------------- -- Instantiation @@ -33,7 +33,8 @@ module TcMType ( -- Checking type validity Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, - checkValidInstHead, instTypeErr, checkAmbiguity, + checkValidInstHead, checkValidInstance, checkAmbiguity, + checkInstTermination, arityErr, -------------------------------- @@ -57,10 +58,10 @@ import TypeRep ( Type(..), PredType(..), -- Friend; can see representation import TcType ( TcType, TcThetaType, TcTauType, TcPredType, TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), MetaDetails(..), SkolemInfo(..), BoxInfo(..), - BoxyTyVar, BoxyThetaType, BoxySigmaType, + BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType, UserTypeCtxt(..), isMetaTyVar, isSigTyVar, metaTvRef, - tcCmpPred, isClassPred, tcEqType, tcGetTyVar, + tcCmpPred, isClassPred, tcGetTyVar, tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, tcValidInstHeadTy, tcSplitForAllTys, tcIsTyVarTy, tcSplitSigmaTy, @@ -72,7 +73,7 @@ import TcType ( TcType, TcThetaType, TcTauType, TcPredType, pprPred, pprTheta, pprClassPred ) import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar, isLiftedTypeKind, isArgTypeKind, isOpenTypeKind, - liftedTypeKind, openTypeKind, defaultKind + liftedTypeKind, defaultKind ) import Type ( TvSubst, zipTopTvSubst, substTy ) import Class ( Class, classArity, className ) @@ -89,13 +90,16 @@ import Kind ( isSubKind ) -- others: import TcRnMonad -- TcType, amongst others -import FunDeps ( grow ) +import FunDeps ( grow, checkInstCoverage ) import Name ( Name, setNameUnique, mkSysTvName ) import VarSet -import DynFlags ( dopt, DynFlag(..) ) +import DynFlags ( dopt, DynFlag(..) ) import Util ( nOfThem, isSingleton, notNull ) -import ListSetOps ( removeDups, findDupsEq ) +import ListSetOps ( removeDups ) import Outputable + +import Control.Monad ( when ) +import Data.List ( (\\) ) \end{code} @@ -303,11 +307,14 @@ zonkSigTyVar sig_tv %************************************************************************ \begin{code} -newBoxyTyVar :: TcM BoxyTyVar -- Of openTypeKind -newBoxyTyVar = newMetaTyVar BoxTv openTypeKind +newBoxyTyVar :: Kind -> TcM BoxyTyVar +newBoxyTyVar kind = newMetaTyVar BoxTv kind + +newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar] +newBoxyTyVars kinds = mapM newBoxyTyVar kinds -newBoxyTyVars :: Int -> TcM [BoxyTyVar] -- Of openTypeKind -newBoxyTyVars n = sequenceM [newMetaTyVar BoxTv openTypeKind | i <- [1..n]] +newBoxyTyVarTys :: [Kind] -> TcM [BoxyType] +newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) } readFilledBox :: BoxyTyVar -> TcM TcType -- Read the contents of the box, which should be filled in by now @@ -863,14 +870,11 @@ data SourceTyCtxt -- f :: N a -> N a | InstThetaCtxt -- Context of an instance decl -- instance => C [a] where ... - | InstHeadCtxt -- Head of an instance decl - -- instance ... => Eq a where ... pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c) pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type") pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc) pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration") -pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration") pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type") \end{code} @@ -904,11 +908,7 @@ check_source_ty dflags ctxt pred@(ClassP cls tys) arity = classArity cls n_tys = length tys arity_err = arityErr "Class" class_name arity n_tys - - how_to_allow = case ctxt of - InstHeadCtxt -> empty -- Should not happen - InstThetaCtxt -> parens undecidableMsg - other -> parens (ptext SLIT("Use -fglasgow-exts to permit this")) + how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this")) check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty -- Implicit parameters only allows in type @@ -927,17 +927,13 @@ check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty) check_class_pred_tys dflags ctxt tys = case ctxt of TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine - InstHeadCtxt -> True -- We check for instance-head - -- formation in checkValidInstHead - InstThetaCtxt -> undecidable_ok || distinct_tyvars tys - other -> gla_exts || all tyvar_head tys + InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys + -- Further checks on head and theta in + -- checkInstTermination + other -> gla_exts || all tyvar_head tys where - undecidable_ok = dopt Opt_AllowUndecidableInstances dflags - gla_exts = dopt Opt_GlasgowExts dflags - -------------------------- -distinct_tyvars tys -- Check that the types are all distinct type variables - = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys) + gla_exts = dopt Opt_GlasgowExts dflags + undecidable_ok = dopt Opt_AllowUndecidableInstances dflags ------------------------- tyvar_head ty -- Haskell 98 allows predicates of form @@ -1030,7 +1026,7 @@ checkThetaCtxt ctxt theta ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty -predTyVarErr pred = sep [ptext SLIT("Non-type variables, or repeated type variables,"), +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) @@ -1080,15 +1076,12 @@ 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 - = check_tyvars dflags clas tys + = mapM_ check_one tys -- WITH HASKELL 98, MUST HAVE C (T a b c) - | isSingleton tys, - tcValidInstHeadTy first_ty - = returnM () - | otherwise - = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg) + = checkTc (isSingleton tys && tcValidInstHeadTy first_ty) + (instTypeErr (pprClassPred clas tys) head_shape_msg) where (first_ty : _) = tys @@ -1096,21 +1089,118 @@ check_inst_head dflags clas tys 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") -check_tyvars dflags clas tys - -- Check that at least one isn't a type variable - -- unless -fallow-undecideable-instances - | dopt Opt_AllowUndecidableInstances dflags = returnM () - | not (all tcIsTyVarTy tys) = returnM () - | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg) - where - msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head") - $$ undecidableMsg) + -- 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 + check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty + ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } -undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this") -\end{code} - -\begin{code} instTypeErr pp_ty msg = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, nest 4 msg] \end{code} + + +%************************************************************************ +%* * +\subsection{Checking instance for termination} +%* * +%************************************************************************ + + +\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 + + ; 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) $ + checkInstTermination theta inst_tys + + -- The Coverage Condition + ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) + (instTypeErr (pprClassPred clas inst_tys) msg) + } + where + msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies")) +\end{code} + +Termination test: 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. +This is only needed with -fglasgow-exts, as Haskell 98 restrictions +(which have already been checked) guarantee termination. + +The underlying idea is that + + for any ground substitution, each assertion in the + context has fewer type constructors than the head. + + +\begin{code} +checkInstTermination :: ThetaType -> [TcType] -> TcM () +checkInstTermination theta tys + = do { mappM_ (check_nomore (fvTypes tys)) theta + ; mappM_ (check_smaller (sizeTypes tys)) theta } + +check_nomore :: [TyVar] -> PredType -> TcM () +check_nomore fvs pred + = checkTc (null (fvPred pred \\ fvs)) + (predUndecErr pred nomoreMsg $$ parens undecidableMsg) + +check_smaller :: Int -> PredType -> TcM () +check_smaller n pred + = checkTc (sizePred pred < n) + (predUndecErr pred smallerMsg $$ parens undecidableMsg) + +predUndecErr pred msg = sep [msg, + nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)] + +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") + +-- Free variables of a type, retaining repetitions, and expanding synonyms +fvType :: Type -> [TyVar] +fvType ty | Just exp_ty <- tcView ty = fvType exp_ty +fvType (TyVarTy tv) = [tv] +fvType (TyConApp _ tys) = fvTypes tys +fvType (NoteTy _ ty) = fvType ty +fvType (PredTy pred) = fvPred pred +fvType (FunTy arg res) = fvType arg ++ fvType res +fvType (AppTy fun arg) = fvType fun ++ fvType arg +fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty) + +fvTypes :: [Type] -> [TyVar] +fvTypes tys = concat (map fvType tys) + +fvPred :: PredType -> [TyVar] +fvPred (ClassP _ tys') = fvTypes tys' +fvPred (IParam _ ty) = fvType ty + +-- Size of a type: the number of variables and constructors +sizeType :: Type -> Int +sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty +sizeType (TyVarTy _) = 1 +sizeType (TyConApp _ tys) = sizeTypes tys + 1 +sizeType (NoteTy _ ty) = sizeType ty +sizeType (PredTy pred) = sizePred pred +sizeType (FunTy arg res) = sizeType arg + sizeType res + 1 +sizeType (AppTy fun arg) = sizeType fun + sizeType arg +sizeType (ForAllTy _ ty) = sizeType ty + +sizeTypes :: [Type] -> Int +sizeTypes xs = sum (map sizeType xs) + +sizePred :: PredType -> Int +sizePred (ClassP _ tys') = sizeTypes tys' +sizePred (IParam _ ty) = sizeType ty +\end{code}