X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMType.lhs;h=688a331b57fe1cff799a08333408b6a2a8956af7;hb=ad68b91e2126681fba942f3038bcf32f9a1e7259;hp=b8ea73a592d2f02910b77c8719d7c8d9b41d3fe6;hpb=c362e21663e6222c01be3106c80ea9452c4ae222;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index b8ea73a..688a331 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -33,7 +33,7 @@ module TcMType ( -- Checking type validity Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, - checkValidInstHead, instTypeErr, checkAmbiguity, + checkValidInstHead, checkValidInstance, checkAmbiguity, arityErr, -------------------------------- @@ -60,7 +60,7 @@ import TcType ( TcType, TcThetaType, TcTauType, TcPredType, BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType, UserTypeCtxt(..), isMetaTyVar, isSigTyVar, metaTvRef, - tcCmpPred, isClassPred, tcEqType, tcGetTyVar, + tcCmpPred, isClassPred, tcGetTyVar, tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, tcValidInstHeadTy, tcSplitForAllTys, tcIsTyVarTy, tcSplitSigmaTy, @@ -89,13 +89,15 @@ 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(..), DynFlags ) import Util ( nOfThem, isSingleton, notNull ) -import ListSetOps ( removeDups, findDupsEq ) +import ListSetOps ( removeDups ) import Outputable + +import Data.List ( (\\) ) \end{code} @@ -866,14 +868,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} @@ -907,11 +906,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 @@ -930,19 +925,14 @@ 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 || 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) - -------------------------- tyvar_head ty -- Haskell 98 allows predicates of form | tcIsTyVarTy ty = True -- C (a ty1 .. tyn) | otherwise -- where a is a type variable @@ -1033,7 +1023,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) @@ -1083,7 +1073,7 @@ 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 + = returnM () -- WITH HASKELL 98, MUST HAVE C (T a b c) | isSingleton tys, @@ -1098,18 +1088,6 @@ 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) - -undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this") \end{code} \begin{code} @@ -1117,3 +1095,102 @@ 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 { dflags <- getDOpts + + ; checkValidTheta InstThetaCtxt theta + ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys) + + -- Check that instance inference will termainate + -- For Haskell 98, checkValidTheta has already done that + ; checkInstTermination dflags theta inst_tys + + -- The Coverage Condition + ; checkTc (dopt Opt_AllowUndecidableInstances dflags || + checkInstCoverage clas inst_tys) + (instTypeErr (pprClassPred clas inst_tys) msg) + } + where + msg = parens (ptext SLIT("the instance types do not agree with the functional dependencies of the class")) +\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. + +\begin{code} +checkInstTermination :: DynFlags -> ThetaType -> [TcType] -> TcM () +checkInstTermination dflags theta tys + | not (dopt Opt_GlasgowExts dflags) = returnM () + | dopt Opt_AllowUndecidableInstances dflags = returnM () + | otherwise = 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}