From 1cdafe99abae1628f34ca8c064e3a8c0fcdbd079 Mon Sep 17 00:00:00 2001 From: Ross Paterson Date: Mon, 6 Feb 2006 11:16:51 +0000 Subject: [PATCH] relaxed instance termination test With -fglasgow-exts but not -fallow-undecidable-instances, GHC 6.4 requires that instances be of the following form: (1) each assertion in the context must constrain distinct variables mentioned in the head, and (2) at least one argument of the head must be a non-variable type. This patch replaces these rules with the requirement that each assertion in the context satisfy (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 allows all instances permitted by the old rule, plus such instances as instance C a instance Show (s a) => Show (Sized s a) instance (Eq a, Show b) => C2 a b instance C2 Int a => C3 Bool [a] instance C2 Int a => C3 [a] b instance C4 a a => C4 [a] [a] but still ensures that under any substitution assertions in the context will be smaller than the head, so context reduction must terminate. This is probably the best we can do if we consider each instance in isolation. --- ghc/compiler/typecheck/TcInstDcls.lhs | 4 +- ghc/compiler/typecheck/TcMType.lhs | 113 +++++++++++++++++++++++++++------ 2 files changed, 95 insertions(+), 22 deletions(-) diff --git a/ghc/compiler/typecheck/TcInstDcls.lhs b/ghc/compiler/typecheck/TcInstDcls.lhs index 88dcd8e..3fec58d 100644 --- a/ghc/compiler/typecheck/TcInstDcls.lhs +++ b/ghc/compiler/typecheck/TcInstDcls.lhs @@ -13,7 +13,8 @@ import TcBinds ( mkPragFun, tcPrags, badBootDeclErr ) import TcClassDcl ( tcMethodBind, mkMethodBind, badMethodErr, tcClassDecl2, getGenericInstances ) import TcRnMonad -import TcMType ( tcSkolSigType, checkValidTheta, checkValidInstHead, instTypeErr, +import TcMType ( tcSkolSigType, checkValidTheta, checkValidInstHead, + checkInstTermination, instTypeErr, checkAmbiguity, SourceTyCtxt(..) ) import TcType ( mkClassPred, tyVarsOfType, tcSplitSigmaTy, tcSplitDFunHead, mkTyVarTys, @@ -195,6 +196,7 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags)) checkValidTheta InstThetaCtxt theta `thenM_` checkAmbiguity tyvars theta (tyVarsOfType tau) `thenM_` checkValidInstHead tau `thenM` \ (clas,inst_tys) -> + checkInstTermination theta inst_tys `thenM_` checkTc (checkInstFDs theta clas inst_tys) (instTypeErr (pprClassPred clas inst_tys) msg) `thenM_` newDFunName clas inst_tys (srcSpanStart loc) `thenM` \ dfun_name -> diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index 200bb26..df1f069 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -34,6 +34,7 @@ module TcMType ( Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, instTypeErr, checkAmbiguity, + checkInstTermination, arityErr, -------------------------------- @@ -60,7 +61,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, @@ -94,8 +95,10 @@ import Name ( Name, setNameUnique, mkSysTvName ) import VarSet import DynFlags ( dopt, DynFlag(..) ) import Util ( nOfThem, isSingleton, notNull ) -import ListSetOps ( removeDups, findDupsEq ) +import ListSetOps ( removeDups ) import Outputable + +import Data.List ( (\\) ) \end{code} @@ -906,6 +909,7 @@ check_source_ty dflags ctxt pred@(ClassP cls 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")) @@ -926,17 +930,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 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 @@ -1027,7 +1028,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) @@ -1077,7 +1078,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, @@ -1092,18 +1093,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} @@ -1111,3 +1100,85 @@ instTypeErr pp_ty msg = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, nest 4 msg] \end{code} + + +%************************************************************************ +%* * +\subsection{Checking instance for termination} +%* * +%************************************************************************ + +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 :: ThetaType -> [TcType] -> TcM () +checkInstTermination theta tys + = do + dflags <- getDOpts + check_inst_termination dflags theta tys + +check_inst_termination 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 +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} -- 1.7.10.4