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,
tcSimplifyBracket, tcSimplifyCheckPat,
tcSimplifyDeriv, tcSimplifyDefault,
- bindInstsOfLocalFuns, bindIrreds,
+ bindInstsOfLocalFuns,
+
+ 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)
-
-
------------------------------------------
-
-Choosing Q
-~~~~~~~~~~
-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
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_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
- (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
- ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound))
+ ; 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 (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
; extendLIEs free
-- To make types simple, reduce as much as possible
- ; let try_me inst = ReduceMe AddSCs
- ; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound
+ ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$
+ ppr gbl_tvs1 $$ ppr free $$ ppr bound))
+ ; (irreds1, binds1) <- tryHardCheckLoop doc bound
+
+ -- Note [Inference and implication constraints]
+ ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
+ ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
+
+ -- 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
- ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
+ -- Turn the quantified meta-type variables into real type variables
+ ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
- -- We can't abstract over implications
- ; let (dicts, implics) = partition isDict irreds
+ -- 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
- ; return (qtvs', dicts, binds `unionBags` implic_bind) }
+ -- Prepare equality instances for quantification
+ ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
+ ; q_eqs <- mappM 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
-- 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_dicts in 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) }
| 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
-- This binding must line up the 'rhs' in reduceImplication
makeImplicationBind loc all_tvs reft
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 name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span)
+ ; 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,
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) $
- return ([implic_inst], unitBag (L span bind)) }
+ 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 }
+ ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
+ ; 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
| 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]
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
+ = go env wanteds []
+ where go env wanteds needed_givens
+ = 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'
+
+ ; 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}
- ; (improved, binds, irreds) <- reduceContext env wanteds'
+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
- ; if not improved then
- return (irreds, binds)
- else do
+ 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.
- -- 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) } }
-\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
-- 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}
\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) <- 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}
, red_givens :: [Inst] -- All guaranteed rigid
-- Always dicts
-- but see Note [Rigidity]
+ , red_reft :: Refinement -- The refinement to apply to the 'givens'
+ -- You should think of it as 'given equalities'
, red_stack :: (Int, [Inst]) -- Recursion stack (for err msg)
-- See Note [RedStack]
}
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_reft = emptyRefinement,
+ 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_reft = emptyRefinement,
+ 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' <- mappM 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
-> [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_dicts0) = 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_dicts0
+ ; 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) <- normaliseGivenEqs given_eqs0
+
+ -- 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"
+ -- Add dicts refined by the current type refinement
+ ; (init_state, extra_givens) <- getLIE $ do
+ { init_state <- foldlM addGiven emptyAvails given_dicts
+ ; let reft = red_reft env
+ ; if isEmptyRefinement reft then return init_state
+ else foldlM (addRefinedGiven reft)
+ init_state given_dicts }
+
+ -- *** ToDo: what to do with the "extra_givens"? For the
+ -- moment I'm simply discarding them, which is probably wrong
+
+ -- 7. Normalise the *wanted* *dictionary* constraints
+ -- wrt. the toplevel and given equations
+ -- NB: normalisation includes zonking as part of what it does
+ -- so it's important to do it after any unifications
+ -- that happened as a result of the addGivens
+ ; (wanted_dicts,normalise_binds1) <- normaliseWantedDicts given_eqs wanted_dicts0
+
+ -- 6. Solve the *wanted* *dictionary* constraints
+ -- This may expose some further equational constraints...
+ ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+ ; let (binds, irreds1, needed_givens) = extractResults avails wanted_dicts
+ ; traceTc $ text "reduceContext extractresults" <+> vcat
+ [ppr avails,ppr wanted_dicts,ppr binds,ppr needed_givens]
+
+ -- *** ToDo: what to do with the "extra_eqs"? For the
+ -- moment I'm simply discarding them, which is probably wrong
+
+ -- 3. Solve the *wanted* *equation* constraints
+ ; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs
+
+ -- 4. Normalise the *wanted* equality constraints with respect to
+ -- each other
+ ; eq_irreds <- normaliseWantedEqs eq_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
+
+ -- Figure out whether we should go round again
+ -- My current plan is to see if any of the mutable tyvars in
+ -- givens or irreds has been filled in by improvement.
+ -- If so, there is merit in going around again, because
+ -- we may make further progress
+ --
+ -- ToDo: is it only mutable stuff? 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 = irreds ++ eq_irreds
+ ; improved <- anyM isFilledMetaTyVar $ varSetElems $
+ tyVarsOfInsts (givens ++ all_irreds)
+
+ -- 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 "(all) irreds = " <+> ppr all_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,
+ all_irreds,
+ needed_givens)
+ }
tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
tcImproveOne avails inst
\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)
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 wanted $$ ppr avails)
+ ; 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)
\begin{code}
---------------------------------------------
reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
+reduceInst env avails (ImplicInst { tci_name = name,
+ 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
+ = reduceImplication env avails name reft tvs extra_givens wanteds loc
reduceInst env avails other_inst
= do { result <- lookupSimpleInst other_inst
; return (avails, result) }
\end{code}
+Note [Equational Constraints in Implication Constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+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
+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
-> Avails
+ -> Name
-> Refinement -- May refine the givens; often empty
-> [TcTyVar] -- Quantified type variables; all skolems
-> [Inst] -- Extra givens; all rigid
\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
-reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
+ -- 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 name 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)
+-- Commented out SLPJ Sept 07; see comment with extractLocalResults below
+ let refined_red_givens = []
-- 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 = extra_givens ++ availsInsts orig_avails
+ , red_reft = reft
+ , 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, ppr avails ])
- ; avails <- reduceList env' wanteds avails
+ ppr reft, ppr wanteds])
+ ; (irreds,binds,needed_givens0) <- 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
+
+ -- needed_givens0 is the free vars of the bindings
+ -- Remove the ones we are going to lambda-bind
+ -- Use the actual dictionary identity *not* equality on Insts
+ -- (Mind you, it should make no difference here.)
+ ; let needed_givens = [ng | ng <- needed_givens0
+ , instToVar ng `notElem` dict_ids]
+
+ -- Note [Reducing implication constraints]
+ -- Tom -- update note, put somewhere!
+
+ ; traceTc (text "reduceImplication result" <+> vcat
+ [ppr irreds, ppr 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
- ; if isEmptyLHsBinds binds then -- No progress
+ -- 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)))
+
+-- 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 return NoInstance
return (ret_avails, NoInstance)
else do
{ (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
-- 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
+ -- 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 = 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
+ <.> mkWpTyLams 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 | 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
- -- If there are any irreds, we back off and return NoInstance
- ; return (ret_avails, GenInst implic_insts (L loc rhs))
- } }
+
+ ; traceTc (vcat [text "reduceImplication" <+> ppr name,
+ ppr implic_insts,
+ text "->" <+> sep [ppr needed_givens, ppr rhs]])
+ ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs))
+ }
+ }
\end{code}
+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 [Reducing implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are trying to simplify
+ ( do: Ord a,
+ ic: (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 GenInst
+like this
+
+ ic = GenInst
+ [ do :: Ord a,
+ ic' :: forall b. C a b => D c b]
+ (/\b \(dc:C a b). (df a b dc do, ic' b dc))
+
+The first arg of GenInst gives the free dictionary variables of the
+second argument -- the "needed givens". And that list in turn is
+vital because it's used to determine what other dicts must be solved.
+This very list ends up in the second field of the Rhs, and drives
+extractResults.
+
+The need for this field is why we have to return "needed givens"
+from extractResults, reduceContext, checkLoop, and so on.
+
+NB: the "needed givens" in a GenInst or Rhs, may contain two dicts
+with the same type but different Ids, e.g. [d12 :: Eq a, d81 :: Eq a]
+That says we must generate a binding for both d12 and d81.
+
+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
+ | 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" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Rhs rhs bs) = sep [text "Rhs" <+> ppr bs,
+ nest 2 (ppr rhs)]
-------------------------
extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
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
+ -> (TcDictBinds, -- Bindings
+ [Inst], -- Irreducible ones
+ [Inst]) -- Needed givens, i.e. ones used in the bindings
+ -- Postcondition: needed-givens = free vars( binds ) \ irreds
+ -- needed-gives is subset of Givens in incoming Avails
+ -- Note [Reducing implication constraints]
extractResults (Avails _ avails) wanteds
- = go avails emptyBag [] wanteds
+ = go emptyBag [] [] emptyFM wanteds
where
- go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
- -> TcM (TcDictBinds, [Inst])
- go avails binds irreds []
- = returnM (binds, irreds)
-
- go avails binds irreds (w:ws)
+ go :: TcDictBinds -- Bindings for dicts
+ -> [Inst] -- Irreds
+ -> [Inst] -- Needed givens
+ -> DoneEnv -- Has an entry for each inst in the above three sets
+ -> [Inst] -- Wanted
+ -> (TcDictBinds, [Inst], [Inst])
+ go binds irreds givens done []
+ = (binds, irreds, givens)
+
+ go binds irreds givens done (w:ws)
+ | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
+ = if w_id `elem` done_ids then
+ go binds irreds givens done ws
+ else
+ go (add_bind (nlHsVar done_id)) irreds givens
+ (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 ws
-
- Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
-
- Just (Given id)
- | id == instToId w
- -> go avails binds irreds ws
- -- The sought Id can be one of the givens, via a superclass chain
- -- and then we definitely don't want to generate an x=x binding!
+ Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+ go binds irreds givens done ws
- | otherwise
- -> go avails (addBind binds w (nlHsVar id)) irreds ws
+ Just IsIrred -> go binds (w:irreds) givens done' ws
- Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
- where
- new_binds = addBind binds w rhs
+ Just (Rhs rhs ws') -> go (add_bind rhs) irreds givens done' (ws' ++ ws)
- add_given avails w = extendAvailEnv avails w (Given (instToId w))
-
-addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst)
- (VarBind (instToId inst) rhs))
+ Just (Given g) -> go binds' irreds (g:givens) (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
+ 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
+addRefinedGiven :: Refinement -> Avails -> Inst -> TcM Avails
+addRefinedGiven reft avails given
| isDict given -- We sometimes have 'given' methods, but they
-- are always optional, so we can drop them
, let pred = dictPred given
= 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) }
+ ; addAvailAndSCs AddSCs avails new_given (Rhs rhs [given]) }
-- 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)
+ = return avails
\end{code}
Note [ImplicInst rigidity]
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}
-- 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
+-- ; (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)
- ; 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 ()
else
- failM
+ 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 ()
+ = return ()
groupErrs report_err (inst:insts)
- = do_one (inst:friends) `thenM_`
- groupErrs report_err others
-
+ = 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,
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 insts, ppr implics, ppr insts1, ppr insts2])
+ ; mapM_ complain_implic implics
+ ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
+ ; groupErrs complain_no_inst insts3
+ ; mapM_ (addErrTcM . mk_eq_err) eqInsts
+ }
where
complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
| 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]
+ 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
-- 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 [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
+ 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)")
-- 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
- ]
-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"))
+ mk_msg dflags docs
+ = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
+ nest 2 (vcat docs),
+ monomorphism_fix dflags]
+
+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 ->
projects / ghc-hetmet.git / blobdiff