X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=db1201131b761bf022568cf5dd32446e4fa83b58;hb=0f5731ee92009fe43e9cc0bd276b4562e0c37089;hp=32fe6cf866ab2166a770aef740222cf62cd3a715;hpb=5c2ecdff9b9e814c2549da0b3efd61d5107c72d6;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 32fe6cf..db12011 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -132,14 +132,9 @@ from. The Right Thing is to improve whenever the constraint set changes at all. Not hard in principle, but it'll take a bit of fiddling to do. - - - -------------------------------------- - Notes on quantification - -------------------------------------- - -Suppose we are about to do a generalisation step. -We have in our hand +Note [Choosing which variables to quantify] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are about to do a generalisation step. We have in our hand G the environment T the type of the RHS @@ -162,11 +157,12 @@ Here are the things that *must* be true: (A) Q intersect fv(G) = EMPTY limits how big Q can be (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be -(A) says we can't quantify over a variable that's free in the -environment. (B) says we must quantify over all the truly free -variables in T, else we won't get a sufficiently general type. We do -not *need* to quantify over any variable that is fixed by the free -vars of the environment G. + (A) says we can't quantify over a variable that's free in the environment. + (B) says we must quantify over all the truly free variables in T, else + we won't get a sufficiently general type. + +We do not *need* to quantify over any variable that is fixed by the +free vars of the environment G. BETWEEN THESE TWO BOUNDS, ANY Q WILL DO! @@ -180,38 +176,15 @@ Example: class H x y | x->y where ... So Q can be {c,d}, {b,c,d} +In particular, it's perfectly OK to quantify over more type variables +than strictly necessary; there is no need to quantify over 'b', since +it is determined by 'a' which is free in the envt, but it's perfectly +OK to do so. However we must not quantify over 'a' itself. + Other things being equal, however, we'd like to quantify over as few variables as possible: smaller types, fewer type applications, more -constraints can get into Ct instead of Cq. - - ------------------------------------------ -We will make use of - - fv(T) the free type vars of T - - oclose(vs,C) The result of extending the set of tyvars vs - using the functional dependencies from C - - grow(vs,C) The result of extend the set of tyvars vs - using all conceivable links from C. - - E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e} - Then grow(vs,C) = {a,b,c} - - Note that grow(vs,C) `superset` grow(vs,simplify(C)) - That is, simplfication can only shrink the result of grow. - -Notice that - oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs - grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C) - - ------------------------------------------ - -Note [Choosing which variables to quantify] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Here's a good way to choose Q: +constraints can get into Ct instead of Cq. Here's a good way to +choose Q: Q = grow( fv(T), C ) \ oclose( fv(G), C ) @@ -245,9 +218,8 @@ all the functional dependencies yet: T = c->c C = (Eq (T c d)) - Now oclose(fv(T),C) = {c}, because the functional dependency isn't - apparent yet, and that's wrong. We must really quantify over d too. - +Now oclose(fv(T),C) = {c}, because the functional dependency isn't +apparent yet, and that's wrong. We must really quantify over d too. There really isn't any point in quantifying over any more than grow( fv(T), C ), because the call sites can't possibly influence @@ -2522,19 +2494,60 @@ tcSimplifyDeriv orig tyvars theta ; wanteds <- newDictBndrsO orig (substTheta tenv theta) ; (irreds, _) <- tryHardCheckLoop doc wanteds + ; let (tv_dicts, others) = partition isTyVarDict irreds + ; addNoInstanceErrs others + ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars) - simpl_theta = substTheta rev_env (map dictPred irreds) + simpl_theta = substTheta rev_env (map dictPred tv_dicts) -- This reverse-mapping is a pain, but the result -- should mention the original TyVars not TcTyVars - -- NB: the caller will further check the tv_dicts for - -- legal instance-declaration form - ; return simpl_theta } where doc = ptext SLIT("deriving classes for a data type") \end{code} +Note [Exotic derived instance contexts] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + data T a b c = MkT (Foo a b c) deriving( Eq ) + instance (C Int a, Eq b, Eq c) => Eq (Foo a b c) + +Notice that this instance (just) satisfies the Paterson termination +conditions. Then we *could* derive an instance decl like this: + + instance (C Int a, Eq b, Eq c) => Eq (T a b c) + +even though there is no instance for (C Int a), because there just +*might* be an instance for, say, (C Int Bool) at a site where we +need the equality instance for T's. + +However, this seems pretty exotic, and it's quite tricky to allow +this, and yet give sensible error messages in the (much more common) +case where we really want that instance decl for C. + +So for now we simply require that the derived instance context +should have only type-variable constraints. + +Here is another example: + data Fix f = In (f (Fix f)) deriving( Eq ) +Here, if we are prepared to allow -fallow-undecidable-instances we +could derive the instance + instance Eq (f (Fix f)) => Eq (Fix f) +but this is so delicate that I don't think it should happen inside +'deriving'. If you want this, write it yourself! + +NB: if you want to lift this condition, make sure you still meet the +termination conditions! If not, the deriving mechanism generates +larger and larger constraints. Example: + data Succ a = S a + data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show + +Note the lack of a Show instance for Succ. First we'll generate + instance (Show (Succ a), Show a) => Show (Seq a) +and then + instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a) +and so on. Instead we want to complain of no instance for (Show (Succ a)). @tcSimplifyDefault@ just checks class-type constraints, essentially; @@ -2675,11 +2688,11 @@ report_no_instances tidy_env mb_what insts (clas,tys) = getDictClassTys wanted mk_overlap_msg dict (matches, unifiers) - = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") + = ASSERT( not (null matches) ) + vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") <+> pprPred (dictPred dict))), sep [ptext SLIT("Matching instances") <> colon, nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])], - ASSERT( not (null matches) ) if not (isSingleton matches) then -- Two or more matches empty @@ -2687,7 +2700,8 @@ report_no_instances tidy_env mb_what insts ASSERT( not (null unifiers) ) parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+> quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))), - ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])] + ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"), + ptext SLIT("when compiling the other instances")])] where ispecs = [ispec | (ispec, _) <- matches]