TcSimplify
\begin{code}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
module TcSimplify (
tcSimplifyInfer, tcSimplifyInferCheck,
tcSimplifyCheck, tcSimplifyRestricted,
tcSimplifyDeriv, tcSimplifyDefault,
bindInstsOfLocalFuns, bindIrreds,
+
+ misMatchMsg
) where
#include "HsVersions.h"
import TcType
import TcMType
import TcIface
+import TcTyFuns
+import TypeRep
import Var
import Name
import NameSet
import BasicTypes
import VarSet
import VarEnv
+import Module
import FiniteMap
import Bag
import Outputable
+import Maybes
import ListSetOps
import Util
+import UniqSet
import SrcLoc
import DynFlags
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))
- ; let try_me inst = ReduceMe AddSCs
- ; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound
- ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
-
- -- Do not quantify over constraints that *now* do not
- -- mention quantified type variables, because they are
- -- simply ambiguous. 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, bur 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 (free2, irreds2) = partition (isFreeWhenInferring (mkVarSet qtvs')) irreds
- ; extendLIEs free2
-
- -- We can't abstract over implications
- ; let (dicts, implics) = partition isDict irreds2
+ ; 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
+
+ -- 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_dicts0, implics) = partition isAbstractableInst irreds3
; loc <- getInstLoc (ImplicOrigin doc)
- ; implic_bind <- bindIrreds loc qtvs' dicts implics
+ ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
+
+ -- Prepare equality instances for quantification
+ ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
+ ; q_eqs <- mappM finalizeEqInst q_eqs0
- ; return (qtvs', dicts, binds `unionBags` implic_bind) }
+ ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
-- NB: when we are done, we might have some bindings, but
-- the final qtvs might be empty. See Note [NO TYVARS] below.
+
+approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
+-- Note [Inference and implication constraints]
+-- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
+-- - fetching any dicts inside them that are free
+-- - using those dicts as cruder constraints, to solve the implications
+-- - returning the extra ones too
+
+approximateImplications doc want_dict irreds
+ | null extra_dicts
+ = return (irreds, emptyBag)
+ | otherwise
+ = do { extra_dicts' <- mapM cloneDict extra_dicts
+ ; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
+ -- By adding extra_dicts', we make them
+ -- available to solve the implication constraints
+ where
+ extra_dicts = get_dicts (filter isImplicInst irreds)
+
+ get_dicts :: [Inst] -> [Inst] -- Returns only Dicts
+ -- Find the wanted constraints in implication constraints that satisfy
+ -- want_dict, and are not bound by forall's in the constraint itself
+ get_dicts ds = concatMap get_dict ds
+
+ get_dict d@(Dict {}) | want_dict d = [d]
+ | otherwise = []
+ get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+ = [ d | let tv_set = mkVarSet tvs
+ , d <- get_dicts wanteds
+ , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
+ get_dict i@(EqInst {}) | want_dict i = [i]
+ | otherwise = []
+ get_dict other = pprPanic "approximateImplications" (ppr other)
\end{code}
+Note [Inference and implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have a wanted implication constraint (perhaps arising from
+a nested pattern match) like
+ C a => D [a]
+and we are now trying to quantify over 'a' when inferring the type for
+a function. In principle it's possible that there might be an instance
+ instance (C a, E a) => D [a]
+so the context (E a) would suffice. The Right Thing is to abstract over
+the implication constraint, but we don't do that (a) because it'll be
+surprising to programmers and (b) because we don't have the machinery to deal
+with 'given' implications.
+
+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 common cases are more clear-cut, when we have things like
+ forall a. C a => C b
+Here, abstracting over (C b) is not an approximation at all -- but see
+Note [Freeness and implications].
+
+See Trac #1430 and test tc228.
+
+
\begin{code}
-----------------------------------------------------------
-- tcSimplifyInferCheck is used when we know the constraints we are to simplify
TcDictBinds) -- Bindings
tcSimplifyInferCheck loc tau_tvs givens wanteds
- = do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+ = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr 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,
-- Now we are back to normal (c.f. tcSimplCheck)
; implic_bind <- bindIrreds loc qtvs' givens irreds
+ ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
; return (qtvs', binds `unionBags` implic_bind) }
\end{code}
-> TcM TcDictBinds -- Bindings
tcSimplifyCheck loc qtvs givens wanteds
= ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+ do { traceTc (text "tcSimplifyCheck")
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
; implic_bind <- bindIrreds loc qtvs givens irreds
; return (binds `unionBags` implic_bind) }
-> TcM TcDictBinds -- Bindings
tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
= ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+ do { traceTc (text "tcSimplifyCheckPat")
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
; implic_bind <- bindIrredsR loc qtvs co_vars reft
givens irreds
; return (binds `unionBags` implic_bind) }
--
-- This binding must line up the 'rhs' in reduceImplication
makeImplicationBind loc all_tvs reft
- givens -- Guaranteed all Dicts
+ givens -- Guaranteed all Dicts (TOMDO: true?)
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) = partition isEqInst givens
+ eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
; let name = mkInternalName uniq (mkVarOcc "ic") span
implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
tci_tyvars = all_tvs,
- tci_given = givens,
+ tci_given = (eq_givens ++ dict_givens),
tci_wanted = irreds, tci_loc = loc }
-
- ; let n_irreds = length irreds
- irred_ids = map instToId irreds
- tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids)
- pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty
+ ; 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 givens) <.> mkWpTyApps (mkTyVarTys all_tvs)
- bind | n_irreds==1 = VarBind (head irred_ids) 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) $
+ 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)) }
-----------------------------------------------------------
-topCheckLoop :: SDoc
+tryHardCheckLoop :: SDoc
-> [Inst] -- Wanted
-> TcM ([Inst], TcDictBinds)
-topCheckLoop doc wanteds
- = checkLoop (mkRedEnv doc try_me []) wanteds
+tryHardCheckLoop doc wanteds
+ = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds
+ ; return (irreds,binds)
+ }
where
try_me inst = ReduceMe AddSCs
+ -- Here's the try-hard bit
-----------------------------------------------------------
-innerCheckLoop :: InstLoc
+gentleCheckLoop :: InstLoc
-> [Inst] -- Given
-> [Inst] -- Wanted
-> TcM ([Inst], TcDictBinds)
-innerCheckLoop inst_loc givens wanteds
- = checkLoop env wanteds
+gentleCheckLoop inst_loc givens wanteds
+ = do { (irreds,binds,_) <- checkLoop env wanteds
+ ; return (irreds,binds)
+ }
where
env = mkRedEnv (pprInstLoc inst_loc) try_me givens
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 knowledge (Show b)
+Later, we will solve this constraint using the knowledg e(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
and methods only, plus common up equal things), deferring the real
work until top level, when we solve the implication constraint
-with topCheckLooop.
+with tryHardCheckLooop.
\begin{code}
-----------------------------------------------------------
checkLoop :: RedEnv
-> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
+ -> TcM ([Inst], TcDictBinds,
+ [Inst]) -- needed givens
-- Precondition: givens are completely rigid
+-- Postcondition: returned Insts are zonked
checkLoop env wanteds
- = do { -- Givens are skolems, so no need to zonk them
- wanteds' <- mappM zonkInst wanteds
-
- ; (improved, binds, irreds) <- reduceContext env wanteds'
-
- ; if not improved then
- return (irreds, binds)
- else do
+ = go env wanteds []
+ where go env wanteds needed_givens
+ = do { -- Givens are skolems, so no need to zonk them
+ wanteds' <- zonkInsts wanteds
+
+ ; (improved, binds, irreds, more_needed_givens) <- reduceContext env wanteds'
- -- 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) <- checkLoop env irreds
- ; return (irreds1, binds `unionBags` binds1) } }
+ ; let all_needed_givens = needed_givens ++ more_needed_givens
+
+ ; if not improved then
+ return (irreds, binds, all_needed_givens)
+ 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) } }
\end{code}
Note [LOOP]
-> [Inst] -- Wanted
-> TcM TcDictBinds
tcSimplifySuperClasses loc givens sc_wanteds
- = do { (irreds, binds1) <- checkLoop env sc_wanteds
+ = do { traceTc (text "tcSimplifySuperClasses")
+ ; (irreds,binds1,_) <- checkLoop env sc_wanteds
; let (tidy_env, tidy_irreds) = tidyInsts irreds
; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
; return binds1 }
where
env = mkRedEnv (pprInstLoc loc) try_me givens
try_me inst = ReduceMe NoSCs
- -- Like topCheckLoop, but with NoSCs
+ -- Like tryHardCheckLoop, but with NoSCs
\end{code}
tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
-- Zonk everything in sight
- = do { wanteds' <- mappM zonkInst wanteds
+ = do { traceTc (text "tcSimplifyRestricted")
+ ; wanteds' <- zonkInsts wanteds
-- 'ReduceMe': Reduce as far as we can. Don't stop at
-- dicts; the idea is to get rid of as many type
-- 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, _) <- reduceContext env wanteds'
-- Next, figure out the tyvars we will quantify over
; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
; gbl_tvs' <- tcGetGlobalTyVars
- ; constrained_dicts' <- mappM zonkInst constrained_dicts
+ ; constrained_dicts' <- zonkInsts constrained_dicts
; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
-- As in tcSimplifyInfer
(is_nested_group || isDict inst) = Stop
| otherwise = ReduceMe AddSCs
env = mkNoImproveRedEnv doc try_me
- ; (_imp, binds, irreds) <- reduceContext env wanteds'
+ ; (_imp, binds, irreds, _) <- reduceContext env wanteds'
-- See "Notes on implicit parameters, Question 4: top level"
; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
\begin{code}
tcSimplifyBracket :: [Inst] -> TcM ()
tcSimplifyBracket wanteds
- = do { topCheckLoop doc wanteds
+ = do { tryHardCheckLoop doc wanteds
; return () }
where
doc = text "tcSimplifyBracket"
-- makes them the same.
tcSimplifyIPs given_ips wanteds
- = do { wanteds' <- mappM zonkInst wanteds
- ; given_ips' <- mappM zonkInst given_ips
+ = do { wanteds' <- zonkInsts wanteds
+ ; given_ips' <- zonkInsts given_ips
-- 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, _) <- reduceContext env wanteds'
; if not improved then
ASSERT( all is_free irreds )
returnM emptyLHsBinds
| otherwise
- = do { (irreds, binds) <- checkLoop env for_me
+ = do { (irreds, binds,_) <- checkLoop env for_me
; extendLIEs not_for_me
; extendLIEs irreds
; return binds }
-- Note [SUPER-CLASS LOOP 1]
\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
-> [Inst] -- Wanted
-> TcM (ImprovementDone,
TcDictBinds, -- Dictionary bindings
- [Inst]) -- Irreducible
+ [Inst], -- Irreducible
+ [Inst]) -- Needed givens
reduceContext env wanteds
= do { traceTc (text "reduceContext" <+> (vcat [
text "----------------------"
]))
- -- Build the Avail mapping from "givens"
- ; init_state <- foldlM addGiven emptyAvails (red_givens env)
-
- -- Do the real work
- ; avails <- reduceList env wanteds init_state
-
- ; let improved = availsImproved avails
- ; (binds, irreds) <- extractResults avails wanteds
+ ; let givens = red_givens env
+ (given_eqs0, given_dicts0) = partition isEqInst givens
+ (wanted_eqs0, wanted_dicts) = partition isEqInst wanteds
+
+ -- 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
+
+ -- 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
+
+ -- 3. Solve the *wanted* *equation* constraints
+ ; eq_irreds0 <- solveWanteds given_eqs wanted_eqs
+
+ -- 4. Normalise the *wanted* equality constraints with respect to
+ -- each other
+ ; eq_irreds <- normaliseWanteds eq_irreds0
+
+ -- 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]
+
+ -- 7. Normalise the *wanted* *dictionary* constraints
+ -- wrt. the toplevel and given equations
+ ; (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
+
+ -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
+ ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
+
+ -- 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)
+ || (any isEqInst irreds)
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
text "----",
text "avails" <+> pprAvails avails,
text "improved =" <+> ppr improved,
+ text "irreds = " <+> ppr irreds,
+ text "binds = " <+> ppr binds,
+ text "needed givens = " <+> ppr needed_givens,
text "----------------------"
]))
- ; return (improved, binds, irreds) }
+ ; return (improved,
+ given_binds `unionBags` normalise_binds1
+ `unionBags` normalise_binds2
+ `unionBags` binds,
+ irreds ++ eq_irreds,
+ needed_givens)
+ }
tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
tcImproveOne avails inst
go wanteds state }
where
go [] state = return state
- go (w:ws) state = do { state' <- reduce (env {red_stack = (n+1, w:stk)}) w 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 ws state' }
-- Base case: we're done!
reduce env wanted avails
-- It's the same as an existing inst, or a superclass thereof
| Just avail <- findAvail avails wanted
- = returnM avails
+ = do { traceTc (text "reduce: found " <+> ppr wanted)
+ ; returnM avails
+ }
| otherwise
- = case red_try_me env wanted of {
- ; Stop -> try_simple (addIrred NoSCs) -- See Note [No superclasses for Stop]
-
- ; ReduceMe want_scs -> -- It should be reduced
- reduceInst env avails wanted `thenM` \ (avails, lookup_result) ->
- case lookup_result of
- NoInstance -> -- No such instance!
+ = do { traceTc (text "reduce" <+> ppr avails <+> ppr wanted)
+ ; case red_try_me env wanted of {
+ Stop -> try_simple (addIrred NoSCs);
+ -- See Note [No superclasses for Stop]
+
+ ReduceMe want_scs -> do -- It should be reduced
+ { (avails, lookup_result) <- reduceInst env avails wanted
+ ; case lookup_result of
+ NoInstance -> addIrred want_scs avails wanted
-- Add it and its superclasses
- addIrred want_scs avails wanted
+
+ GenInst [] rhs -> addWanted want_scs avails wanted rhs []
- GenInst [] rhs -> addWanted want_scs avails wanted rhs []
-
- GenInst wanteds' rhs -> do { avails1 <- addIrred NoSCs avails wanted
- ; avails2 <- reduceList env wanteds' avails1
- ; addWanted want_scs avails2 wanted rhs wanteds' }
+ GenInst wanteds' rhs
+ -> do { avails1 <- addIrred NoSCs avails wanted
+ ; avails2 <- reduceList env wanteds' avails1
+ ; addWanted want_scs avails2 wanted rhs wanteds' } }
-- Temporarily do addIrred *before* the reduceList,
-- which has the effect of adding the thing we are trying
-- to prove to the database before trying to prove the things it
-- needs. See note [RECURSIVE DICTIONARIES]
-- NB: we must not do an addWanted before, because that adds the
- -- superclasses too, and thaat can lead to a spurious loop; see
+ -- superclasses too, and that can lead to a spurious loop; see
-- the examples in [SUPERCLASS-LOOP]
-- So we do an addIrred before, and then overwrite it afterwards with addWanted
-
- }
+ } }
where
-- First, see if the inst can be reduced to a constant in one step
-- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
; return (avails, result) }
\end{code}
+Note [Equational Constraints in Implication Constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+An equational 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
+is distinct:
+
+-) In the generated code, wanted Dictionary constraints are wrapped up in an
+ implication constraint that is created at the code site where the wanted
+ dictionaries can be reduced via a let-binding. This let-bound implication
+ constraint is deconstructed at the use-site of the wanted dictionaries.
+
+-) While the reduction of equational constraints is also delayed, the delay
+ is not manifest in the generated code. The required evidence is generated
+ in the code directly at the use-site. There is no let-binding and deconstruction
+ necessary. The main disadvantage is that we cannot exploit sharing as the
+ same evidence may be generated at multiple use-sites. However, this disadvantage
+ is limited because it only concerns coercions which are erased.
+
+The different treatment is motivated by the different in representation. Dictionary
+constraints require manifest runtime dictionaries, while equations require coercions
+which are types.
+
\begin{code}
---------------------------------------------
reduceImplication :: RedEnv
\begin{code}
-- ToDo: should we instantiate tvs? I think it's not necessary
--
- -- ToDo: what about improvement? There may be some improvement
- -- exposed as a result of the simplifications done by reduceList
- -- which are discarded if we back off.
- -- This is almost certainly Wrong, but we'll fix it when dealing
- -- better with equality constraints
+ -- Note on coercion variables:
+ --
+ -- The extra given coercion variables are bound at two different sites:
+ -- -) in the creation context of the implication constraint
+ -- the solved equational constraints use these binders
+ --
+ -- -) at the solving site of the implication constraint
+ -- 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
- (refined_red_givens, avails)
- <- if isEmptyRefinement reft then return (red_givens env, orig_avails)
- else foldlM (addRefinedGiven reft) ([], orig_avails) (red_givens env)
- ; avails <- foldlM addGiven avails 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
+ env' = env { red_givens = refined_red_givens ++ extra_givens ++ availsInsts orig_avails
, red_try_me = try_me }
; traceTc (text "reduceImplication" <+> vcat
[ ppr orig_avails,
ppr (red_givens env), ppr extra_givens,
- ppr reft, ppr wanteds, ppr avails ])
- ; avails <- reduceList env' wanteds avails
+ ppr reft, ppr wanteds])
+ ; (irreds,binds,needed_givens0) <- checkLoop env' wanteds
+ ; let needed_givens1 = [ng | ng <- needed_givens0, notElem ng extra_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])
+
+ ; -- extract superclass binds
+ -- (sc_binds,_) <- extractResults avails []
+-- ; traceTc (text "reduceImplication sc_binds" <+> vcat
+-- [ppr sc_binds, ppr avails])
+--
- -- Extract the binding
- ; (binds, irreds) <- extractResults avails wanteds
-
-- 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
+-- ; let ret_avails = avails
+ ; let ret_avails = orig_avails
+-- ; let ret_avails = updateImprovement orig_avails avails
+
+ ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
- ; if isEmptyLHsBinds binds then -- No progress
+-- 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)
else do
- { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+ {
+ ; (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.
- ; let dict_ids = map instToId extra_givens
- co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
+ ; let dict_wanteds = filter (not . isEqInst) wanteds
+ (extra_eq_givens, extra_dict_givens) = partition isEqInst 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)
rhs = mkHsWrap co payload
loc = instLocSpan inst_loc
- payload | isSingleton wanteds = HsVar (instToId (head wanteds))
- | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
+ 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 (L loc rhs))
- } }
+ ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (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 -- 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 = 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
extractResults :: Avails
-> [Inst] -- Wanted
-> TcM ( TcDictBinds, -- Bindings
- [Inst]) -- Irreducible ones
+ [Inst], -- Irreducible ones
+ [Inst]) -- Needed givens, i.e. ones used in the bindings
extractResults (Avails _ avails) wanteds
+ = go avails emptyBag [] [] wanteds
+ where
+ go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] -> [Inst]
+ -> TcM (TcDictBinds, [Inst], [Inst])
+ go avails binds irreds givens []
+ = returnM (binds, irreds, givens)
+
+ go avails binds irreds givens (w:ws)
+ = 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 irreds []
- = returnM (binds, irreds)
+ go avails binds givens []
+ = returnM (binds, givens)
- go avails binds irreds (w:ws)
+ go avails binds givens (w:ws)
= case findAvailEnv avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds ws
+ Nothing -> -- pprTrace "Urk: extractLocalResults" (ppr w) $
+ go avails binds givens ws
- Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
+ Just IsIrred ->
+ go avails binds givens ws
Just (Given id)
- | id == instToId w
- -> go avails binds irreds ws
+ | 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!
- | otherwise
- -> go avails (addBind binds w (nlHsVar id)) irreds ws
-
- Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
- where
+ Just (Rhs rhs ws') -> go (add_given avails w) new_binds givens (ws' ++ ws)
+ where
new_binds = addBind binds w rhs
+ where
+ w_id = instToId w
add_given avails w = extendAvailEnv avails w (Given (instToId w))
-
-addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst)
- (VarBind (instToId inst) rhs))
\end{code}
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
; 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}
-- The TcLclEnv should be valid here, solely to improve
-- error message generation for the monomorphism restriction
tc_simplify_top doc interactive wanteds
- = do { wanteds <- mapM zonkInst wanteds
+ = do { dflags <- getDOpts
+ ; wanteds <- zonkInsts wanteds
; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
- ; (irreds1, binds1) <- topCheckLoop doc wanteds
+ ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
+ ; (irreds1, binds1) <- tryHardCheckLoop 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)
- ; if null irreds1 then
- return binds1
- else do
- -- OK, so there are some errors
- { -- Use the defaulting rules to do extra unification
- -- NB: irreds are already zonked
- ; dflags <- getDOpts
- ; disambiguate interactive dflags irreds1 -- Does unification
- ; (irreds2, binds2) <- topCheckLoop doc irreds1
-
- -- Deal with implicit parameter
- ; let (bad_ips, non_ips) = partition isIPDict irreds2
+ -- Use the defaulting rules to do extra unification
+ -- NB: irreds2 are already zonked
+ ; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
+
+ -- Deal with implicit parameters
+ ; let (bad_ips, non_ips) = partition isIPDict irreds3
(ambigs, others) = partition isTyVarDict non_ips
; topIPErrs bad_ips -- Can arise from f :: Int -> Int
; addNoInstanceErrs others
; addTopAmbigErrs ambigs
- ; return (binds1 `unionBags` binds2) }}
+ ; return (binds1 `unionBags` binds2 `unionBags` binds3) }
+ where
+ doc1 = doc <+> ptext SLIT("(first round)")
+ doc2 = doc <+> ptext SLIT("(approximate)")
+ doc3 = doc <+> ptext SLIT("(disambiguate)")
\end{code}
If a dictionary constrains a type variable which is
@void@.
\begin{code}
-disambiguate :: Bool -> DynFlags -> [Inst] -> TcM ()
+disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
-- Just does unification to fix the default types
-- The Insts are assumed to be pre-zonked
-disambiguate interactive dflags insts
+disambiguate doc interactive dflags insts
+ | null insts
+ = return (insts, emptyBag)
+
| null defaultable_groups
- = do { traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
- ; return () }
+ = do { traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, 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
+ default_tys <- getDefaultTys extended_defaulting ovl_strings
+
+ ; 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
+ ; tryHardCheckLoop doc insts }
- ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
- ; mapM_ (disambigGroup default_tys) defaultable_groups }
where
extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
ovl_strings = dopt Opt_OverloadedStrings dflags
- unaries :: [(Inst,Class, TcTyVar)] -- (C tv) constraints
- bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
- (unaries, bad_tvs) = getDefaultableDicts insts
+ unaries :: [(Inst, Class, TcTyVar)] -- (C tv) constraints
+ bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
+ (unaries, bad_tvs_s) = partitionWith find_unary insts
+ bad_tvs = unionVarSets bad_tvs_s
+
+ -- Finds unary type-class constraints
+ find_unary d@(Dict {tci_pred = ClassP cls [ty]})
+ | Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
+ find_unary inst = Right (tyVarsOfInst inst)
-- Group by type variable
defaultable_groups :: [[(Inst,Class,TcTyVar)]]
is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
-- Similarly is_std_class
+-----------------------
disambigGroup :: [Type] -- The default types
-> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
-> TcM () -- Just does unification, to fix the default types
disambigGroup default_tys dicts
= try_default default_tys
where
- (_,_,tyvar) = head dicts -- Should be non-empty
+ (_,_,tyvar) = ASSERT(not (null dicts)) head dicts -- Should be non-empty
classes = [c | (_,c,_) <- dicts]
try_default [] = return ()
-- After this we can't fail
; warnDefault dicts default_ty
- ; unifyType default_ty (mkTyVarTy tyvar) }
+ ; unifyType default_ty (mkTyVarTy tyvar)
+ ; return () -- TOMDO: do something with the coercion
+ }
+-----------------------
getDefaultTys :: Bool -> Bool -> TcM [Type]
getDefaultTys extended_deflts ovl_strings
= do { mb_defaults <- getDeclaredDefaultTys
-> 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
-- it doesn't see a TcTyVar, so we have to instantiate. Sigh
-- ToDo: what if two of them do get unified?
; wanteds <- newDictBndrsO orig (substTheta tenv theta)
- ; (irreds, _) <- topCheckLoop doc wanteds
+ ; (irreds, _) <- tryHardCheckLoop doc wanteds
+
+ ; 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 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}
+ ok dict | isDict dict = validDerivPred (dictPred dict)
+ | otherwise = False
+\end{code}
@tcSimplifyDefault@ just checks class-type constraints, essentially;
tcSimplifyDefault theta
= newDictBndrsO DefaultOrigin theta `thenM` \ wanteds ->
- topCheckLoop doc wanteds `thenM` \ (irreds, _) ->
+ tryHardCheckLoop doc wanteds `thenM` \ (irreds, _) ->
addNoInstanceErrs irreds `thenM_`
if null irreds then
returnM ()
addTopIPErrs bndrs []
= return ()
addTopIPErrs bndrs ips
- = addErrTcM (tidy_env, mk_msg tidy_ips)
+ = do { dflags <- getDOpts
+ ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
where
(tidy_env, tidy_ips) = tidyInsts ips
- mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
- nest 2 (ptext SLIT("the monomorphic top-level binding")
+ mk_msg dflags ips
+ = vcat [sep [ptext SLIT("Implicit parameters escape from"),
+ nest 2 (ptext SLIT("the monomorphic top-level binding")
<> plural bndrs <+> ptext SLIT("of")
<+> pprBinders bndrs <> colon)],
- nest 2 (vcat (map ppr_ip ips)),
- monomorphism_fix]
+ nest 2 (vcat (map ppr_ip ips)),
+ monomorphism_fix dflags]
ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
topIPErrs :: [Inst] -> TcM ()
= groupErrs (report_no_instances tidy_env mb_what) insts
report_no_instances tidy_env mb_what insts
- = do { inst_envs <- tcGetInstEnvs
- ; let (implics, insts1) = partition isImplicInst insts
- (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
- ; traceTc (text "reportNoInstnces" <+> vcat
- [ppr implics, ppr insts1, ppr insts2])
- ; mapM_ complain_implic implics
- ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
- ; groupErrs complain_no_inst insts2 }
+ = do { inst_envs <- tcGetInstEnvs
+ ; let (implics, insts1) = partition isImplicInst insts
+ (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
+ (eqInsts, insts3) = partition isEqInst insts2
+ ; traceTc (text "reportNoInstances" <+> vcat
+ [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
+ }
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
| not (isClassDict wanted) = Left wanted
| otherwise
= case lookupInstEnv inst_envs clas tys of
- -- The case of exactly one match and no unifiers means
- -- a successful lookup. That can't happen here, becuase
- -- dicts only end up here if they didn't match in Inst.lookupInst
+ -- The case of exactly one match and no unifiers means a
+ -- successful lookup. That can't happen here, because dicts
+ -- only end up here if they didn't match in Inst.lookupInst
#ifdef DEBUG
([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
#endif
(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]
-- Try to identify the offending variable
-- ASSUMPTION: the Insts are fully zonked
mkMonomorphismMsg tidy_env inst_tvs
- = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
- returnM (tidy_env, mk_msg docs)
+ = do { dflags <- getDOpts
+ ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
+ ; return (tidy_env, mk_msg dflags docs) }
where
- mk_msg _ | any isRuntimeUnk inst_tvs
+ mk_msg _ _ | any isRuntimeUnk inst_tvs
= vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
(pprWithCommas ppr inst_tvs),
ptext SLIT("Use :print or :force to determine these types")]
- mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
+ mk_msg _ [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
-- This happens in things like
-- f x = show (read "foo")
-- where monomorphism doesn't play any role
- mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
- nest 2 (vcat docs),
- monomorphism_fix
- ]
+ mk_msg dflags docs
+ = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
+ nest 2 (vcat docs),
+ monomorphism_fix dflags]
isRuntimeUnk :: TcTyVar -> Bool
isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
| otherwise = False
-monomorphism_fix :: SDoc
-monomorphism_fix = ptext SLIT("Probable fix:") <+>
- (ptext SLIT("give these definition(s) an explicit type signature")
- $$ ptext SLIT("or use -fno-monomorphism-restriction"))
+monomorphism_fix :: DynFlags -> SDoc
+monomorphism_fix dflags
+ = ptext SLIT("Probable fix:") <+> vcat
+ [ptext SLIT("give these definition(s) an explicit type signature"),
+ if dopt Opt_MonomorphismRestriction dflags
+ then ptext SLIT("or use -fno-monomorphism-restriction")
+ else empty] -- Only suggest adding "-fno-monomorphism-restriction"
+ -- if it is not already set!
warnDefault ups default_ty
= doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
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
+ ; ty_exp <- zonkTcType ty_exp
+ ; ty_act <- zonkTcType ty_act
+ ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
+ ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
+ ; 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 -> TcM (TidyEnv, SDoc, SDoc)
+ppr_ty env ty
+ = do { let (env1, tidy_ty) = tidyOpenType env ty
+ ; (env2, extra) <- ppr_extra env1 tidy_ty
+ ; return (env2, quotes (ppr tidy_ty), extra) }
+
+-- (ppr_extra env ty) shows extra info about 'ty'
+ppr_extra env (TyVarTy tv)
+ | isSkolemTyVar tv || isSigTyVar tv
+ = return (env1, pprSkolTvBinding tv1)
+ where
+ (env1, tv1) = tidySkolemTyVar env tv
+
+ppr_extra env ty = return (env, empty) -- Normal case
\end{code}
projects / ghc-hetmet.git / blobdiff