import FiniteMap
import Bag
import Outputable
+import Maybes
import ListSetOps
import Util
import SrcLoc
\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
parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"),
- ptext SLIT("when compiling the other instances")])]
+ ptext SLIT("when compiling the other instance declarations")])]
where
ispecs = [ispec | (ispec, _) <- matches]
projects / ghc-hetmet.git / blobdiff