import FiniteMap
import Bag
import Outputable
+import Maybes
import ListSetOps
import Util
import SrcLoc
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
(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!
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 )
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
\begin{code}
tcSimplifyInfer doc tau_tvs wanted
- = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars
+ = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+ ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars
; gbl_tvs <- tcGetGlobalTyVars
- ; let preds = fdPredsOfInsts wanted'
- qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
+ ; let preds1 = fdPredsOfInsts wanted'
+ gbl_tvs1 = oclose preds1 gbl_tvs
+ qtvs = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
-- See Note [Choosing which variables to quantify]
-- To maximise sharing, remove from consideration any
-- constraints that don't mention qtvs at all
- ; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted'
- ; extendLIEs free1
+ ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
+ ; extendLIEs free
-- To make types simple, reduce as much as possible
- ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$
- ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
+ ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$
+ ppr gbl_tvs1 $$ ppr free $$ ppr bound))
; (irreds1, binds1) <- tryHardCheckLoop doc bound
-- Note [Inference and implication constraints]
; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
- -- By now improvment may have taken place, and we must *not*
- -- quantify over any variable free in the environment
- -- tc137 (function h inside g) is an example
- ; gbl_tvs <- tcGetGlobalTyVars
- ; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs)
- ; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs))
-
- -- Do not quantify over constraints that *now* do not
- -- mention quantified type variables, because they are
- -- simply ambiguous (or might be bound further out). Example:
- -- f :: Eq b => a -> (a, b)
- -- g x = fst (f x)
- -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
- -- We decide to quantify over 'alpha' alone, but free1 does not include f77
- -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
- -- constraint (Eq beta), which we dump back into the free set
- -- See test tcfail181
- ; let (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2
- ; extendLIEs free3
-
+ -- Now work out all over again which type variables to quantify,
+ -- exactly in the same way as before, but starting from irreds2. Why?
+ -- a) By now improvment may have taken place, and we must *not*
+ -- quantify over any variable free in the environment
+ -- tc137 (function h inside g) is an example
+ --
+ -- b) Do not quantify over constraints that *now* do not
+ -- mention quantified type variables, because they are
+ -- simply ambiguous (or might be bound further out). Example:
+ -- f :: Eq b => a -> (a, b)
+ -- g x = fst (f x)
+ -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+ -- We decide to quantify over 'alpha' alone, but free1 does not include f77
+ -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
+ -- constraint (Eq beta), which we dump back into the free set
+ -- See test tcfail181
+ --
+ -- c) irreds may contain type variables not previously mentioned,
+ -- e.g. instance D a x => Foo [a]
+ -- wanteds = Foo [a]
+ -- Then after simplifying we'll get (D a x), and x is fresh
+ -- We must quantify over x else it'll be totally unbound
+ ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
+ ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
+ -- Note that we start from gbl_tvs1
+ -- We use tcGetGlobalTyVars, then oclose wrt preds2, because
+ -- we've already put some of the original preds1 into frees
+ -- E.g. wanteds = C a b (where a->b)
+ -- gbl_tvs = {a}
+ -- tau_tvs = {b}
+ -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
+ -- irreds2 will be empty. But we don't want to generalise over b!
+ ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked
+ qtvs = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
+ ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
+ ; extendLIEs free
+
+ -- Turn the quantified meta-type variables into real type variables
+ ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
+
-- We can't abstract over any remaining unsolved
-- implications so instead just float them outwards. Ugh.
; let (q_dicts, implics) = partition isDict irreds3
So our best approximation is to make (D [a]) part of the inferred
context, so we can use that to discharge the implication. Hence
-the strange function getImplicWanteds.
+the strange function get_dictsin approximateImplications.
The common cases are more clear-cut, when we have things like
forall a. C a => C b
ppr reft, ppr wanteds, ppr avails ])
; avails <- reduceList env' wanteds avails
- -- Extract the binding
+ -- Extract the results
+ -- Note [Reducing implication constraints]
; (binds, irreds) <- extractResults avails wanteds
-
+ ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds
+
; traceTc (text "reduceImplication result" <+> vcat
- [ ppr irreds, ppr binds])
+ [ ppr outer, ppr inner, ppr binds])
-- We always discard the extra avails we've generated;
-- but we remember if we have done any (global) improvement
; let ret_avails = updateImprovement orig_avails avails
- ; if isEmptyLHsBinds binds then -- No progress
+ ; if isEmptyLHsBinds binds && null outer then -- No progress
return (ret_avails, NoInstance)
else do
- { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+ { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens inner
; let dict_ids = map instToId extra_givens
co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
payload | [wanted] <- wanteds = HsVar (instToId wanted)
| otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
- -- If there are any irreds, we back off and return NoInstance
- ; return (ret_avails, GenInst implic_insts (L loc rhs))
+ ; return (ret_avails, GenInst (implic_insts ++ outer) (L loc rhs))
} }
\end{code}
+Note [Reducing implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are trying to simplify
+ (Ord a, forall b. C a b => (W [a] b, D c b))
+where
+ instance (C a b, Ord a) => W [a] b
+When solving the implication constraint, we'll start with
+ Ord a -> Irred
+in the Avails. Then we add (C a b -> Given) and solve. Extracting
+the results gives us a binding for the (W [a] b), with an Irred of
+(Ord a, D c b). Now, the (Ord a) comes from "outside" the implication,
+but the (D d b) is from "inside". So we want to generate a Rhs binding
+like this
+
+ ic = /\b \dc:C a b). (df a b dc do, ic' b dc)
+ depending on
+ do :: Ord a
+ ic' :: forall b. C a b => D c b
+
+The 'depending on' part of the Rhs is important, because it drives
+the extractResults code.
+
+The "inside" and "outside" distinction is what's going on with 'inner' and
+'outer' in reduceImplication
+
+
Note [Freeness and implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's hard to say when an implication constraint can be floated out. Consider
type AvailEnv = FiniteMap Inst AvailHow
data AvailHow
- = IsIrred TcId -- Used for irreducible dictionaries,
+ = IsIrred -- Used for irreducible dictionaries,
-- which are going to be lambda bound
| Given TcId -- Used for dictionaries for which we have a binding
-------------------------
pprAvail :: AvailHow -> SDoc
-pprAvail (IsIrred x) = text "Irred" <+> ppr x
+pprAvail IsIrred = text "Irred"
pprAvail (Given x) = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Rhs rhs bs) = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
-------------------------
extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
go avails binds irreds (w:ws)
= case findAvailEnv avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds ws
+ Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+ go avails binds irreds ws
Just (Given id)
| id == w_id -> go avails binds irreds ws
-- The sought Id can be one of the givens, via a superclass chain
-- and then we definitely don't want to generate an x=x binding!
- Just (IsIrred id)
- | id == w_id -> go (add_given avails w) binds (w:irreds) ws
- | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
+ Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
-- The add_given handles the case where we want (Ord a, Eq a), and we
-- don't want to emit *two* Irreds for Ord a, one via the superclass chain
-- This showed up in a dupliated Ord constraint in the error message for
\begin{code}
addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
- addAvailAndSCs want_scs avails irred (IsIrred (instToId irred))
+ addAvailAndSCs want_scs avails irred IsIrred
addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
addAvailAndSCs want_scs avails inst avail
= return (insts, emptyBag)
| null defaultable_groups
- = do { traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
; return (insts, emptyBag) }
| otherwise
= do { -- Figure out what default types to use
default_tys <- getDefaultTys extended_defaulting ovl_strings
- ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
; mapM_ (disambigGroup default_tys) defaultable_groups
-- disambigGroup does unification, hence try again
; 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;
(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
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 instance declarations")])]
where
ispecs = [ispec | (ispec, _) <- matches]
projects / ghc-hetmet.git / blobdiff