From 8e512635b618e1daa97022265f268ad4eafda6b4 Mon Sep 17 00:00:00 2001 From: Ross Paterson Date: Mon, 13 Feb 2006 16:10:44 +0000 Subject: [PATCH] Loosen the rules for instance declarations (Part 3) Relax the restrictions on derived instances in the same way, so we can write data MinHeap h a = H a (h a) deriving (Show) --- ghc/compiler/typecheck/TcDeriv.lhs | 2 +- ghc/compiler/typecheck/TcMType.lhs | 21 +++++++------ ghc/compiler/typecheck/TcSimplify.lhs | 29 ++++++++++------- ghc/docs/users_guide/glasgow_exts.xml | 55 ++++++++++++++++++++------------- 4 files changed, 62 insertions(+), 45 deletions(-) diff --git a/ghc/compiler/typecheck/TcDeriv.lhs b/ghc/compiler/typecheck/TcDeriv.lhs index 3974bf0..472ce6b 100644 --- a/ghc/compiler/typecheck/TcDeriv.lhs +++ b/ghc/compiler/typecheck/TcDeriv.lhs @@ -727,7 +727,7 @@ solveDerivEqns overlap_flag orig_eqns gen_soln (_, clas, tc,tyvars,deriv_rhs) = setSrcSpan (srcLocSpan (getSrcLoc tc)) $ addErrCtxt (derivCtxt (Just clas) tc) $ - tcSimplifyDeriv tyvars deriv_rhs `thenM` \ theta -> + tcSimplifyDeriv tc tyvars deriv_rhs `thenM` \ theta -> returnM (sortLe (<=) theta) -- Canonicalise before returning the soluction ------------------------------------------------------------------ diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index 688a331..e865ecf 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, checkValidInstance, checkAmbiguity, + checkInstTermination, arityErr, -------------------------------- @@ -97,6 +98,7 @@ import Util ( nOfThem, isSingleton, notNull ) import ListSetOps ( removeDups ) import Outputable +import Control.Monad ( when ) import Data.List ( (\\) ) \end{code} @@ -1107,18 +1109,19 @@ instTypeErr pp_ty msg \begin{code} checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM () checkValidInstance tyvars theta clas inst_tys - = do { dflags <- getDOpts + = 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 termainate + -- Check that instance inference will terminate (if we care) -- For Haskell 98, checkValidTheta has already done that - ; checkInstTermination dflags theta inst_tys + ; when (gla_exts && not undecidable_ok) $ + checkInstTermination theta inst_tys -- The Coverage Condition - ; checkTc (dopt Opt_AllowUndecidableInstances dflags || - checkInstCoverage clas inst_tys) + ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) (instTypeErr (pprClassPred clas inst_tys) msg) } where @@ -1133,11 +1136,9 @@ 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 +checkInstTermination :: ThetaType -> [TcType] -> TcM () +checkInstTermination theta tys + = do mappM_ (check_nomore (fvTypes tys)) theta mappM_ (check_smaller (sizeTypes tys)) theta diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs index f187cdc..241b2e2 100644 --- a/ghc/compiler/typecheck/TcSimplify.lhs +++ b/ghc/compiler/typecheck/TcSimplify.lhs @@ -21,6 +21,7 @@ module TcSimplify ( #include "HsVersions.h" import {-# SOURCE #-} TcUnify( unifyType ) +import TypeRep ( Type(..) ) import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds ) import TcHsSyn ( mkHsApp, mkHsTyApp, mkHsDictApp ) @@ -41,7 +42,8 @@ import Inst ( lookupInst, LookupInstResult(..), import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders, lclEnvElts, tcMetaTy ) import InstEnv ( lookupInstEnv, classInstances, pprInstances ) -import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity ) +import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, + checkAmbiguity, checkInstTermination ) import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar, mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys, @@ -49,6 +51,7 @@ import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, import TcIface ( checkWiredInTyCon ) import Id ( idType, mkUserLocal ) import Var ( TyVar ) +import TyCon ( TyCon ) import Name ( Name, getOccName, getSrcLoc ) import NameSet ( NameSet, mkNameSet, elemNameSet ) import Class ( classBigSig, classKey ) @@ -2225,11 +2228,12 @@ a,b,c are type variables. This is required for the context of instance declarations. \begin{code} -tcSimplifyDeriv :: [TyVar] +tcSimplifyDeriv :: TyCon + -> [TyVar] -> ThetaType -- Wanted -> TcM ThetaType -- Needed -tcSimplifyDeriv tyvars theta +tcSimplifyDeriv tc tyvars theta = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) -> -- The main loop may do unification, and that may crash if -- it doesn't see a TcTyVar, so we have to instantiate. Sigh @@ -2238,6 +2242,7 @@ tcSimplifyDeriv tyvars theta simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) -> ASSERT( null frees ) -- reduceMe never returns Free + doptM Opt_GlasgowExts `thenM` \ gla_exts -> doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok -> let tv_set = mkVarSet tvs @@ -2247,15 +2252,7 @@ tcSimplifyDeriv tyvars theta = let pred = dictPred dict -- reduceMe squashes all non-dicts in isEmptyVarSet (tyVarsOfPred pred) -- Things like (Eq T) are bad - || (not undecidable_ok && not (isTyVarClassPred pred)) - -- The returned dictionaries should be of form (C a b) - -- (where a, b are type variables). - -- We allow non-tyvar dicts if we had -fallow-undecidable-instances, - -- but note that risks non-termination in the 'deriving' context-inference - -- fixpoint loop. It is useful for situations like - -- data Min h a = E | M a (h a) - -- which gives the instance decl - -- instance (Eq a, Eq (h a)) => Eq (Min h a) + || (not gla_exts && not (isTyVarClassPred pred)) simpl_theta = map dictPred ok_insts weird_preds = [pred | pred <- simpl_theta @@ -2269,11 +2266,19 @@ tcSimplifyDeriv tyvars theta rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars) -- This reverse-mapping is a Royal Pain, -- but the result should mention TyVars not TcTyVars + + head_ty = TyConApp tc (map TyVarTy tvs) in addNoInstanceErrs Nothing [] bad_insts `thenM_` mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_` checkAmbiguity tvs simpl_theta tv_set `thenM_` + -- Check instance termination as for user-declared instances. + -- unless we had -fallow-undecidable-instances (which risks + -- non-termination in the 'deriving' context-inference fixpoint + -- loop). + ifM (gla_exts && not undecidable_ok) + (checkInstTermination simpl_theta [head_ty]) `thenM_` returnM (substTheta rev_env simpl_theta) where doc = ptext SLIT("deriving classes for a data type") diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml index 3b38c1b..beaaad6 100644 --- a/ghc/docs/users_guide/glasgow_exts.xml +++ b/ghc/docs/users_guide/glasgow_exts.xml @@ -1933,8 +1933,9 @@ 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. +Furthermore, the assertions in the context of the instance declaration +must be of the form C a where a +is a type variable that occurs in the head. The flag loosens these restrictions @@ -1963,7 +1964,7 @@ corresponding type in the instance declaration. These restrictions ensure that context reduction terminates: each reduction -step makes the problem smaller +step makes the problem smaller by at least one constructor. For example, the following would make the type checker loop if it wasn't excluded: @@ -1989,34 +1990,52 @@ For example, these are OK: But these are not: - instance C a => C a where ... -- Context assertion no smaller than head - instance C b b => Foo [b] where ... + instance C a => C a where ... -- (C b b) has more more occurrences of b than the head + instance C b b => Foo [b] where ... -A couple of useful idioms are these. First, -if one allows overlapping instance declarations then it's quite +The same restrictions apply to instances generated by +deriving clauses. Thus the following is accepted: + + data MinHeap h a = H a (h a) + deriving (Show) + +because the derived instance + + instance (Show a, Show (h a)) => Show (MinHeap h a) + +conforms to the above rules. + + + +A useful idiom permitted by the above rules is as follows. +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": - + +Undecidable instances + +Sometimes even the rules of are too onerous. +For example, 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 => ... @@ -2024,17 +2043,9 @@ instead of f :: (C1 a, C2 a, C3 a) => ... - - - - -Undecidable instances - - -Sometimes even the rules of are too onerous. -For example, with functional dependencies () -it is tempting to introduce type variables in the context that do not appear in +The restrictions on functional dependencies () are particularly troublesome. +It is tempting to introduce type variables in the context that do not appear in the head, something that is excluded by the normal rules. For example: class HasConverter a b | a -> b where -- 1.7.10.4