From: simonpj@microsoft.com Date: Thu, 9 Feb 2006 10:21:29 +0000 (+0000) Subject: Loosen the rules for instance declarations (Part 2) X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=59c9c122f942f348008d4ed8ba088286343d63d3 Loosen the rules for instance declarations (Part 2) Tidying up to Ross's patch, plus adding documenation for it. --- diff --git a/ghc/compiler/typecheck/TcInstDcls.lhs b/ghc/compiler/typecheck/TcInstDcls.lhs index 3fec58d..45338d0 100644 --- a/ghc/compiler/typecheck/TcInstDcls.lhs +++ b/ghc/compiler/typecheck/TcInstDcls.lhs @@ -13,12 +13,9 @@ import TcBinds ( mkPragFun, tcPrags, badBootDeclErr ) import TcClassDcl ( tcMethodBind, mkMethodBind, badMethodErr, tcClassDecl2, getGenericInstances ) import TcRnMonad -import TcMType ( tcSkolSigType, checkValidTheta, checkValidInstHead, - checkInstTermination, instTypeErr, - checkAmbiguity, SourceTyCtxt(..) ) -import TcType ( mkClassPred, tyVarsOfType, - tcSplitSigmaTy, tcSplitDFunHead, mkTyVarTys, - SkolemInfo(InstSkol), tcSplitDFunTy, pprClassPred ) +import TcMType ( tcSkolSigType, checkValidInstance, checkValidInstHead ) +import TcType ( mkClassPred, tcSplitSigmaTy, tcSplitDFunHead, mkTyVarTys, + SkolemInfo(InstSkol), tcSplitDFunTy ) import Inst ( tcInstClassOp, newDicts, instToId, showLIE, getOverlapFlag, tcExtendLocalInstEnv ) import InstEnv ( mkLocalInstance, instanceDFunId ) @@ -33,8 +30,7 @@ import Type ( zipOpenTvSubst, substTheta, substTys ) import DataCon ( classDataCon ) import Class ( classBigSig ) import Var ( Id, idName, idType ) -import MkId ( mkDictFunId, rUNTIME_ERROR_ID ) -import FunDeps ( checkInstFDs ) +import MkId ( mkDictFunId ) import Name ( Name, getSrcLoc ) import Maybe ( catMaybes ) import SrcLoc ( srcLocSpan, unLoc, noLoc, Located(..), srcSpanStart ) @@ -186,32 +182,25 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags)) setSrcSpan loc $ addErrCtxt (instDeclCtxt1 poly_ty) $ + do { is_boot <- tcIsHsBoot + ; checkTc (not is_boot || (isEmptyLHsBinds binds && null uprags)) + badBootDeclErr + -- Typecheck the instance type itself. We can't use -- tcHsSigType, because it's not a valid user type. - kcHsSigType poly_ty `thenM` \ kinded_ty -> - tcHsKindedType kinded_ty `thenM` \ poly_ty' -> - let - (tyvars, theta, tau) = tcSplitSigmaTy poly_ty' - in - 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 -> - getOverlapFlag `thenM` \ overlap_flag -> - let dfun = mkDictFunId dfun_name tyvars theta clas inst_tys - ispec = mkLocalInstance dfun overlap_flag - in - - tcIsHsBoot `thenM` \ is_boot -> - checkTc (not is_boot || (isEmptyLHsBinds binds && null uprags)) - badBootDeclErr `thenM_` - - returnM (Just (InstInfo { iSpec = ispec, iBinds = VanillaInst binds uprags })) - where - msg = parens (ptext SLIT("the instance types do not agree with the functional dependencies of the class")) + ; kinded_ty <- kcHsSigType poly_ty + ; poly_ty' <- tcHsKindedType kinded_ty + ; let (tyvars, theta, tau) = tcSplitSigmaTy poly_ty' + + ; (clas, inst_tys) <- checkValidInstHead tau + ; checkValidInstance tyvars theta clas inst_tys + + ; dfun_name <- newDFunName clas inst_tys (srcSpanStart loc) + ; overlap_flag <- getOverlapFlag + ; let dfun = mkDictFunId dfun_name tyvars theta clas inst_tys + ispec = mkLocalInstance dfun overlap_flag + + ; return (Just (InstInfo { iSpec = ispec, iBinds = VanillaInst binds uprags })) } \end{code} @@ -401,9 +390,6 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = binds }) -- member) are dealt with by the common MkId.mkDataConWrapId code rather -- than needing to be repeated here. - where - msg = "Compiler error: bad dictionary " ++ showSDoc (ppr clas) - dict_bind = noLoc (VarBind this_dict_id dict_rhs) all_binds = dict_bind `consBag` (sc_binds `unionBags` meth_binds) diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index df1f069..3a232b7 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -33,8 +33,7 @@ module TcMType ( -- Checking type validity Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, - checkValidInstHead, instTypeErr, checkAmbiguity, - checkInstTermination, + checkValidInstHead, checkValidInstance, checkAmbiguity, arityErr, -------------------------------- @@ -90,10 +89,10 @@ import Kind ( isSubKind ) -- others: import TcRnMonad -- TcType, amongst others -import FunDeps ( grow ) +import FunDeps ( grow, checkInstFDs ) import Name ( Name, setNameUnique, mkSysTvName ) import VarSet -import DynFlags ( dopt, DynFlag(..) ) +import DynFlags ( dopt, DynFlag(..), DynFlags ) import Util ( nOfThem, isSingleton, notNull ) import ListSetOps ( removeDups ) import Outputable @@ -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,10 +925,10 @@ 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 gla_exts = dopt Opt_GlasgowExts dflags @@ -1108,6 +1103,27 @@ instTypeErr pp_ty msg %* * %************************************************************************ + +\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 (checkInstFDs theta 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 @@ -1116,13 +1132,8 @@ 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 +checkInstTermination :: DynFlags -> ThetaType -> [TcType] -> TcM () +checkInstTermination dflags theta tys | not (dopt Opt_GlasgowExts dflags) = returnM () | dopt Opt_AllowUndecidableInstances dflags = returnM () | otherwise = do @@ -1146,7 +1157,7 @@ nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the i 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 +-- 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] @@ -1164,7 +1175,7 @@ fvPred :: PredType -> [TyVar] fvPred (ClassP _ tys') = fvTypes tys' fvPred (IParam _ ty) = fvType ty --- size of a type: the number of variables and constructors +-- 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 diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml index 4d7577d..a5ac2b3 100644 --- a/ghc/docs/users_guide/glasgow_exts.xml +++ b/ghc/docs/users_guide/glasgow_exts.xml @@ -1673,38 +1673,124 @@ class like this: Instance declarations - -Instance heads + +Relaxed rules for instance declarations + +An instance declaration has the form + + instance ( assertion1, ..., assertionn) => class type1 ... typem where ... + +The part before the "=>" is the +context, while the part after the +"=>" is the head of the instance declaration. + -The head of an instance declaration is the part to the -right of the "=>". In Haskell 98 the head of an instance -declaration +In Haskell 98 the head of an instance declaration must be of the form C (T a1 ... an), where C is the class, T is a type constructor, and the a1 ... an are distinct type variables. +Furthermore, the assertions in the context of the instance declaration be of +the form C a where a is a type variable. -The flag lifts this restriction and allows the -instance head to be of form C t1 ... tn where t1 -... tn are arbitrary types (provided, of course, everything is -well-kinded). In particular, types ti can be type variables -or structured types, and can contain repeated occurrences of a single type -variable. -Examples: +The flag loosens these restrictions +considerably. Firstly, multi-parameter type classes are permitted. Secondly, +the context and head of the instance declaration can each consist of arbitrary +(well-kinded) assertions (C t1 ... tn) subject only to the following rule: +for each assertion in the context + +No type variable has more occurrences in the assertion than in the head +Tthe assertion has fewer constructors and variables (taken together + and counting repetitions) than the head + +These restrictions ensure that context reduction terminates: each reduction +step makes the problem smaller +constructor. For example, the following would make the type checker +loop if it wasn't excluded: + + instance C a => C a where ... + +For example, these are OK: - instance Eq (T a a) where ... - -- Repeated type variable + instance C Int [a] -- Multiple parameters + instance Eq (S [a]) -- Structured type in head - instance Eq (S [a]) where ... - -- Structured type + -- Repeated type variable in head + instance C4 a a => C4 [a] [a] + instance Stateful (ST s) (MutVar s) - instance C Int [a] where ... - -- Multiple parameters + -- Head can consist of type variables only + instance C a + instance (Eq a, Show b) => C2 a b + + -- Non-type variables in context + instance Show (s a) => Show (Sized s a) + instance C2 Int a => C3 Bool [a] + instance C2 Int a => C3 [a] b + +But these are not: + + instance C a => C a where ... + -- Context assertion no smaller than head + instance C b b => Foo [b] where ... + -- (C b b) has more more occurrences of b than the head + + +A couple of useful idioms are these. First, +if one allows overlapping instance declarations then it's quite +convenient to have a "default instance" declaration that applies if +something more specific does not: + + instance C a where + op = ... -- Default + + +Second, sometimes you might want to use the following to get the +effect of a "class synonym": + + + + class (C1 a, C2 a, C3 a) => C a where { } + + instance (C1 a, C2 a, C3 a) => C a where { } + +This allows you to write shorter signatures: + + + f :: C a => ... + +instead of + + f :: (C1 a, C2 a, C3 a) => ... + + + + + +Undecidable instances + + +Sometimes even the rules of are too onerous. +Voluminous correspondence on the Haskell mailing list has convinced me +that it's worth experimenting with more liberal rules. If you use +the experimental flag +-fallow-undecidable-instances +option, you can use arbitrary +types in both an instance context and instance head. Termination is ensured by having a +fixed-depth recursion stack. If you exceed the stack depth you get a +sort of backtrace, and the opportunity to increase the stack depth +with N. + + +I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while +allowing these idioms interesting idioms. + + Overlapping instances @@ -1835,117 +1921,6 @@ reversed, but it makes sense to me. - -Undecidable instances - -An instance declaration must normally obey the following rules: - -At least one of the types in the head of -an instance declaration must not be a type variable. -For example, these are OK: - - - instance C Int a where ... - - instance D (Int, Int) where ... - - instance E [[a]] where ... - -but this is not: - - instance F a where ... - -Note that instance heads may contain repeated type variables (). -For example, this is OK: - - instance Stateful (ST s) (MutVar s) where ... - - - - - - -All of the types in the context of -an instance declaration must be type variables, and -there must be no repeated type variables in any one constraint. -Thus - -instance C a b => Eq (a,b) where ... - -is OK, but - -instance C Int b => Foo [b] where ... - -is not OK (because of the non-type-variable Int in the context), and nor is - -instance C b b => Foo [b] where ... - -(because of the repeated type variable). - - - -These restrictions ensure that -context reduction terminates: each reduction step removes one type -constructor. For example, the following would make the type checker -loop if it wasn't excluded: - - instance C a => C a where ... - -There are two situations in which the rule is a bit of a pain. First, -if one allows overlapping instance declarations then it's quite -convenient to have a "default instance" declaration that applies if -something more specific does not: - - - - instance C a where - op = ... -- Default - - - -Second, sometimes you might want to use the following to get the -effect of a "class synonym": - - - - class (C1 a, C2 a, C3 a) => C a where { } - - instance (C1 a, C2 a, C3 a) => C a where { } - - - -This allows you to write shorter signatures: - - - - f :: C a => ... - - - -instead of - - - - f :: (C1 a, C2 a, C3 a) => ... - - - -Voluminous correspondence on the Haskell mailing list has convinced me -that it's worth experimenting with more liberal rules. If you use -the experimental flag --fallow-undecidable-instances -option, you can use arbitrary -types in both an instance context and instance head. Termination is ensured by having a -fixed-depth recursion stack. If you exceed the stack depth you get a -sort of backtrace, and the opportunity to increase the stack depth -with N. - - -I'm on the lookout for a less brutal solution: a simple rule that preserves decidability while -allowing these idioms interesting idioms. - - -