tcSimplifyBracket, tcSimplifyCheckPat,
tcSimplifyDeriv, tcSimplifyDefault,
- bindInstsOfLocalFuns, bindIrreds,
+ bindInstsOfLocalFuns,
misMatchMsg
) where
import Inst
import TcEnv
import InstEnv
-import TcGadt
import TcType
import TcMType
import TcIface
Note [Implicit parameters and ambiguity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What type should we infer for this?
- f x = (show ?y, x::Int)
-Since we must quantify over the ?y, the most plausible type is
- f :: (Show a, ?y::a) => Int -> (String, Int)
-But notice that the type of the RHS is (String,Int), with no type
-varibables mentioned at all! The type of f looks ambiguous. But
-it isn't, because at a call site we might have
- let ?y = 5::Int in f 7
+Only a *class* predicate can give rise to ambiguity
+An *implicit parameter* cannot. For example:
+ foo :: (?x :: [a]) => Int
+ foo = length ?x
+is fine. The call site will suppply a particular 'x'
+
+Furthermore, the type variables fixed by an implicit parameter
+propagate to the others. E.g.
+ foo :: (Show a, ?x::[a]) => Int
+ foo = show (?x++?x)
+The type of foo looks ambiguous. But it isn't, because at a call site
+we might have
+ let ?x = 5::Int in foo
and all is well. In effect, implicit parameters are, well, parameters,
so we can take their type variables into account as part of the
"tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
\begin{code}
tcSimplifyInfer doc tau_tvs wanted
= do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars
+ ; wanted' <- mapM zonkInst wanted -- Zonk before deciding quantified tyvars
; gbl_tvs <- tcGetGlobalTyVars
; let preds1 = fdPredsOfInsts wanted'
gbl_tvs1 = oclose preds1 gbl_tvs
-- Prepare equality instances for quantification
; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
- ; q_eqs <- mappM finalizeEqInst q_eqs0
+ ; q_eqs <- mapM finalizeEqInst q_eqs0
; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
-- NB: when we are done, we might have some bindings, but
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 get_dictsin approximateImplications.
+the strange function get_dicts in approximateImplications.
The common cases are more clear-cut, when we have things like
forall a. C a => C b
tcSimplifyInferCheck loc tau_tvs givens wanteds
= do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
- ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
-- Figure out which type variables to quantify over
-- You might think it should just be the signature tyvars,
-----------------------------------------------------------
-- tcSimplifyCheckPat is used for existential pattern match
tcSimplifyCheckPat :: InstLoc
- -> [CoVar] -> Refinement
-> [TcTyVar] -- Quantify over these
-> [Inst] -- Given
-> [Inst] -- Wanted
-> TcM TcDictBinds -- Bindings
-tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
+tcSimplifyCheckPat loc qtvs givens wanteds
= ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
do { traceTc (text "tcSimplifyCheckPat")
; (irreds, binds) <- gentleCheckLoop loc givens wanteds
- ; implic_bind <- bindIrredsR loc qtvs co_vars reft
- givens irreds
+ ; implic_bind <- bindIrredsR loc qtvs givens irreds
; return (binds `unionBags` implic_bind) }
-----------------------------------------------------------
-> [Inst] -> [Inst]
-> TcM TcDictBinds
bindIrreds loc qtvs givens irreds
- = bindIrredsR loc qtvs [] emptyRefinement givens irreds
+ = bindIrredsR loc qtvs givens irreds
-bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar]
- -> Refinement -> [Inst] -> [Inst]
- -> TcM TcDictBinds
+bindIrredsR :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds
-- Make a binding that binds 'irreds', by generating an implication
-- constraint for them, *and* throwing the constraint into the LIE
-bindIrredsR loc qtvs co_vars reft givens irreds
+bindIrredsR loc qtvs givens irreds
| null irreds
= return emptyBag
| otherwise
- = do { let givens' = filter isDict givens
- -- The givens can include methods
+ = do { let givens' = filter isAbstractableInst givens
+ -- The givens can (redundantly) include methods
+ -- We want to retain both EqInsts and Dicts
+ -- There should be no implicadtion constraints
-- See Note [Pruning the givens in an implication constraint]
- -- If there are no 'givens' *and* the refinement is empty
- -- (the refinement is like more givens), then it's safe to
+ -- If there are no 'givens', then it's safe to
-- partition the 'wanteds' by their qtvs, thereby trimming irreds
-- See Note [Freeness and implications]
- ; irreds' <- if null givens' && isEmptyRefinement reft
+ ; irreds' <- if null givens'
then do
{ let qtv_set = mkVarSet qtvs
(frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
; return real_irreds }
else return irreds
- ; let all_tvs = qtvs ++ co_vars -- Abstract over all these
- ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
+ ; (implics, bind) <- makeImplicationBind loc qtvs givens' irreds'
-- This call does the real work
-- If irreds' is empty, it does something sensible
; extendLIEs implics
; return bind }
-makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
+makeImplicationBind :: InstLoc -> [TcTyVar]
-> [Inst] -> [Inst]
-> TcM ([Inst], TcDictBinds)
-- Make a binding that binds 'irreds', by generating an implication
-- qtvs includes coercion variables
--
-- This binding must line up the 'rhs' in reduceImplication
-makeImplicationBind loc all_tvs reft
- givens -- Guaranteed all Dicts (TOMDO: true?)
+makeImplicationBind loc all_tvs
+ givens -- Guaranteed all Dicts
+ -- or EqInsts
irreds
| null irreds -- If there are no irreds, we are done
= return ([], emptyBag)
| otherwise -- Otherwise we must generate a binding
= do { uniq <- newUnique
; span <- getSrcSpanM
- ; let (eq_givens,dict_givens) = partitionGivenEqInsts givens
- eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
+ ; let (eq_givens, dict_givens) = partition isEqInst givens
+ eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens)
+ -- Urgh! See line 2187 or thereabouts. I believe that all these
+ -- 'givens' must be a simple CoVar. This MUST be cleaned up.
+
; let name = mkInternalName uniq (mkVarOcc "ic") span
- implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
+ implic_inst = ImplicInst { tci_name = name,
tci_tyvars = all_tvs,
tci_given = (eq_givens ++ dict_givens),
tci_wanted = irreds, tci_loc = loc }
- ; let
- -- only create binder for dict_irreds
- -- we
- (eq_irreds,dict_irreds) = partitionWantedEqInsts irreds
+ ; let -- only create binder for dict_irreds
+ (eq_irreds, dict_irreds) = partition isEqInst irreds
n_dict_irreds = length dict_irreds
dict_irred_ids = map instToId dict_irreds
tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
- co = mkWpApps (map instToId dict_givens) <.> mkWpTyApps eq_tyvar_cos <.> mkWpTyApps (mkTyVarTys all_tvs)
+ co = mkWpApps (map instToId dict_givens)
+ <.> mkWpTyApps eq_tyvar_cos
+ <.> mkWpTyApps (mkTyVarTys all_tvs)
bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs
| otherwise = PatBind { pat_lhs = L span pat,
pat_rhs = unguardedGRHSs rhs,
pat_rhs_ty = tup_ty,
bind_fvs = placeHolderNames }
- ; -- pprTrace "Make implic inst" (ppr (implic_inst,irreds,dict_irreds,tup_ty)) $
- return ([implic_inst], unitBag (L span bind)) }
+ ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
+ ; return ([implic_inst], unitBag (L span bind))
+ }
-----------------------------------------------------------
tryHardCheckLoop :: SDoc
-> TcM ([Inst], TcDictBinds)
tryHardCheckLoop doc wanteds
- = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds
+ = do { (irreds,binds) <- checkLoop (mkRedEnv doc try_me []) wanteds
; return (irreds,binds)
}
where
-> TcM ([Inst], TcDictBinds)
gentleCheckLoop inst_loc givens wanteds
- = do { (irreds,binds,_) <- checkLoop env wanteds
+ = do { (irreds,binds) <- checkLoop env wanteds
; return (irreds,binds)
}
where
| otherwise = Stop
-- When checking against a given signature
-- we MUST be very gentle: Note [Check gently]
+
+gentleInferLoop :: SDoc -> [Inst]
+ -> TcM ([Inst], TcDictBinds)
+gentleInferLoop doc wanteds
+ = do { (irreds, binds) <- checkLoop env wanteds
+ ; return (irreds, binds) }
+ where
+ env = mkRedEnv doc try_me []
+ try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ | otherwise = Stop
\end{code}
Note [Check gently]
Hence we have a dictionary for Show [a] available; and indeed we
need it. We are going to build an implication contraint
forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledg e(Show b)
+Later, we will solve this constraint using the knowledge (Show b)
But we MUST NOT reduce (Show [a]) to (Show a), else the whole
thing becomes insoluble. So we simplify gently (get rid of literals
-----------------------------------------------------------
checkLoop :: RedEnv
-> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds,
- [Inst]) -- needed givens
+ -> TcM ([Inst], TcDictBinds)
-- Precondition: givens are completely rigid
-- Postcondition: returned Insts are zonked
checkLoop env wanteds
- = go env wanteds []
- where go env wanteds needed_givens
- = do { -- Givens are skolems, so no need to zonk them
- wanteds' <- zonkInsts wanteds
+ = go env wanteds (return ())
+ where go env wanteds elim_skolems
+ = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+ ; env' <- zonkRedEnv env
+ ; wanteds' <- zonkInsts wanteds
- ; (improved, binds, irreds, more_needed_givens) <- reduceContext env wanteds'
+ ; (improved, binds, irreds, elim_more_skolems)
+ <- reduceContext env' wanteds'
+ ; let elim_skolems' = elim_skolems >> elim_more_skolems
- ; let all_needed_givens = needed_givens ++ more_needed_givens
-
; if not improved then
- return (irreds, binds, all_needed_givens)
+ elim_skolems' >> return (irreds, binds)
else do
-- If improvement did some unification, we go round again.
-- We start again with irreds, not wanteds
- -- Using an instance decl might have introduced a fresh type variable
- -- which might have been unified, so we'd get an infinite loop
- -- if we started again with wanteds! See Note [LOOP]
- { (irreds1, binds1, all_needed_givens1) <- go env irreds all_needed_givens
- ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
+ -- Using an instance decl might have introduced a fresh type
+ -- variable which might have been unified, so we'd get an
+ -- infinite loop if we started again with wanteds!
+ -- See Note [LOOP]
+ { (irreds1, binds1) <- go env' irreds elim_skolems'
+ ; return (irreds1, binds `unionBags` binds1) } }
\end{code}
+Note [Zonking RedEnv]
+~~~~~~~~~~~~~~~~~~~~~
+It might appear as if the givens in RedEnv are always rigid, but that is not
+necessarily the case for programs involving higher-rank types that have class
+contexts constraining the higher-rank variables. An example from tc237 in the
+testsuite is
+
+ class Modular s a | s -> a
+
+ wim :: forall a w. Integral a
+ => a -> (forall s. Modular s a => M s w) -> w
+ wim i k = error "urk"
+
+ test5 :: (Modular s a, Integral a) => M s a
+ test5 = error "urk"
+
+ test4 = wim 4 test4'
+
+Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
+quantified further outside. When type checking test4, we have to check
+whether the signature of test5 is an instance of
+
+ (forall s. Modular s a => M s w)
+
+Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
+givens.
+
+Given the FD of Modular in this example, class improvement will instantiate
+t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
+Modular s a predicate in that signature). If we don't zonk (Modular s t_a) in
+the givens, we will get into a loop as improveOne uses the unification engine
+TcGadt.tcUnifyTys, which doesn't know about mutable type variables.
+
+
Note [LOOP]
~~~~~~~~~~~
class If b t e r | b t e -> r
-> TcM TcDictBinds
tcSimplifySuperClasses loc givens sc_wanteds
= do { traceTc (text "tcSimplifySuperClasses")
- ; (irreds,binds1,_) <- checkLoop env sc_wanteds
+ ; (irreds,binds1) <- checkLoop env sc_wanteds
; let (tidy_env, tidy_irreds) = tidyInsts irreds
; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
; return binds1 }
-- HOWEVER, some unification may take place, if we instantiate
-- a method Inst with an equality constraint
; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
- ; (_imp, _binds, constrained_dicts, _) <- reduceContext env wanteds'
+ ; (_imp, _binds, constrained_dicts, elim_skolems)
+ <- reduceContext env wanteds'
+ ; elim_skolems
-- Next, figure out the tyvars we will quantify over
; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
(is_nested_group || isDict inst) = Stop
| otherwise = ReduceMe AddSCs
env = mkNoImproveRedEnv doc try_me
- ; (_imp, binds, irreds, _) <- reduceContext env wanteds'
+ ; (_imp, binds, irreds, elim_skolems) <- reduceContext env wanteds'
+ ; elim_skolems
-- See "Notes on implicit parameters, Question 4: top level"
; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
-- to fromInteger; this looks fragile to me
; lookup_result <- lookupSimpleInst w'
; case lookup_result of
- GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
+ GenInst ws' rhs ->
+ go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
}
\end{code}
-- Unusually for checking, we *must* zonk the given_ips
; let env = mkRedEnv doc try_me given_ips'
- ; (improved, binds, irreds, _) <- reduceContext env wanteds'
+ ; (improved, binds, irreds, elim_skolems) <- reduceContext env wanteds'
+ ; elim_skolems
; if not improved then
ASSERT( all is_free irreds )
-- arguably a bug in Match.tidyEqnInfo (see notes there)
bindInstsOfLocalFuns wanteds local_ids
- | null overloaded_ids
+ | null overloaded_ids = do
-- Common case
- = extendLIEs wanteds `thenM_`
- returnM emptyLHsBinds
+ extendLIEs wanteds
+ return emptyLHsBinds
| otherwise
- = do { (irreds, binds,_) <- checkLoop env for_me
+ = do { (irreds, binds) <- gentleInferLoop doc for_me
; extendLIEs not_for_me
; extendLIEs irreds
; return binds }
where
- env = mkRedEnv doc try_me []
doc = text "bindInsts" <+> ppr local_ids
overloaded_ids = filter is_overloaded local_ids
is_overloaded id = isOverloadedTy (idType id)
overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
-- so it's worth building a set, so that
-- lookup (in isMethodFor) is faster
- try_me inst | isMethod inst = ReduceMe NoSCs
- | otherwise = Stop
\end{code}
mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
mkRedEnv doc try_me givens
= RedEnv { red_doc = doc, red_try_me = try_me,
- red_givens = givens, red_stack = (0,[]),
+ red_givens = givens,
+ red_stack = (0,[]),
red_improve = True }
mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
-- Do not do improvement; no givens
mkNoImproveRedEnv doc try_me
= RedEnv { red_doc = doc, red_try_me = try_me,
- red_givens = [], red_stack = (0,[]),
+ red_givens = [],
+ red_stack = (0,[]),
red_improve = True }
data WhatToDo
-- of a predicate when adding it to the avails
-- The reason for this flag is entirely the super-class loop problem
-- Note [SUPER-CLASS LOOP 1]
+
+zonkRedEnv :: RedEnv -> TcM RedEnv
+zonkRedEnv env
+ = do { givens' <- mapM zonkInst (red_givens env)
+ ; return $ env {red_givens = givens'}
+ }
\end{code}
+
%************************************************************************
%* *
\subsection[reduce]{@reduce@}
%* *
%************************************************************************
+Note [Ancestor Equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+During context reduction, we add to the wanted equalities also those
+equalities that (transitively) occur in superclass contexts of wanted
+class constraints. Consider the following code
+
+ class a ~ Int => C a
+ instance C Int
+
+If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
+substituting Int for a. Hence, we ultimately want (C Int), which we
+discharge with the explicit instance.
\begin{code}
reduceContext :: RedEnv
-> TcM (ImprovementDone,
TcDictBinds, -- Dictionary bindings
[Inst], -- Irreducible
- [Inst]) -- Needed givens
+ TcM ()) -- Undo skolems from SkolemOccurs
reduceContext env wanteds
= do { traceTc (text "reduceContext" <+> (vcat [
]))
- ; let givens = red_givens env
- (given_eqs0,given_dicts0) = partitionGivenEqInsts givens
- (wanted_eqs,wanted_dicts) = partitionWantedEqInsts wanteds
-
- ; -- 1. Normalise the *given* *equality* constraints
- (given_eqs,eliminate_skolems) <- normaliseGivens given_eqs0
-
- ; -- 2. Normalise the *given* *dictionary* constraints
- -- wrt. the toplevel and given equations
- (given_dicts,given_binds) <- normaliseGivenDicts given_eqs given_dicts0
+ ; let givens = red_givens env
+ (given_eqs0, given_dicts0) = partition isEqInst givens
+ (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds
+ (wanted_implics0, wanted_dicts) = partition isImplicInst wanted_non_eqs
- ; -- 3. Solve the *wanted* *equation* constraints
- eq_irreds0 <- solveWanteds given_eqs wanted_eqs
+ -- We want to add as wanted equalities those that (transitively)
+ -- occur in superclass contexts of wanted class constraints.
+ -- See Note [Ancestor Equalities]
+ ; ancestor_eqs <- ancestorEqualities wanted_dicts
+ ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
+ ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
- -- 4. Normalise the *wanted* equality constraints with respect to each other
- ; eq_irreds <- normaliseWanteds eq_irreds0
+ -- 1. Normalise the *given* *equality* constraints
+ ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
--- -- Do the real work
--- -- Process non-implication constraints first, so that they are
--- -- available to help solving the implication constraints
--- -- ToDo: seems a bit inefficient and ad-hoc
--- ; let (implics, rest) = partition isImplicInst wanteds
--- ; avails <- reduceList env (rest ++ implics) init_state
+ -- 2. Normalise the *given* *dictionary* constraints
+ -- wrt. the toplevel and given equations
+ ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs
+ given_dicts0
-- 5. Build the Avail mapping from "given_dicts"
- ; init_state <- foldlM addGiven emptyAvails given_dicts
-
- -- 6. Solve the *wanted* *dictionary* constraints
- -- This may expose some further equational constraints...
- ; wanted_dicts' <- zonkInsts wanted_dicts
- ; avails <- reduceList env wanted_dicts' init_state
- ; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts'
- ; traceTc (text "reduceContext extractresults" <+> vcat
- [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens])
+ ; (init_state, extra_givens) <- getLIE $ do
+ { init_state <- foldlM addGiven emptyAvails given_dicts
+ ; return init_state
+ }
- ; -- 7. Normalise the *wanted* *dictionary* constraints
- -- wrt. the toplevel and given equations
- (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
+ -- *** ToDo: what to do with the "extra_givens"? For the
+ -- moment I'm simply discarding them, which is probably wrong
- ; -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
- (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
+ -- 6. Solve the *wanted* *dictionary* constraints (not implications)
+ -- This may expose some further equational constraints...
+ ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+ ; (dict_binds, bound_dicts, dict_irreds)
+ <- extractResults avails wanted_dicts
+ ; traceTc $ text "reduceContext extractresults" <+> vcat
+ [ppr avails, ppr wanted_dicts, ppr dict_binds]
+
+ -- Solve the wanted *implications*. In doing so, we can provide
+ -- as "given" all the dicts that were originally given,
+ -- *or* for which we now have bindings,
+ -- *or* which are now irreds
+ ; let implic_env = env { red_givens = givens ++ bound_dicts
+ ++ dict_irreds }
+ ; (implic_binds_s, implic_irreds_s)
+ <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0
+ ; let implic_binds = unionManyBags implic_binds_s
+ implic_irreds = concat implic_irreds_s
+
+ -- Normalise the wanted equality constraints
+ ; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs)
+
+ -- Normalise the wanted dictionaries
+ ; let irreds = dict_irreds ++ implic_irreds
+ eqs = eq_irreds ++ given_eqs
+ ; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds
- ; -- 9. eliminate the artificial skolem constants introduced in 1.
- eliminate_skolems
-
- -- If there was some FD improvement,
- -- or new wanted equations have been exposed,
- -- we should have another go at solving.
- ; let improved = availsImproved avails
- || (not $ isEmptyBag normalise_binds1)
- || (not $ isEmptyBag normalise_binds2)
- || (not $ null $ fst $ partitionGivenEqInsts irreds)
+ -- Figure out whether we should go round again. We do so in either
+ -- two cases:
+ -- (1) If any of the mutable tyvars in givens or irreds has been
+ -- filled in by improvement, there is merit in going around
+ -- again, because we may make further progress.
+ -- (2) If we managed to normalise any dicts, there is merit in going
+ -- around gain, because reduceList may be able to get further.
+ --
+ -- ToDo: We may have exposed new
+ -- equality constraints and should probably go round again
+ -- then as well. But currently we are dropping them on the
+ -- floor anyway.
+
+ ; let all_irreds = norm_irreds ++ eq_irreds
+ ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $
+ tyVarsOfInsts (givens ++ all_irreds)
+ ; let improvedDicts = not $ isEmptyBag normalise_binds
+ improved = improvedMetaTy || improvedDicts
+
+ -- The old plan (fragile)
+ -- improveed = availsImproved avails
+ -- || (not $ isEmptyBag normalise_binds1)
+ -- || (not $ isEmptyBag normalise_binds2)
+ -- || (any isEqInst irreds)
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
red_doc env,
- text "given" <+> ppr (red_givens env),
+ text "given" <+> ppr givens,
+ text "given_eqs" <+> ppr given_eqs,
text "wanted" <+> ppr wanteds,
+ text "wanted_dicts" <+> ppr wanted_dicts,
text "----",
text "avails" <+> pprAvails avails,
text "improved =" <+> ppr improved,
- text "irreds = " <+> ppr irreds,
- text "binds = " <+> ppr binds,
- text "needed givens = " <+> ppr needed_givens,
+ text "(all) irreds = " <+> ppr all_irreds,
+ text "dict-binds = " <+> ppr dict_binds,
+ text "implic-binds = " <+> ppr implic_binds,
text "----------------------"
]))
- ; return (improved, given_binds `unionBags` normalise_binds1 `unionBags` normalise_binds2 `unionBags` binds, irreds ++ eq_irreds, needed_givens) }
+ ; return (improved,
+ given_binds `unionBags` normalise_binds
+ `unionBags` dict_binds
+ `unionBags` implic_binds,
+ all_irreds,
+ eliminate_skolems)
+ }
tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
tcImproveOne avails inst
unifyEqns [] = return False
unifyEqns eqns
= do { traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))
- ; mappM_ unify eqns
+ ; mapM_ unify eqns
; return True }
where
unify ((qtvs, pairs), what1, what2)
- = addErrCtxtM (mkEqnMsg what1 what2) $
- tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
- mapM_ (unif_pr tenv) pairs
+ = addErrCtxtM (mkEqnMsg what1 what2) $ do
+ (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+ mapM_ (unif_pr tenv) pairs
unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
\begin{code}
reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
- = do { dopts <- getDOpts
+ = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
+ ; dopts <- getDOpts
#ifdef DEBUG
; if n > 8 then
dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n)
go wanteds state }
where
go [] state = return state
- go (w:ws) state = do { traceTc (text "reduceList " <+> ppr (w:ws) <+> ppr state)
- ; state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
+ go (w:ws) state = do { state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
; go ws state' }
-- Base case: we're done!
-- It's the same as an existing inst, or a superclass thereof
| Just avail <- findAvail avails wanted
= do { traceTc (text "reduce: found " <+> ppr wanted)
- ; returnM avails
+ ; return avails
}
| otherwise
- = do { traceTc (text "reduce" <+> ppr avails <+> ppr wanted)
+ = do { traceTc (text "reduce" <+> ppr wanted $$ ppr avails)
; case red_try_me env wanted of {
Stop -> try_simple (addIrred NoSCs);
-- See Note [No superclasses for Stop]
GenInst [] rhs -> addWanted want_scs avails wanted rhs []
- GenInst wanteds' rhs
+ GenInst wanteds' rhs
-> do { avails1 <- addIrred NoSCs avails wanted
; avails2 <- reduceList env wanteds' avails1
; addWanted want_scs avails2 wanted rhs wanteds' } }
\begin{code}
---------------------------------------------
reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
- tci_given = extra_givens, tci_wanted = wanteds })
- = reduceImplication env avails reft tvs extra_givens wanteds loc
-
reduceInst env avails other_inst
= do { result <- lookupSimpleInst other_inst
; return (avails, result) }
Note [Equational Constraints in Implication Constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-An equational constraint is of the form
+An implication constraint is of the form
Given => Wanted
where Given and Wanted may contain both equational and dictionary
constraints. The delay and reduction of these two kinds of constraints
\begin{code}
---------------------------------------------
reduceImplication :: RedEnv
- -> Avails
- -> Refinement -- May refine the givens; often empty
- -> [TcTyVar] -- Quantified type variables; all skolems
- -> [Inst] -- Extra givens; all rigid
- -> [Inst] -- Wanted
- -> InstLoc
- -> TcM (Avails, LookupInstResult)
+ -> Inst
+ -> TcM (TcDictBinds, [Inst])
\end{code}
Suppose we are simplifying the constraint
forall bs. extras => wanted
-in the context of an overall simplification problem with givens 'givens',
-and refinment 'reft'.
+in the context of an overall simplification problem with givens 'givens'.
Note that
- * The refinement is often empty
-
- * The 'extra givens' need not mention any of the quantified type variables
+ * The 'givens' need not mention any of the quantified type variables
e.g. forall {}. Eq a => Eq [a]
forall {}. C Int => D (Tree Int)
-- the solved dictionaries use these binders
-- these binders are generated by reduceImplication
--
-reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
- = do { -- Add refined givens, and the extra givens
- -- Todo fix this
- (refined_red_givens,refined_avails)
- <- if isEmptyRefinement reft then return (red_givens env,orig_avails)
- else foldlM (addRefinedGiven reft) ([],orig_avails) (red_givens env)
-
- -- Solve the sub-problem
- ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
- env' = env { red_givens = refined_red_givens ++ extra_givens ++ availsInsts orig_avails
+reduceImplication env
+ orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
+ tci_tyvars = tvs,
+ tci_given = extra_givens, tci_wanted = wanteds })
+ = do { -- Solve the sub-problem
+ ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
+ env' = env { red_givens = extra_givens ++ red_givens env
+ , red_doc = sep [ptext SLIT("reduceImplication for")
+ <+> ppr name,
+ nest 2 (parens $ ptext SLIT("within")
+ <+> red_doc env)]
, red_try_me = try_me }
; traceTc (text "reduceImplication" <+> vcat
- [ ppr orig_avails,
- ppr (red_givens env), ppr extra_givens,
- ppr reft, ppr wanteds])
- ; (irreds,binds,needed_givens0) <- checkLoop env' wanteds
- ; let needed_givens1 = [ng | ng <- needed_givens0, notElem ng extra_givens]
+ [ ppr (red_givens env), ppr extra_givens,
+ ppr wanteds])
+ ; (irreds, binds) <- checkLoop env' wanteds
+ ; let (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
+ -- SLPJ Sept 07: I think this is bogus; currently
+ -- there are no Eqinsts in extra_givens
+ dict_ids = map instToId extra_dict_givens
-- Note [Reducing implication constraints]
-- Tom -- update note, put somewhere!
; traceTc (text "reduceImplication result" <+> vcat
- [ppr irreds, ppr binds, ppr needed_givens1])
--- ; avails <- reduceList env' wanteds avails
---
--- -- Extract the binding
--- ; (binds, irreds) <- extractResults avails wanteds
- ; (refinement_binds,needed_givens) <- extractLocalResults refined_avails needed_givens1
- ; traceTc (text "reduceImplication local results" <+> vcat
- [ppr refinement_binds, ppr needed_givens])
+ [ppr irreds, ppr binds])
; -- extract superclass binds
-- (sc_binds,_) <- extractResults avails []
-- [ppr sc_binds, ppr avails])
--
- -- We always discard the extra avails we've generated;
- -- but we remember if we have done any (global) improvement
--- ; let ret_avails = avails
- ; let ret_avails = orig_avails
--- ; let ret_avails = updateImprovement orig_avails avails
+ -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
+ -- Then we must iterate the outer loop too!
; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
--- Porgress is no longer measered by the number of bindings
--- ; if isEmptyLHsBinds binds then -- No progress
- ; if (isEmptyLHsBinds binds) && (not $ null irreds) then
- return (ret_avails, NoInstance)
+-- Progress is no longer measered by the number of bindings
+ ; if (isEmptyLHsBinds binds) && (not $ null irreds) then -- No progress
+ -- If there are any irreds, we back off and do nothing
+ return (emptyBag, [orig_implic])
else do
- {
- ; (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
- -- This binding is useless if the recursive simplification
- -- made no progress; but currently we don't try to optimise that
- -- case. After all, we only try hard to reduce at top level, or
- -- when inferring types.
+ { (simpler_implic_insts, bind)
+ <- makeImplicationBind inst_loc tvs extra_givens irreds
+ -- This binding is useless if the recursive simplification
+ -- made no progress; but currently we don't try to optimise that
+ -- case. After all, we only try hard to reduce at top level, or
+ -- when inferring types.
; let dict_wanteds = filter (not . isEqInst) wanteds
- (extra_eq_givens,extra_dict_givens) = partitionGivenEqInsts extra_givens
- dict_ids = map instToId extra_dict_givens
-- TOMDO: given equational constraints bug!
-- we need a different evidence for given
-- equations depending on whether we solve
-- dictionary constraints or equational constraints
- eq_tyvars = uniqSetToList $ tyVarsOfTypes $ map eqInstType extra_eq_givens
- -- dict_ids = map instToId extra_givens
- co = mkWpTyLams tvs <.> mkWpTyLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` refinement_binds `unionBags` bind)
+
+ eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens
+ -- SLPJ Sept07: this looks Utterly Wrong to me, but I think
+ -- that current extra_givens has no EqInsts, so
+ -- it makes no difference
+ co = wrap_inline -- Note [Always inline implication constraints]
+ <.> mkWpTyLams tvs
+ <.> mkWpLams eq_tyvars
+ <.> mkWpLams dict_ids
+ <.> WpLet (binds `unionBags` bind)
+ wrap_inline | null dict_ids = idHsWrapper
+ | otherwise = WpInline
rhs = mkHsWrap co payload
loc = instLocSpan inst_loc
payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
| otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
- ; traceTc (text "reduceImplication ->" <+> vcat
- [ ppr ret_avails,
- ppr implic_insts])
- -- If there are any irreds, we back off and return NoInstance
- ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs))
+ ; traceTc (vcat [text "reduceImplication" <+> ppr name,
+ ppr simpler_implic_insts,
+ text "->" <+> ppr rhs])
+ ; return (unitBag (L loc (VarBind (instToId orig_implic) (L loc rhs))),
+ simpler_implic_insts)
}
}
\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 [Always inline implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose an implication constraint floats out of an INLINE function.
+Then although the implication has a single call site, it won't be
+inlined. And that is bad because it means that even if there is really
+*no* overloading (type signatures specify the exact types) there will
+still be dictionary passing in the resulting code. To avert this,
+we mark the implication constraints themselves as INLINE, at least when
+there is no loss of sharing as a result.
Note [Freeness and implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
= IsIrred -- Used for irreducible dictionaries,
-- which are going to be lambda bound
- | Given TcId -- Used for dictionaries for which we have a binding
+ | Given Inst -- Used for dictionaries for which we have a binding
-- e.g. those "given" in a signature
| Rhs -- Used when there is a RHS
pprAvails (Avails imp avails)
= vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
- , nest 2 (vcat [sep [ppr inst, nest 2 (equals <+> ppr avail)]
- | (inst,avail) <- fmToList avails ])]
+ , nest 2 $ braces $
+ vcat [ sep [ppr inst, nest 2 (equals <+> ppr avail)]
+ | (inst,avail) <- fmToList avails ]]
instance Outputable AvailHow where
ppr = pprAvail
pprAvail :: AvailHow -> SDoc
pprAvail IsIrred = text "Irred"
pprAvail (Given x) = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs) = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
+pprAvail (Rhs rhs bs) = sep [text "Rhs" <+> ppr bs,
+ nest 2 (ppr rhs)]
-------------------------
extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
-- Does improvement
-extendAvails avails@(Avails imp env) inst avail
+extendAvails avails@(Avails imp env) inst avail
= do { imp1 <- tcImproveOne avails inst -- Do any improvement
; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
dependency analyser can sort them out later
\begin{code}
+type DoneEnv = FiniteMap Inst [Id]
+-- Tracks which things we have evidence for
+
extractResults :: Avails
-> [Inst] -- Wanted
- -> TcM ( TcDictBinds, -- Bindings
- [Inst], -- Irreducible ones
- [Inst]) -- Needed givens, i.e. ones used in the bindings
+ -> TcM (TcDictBinds, -- Bindings
+ [Inst], -- The insts bound by the bindings
+ [Inst]) -- Irreducible ones
+ -- Note [Reducing implication constraints]
extractResults (Avails _ avails) wanteds
- = go avails emptyBag [] [] wanteds
+ = go emptyBag [] [] emptyFM wanteds
where
- go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] -> [Inst]
+ go :: TcDictBinds -- Bindings for dicts
+ -> [Inst] -- Bound by the bindings
+ -> [Inst] -- Irreds
+ -> DoneEnv -- Has an entry for each inst in the above three sets
+ -> [Inst] -- Wanted
-> TcM (TcDictBinds, [Inst], [Inst])
- go avails binds irreds givens []
- = returnM (binds, irreds, givens)
-
- go avails binds irreds givens (w:ws)
+ go binds bound_dicts irreds done []
+ = return (binds, bound_dicts, irreds)
+
+ go binds bound_dicts irreds done (w:ws)
+ | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
+ = if w_id `elem` done_ids then
+ go binds bound_dicts irreds done ws
+ else
+ go (add_bind (nlHsVar done_id)) bound_dicts irreds
+ (addToFM done w (done_id : w_id : rest_done_ids)) ws
+
+ | otherwise -- Not yet done
= case findAvailEnv avails w of
Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds givens ws
-
- Just (Given id)
- | id == w_id -> go avails binds irreds (w:givens) ws
- | otherwise -> go avails (addBind binds w (nlHsVar id)) irreds (update_id w id:givens) 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 -> go (add_given avails w) binds (w:irreds) givens 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
- -- test tcfail043
-
- Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds givens (ws' ++ ws)
- where
- new_binds = addBind binds w rhs
- where
- w_id = instToId w
- update_id m@(Method{}) id = m {tci_id = id}
- update_id w id = w {tci_name = idName id}
-
- add_given avails w = extendAvailEnv avails w (Given (instToId w))
-
-extractLocalResults :: Avails
- -> [Inst] -- Wanted
- -> TcM ( TcDictBinds, -- Bindings
- [Inst]) -- Needed givens, i.e. ones used in the bindings
-
-extractLocalResults (Avails _ avails) wanteds
- = go avails emptyBag [] wanteds
- where
- go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
- -> TcM (TcDictBinds, [Inst])
- go avails binds givens []
- = returnM (binds, givens)
+ go binds bound_dicts irreds done ws
- go avails binds givens (w:ws)
- = case findAvailEnv avails w of
- Nothing -> -- pprTrace "Urk: extractLocalResults" (ppr w) $
- go avails binds givens ws
-
- Just IsIrred ->
- go avails binds givens ws
+ Just IsIrred -> go binds bound_dicts (w:irreds) done' ws
- Just (Given id)
- | id == w_id -> go avails binds (w:givens) ws
- | otherwise -> go avails binds (w{tci_name=idName id}:givens) 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 (Rhs rhs ws') -> go (add_bind rhs) (w:bound_dicts) irreds done' (ws' ++ ws)
- Just (Rhs rhs ws') -> go (add_given avails w) new_binds givens (ws' ++ ws)
- where
- new_binds = addBind binds w rhs
+ Just (Given g) -> go binds' bound_dicts irreds (addToFM done w [g_id]) ws
+ where
+ g_id = instToId g
+ binds' | w_id == g_id = binds
+ | otherwise = add_bind (nlHsVar g_id)
where
- w_id = instToId w
-
- add_given avails w = extendAvailEnv avails w (Given (instToId w))
+ w_id = instToId w
+ done' = addToFM done w [w_id]
+ add_bind rhs = addInstToDictBind binds w rhs
\end{code}
avail = Rhs rhs_expr wanteds
addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
+addGiven avails given = addAvailAndSCs AddSCs avails given (Given given)
-- Always add superclasses for 'givens'
--
-- No ASSERT( not (given `elemAvails` avails) ) because in an instance
-- decl for Ord t we can add both Ord t and Eq t as 'givens',
-- so the assert isn't true
-
-addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
-addRefinedGiven reft (refined_givens, avails) given
- | isDict given -- We sometimes have 'given' methods, but they
- -- are always optional, so we can drop them
- , let pred = dictPred given
- , isRefineablePred pred -- See Note [ImplicInst rigidity]
- , Just (co, pred) <- refinePred reft pred
- = do { new_given <- newDictBndr (instLoc given) pred
- ; let rhs = L (instSpan given) $
- HsWrap (WpCo co) (HsVar (instToId given))
- ; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
- ; return (new_given:refined_givens, avails) }
- -- ToDo: the superclasses of the original given all exist in Avails
- -- so we could really just cast them, but it's more awkward to do,
- -- and hopefully the optimiser will spot the duplicated work
- | otherwise
- = return (refined_givens, avails)
-
-addRefinedGiven' :: Refinement -> [Inst] -> Inst -> TcM [Inst]
-addRefinedGiven' reft refined_givens given
- | isDict given -- We sometimes have 'given' methods, but they
- -- are always optional, so we can drop them
- , let pred = dictPred given
- , isRefineablePred pred -- See Note [ImplicInst rigidity]
- , Just (co, pred) <- refinePred reft pred
- = do { new_given <- newDictBndr (instLoc given) pred
- ; return (new_given:refined_givens) }
- -- ToDo: the superclasses of the original given all exist in Avails
- -- so we could really just cast them, but it's more awkward to do,
- -- and hopefully the optimiser will spot the duplicated work
- | otherwise
- = return refined_givens
\end{code}
-Note [ImplicInst rigidity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- C :: forall ab. (Eq a, Ord b) => b -> T a
-
- ...(case x of C v -> <body>)...
-
-From the case (where x::T ty) we'll get an implication constraint
- forall b. (Eq ty, Ord b) => <body-constraints>
-Now suppose <body-constraints> itself has an implication constraint
-of form
- forall c. <reft> => <payload>
-Then, we can certainly apply the refinement <reft> to the Ord b, becuase it is
-existential, but we probably should not apply it to the (Eq ty) because it may
-be wobbly. Hence the isRigidInst
-
-@Insts@ are ordered by their class/type info, rather than by their
-unique. This allows the context-reduction mechanism to use standard finite
-maps to do their stuff. It's horrible that this code is here, rather
-than with the Avails handling stuff in TcSimplify
-
\begin{code}
addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
where
is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
-- Note: this compares by *type*, not by Unique
- deps = findAllDeps (unitVarSet (instToId inst)) avail
+ deps = findAllDeps (unitVarSet (instToVar inst)) avail
dep_tys = map idType (varSetElems deps)
findAllDeps :: IdSet -> AvailHow -> IdSet
find_all :: IdSet -> Inst -> IdSet
find_all so_far kid
+ | isEqInst kid = so_far
| kid_id `elemVarSet` so_far = so_far
| Just avail <- findAvail avails kid = findAllDeps so_far' avail
| otherwise = so_far'
addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
-- Add all the superclasses of the Inst to Avails
- -- The first param says "dont do this because the original thing
+ -- The first param says "don't do this because the original thing
-- depends on this one, so you'd build a loop"
-- Invariant: the Inst is already in Avails.
where
(clas, tys) = getDictClassTys dict
(tyvars, sc_theta, sc_sels, _) = classBigSig clas
- sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
+ sc_theta' = filter (not . isEqPred) $
+ substTheta (zipTopTvSubst tyvars tys) sc_theta
add_sc avails (sc_dict, sc_sel)
| is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
; addSCs is_loop avails' sc_dict }
where
sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
- co_fn = WpApp (instToId dict) <.> mkWpTyApps tys
+ co_fn = WpApp (instToVar dict) <.> mkWpTyApps tys
is_given :: Inst -> Bool
is_given sc_dict = case findAvail avails sc_dict of
Just (Given _) -> True -- Given is cheaper than superclass selection
other -> False
+
+-- From the a set of insts obtain all equalities that (transitively) occur in
+-- superclass contexts of class constraints (aka the ancestor equalities).
+--
+ancestorEqualities :: [Inst] -> TcM [Inst]
+ancestorEqualities
+ = mapM mkWantedEqInst -- turn only equality predicates..
+ . filter isEqPred -- ..into wanted equality insts
+ . bagToList
+ . addAEsToBag emptyBag -- collect the superclass constraints..
+ . map dictPred -- ..of all predicates in a bag
+ . filter isClassDict
+ where
+ addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType
+ addAEsToBag bag [] = bag
+ addAEsToBag bag (pred:preds)
+ | pred `elemBag` bag = addAEsToBag bag preds
+ | isEqPred pred = addAEsToBag bagWithPred preds
+ | isClassPred pred = addAEsToBag bagWithPred predsWithSCs
+ | otherwise = addAEsToBag bag preds
+ where
+ bagWithPred = bag `snocBag` pred
+ predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta
+ --
+ (tyvars, sc_theta, _, _) = classBigSig clas
+ (clas, tys) = getClassPredTys pred
\end{code}
+
%************************************************************************
%* *
\section{tcSimplifyTop: defaulting}
-- error message generation for the monomorphism restriction
tc_simplify_top doc interactive wanteds
= do { dflags <- getDOpts
- ; wanteds <- zonkInsts wanteds
+ ; wanteds <- zonkInsts wanteds
; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
+-- ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds
; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
-> TcM ThetaType -- Needed
-- Given instance (wanted) => C inst_ty
-- Simplify 'wanted' as much as possible
--- The inst_ty is needed only for the termination check
tcSimplifyDeriv orig tyvars theta
= do { (tvs, _, tenv) <- tcInstTyVars tyvars
; wanteds <- newDictBndrsO orig (substTheta tenv theta)
; (irreds, _) <- tryHardCheckLoop doc wanteds
- ; let (tv_dicts, others) = partition isTyVarDict irreds
+ ; let (tv_dicts, others) = partition ok irreds
; addNoInstanceErrs others
+ -- See Note [Exotic derived instance contexts] in TcMType
; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
simpl_theta = substTheta rev_env (map dictPred tv_dicts)
; 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)).
+ ok dict | isDict dict = validDerivPred (dictPred dict)
+ | otherwise = False
+\end{code}
@tcSimplifyDefault@ just checks class-type constraints, essentially;
tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
-> TcM ()
-tcSimplifyDefault theta
- = newDictBndrsO DefaultOrigin theta `thenM` \ wanteds ->
- tryHardCheckLoop doc wanteds `thenM` \ (irreds, _) ->
- addNoInstanceErrs irreds `thenM_`
+tcSimplifyDefault theta = do
+ wanteds <- newDictBndrsO DefaultOrigin theta
+ (irreds, _) <- tryHardCheckLoop doc wanteds
+ addNoInstanceErrs irreds
if null irreds then
- returnM ()
- else
- failM
+ return ()
+ else
+ traceTc (ptext SLIT("tcSimplifyDefault failing")) >> failM
where
doc = ptext SLIT("default declaration")
\end{code}
-- We want to report them together in error messages
groupErrs report_err []
- = returnM ()
-groupErrs report_err (inst:insts)
- = do_one (inst:friends) `thenM_`
- groupErrs report_err others
-
+ = return ()
+groupErrs report_err (inst:insts)
+ = do { do_one (inst:friends)
+ ; groupErrs report_err others }
where
-- (It may seem a bit crude to compare the error messages,
-- but it makes sure that we combine just what the user sees,
(insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
(eqInsts, insts3) = partition isEqInst insts2
; traceTc (text "reportNoInstances" <+> vcat
- [ppr implics, ppr insts1, ppr insts2])
+ [ppr insts, ppr implics, ppr insts1, ppr insts2])
; mapM_ complain_implic implics
; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
; groupErrs complain_no_inst insts3
- ; mapM_ complain_eq eqInsts
+ ; mapM_ (addErrTcM . mk_eq_err) eqInsts
}
where
complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
(Just (tci_loc inst, tci_given inst))
(tci_wanted inst)
- complain_eq EqInst {tci_left = lty, tci_right = rty,
- tci_loc = InstLoc _ _ ctxt}
- = do { (env, msg) <- misMatchMsg lty rty
- ; setErrCtxt ctxt $
- failWithTcM (env, msg)
- }
-
check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
-- Right msg => overlap message
-- Left inst => no instance
where
ispecs = [ispec | (ispec, _) <- matches]
+ mk_eq_err :: Inst -> (TidyEnv, SDoc)
+ mk_eq_err inst = misMatchMsg tidy_env (eqInstTys inst)
+
mk_no_inst_err insts
| null insts = empty
cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
report :: [(Inst,[TcTyVar])] -> TcM ()
- report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
- = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
+ report pairs@((inst,tvs) : _) = do -- The pairs share a common set of ambiguous tyvars
+ (tidy_env, mono_msg) <- mkMonomorphismMsg tidy_env tvs
setSrcSpan (instSpan inst) $
-- the location of the first one will do for the err message
- addErrTcM (tidy_env, msg $$ mono_msg)
+ addErrTcM (tidy_env, msg $$ mono_msg)
where
dicts = map fst pairs
msg = sep [text "Ambiguous type variable" <> plural tvs <+>
nest 2 (vcat docs),
monomorphism_fix dflags]
-isRuntimeUnk :: TcTyVar -> Bool
-isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
- | otherwise = False
-
monomorphism_fix :: DynFlags -> SDoc
monomorphism_fix dflags
= ptext SLIT("Probable fix:") <+> vcat
else empty] -- Only suggest adding "-fno-monomorphism-restriction"
-- if it is not already set!
-warnDefault ups default_ty
- = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
+warnDefault ups default_ty = do
+ warn_flag <- doptM Opt_WarnTypeDefaults
addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
where
dicts = [d | (d,_,_) <- ups]
nest 4 (pprStack stack)]
pprStack stack = vcat (map pprInstInFull stack)
-
------------------------
-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
--- Generate the message when two types fail to match,
--- going to some trouble to make it helpful.
--- The argument order is: actual type, expected type
-misMatchMsg ty_act ty_exp
- = do { env0 <- tcInitTidyEnv
- ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp ty_act
- ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act ty_exp
- ; return (env2,
- sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
- nest 7 $
- ptext SLIT("against inferred type") <+> pp_act],
- nest 2 (extra_exp $$ extra_act)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty other_ty
- = do { ty' <- zonkTcType ty
- ; let (env1, tidy_ty) = tidyOpenType env ty'
- ; (env2, extra) <- ppr_extra env1 tidy_ty other_ty
- ; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (ppr_extra env ty other_ty) shows extra info about 'ty'
-ppr_extra env (TyVarTy tv) other_ty
- | isSkolemTyVar tv || isSigTyVar tv
- = return (env1, pprSkolTvBinding tv1)
- where
- (env1, tv1) = tidySkolemTyVar env tv
-
-ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _)
- | getOccName tc1 == getOccName tc2
- = -- This case helps with messages that would otherwise say
- -- Could not match 'T' does not match 'M.T'
- -- which is not helpful
- do { this_mod <- getModule
- ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined") <+> mk_mod this_mod) }
- where
- tc_mod = nameModule (getName tc1)
- tc_pkg = modulePackageId tc_mod
- tc2_pkg = modulePackageId (nameModule (getName tc2))
- mk_mod this_mod
- | tc_mod == this_mod = ptext SLIT("in this module")
-
- | not home_pkg && tc2_pkg /= tc_pkg = pp_pkg
- -- Suppress the module name if (a) it's from another package
- -- (b) other_ty isn't from that same package
-
- | otherwise = ptext SLIT("in module") <+> quotes (ppr tc_mod) <+> pp_pkg
- where
- home_pkg = tc_pkg == modulePackageId this_mod
- pp_pkg | home_pkg = empty
- | otherwise = ptext SLIT("in package") <+> quotes (ppr tc_pkg)
-
-ppr_extra env ty other_ty = return (env, empty) -- Normal case
\end{code}