tcSimplifyBracket, tcSimplifyCheckPat,
tcSimplifyDeriv, tcSimplifyDefault,
- bindInstsOfLocalFuns, bindIrreds,
+ bindInstsOfLocalFuns,
+
+ misMatchMsg
) where
#include "HsVersions.h"
import HsSyn
import TcRnMonad
+import TcHsSyn ( hsLPatType )
import Inst
import TcEnv
import InstEnv
-import TcGadt
import TcType
import TcMType
import TcIface
+import TcTyFuns
+import DsUtils -- Big-tuple functions
import Var
+import Id
import Name
import NameSet
import Class
import FiniteMap
import Bag
import Outputable
+import Maybes
import ListSetOps
import Util
import SrcLoc
import DynFlags
-
+import FastString
+import Control.Monad
import Data.List
\end{code}
Here is a more complicated example:
-| > class Foo a b | a->b
-| >
-| > class Bar a b | a->b
-| >
-| > data Obj = Obj
-| >
-| > instance Bar Obj Obj
-| >
-| > instance (Bar a b) => Foo a b
-| >
-| > foo:: (Foo a b) => a -> String
-| > foo _ = "works"
-| >
-| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
-| > runFoo f = f Obj
-|
-| *Test> runFoo foo
-|
-| <interactive>:1:
-| Could not deduce (Bar a b) from the context (Foo a b)
-| arising from use of `foo' at <interactive>:1
-| Probable fix:
-| Add (Bar a b) to the expected type of an expression
-| In the first argument of `runFoo', namely `foo'
-| In the definition of `it': it = runFoo foo
-|
-| Why all of the sudden does GHC need the constraint Bar a b? The
-| function foo didn't ask for that...
+@
+ > class Foo a b | a->b
+ >
+ > class Bar a b | a->b
+ >
+ > data Obj = Obj
+ >
+ > instance Bar Obj Obj
+ >
+ > instance (Bar a b) => Foo a b
+ >
+ > foo:: (Foo a b) => a -> String
+ > foo _ = "works"
+ >
+ > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
+ > runFoo f = f Obj
+
+ *Test> runFoo foo
+
+ <interactive>:1:
+ Could not deduce (Bar a b) from the context (Foo a b)
+ arising from use of `foo' at <interactive>:1
+ Probable fix:
+ Add (Bar a b) to the expected type of an expression
+ In the first argument of `runFoo', namely `foo'
+ In the definition of `it': it = runFoo foo
+
+ Why all of the sudden does GHC need the constraint Bar a b? The
+ function foo didn't ask for that...
+@
The trouble is that to type (runFoo foo), GHC has to solve the problem:
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
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' <- mapM zonkInst wanted -- Zonk before deciding quantified tyvars
; gbl_tvs <- tcGetGlobalTyVars
- ; let preds = fdPredsOfInsts wanted'
- qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
+ ; let preds1 = fdPredsOfInsts wanted'
+ gbl_tvs1 = oclose preds1 gbl_tvs
+ qtvs = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
-- See Note [Choosing which variables to quantify]
-- To maximise sharing, remove from consideration any
-- constraints that don't mention qtvs at all
- ; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted'
- ; extendLIEs free1
+ ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
+ ; extendLIEs free
-- To make types simple, reduce as much as possible
- ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$
- ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
+ ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$
+ ppr gbl_tvs1 $$ ppr free $$ ppr bound))
; (irreds1, binds1) <- tryHardCheckLoop doc bound
-- Note [Inference and implication constraints]
; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
- -- By now improvment may have taken place, and we must *not*
- -- quantify over any variable free in the environment
- -- tc137 (function h inside g) is an example
- ; gbl_tvs <- tcGetGlobalTyVars
- ; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs)
- ; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs))
-
- -- Do not quantify over constraints that *now* do not
- -- mention quantified type variables, because they are
- -- simply ambiguous (or might be bound further out). Example:
- -- f :: Eq b => a -> (a, b)
- -- g x = fst (f x)
- -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
- -- We decide to quantify over 'alpha' alone, but free1 does not include f77
- -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
- -- constraint (Eq beta), which we dump back into the free set
- -- See test tcfail181
- ; let (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2
- ; extendLIEs free3
-
+ -- Now work out all over again which type variables to quantify,
+ -- exactly in the same way as before, but starting from irreds2. Why?
+ -- a) By now improvment may have taken place, and we must *not*
+ -- quantify over any variable free in the environment
+ -- tc137 (function h inside g) is an example
+ --
+ -- b) Do not quantify over constraints that *now* do not
+ -- mention quantified type variables, because they are
+ -- simply ambiguous (or might be bound further out). Example:
+ -- f :: Eq b => a -> (a, b)
+ -- g x = fst (f x)
+ -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+ -- We decide to quantify over 'alpha' alone, but free1 does not include f77
+ -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
+ -- constraint (Eq beta), which we dump back into the free set
+ -- See test tcfail181
+ --
+ -- c) irreds may contain type variables not previously mentioned,
+ -- e.g. instance D a x => Foo [a]
+ -- wanteds = Foo [a]
+ -- Then after simplifying we'll get (D a x), and x is fresh
+ -- We must quantify over x else it'll be totally unbound
+ ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
+ ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
+ -- Note that we start from gbl_tvs1
+ -- We use tcGetGlobalTyVars, then oclose wrt preds2, because
+ -- we've already put some of the original preds1 into frees
+ -- E.g. wanteds = C a b (where a->b)
+ -- gbl_tvs = {a}
+ -- tau_tvs = {b}
+ -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
+ -- irreds2 will be empty. But we don't want to generalise over b!
+ ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked
+ qtvs = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
+ ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
+ ; extendLIEs free
+
+ -- Turn the quantified meta-type variables into real type variables
+ ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
+
-- We can't abstract over any remaining unsolved
-- implications so instead just float them outwards. Ugh.
- ; let (q_dicts, implics) = partition isDict irreds3
+ ; let (q_dicts0, implics) = partition isAbstractableInst irreds3
; loc <- getInstLoc (ImplicOrigin doc)
- ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics
+ ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
- ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
+ -- Prepare equality instances for quantification
+ ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
+ ; q_eqs <- mapM finalizeEqInst q_eqs0
+
+ ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
-- NB: when we are done, we might have some bindings, but
-- the final qtvs might be empty. See Note [NO TYVARS] below.
= [ 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}
So our best approximation is to make (D [a]) part of the inferred
context, so we can use that to discharge the implication. Hence
-the strange function getImplicWanteds.
+the strange function get_dicts in approximateImplications.
The common cases are more clear-cut, when we have things like
forall a. C a => C b
TcDictBinds) -- Bindings
tcSimplifyInferCheck loc tau_tvs givens wanteds
- = do { (irreds, binds) <- gentleCheckLoop 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}
&& isFreeWrtIPs ips inst
-}
+isFreeWrtTyVars :: VarSet -> Inst -> Bool
isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
+isFreeWrtIPs :: NameSet -> Inst -> Bool
isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
\end{code}
-> TcM TcDictBinds -- Bindings
tcSimplifyCheck loc qtvs givens wanteds
= ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { (irreds, binds) <- gentleCheckLoop 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) }
-----------------------------------------------------------
-- tcSimplifyCheckPat is used for existential pattern match
tcSimplifyCheckPat :: InstLoc
- -> [CoVar] -> Refinement
-> [TcTyVar] -- Quantify over these
-> [Inst] -- Given
-> [Inst] -- Wanted
-> TcM TcDictBinds -- Bindings
-tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
+tcSimplifyCheckPat loc qtvs givens wanteds
= ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
- ; implic_bind <- bindIrredsR loc qtvs co_vars reft
- givens irreds
+ do { traceTc (text "tcSimplifyCheckPat")
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
+ ; implic_bind <- bindIrredsR loc qtvs givens irreds
; return (binds `unionBags` implic_bind) }
-----------------------------------------------------------
-> [Inst] -> [Inst]
-> TcM TcDictBinds
bindIrreds loc qtvs givens irreds
- = bindIrredsR loc qtvs [] emptyRefinement givens irreds
+ = bindIrredsR loc qtvs givens irreds
-bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar]
- -> Refinement -> [Inst] -> [Inst]
- -> TcM TcDictBinds
+bindIrredsR :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds
-- Make a binding that binds 'irreds', by generating an implication
-- constraint for them, *and* throwing the constraint into the LIE
-bindIrredsR loc qtvs co_vars reft givens irreds
+bindIrredsR loc qtvs givens irreds
| null irreds
= return emptyBag
| otherwise
- = do { let givens' = filter isDict givens
- -- The givens can include methods
+ = do { let givens' = filter isAbstractableInst givens
+ -- The givens can (redundantly) include methods
+ -- We want to retain both EqInsts and Dicts
+ -- There should be no implicadtion constraints
-- See Note [Pruning the givens in an implication constraint]
- -- If there are no 'givens' *and* the refinement is empty
- -- (the refinement is like more givens), then it's safe to
+ -- If there are no 'givens', then it's safe to
-- partition the 'wanteds' by their qtvs, thereby trimming irreds
-- See Note [Freeness and implications]
- ; irreds' <- if null givens' && isEmptyRefinement reft
+ ; irreds' <- if null givens'
then do
{ let qtv_set = mkVarSet qtvs
(frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
; return real_irreds }
else return irreds
- ; let all_tvs = qtvs ++ co_vars -- Abstract over all these
- ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
+ ; (implics, bind) <- makeImplicationBind loc qtvs givens' irreds'
-- This call does the real work
-- If irreds' is empty, it does something sensible
; extendLIEs implics
; return bind }
-makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
+makeImplicationBind :: InstLoc -> [TcTyVar]
-> [Inst] -> [Inst]
-> TcM ([Inst], TcDictBinds)
-- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
+-- constraint for them.
+--
-- The binding looks like
-- (ir1, .., irn) = f qtvs givens
-- where f is (evidence for) the new implication constraint
--- f :: forall qtvs. {reft} givens => (ir1, .., irn)
--- qtvs includes coercion variables
+-- f :: forall qtvs. givens => (ir1, .., irn)
+-- qtvs includes coercion variables.
--
-- This binding must line up the 'rhs' in reduceImplication
-makeImplicationBind loc all_tvs reft
- givens -- Guaranteed all Dicts
+makeImplicationBind loc all_tvs
+ givens -- Guaranteed all Dicts or EqInsts
irreds
| null irreds -- If there are no irreds, we are done
= return ([], emptyBag)
| otherwise -- Otherwise we must generate a binding
= do { uniq <- newUnique
; span <- getSrcSpanM
- ; let name = mkInternalName uniq (mkVarOcc "ic") span
- implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
+ ; let (eq_givens, dict_givens) = partition isEqInst givens
+
+ -- extract equality binders
+ eq_cotvs = map eqInstType eq_givens
+
+ -- make the implication constraint instance
+ name = mkInternalName uniq (mkVarOcc "ic") span
+ implic_inst = ImplicInst { tci_name = name,
tci_tyvars = all_tvs,
- tci_given = 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
- 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)) }
+ tci_given = (eq_givens ++ dict_givens),
+ -- same order as binders
+ tci_wanted = irreds,
+ tci_loc = loc }
+
+ -- create binders for the irreducible dictionaries
+ dict_irreds = filter (not . isEqInst) irreds
+ dict_irred_ids = map instToId dict_irreds
+ lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
+
+ -- create the binding
+ rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
+ co = mkWpApps (map instToId dict_givens)
+ <.> mkWpTyApps eq_cotvs
+ <.> mkWpTyApps (mkTyVarTys all_tvs)
+ bind | [dict_irred_id] <- dict_irred_ids
+ = VarBind dict_irred_id rhs
+ | otherwise
+ = PatBind { pat_lhs = lpat
+ , pat_rhs = unguardedGRHSs rhs
+ , pat_rhs_ty = hsLPatType lpat
+ , bind_fvs = placeHolderNames
+ }
+
+ ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
+ ; return ([implic_inst], unitBag (L span bind))
+ }
-----------------------------------------------------------
tryHardCheckLoop :: SDoc
-> TcM ([Inst], TcDictBinds)
tryHardCheckLoop doc wanteds
- = checkLoop (mkRedEnv doc try_me []) wanteds
+ = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds
+ ; return (irreds,binds)
+ }
where
- try_me inst = ReduceMe AddSCs
+ try_me _ = ReduceMe
-- Here's the try-hard bit
-----------------------------------------------------------
-> TcM ([Inst], TcDictBinds)
gentleCheckLoop inst_loc givens wanteds
- = checkLoop env wanteds
+ = do { (irreds,binds) <- checkLoop env wanteds
+ ; return (irreds,binds)
+ }
where
env = mkRedEnv (pprInstLoc inst_loc) try_me givens
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ try_me inst | isMethodOrLit inst = ReduceMe
| 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 = mkInferRedEnv doc try_me
+ try_me inst | isMethodOrLit inst = ReduceMe
+ | otherwise = Stop
\end{code}
Note [Check gently]
Hence we have a dictionary for Show [a] available; and indeed we
need it. We are going to build an implication contraint
forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledg e(Show b)
+Later, we will solve this constraint using the knowledge (Show b)
But we MUST NOT reduce (Show [a]) to (Show a), else the whole
thing becomes insoluble. So we simplify gently (get rid of literals
-----------------------------------------------------------
checkLoop :: RedEnv
-> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
+ -> TcM ([Inst], TcDictBinds)
-- 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
+ = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+ ; env' <- zonkRedEnv env
+ ; wanteds' <- zonkInsts wanteds
+
+ ; (improved, binds, irreds) <- reduceContext env' wanteds'
- ; (improved, binds, irreds) <- reduceContext env wanteds'
+ ; if null irreds || not improved then
+ return (irreds, binds)
+ else do
+
+ -- If improvement did some unification, we go round again.
+ -- We start again with irreds, not wanteds
+ -- Using an instance decl might have introduced a fresh type
+ -- variable which might have been unified, so we'd get an
+ -- infinite loop if we started again with wanteds!
+ -- See Note [LOOP]
+ { (irreds1, binds1) <- go env' irreds
+ ; return (irreds1, binds `unionBags` binds1) } }
+\end{code}
- ; if not improved then
- return (irreds, binds)
- else do
+Note [Zonking RedEnv]
+~~~~~~~~~~~~~~~~~~~~~
+It might appear as if the givens in RedEnv are always rigid, but that is not
+necessarily the case for programs involving higher-rank types that have class
+contexts constraining the higher-rank variables. An example from tc237 in the
+testsuite is
+
+ class Modular s a | s -> a
+
+ wim :: forall a w. Integral a
+ => a -> (forall s. Modular s a => M s w) -> w
+ wim i k = error "urk"
+
+ test5 :: (Modular s a, Integral a) => M s a
+ test5 = error "urk"
+
+ test4 = wim 4 test4'
+
+Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
+quantified further outside. When type checking test4, we have to check
+whether the signature of test5 is an instance of
+
+ (forall s. Modular s a => M s w)
+
+Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
+givens.
+
+Given the FD of Modular in this example, class improvement will instantiate
+t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
+Modular s a predicate in that signature). If we don't zonk (Modular s t_a) in
+the givens, we will get into a loop as improveOne uses the unification engine
+Unify.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]
~~~~~~~~~~~
ds2 = $p1 dc
And now we've defined the superclass in terms of itself.
-
-Solution: never generate a superclass selectors at all when
-satisfying the superclass context of an instance declaration.
-
Two more nasty cases are in
tcrun021
tcrun033
+Solution:
+ - Satisfy the superclass context *all by itself*
+ (tcSimplifySuperClasses)
+ - And do so completely; i.e. no left-over constraints
+ to mix with the constraints arising from method declarations
+
+
+Note [Recursive instances and superclases]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this code, which arises in the context of "Scrap Your
+Boilerplate with Class".
+
+ class Sat a
+ class Data ctx a
+ instance Sat (ctx Char) => Data ctx Char
+ instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
+
+ class Data Maybe a => Foo a
+
+ instance Foo t => Sat (Maybe t)
+
+ instance Data Maybe a => Foo a
+ instance Foo a => Foo [a]
+ instance Foo [Char]
+
+In the instance for Foo [a], when generating evidence for the superclasses
+(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
+Using the instance for Data, we therefore need
+ (Sat (Maybe [a], Data Maybe a)
+But we are given (Foo a), and hence its superclass (Data Maybe a).
+So that leaves (Sat (Maybe [a])). Using the instance for Sat means
+we need (Foo [a]). And that is the very dictionary we are bulding
+an instance for! So we must put that in the "givens". So in this
+case we have
+ Given: Foo a, Foo [a]
+ Watend: Data Maybe [a]
+
+BUT we must *not not not* put the *superclasses* of (Foo [a]) in
+the givens, which is what 'addGiven' would normally do. Why? Because
+(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
+by selecting a superclass from Foo [a], which simply makes a loop.
+
+On the other hand we *must* put the superclasses of (Foo a) in
+the givens, as you can see from the derivation described above.
+
+Conclusion: in the very special case of tcSimplifySuperClasses
+we have one 'given' (namely the "this" dictionary) whose superclasses
+must not be added to 'givens' by addGiven. That is the *whole* reason
+for the red_given_scs field in RedEnv, and the function argument to
+addGiven.
+
\begin{code}
-tcSimplifySuperClasses
+tcSimplifySuperClasses
:: InstLoc
+ -> Inst -- The dict whose superclasses
+ -- are being figured out
-> [Inst] -- Given
-> [Inst] -- Wanted
-> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
- = do { (irreds, binds1) <- checkLoop env sc_wanteds
+tcSimplifySuperClasses loc this givens 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 tryHardCheckLoop, but with NoSCs
+ env = RedEnv { red_doc = pprInstLoc loc,
+ red_try_me = try_me,
+ red_givens = this:givens,
+ red_given_scs = add_scs,
+ red_stack = (0,[]),
+ red_improve = False } -- No unification vars
+ add_scs g | g==this = NoSCs
+ | otherwise = AddSCs
+
+ try_me _ = ReduceMe -- Try hard, so we completely solve the superclass
+ -- constraints right here. See Note [SUPERCLASS-LOOP 1]
\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
-- BUT do no improvement! See Plan D above
-- HOWEVER, some unification may take place, if we instantiate
-- a method Inst with an equality constraint
- ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
+ ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
; (_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
-- Warn in the mono
; warn_mono <- doptM Opt_WarnMonomorphism
; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
- (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding")
- <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs,
- ptext SLIT("Consider giving a type signature for") <+> pp_bndrs])
+ (vcat[ ptext (sLit "the Monomorphism Restriction applies to the binding")
+ <> plural bndrs <+> ptext (sLit "for") <+> pp_bndrs,
+ ptext (sLit "Consider giving a type signature for") <+> pp_bndrs])
; traceTc (text "tcSimplifyRestricted" <+> vcat [
pprInsts wanteds, pprInsts constrained_dicts',
; let is_nested_group = isNotTopLevel top_lvl
try_me inst | isFreeWrtTyVars qtvs inst,
(is_nested_group || isDict inst) = Stop
- | otherwise = ReduceMe AddSCs
+ | otherwise = ReduceMe
env = mkNoImproveRedEnv doc try_me
; (_imp, binds, irreds) <- reduceContext env wanteds'
In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
all dicts unchanged, with absolutely no sharing. It's simpler to do this
-from scratch, rather than further parameterise simpleReduceLoop etc
+from scratch, rather than further parameterise simpleReduceLoop etc.
+Simpler, maybe, but alas not simple (see Trac #2494)
+
+* Type errors may give rise to an (unsatisfiable) equality constraint
+
+* Applications of a higher-rank function on the LHS may give
+ rise to an implication constraint, esp if there are unsatisfiable
+ equality constraints inside.
\begin{code}
tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
tcSimplifyRuleLhs wanteds
- = go [] emptyBag wanteds
+ = do { wanteds' <- zonkInsts wanteds
+ ; (irreds, binds) <- go [] emptyBag wanteds'
+ ; let (dicts, bad_irreds) = partition isDict irreds
+ ; traceTc (text "tcSimplifyrulelhs" <+> pprInsts bad_irreds)
+ ; addNoInstanceErrs (nub bad_irreds)
+ -- The nub removes duplicates, which has
+ -- not happened otherwise (see notes above)
+ ; return (dicts, binds) }
where
- go dicts binds []
- = return (dicts, binds)
- go dicts binds (w:ws)
+ go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds)
+ go irreds binds []
+ = return (irreds, binds)
+ go irreds binds (w:ws)
| isDict w
- = go (w:dicts) binds ws
+ = go (w:irreds) binds ws
+ | isImplicInst w -- Have a go at reducing the implication
+ = do { (binds1, irreds1) <- reduceImplication red_env w
+ ; let (bad_irreds, ok_irreds) = partition isImplicInst irreds1
+ ; go (bad_irreds ++ irreds)
+ (binds `unionBags` binds1)
+ (ok_irreds ++ ws)}
| otherwise
= do { w' <- zonkInst w -- So that (3::Int) does not generate a call
-- to fromInteger; this looks fragile to me
; lookup_result <- lookupSimpleInst w'
; case lookup_result of
- GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws)
- NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
+ NoInstance -> go (w:irreds) binds ws
+ GenInst ws' rhs -> go irreds binds' (ws' ++ ws)
+ where
+ binds' = addInstToDictBind binds w rhs
}
+
+ -- Sigh: we need to reduce inside implications
+ red_env = mkInferRedEnv doc try_me
+ doc = ptext (sLit "Implication constraint in RULE lhs")
+ try_me inst | isMethodOrLit inst = ReduceMe
+ | otherwise = Stop -- Be gentle
\end{code}
tcSimplifyBracket is used when simplifying the constraints arising from
-- 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'
- ; if not improved then
+ ; if null irreds || not improved then
ASSERT( all is_free irreds )
do { extendLIEs irreds
; return binds }
- else
- tcSimplifyIPs given_ips wanteds }
+ 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]
+ { binds1 <- tcSimplifyIPs given_ips' irreds
+ ; return $ binds `unionBags` binds1
+ } }
where
doc = text "tcSimplifyIPs" <+> ppr given_ips
ip_set = mkNameSet (ipNamesOfInsts given_ips)
-- Simplify any methods that mention the implicit parameter
try_me inst | is_free inst = Stop
- | otherwise = ReduceMe NoSCs
+ | otherwise = ReduceMe
\end{code}
-- arguably a bug in Match.tidyEqnInfo (see notes there)
bindInstsOfLocalFuns wanteds local_ids
- | null overloaded_ids
+ | null overloaded_ids = do
-- Common case
- = extendLIEs wanteds `thenM_`
- returnM emptyLHsBinds
+ extendLIEs wanteds
+ return emptyLHsBinds
| otherwise
- = do { (irreds, binds) <- checkLoop env for_me
+ = do { (irreds, binds) <- gentleInferLoop doc for_me
; extendLIEs not_for_me
; extendLIEs irreds
; return binds }
where
- env = mkRedEnv doc try_me []
doc = text "bindInsts" <+> ppr local_ids
overloaded_ids = filter is_overloaded local_ids
is_overloaded id = isOverloadedTy (idType id)
overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
-- so it's worth building a set, so that
-- lookup (in isMethodFor) is faster
- try_me inst | isMethod inst = ReduceMe NoSCs
- | otherwise = Stop
\end{code}
, red_try_me :: Inst -> WhatToDo
, red_improve :: Bool -- True <=> do improvement
, red_givens :: [Inst] -- All guaranteed rigid
- -- Always dicts
+ -- Always dicts & equalities
-- but see Note [Rigidity]
+
+ , red_given_scs :: Inst -> WantSCs -- See Note [Recursive instances and superclases]
+
, 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_given_scs = const AddSCs,
+ red_stack = (0,[]),
+ red_improve = True }
+
+mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
+-- No givens at all
+mkInferRedEnv doc try_me
+ = RedEnv { red_doc = doc, red_try_me = try_me,
+ red_givens = [],
+ red_given_scs = const AddSCs,
+ 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_given_scs = const AddSCs,
+ red_stack = (0,[]),
red_improve = True }
data WhatToDo
- = ReduceMe WantSCs -- Try to reduce this
- -- If there's no instance, add the inst to the
- -- irreductible ones, but don't produce an error
- -- message of any kind.
- -- It might be quite legitimate such as (Eq a)!
+ = ReduceMe -- Try to reduce this
+ -- If there's no instance, add the inst to the
+ -- irreductible ones, but don't produce an error
+ -- message of any kind.
+ -- It might be quite legitimate such as (Eq a)!
| Stop -- Return as irreducible unless it can
-- be reduced to a constant in one step
-- of a predicate when adding it to the avails
-- The reason for this flag is entirely the super-class loop problem
-- Note [SUPER-CLASS LOOP 1]
+
+zonkRedEnv :: RedEnv -> TcM RedEnv
+zonkRedEnv env
+ = do { givens' <- mapM zonkInst (red_givens env)
+ ; return $ env {red_givens = givens'}
+ }
\end{code}
+
%************************************************************************
%* *
\subsection[reduce]{@reduce@}
%* *
%************************************************************************
+Note [Ancestor Equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+During context reduction, we add to the wanted equalities also those
+equalities that (transitively) occur in superclass contexts of wanted
+class constraints. Consider the following code
+
+ class a ~ Int => C a
+ instance C Int
+
+If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
+substituting Int for a. Hence, we ultimately want (C Int), which we
+discharge with the explicit instance.
\begin{code}
reduceContext :: RedEnv
TcDictBinds, -- Dictionary bindings
[Inst]) -- Irreducible
-reduceContext env wanteds
+reduceContext env wanteds0
= do { traceTc (text "reduceContext" <+> (vcat [
text "----------------------",
red_doc env,
text "given" <+> ppr (red_givens env),
- text "wanted" <+> ppr wanteds,
+ text "wanted" <+> ppr wanteds0,
text "----------------------"
]))
- -- Build the Avail mapping from "givens"
- ; init_state <- foldlM addGiven emptyAvails (red_givens env)
-
- -- Do the real work
- -- Process non-implication constraints first, so that they are
- -- available to help solving the implication constraints
- -- ToDo: seems a bit inefficient and ad-hoc
- ; let (implics, rest) = partition isImplicInst wanteds
- ; avails <- reduceList env (rest ++ implics) init_state
-
- ; let improved = availsImproved avails
- ; (binds, irreds) <- extractResults avails 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 wanteds0
+ ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
+
+ -- Normalise and solve all equality constraints as far as possible
+ -- and normalise all dictionary constraints wrt to the reduced
+ -- equalities. The returned wanted constraints include the
+ -- irreducible wanted equalities.
+ ; let wanteds = wanteds0 ++ ancestor_eqs
+ givens = red_givens env
+ ; (givens',
+ wanteds',
+ normalise_binds,
+ eq_improved) <- tcReduceEqs givens wanteds
+ ; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
+ [ppr givens', ppr wanteds', ppr normalise_binds]
+
+ -- Build the Avail mapping from "given_dicts"
+ ; (init_state, _) <- getLIE $ do
+ { init_state <- foldlM (addGiven (red_given_scs env))
+ emptyAvails givens'
+ ; return init_state
+ }
+
+ -- Solve the *wanted* *dictionary* constraints (not implications)
+ -- This may expose some further equational constraints...
+ ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
+ ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+ -- The getLIE is reqd because reduceList does improvement
+ -- (via extendAvails) which may in turn do unification
+ ; (dict_binds,
+ bound_dicts,
+ dict_irreds) <- extractResults avails wanted_dicts
+ ; traceTc $ text "reduceContext: extractResults" <+> vcat
+ [ppr avails, ppr wanted_dicts, ppr dict_binds]
+
+ -- Solve the wanted *implications*. In doing so, we can provide
+ -- as "given" all the dicts that were originally given,
+ -- *or* for which we now have bindings,
+ -- *or* which are now irreds
+ -- NB: Equality irreds need to be converted, as the recursive
+ -- invocation of the solver will still treat them as wanteds
+ -- otherwise.
+ ; let implic_env = env { red_givens
+ = givens ++ bound_dicts ++
+ map wantedToLocalEqInst dict_irreds }
+ ; (implic_binds_s, implic_irreds_s)
+ <- mapAndUnzipM (reduceImplication implic_env) wanted_implics
+ ; let implic_binds = unionManyBags implic_binds_s
+ implic_irreds = concat implic_irreds_s
+
+ -- Collect all irreducible instances, and determine whether we should
+ -- go round again. We do so in either of two cases:
+ -- (1) If dictionary reduction or equality solving led to
+ -- improvement (i.e., instantiated type variables).
+ -- (2) If we uncovered extra equalities. We will try to solve them
+ -- in the next iteration.
+ -- (3) If we reduced dictionaries (i.e., got dictionary bindings),
+ -- they may have exposed further opportunities to normalise
+ -- family applications. See Note [Dictionary Improvement]
+
+ ; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs
+ avails_improved = availsImproved avails
+ improvedFlexible = avails_improved || eq_improved
+ extraEqs = (not . null) extra_eqs
+ reduced_dicts = not (isEmptyBag dict_binds)
+ improved = improvedFlexible || extraEqs || reduced_dicts
+ --
+ improvedHint = (if avails_improved then " [AVAILS]" else "") ++
+ (if eq_improved then " [EQ]" else "") ++
+ (if extraEqs then " [EXTRA EQS]" else "")
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
red_doc env,
- text "given" <+> ppr (red_givens env),
- text "wanted" <+> ppr wanteds,
+ text "given" <+> ppr givens,
+ text "wanted" <+> ppr wanteds0,
text "----",
text "avails" <+> pprAvails avails,
- text "improved =" <+> ppr improved,
- text "irreds = " <+> ppr irreds,
+ text "improved =" <+> ppr improved <+> text improvedHint,
+ text "(all) irreds = " <+> ppr all_irreds,
+ text "dict-binds = " <+> ppr dict_binds,
+ text "implic-binds = " <+> ppr implic_binds,
text "----------------------"
]))
- ; return (improved, binds, irreds) }
+ ; return (improved,
+ normalise_binds `unionBags` dict_binds
+ `unionBags` implic_binds,
+ all_irreds)
+ }
tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
tcImproveOne avails inst
-- Avails has all the superclasses etc (good)
-- It also has all the intermediates of the deduction (good)
-- It does not have duplicates (good)
- -- NB that (?x::t1) and (?x::t2) will be held separately in avails
- -- so that improve will see them separate
+ -- NB that (?x::t1) and (?x::t2) will be held separately in
+ -- avails so that improve will see them separate
; traceTc (text "improveOne" <+> ppr inst)
; unifyEqns eqns }
-unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))]
+unifyEqns :: [(Equation, (PredType, SDoc), (PredType, SDoc))]
-> TcM ImprovementDone
unifyEqns [] = return False
unifyEqns eqns
- = do { traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))
- ; mappM_ unify eqns
- ; return True }
+ = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
+ ; improved <- mapM unify eqns
+ ; return $ or improved
+ }
where
unify ((qtvs, pairs), what1, what2)
- = addErrCtxtM (mkEqnMsg what1 what2) $
- tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
- mapM_ (unif_pr tenv) pairs
- unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
+ = addErrCtxtM (mkEqnMsg what1 what2) $
+ do { let freeTyVars = unionVarSets (map tvs_pr pairs)
+ `minusVarSet` qtvs
+ ; (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+ ; mapM_ (unif_pr tenv) pairs
+ ; anyM isFilledMetaTyVar $ varSetElems freeTyVars
+ }
+
+ unif_pr tenv (ty1, ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+ tvs_pr (ty1, ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
+pprEquationDoc (eqn, (p1, _), (p2, _))
+ = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+ -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
- = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
- ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
- ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
+ = do { pred1' <- zonkTcPredType pred1
+ ; pred2' <- zonkTcPredType pred2
+ ; let { pred1'' = tidyPred tidy_env pred1'
+ ; pred2'' = tidyPred tidy_env pred2' }
+ ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
; return (tidy_env, msg) }
\end{code}
+Note [Dictionary Improvement]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In reduceContext, we first reduce equalities and then class constraints.
+However, the letter may expose further opportunities for the former. Hence,
+we need to go around again if dictionary reduction produced any dictionary
+bindings. The following example demonstrated the point:
+
+ data EX _x _y (p :: * -> *)
+ data ANY
+
+ class Base p
+
+ class Base (Def p) => Prop p where
+ type Def p
+
+ instance Base ()
+ instance Prop () where
+ type Def () = ()
+
+ instance (Base (Def (p ANY))) => Base (EX _x _y p)
+ instance (Prop (p ANY)) => Prop (EX _x _y p) where
+ type Def (EX _x _y p) = EX _x _y p
+
+ data FOO x
+ instance Prop (FOO x) where
+ type Def (FOO x) = ()
+
+ data BAR
+ instance Prop BAR where
+ type Def BAR = EX () () FOO
+
+During checking the last instance declaration, we need to check the superclass
+cosntraint Base (Def BAR), which family normalisation reduced to
+Base (EX () () FOO). Chasing the instance for Base (EX _x _y p), gives us
+Base (Def (FOO ANY)), which again requires family normalisation of Def to
+Base () before we can finish.
+
+
The main context-reduction function is @reduce@. Here's its game plan.
\begin{code}
reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
- = do { dopts <- getDOpts
-#ifdef DEBUG
- ; if n > 8 then
- dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n)
+ = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
+ ; dopts <- getDOpts
+ ; when (debugIsOn && (n > 8)) $ do
+ debugDumpTcRn (hang (ptext (sLit "Interesting! Context reduction stack depth") <+> int n)
2 (ifPprDebug (nest 2 (pprStack stk))))
- else return ()
-#endif
; if n >= ctxtStkDepth dopts then
failWithTc (reduceDepthErr n stk)
else
; go ws state' }
-- Base case: we're done!
+reduce :: RedEnv -> Inst -> Avails -> TcM Avails
reduce env wanted avails
+
+ -- We don't reduce equalities here (and they must not end up as irreds
+ -- in the Avails!)
+ | isEqInst wanted
+ = return avails
+
-- It's the same as an existing inst, or a superclass thereof
- | Just avail <- findAvail avails wanted
- = returnM avails
+ | Just _ <- findAvail avails wanted
+ = do { traceTc (text "reduce: found " <+> ppr wanted)
+ ; return 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 -> do -- It should be reduced
+ { (avails, lookup_result) <- reduceInst env avails wanted
+ ; case lookup_result of
+ NoInstance -> addIrred AddSCs avails wanted
-- Add it and its superclasses
- addIrred want_scs avails wanted
-
- GenInst [] rhs -> addWanted want_scs avails wanted rhs []
+
+ GenInst [] rhs -> addWanted AddSCs 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 AddSCs 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)
= do { res <- lookupSimpleInst wanted
; case res of
GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
- other -> do_this_otherwise avails wanted }
+ _ -> do_this_otherwise avails wanted }
\end{code}
+Note [RECURSIVE DICTIONARIES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data D r = ZeroD | SuccD (r (D r));
+
+ instance (Eq (r (D r))) => Eq (D r) where
+ ZeroD == ZeroD = True
+ (SuccD a) == (SuccD b) = a == b
+ _ == _ = False;
+
+ equalDC :: D [] -> D [] -> Bool;
+ equalDC = (==);
+
+We need to prove (Eq (D [])). Here's how we go:
+
+ d1 : Eq (D [])
+
+by instance decl, holds if
+ d2 : Eq [D []]
+ where d1 = dfEqD d2
+
+by instance decl of Eq, holds if
+ d3 : D []
+ where d2 = dfEqList d3
+ d1 = dfEqD d2
+
+But now we can "tie the knot" to give
+
+ d3 = d1
+ d2 = dfEqList d3
+ d1 = dfEqD d2
+
+and it'll even run! The trick is to put the thing we are trying to prove
+(in this case Eq (D []) into the database before trying to prove its
+contributing clauses.
+
Note [SUPERCLASS-LOOP 2]
~~~~~~~~~~~~~~~~~~~~~~~~
-But the above isn't enough. Suppose we are *given* d1:Ord a,
-and want to deduce (d2:C [a]) where
+We need to be careful when adding "the constaint we are trying to prove".
+Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
class Ord a => C a where
instance Ord [a] => C [a] where ...
when adding superclasses. It's a bit like the occurs check in unification.
-Note [RECURSIVE DICTIONARIES]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- data D r = ZeroD | SuccD (r (D r));
-
- instance (Eq (r (D r))) => Eq (D r) where
- ZeroD == ZeroD = True
- (SuccD a) == (SuccD b) = a == b
- _ == _ = False;
-
- equalDC :: D [] -> D [] -> Bool;
- equalDC = (==);
-
-We need to prove (Eq (D [])). Here's how we go:
-
- d1 : Eq (D [])
-
-by instance decl, holds if
- d2 : Eq [D []]
- where d1 = dfEqD d2
-
-by instance decl of Eq, holds if
- d3 : D []
- where d2 = dfEqList d3
- d1 = dfEqD d2
-
-But now we can "tie the knot" to give
-
- d3 = d1
- d2 = dfEqList d3
- d1 = dfEqD d2
-
-and it'll even run! The trick is to put the thing we are trying to prove
-(in this case Eq (D []) into the database before trying to prove its
-contributing clauses.
-
%************************************************************************
%* *
\begin{code}
---------------------------------------------
reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
- tci_given = extra_givens, tci_wanted = wanteds })
- = reduceImplication env avails reft tvs extra_givens wanteds loc
-
-reduceInst env avails other_inst
+reduceInst _ 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
- -> Refinement -- May refine the givens; often empty
- -> [TcTyVar] -- Quantified type variables; all skolems
- -> [Inst] -- Extra givens; all rigid
- -> [Inst] -- Wanted
- -> InstLoc
- -> TcM (Avails, LookupInstResult)
+ -> Inst
+ -> TcM (TcDictBinds, [Inst])
\end{code}
Suppose we are simplifying the constraint
forall bs. extras => wanted
-in the context of an overall simplification problem with givens 'givens',
-and refinment 'reft'.
+in the context of an overall simplification problem with givens 'givens'.
Note that
- * The refinement is often empty
-
- * The 'extra givens' need not mention any of the quantified type variables
+ * The 'givens' need not mention any of the quantified type variables
e.g. forall {}. Eq a => Eq [a]
forall {}. C Int => D (Tree Int)
\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
- = 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
-
- -- Solve the sub-problem
- ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
- env' = env { red_givens = refined_red_givens ++ extra_givens
+ -- 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
+ --
+ -- Note [Binders for equalities]
+ -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ -- To reuse the binders of local/given equalities in the binders of
+ -- implication constraints, it is crucial that these given equalities
+ -- always have the form
+ -- cotv :: t1 ~ t2
+ -- where cotv is a simple coercion type variable (and not a more
+ -- complex coercion term). We require that the extra_givens always
+ -- have this form and exploit the special form when generating binders.
+reduceImplication env
+ orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
+ tci_tyvars = tvs,
+ tci_given = extra_givens, tci_wanted = wanteds
+ })
+ = do { -- Solve the sub-problem
+ ; let try_me _ = ReduceMe -- Note [Freeness and implications]
+ env' = env { red_givens = extra_givens ++ red_givens env
+ , red_doc = sep [ptext (sLit "reduceImplication for")
+ <+> ppr name,
+ nest 2 (parens $ ptext (sLit "within")
+ <+> red_doc env)]
, red_try_me = try_me }
; traceTc (text "reduceImplication" <+> vcat
- [ ppr orig_avails,
- ppr (red_givens env), ppr extra_givens,
- ppr reft, ppr wanteds, ppr avails ])
- ; avails <- reduceList env' wanteds avails
+ [ ppr (red_givens env), ppr extra_givens,
+ ppr wanteds])
+ ; (irreds, binds) <- checkLoop env' wanteds
- -- Extract the binding
- ; (binds, irreds) <- extractResults avails wanteds
-
; traceTc (text "reduceImplication result" <+> vcat
- [ ppr irreds, ppr binds])
+ [ppr irreds, ppr binds])
+
+ ; -- extract superclass binds
+ -- (sc_binds,_) <- extractResults avails []
+-- ; traceTc (text "reduceImplication sc_binds" <+> vcat
+-- [ppr sc_binds, ppr avails])
+--
- -- We always discard the extra avails we've generated;
- -- but we remember if we have done any (global) improvement
- ; let ret_avails = updateImprovement orig_avails avails
+ -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
+ -- Then we must iterate the outer loop too!
- ; if isEmptyLHsBinds binds then -- No progress
- return (ret_avails, NoInstance)
+ ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
+ -- we solve wanted eqs by side effect!
+
+ -- Progress is no longer measered by the number of bindings
+ -- If there are any irreds, but no bindings and no solved
+ -- equalities, we back off and do nothing
+ ; let backOff = isEmptyLHsBinds binds && -- no new bindings
+ (not $ null irreds) && -- but still some irreds
+ didntSolveWantedEqs -- no instantiated cotv
+
+ ; if backOff then -- No progress
+ return (emptyBag, [orig_implic])
else do
- { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
-
- ; let dict_ids = map instToId extra_givens
- co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
- rhs = mkHsWrap co payload
- loc = instLocSpan inst_loc
- payload | [wanted] <- wanteds = HsVar (instToId wanted)
- | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
-
- -- If there are any irreds, we back off and return NoInstance
- ; return (ret_avails, GenInst implic_insts (L loc rhs))
- } }
+ { (simpler_implic_insts, bind)
+ <- makeImplicationBind inst_loc tvs extra_givens irreds
+ -- This binding is useless if the recursive simplification
+ -- made no progress; but currently we don't try to optimise that
+ -- case. After all, we only try hard to reduce at top level, or
+ -- when inferring types.
+
+ ; let -- extract Id binders for dicts and CoTyVar binders for eqs;
+ -- see Note [Binders for equalities]
+ (extra_eq_givens, extra_dict_givens) = partition isEqInst
+ extra_givens
+ eq_cotvs = map instToVar extra_eq_givens
+ dict_ids = map instToId extra_dict_givens
+
+ -- Note [Always inline implication constraints]
+ wrap_inline | null dict_ids = idHsWrapper
+ | otherwise = WpInline
+ co = wrap_inline
+ <.> mkWpTyLams tvs
+ <.> mkWpTyLams eq_cotvs
+ <.> mkWpLams dict_ids
+ <.> WpLet (binds `unionBags` bind)
+ rhs = mkLHsWrap co payload
+ loc = instLocSpan inst_loc
+ -- wanted equalities are solved by updating their
+ -- cotv; we don't generate bindings for them
+ dict_bndrs = map (L loc . HsVar . instToId)
+ . filter (not . isEqInst)
+ $ wanteds
+ payload = mkBigLHsTup dict_bndrs
+
+
+ ; traceTc (vcat [text "reduceImplication" <+> ppr name,
+ ppr simpler_implic_insts,
+ text "->" <+> ppr rhs])
+ ; return (unitBag (L loc (VarBind (instToId orig_implic) rhs)),
+ simpler_implic_insts)
+ }
+ }
+reduceImplication _ i = pprPanic "reduceImplication" (ppr i)
\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 [Freeness and implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's hard to say when an implication constraint can be floated out. Consider
to float the (C Int) out, even though it mentions no type variable in
the constraints!
+One more example: the constraint
+ class C a => D a b
+ instance (C a, E c) => E (a,c)
+
+ constraint: forall b. D Int b => E (Int,c)
+
+You might think that the (D Int b) can't possibly contribute
+to solving (E (Int,c)), since the latter mentions 'c'. But
+in fact it can, because solving the (E (Int,c)) constraint needs
+dictionaries
+ C Int, E c
+and the (C Int) can be satisfied from the superclass of (D Int b).
+So we must still not float (E (Int,c)) out.
+
+To think about: special cases for unary type classes?
+
Note [Pruning the givens in an implication constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are about to form the implication constraint
forall tvs. Eq a => Ord b
The (Eq a) cannot contribute to the (Ord b), because it has no access to
the type variable 'b'. So we could filter out the (Eq a) from the givens.
+But BE CAREFUL of the examples above in [Freeness and implications].
Doing so would be a bit tidier, but all the implication constraints get
simplified away by the optimiser, so it's no great win. So I don't take
type AvailEnv = FiniteMap Inst AvailHow
data AvailHow
- = IsIrred TcId -- Used for irreducible dictionaries,
+ = IsIrred -- Used for irreducible dictionaries,
-- which are going to be lambda bound
- | Given TcId -- Used for dictionaries for which we have a binding
+ | 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
instance Outputable Avails where
ppr = pprAvails
+pprAvails :: Avails -> SDoc
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 ])]
+ = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty)
+ , 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 x) = text "Irred" <+> ppr x
+pprAvail IsIrred = text "Irred"
pprAvail (Given x) = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Rhs rhs bs) = sep [text "Rhs" <+> ppr bs,
+ nest 2 (ppr rhs)]
-------------------------
extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
-- Does improvement
-extendAvails avails@(Avails imp env) inst avail
+extendAvails avails@(Avails imp env) inst avail
= do { imp1 <- tcImproveOne avails inst -- Do any improvement
; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
availsInsts :: Avails -> [Inst]
availsInsts (Avails _ avails) = keysFM avails
+availsImproved :: Avails -> ImprovementDone
availsImproved (Avails imp _) = imp
-
-updateImprovement :: Avails -> Avails -> Avails
--- (updateImprovement a1 a2) sets a1's improvement flag from a2
-updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
\end{code}
Extracting the bindings from a bunch of Avails.
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
+ -> TcM (TcDictBinds, -- Bindings
+ [Inst], -- The insts bound by the bindings
+ [Inst]) -- Irreducible ones
+ -- Note [Reducing implication constraints]
extractResults (Avails _ avails) wanteds
- = go avails emptyBag [] wanteds
+ = go emptyBag [] [] emptyFM wanteds
where
- go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
- -> TcM (TcDictBinds, [Inst])
- go avails binds irreds []
- = returnM (binds, irreds)
-
- go avails binds irreds (w:ws)
+ go :: TcDictBinds -- Bindings for dicts
+ -> [Inst] -- Bound by the bindings
+ -> [Inst] -- Irreds
+ -> DoneEnv -- Has an entry for each inst in the above three sets
+ -> [Inst] -- Wanted
+ -> TcM (TcDictBinds, [Inst], [Inst])
+ go binds bound_dicts irreds _ []
+ = return (binds, bound_dicts, irreds)
+
+ go binds bound_dicts irreds done (w:ws)
+ | isEqInst w
+ = go binds bound_dicts (w:irreds) done' ws
+
+ | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
+ = if w_id `elem` done_ids then
+ go binds bound_dicts irreds done ws
+ else
+ go (add_bind (nlHsVar done_id)) bound_dicts irreds
+ (addToFM done w (done_id : w_id : rest_done_ids)) ws
+
+ | otherwise -- Not yet done
= case findAvailEnv avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds ws
-
- Just (Given id)
- | id == w_id -> go avails binds irreds ws
- | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
- -- The sought Id can be one of the givens, via a superclass chain
- -- and then we definitely don't want to generate an x=x binding!
-
- Just (IsIrred id)
- | id == w_id -> go (add_given avails w) binds (w:irreds) ws
- | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
- -- 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 (ws' ++ ws)
- where
- new_binds = addBind binds w_id rhs
- where
- w_id = instToId w
+ Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+ go binds bound_dicts irreds done ws
+
+ Just IsIrred -> go binds bound_dicts (w:irreds) done' ws
- add_given avails w = extendAvailEnv avails w (Given (instToId w))
- -- Don't add the same binding twice
+ Just (Rhs rhs ws') -> go (add_bind rhs) (w:bound_dicts) irreds done' (ws' ++ ws)
-addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs))
+ Just (Given g) -> go binds' bound_dicts irreds (addToFM done w [g_id]) ws
+ where
+ g_id = instToId g
+ binds' | w_id == g_id = binds
+ | otherwise = add_bind (nlHsVar g_id)
+ where
+ w_id = instToId w
+ done' = addToFM done w [w_id]
+ add_bind rhs = addInstToDictBind binds w rhs
\end{code}
where
avail = Rhs rhs_expr wanteds
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
- -- Always add superclasses for 'givens'
+addGiven :: (Inst -> WantSCs) -> Avails -> Inst -> TcM Avails
+addGiven want_scs avails given = addAvailAndSCs (want_scs given) avails given (Given given)
+ -- Conditionally add superclasses for 'givens'
+ -- See Note [Recursive instances and superclases]
--
-- No ASSERT( not (given `elemAvails` avails) ) because in an instance
-- decl for Ord t we can add both Ord t and Eq t as 'givens',
-- so the assert isn't true
-
-addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
-addRefinedGiven reft (refined_givens, avails) given
- | isDict given -- We sometimes have 'given' methods, but they
- -- are always optional, so we can drop them
- , let pred = dictPred given
- , isRefineablePred pred -- See Note [ImplicInst rigidity]
- , Just (co, pred) <- refinePred reft pred
- = do { new_given <- newDictBndr (instLoc given) pred
- ; let rhs = L (instSpan given) $
- HsWrap (WpCo co) (HsVar (instToId given))
- ; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
- ; return (new_given:refined_givens, avails) }
- -- ToDo: the superclasses of the original given all exist in Avails
- -- so we could really just cast them, but it's more awkward to do,
- -- and hopefully the optimiser will spot the duplicated work
- | otherwise
- = return (refined_givens, avails)
\end{code}
-Note [ImplicInst rigidity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- C :: forall ab. (Eq a, Ord b) => b -> T a
-
- ...(case x of C v -> <body>)...
-
-From the case (where x::T ty) we'll get an implication constraint
- forall b. (Eq ty, Ord b) => <body-constraints>
-Now suppose <body-constraints> itself has an implication constraint
-of form
- forall c. <reft> => <payload>
-Then, we can certainly apply the refinement <reft> to the Ord b, becuase it is
-existential, but we probably should not apply it to the (Eq ty) because it may
-be wobbly. Hence the isRigidInst
-
-@Insts@ are ordered by their class/type info, rather than by their
-unique. This allows the context-reduction mechanism to use standard finite
-maps to do their stuff. It's horrible that this code is here, rather
-than with the Avails handling stuff in TcSimplify
-
\begin{code}
addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
- addAvailAndSCs want_scs avails irred (IsIrred (instToId irred))
+ addAvailAndSCs want_scs avails irred IsIrred
addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
addAvailAndSCs want_scs avails inst avail
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
-- Watch out, though. Since the avails may contain loops
-- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
- findAllDeps so_far other = so_far
+ findAllDeps so_far _ = so_far
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
+ _ -> 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 :: SDoc -> Bool -> [Inst] -> TcM (Bag (LHsBind TcId))
tc_simplify_top doc interactive wanteds
= do { dflags <- getDOpts
- ; wanteds <- mapM zonkInst wanteds
+ ; wanteds <- zonkInsts wanteds
; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
+ ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
- ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
+-- ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds
+ ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
+ ; (irreds2, binds2) <- approximateImplications doc2 (\_ -> True) irreds1
+ ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
-- Use the defaulting rules to do extra unification
-- NB: irreds2 are already zonked
; return (binds1 `unionBags` binds2 `unionBags` binds3) }
where
- doc1 = doc <+> ptext SLIT("(first round)")
- doc2 = doc <+> ptext SLIT("(approximate)")
- doc3 = doc <+> ptext SLIT("(disambiguate)")
+ 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
= return (insts, emptyBag)
| null defaultable_groups
- = do { traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ = 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
- ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
; mapM_ (disambigGroup default_tys) defaultable_groups
-- disambigGroup does unification, hence try again
| extended_defaulting = any isInteractiveClass clss
| otherwise = all is_std_class clss && (any is_num_class clss)
- -- In interactive mode, or with -fextended-default-rules,
+ -- In interactive mode, or with -XExtendedDefaultRules,
-- we default Show a to Show () to avoid graututious errors on "show []"
isInteractiveClass cls
= is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
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
+ }
-----------------------
opt_deflt ovl_strings string_ty) } } }
where
opt_deflt True ty = [ty]
- opt_deflt False ty = []
+ opt_deflt False _ = []
\end{code}
Note [Default unitTy]
~~~~~~~~~~~~~~~~~~~~~
-In interative mode (or with -fextended-default-rules) we add () as the first type we
+In interative mode (or with -XExtendedDefaultRules) we add () as the first type we
try when defaulting. This has very little real impact, except in the following case.
Consider:
Text.Printf.printf "hello"
-> TcM ThetaType -- Needed
-- Given instance (wanted) => C inst_ty
-- Simplify 'wanted' as much as possible
--- The inst_ty is needed only for the termination check
tcSimplifyDeriv orig tyvars theta
= do { (tvs, _, tenv) <- tcInstTyVars tyvars
; wanteds <- newDictBndrsO orig (substTheta tenv theta)
; (irreds, _) <- tryHardCheckLoop doc wanteds
- ; let (tv_dicts, others) = partition isTyVarDict irreds
+ ; let (tv_dicts, others) = partition ok irreds
; addNoInstanceErrs others
+ -- See Note [Exotic derived instance contexts] in TcMType
; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
simpl_theta = substTheta rev_env (map dictPred tv_dicts)
; return simpl_theta }
where
- doc = ptext SLIT("deriving classes for a data type")
-\end{code}
+ doc = ptext (sLit "deriving classes for a data type")
-Note [Exotic derived instance contexts]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- data T a b c = MkT (Foo a b c) deriving( Eq )
- instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
-
-Notice that this instance (just) satisfies the Paterson termination
-conditions. Then we *could* derive an instance decl like this:
-
- instance (C Int a, Eq b, Eq c) => Eq (T a b c)
-
-even though there is no instance for (C Int a), because there just
-*might* be an instance for, say, (C Int Bool) at a site where we
-need the equality instance for T's.
-
-However, this seems pretty exotic, and it's quite tricky to allow
-this, and yet give sensible error messages in the (much more common)
-case where we really want that instance decl for C.
-
-So for now we simply require that the derived instance context
-should have only type-variable constraints.
-
-Here is another example:
- data Fix f = In (f (Fix f)) deriving( Eq )
-Here, if we are prepared to allow -fallow-undecidable-instances we
-could derive the instance
- instance Eq (f (Fix f)) => Eq (Fix f)
-but this is so delicate that I don't think it should happen inside
-'deriving'. If you want this, write it yourself!
-
-NB: if you want to lift this condition, make sure you still meet the
-termination conditions! If not, the deriving mechanism generates
-larger and larger constraints. Example:
- data Succ a = S a
- data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
-
-Note the lack of a Show instance for Succ. First we'll generate
- instance (Show (Succ a), Show a) => Show (Seq a)
-and then
- instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
-and so on. Instead we want to complain of no instance for (Show (Succ a)).
+ ok dict | isDict dict = validDerivPred (dictPred dict)
+ | otherwise = False
+\end{code}
@tcSimplifyDefault@ just checks class-type constraints, essentially;
tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
-> TcM ()
-tcSimplifyDefault theta
- = newDictBndrsO DefaultOrigin theta `thenM` \ wanteds ->
- tryHardCheckLoop doc wanteds `thenM` \ (irreds, _) ->
- addNoInstanceErrs irreds `thenM_`
+tcSimplifyDefault theta = do
+ wanteds <- newDictBndrsO DefaultOrigin theta
+ (irreds, _) <- tryHardCheckLoop doc wanteds
+ addNoInstanceErrs irreds
if null irreds then
- returnM ()
- else
- failM
+ return ()
+ else
+ traceTc (ptext (sLit "tcSimplifyDefault failing")) >> failM
where
- doc = ptext SLIT("default declaration")
+ doc = ptext (sLit "default declaration")
\end{code}
-- Group together insts with the same origin
-- We want to report them together in error messages
-groupErrs report_err []
- = returnM ()
-groupErrs report_err (inst:insts)
- = do_one (inst:friends) `thenM_`
- groupErrs report_err others
-
+groupErrs _ []
+ = return ()
+groupErrs report_err (inst:insts)
+ = do { do_one (inst:friends)
+ ; groupErrs report_err others }
where
-- (It may seem a bit crude to compare the error messages,
-- but it makes sure that we combine just what the user sees,
addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
addTopIPErrs :: [Name] -> [Inst] -> TcM ()
-addTopIPErrs bndrs []
+addTopIPErrs _ []
= return ()
addTopIPErrs bndrs ips
= do { dflags <- getDOpts
where
(tidy_env, tidy_ips) = tidyInsts ips
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")
+ = 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 dflags]
where
(tidy_env, tidy_dicts) = tidyInsts dicts
report dicts = addErrTcM (tidy_env, mk_msg dicts)
- mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
+ mk_msg dicts = addInstLoc dicts (ptext (sLit "Unbound implicit parameter") <>
plural tidy_dicts <+> pprDictsTheta tidy_dicts)
addNoInstanceErrs :: [Inst] -- Wanted (can include implications)
reportNoInstances tidy_env mb_what insts
= groupErrs (report_no_instances tidy_env mb_what) insts
+report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [Inst] -> TcM ()
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
-#ifdef DEBUG
- ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
-#endif
- ([], _) -> Left wanted -- No match
- res -> Right (mk_overlap_msg wanted res)
+ ([], _) -> Left wanted -- No match
+ -- 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
+ ([_],[])
+ | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted)
+ res -> Right (mk_overlap_msg wanted res)
where
(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,
+ 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
else -- One match, plus some unifiers
ASSERT( not (null unifiers) )
- parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
+ 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 -XIncoherentInstances"),
+ ptext (sLit "when compiling the other instance declarations")])]
where
ispecs = [ispec | (ispec, _) <- matches]
+ mk_eq_err :: Inst -> (TidyEnv, SDoc)
+ mk_eq_err inst = misMatchMsg tidy_env (eqInstTys inst)
+
mk_no_inst_err insts
| null insts = empty
| Just (loc, givens) <- mb_what, -- Nested (type signatures, instance decls)
not (isEmptyVarSet (tyVarsOfInsts insts))
= vcat [ addInstLoc insts $
- sep [ ptext SLIT("Could not deduce") <+> pprDictsTheta insts
- , nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta givens]
+ sep [ ptext (sLit "Could not deduce") <+> pprDictsTheta insts
+ , nest 2 $ ptext (sLit "from the context") <+> pprDictsTheta givens]
, show_fixes (fix1 loc : fixes2) ]
| otherwise -- Top level
= vcat [ addInstLoc insts $
- ptext SLIT("No instance") <> plural insts
- <+> ptext SLIT("for") <+> pprDictsTheta insts
+ ptext (sLit "No instance") <> plural insts
+ <+> ptext (sLit "for") <+> pprDictsTheta insts
, show_fixes fixes2 ]
where
- fix1 loc = sep [ ptext SLIT("add") <+> pprDictsTheta insts
- <+> ptext SLIT("to the context of"),
+ fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts
+ <+> ptext (sLit "to the context of"),
nest 2 (ppr (instLocOrigin loc)) ]
-- I'm not sure it helps to add the location
- -- nest 2 (ptext SLIT("at") <+> ppr (instLocSpan loc)) ]
+ -- nest 2 (ptext (sLit "at") <+> ppr (instLocSpan loc)) ]
fixes2 | null instance_dicts = []
- | otherwise = [sep [ptext SLIT("add an instance declaration for"),
+ | otherwise = [sep [ptext (sLit "add an instance declaration for"),
pprDictsTheta instance_dicts]]
instance_dicts = [d | d <- insts, isClassDict d, not (isTyVarDict d)]
-- Insts for which it is worth suggesting an adding an instance declaration
show_fixes :: [SDoc] -> SDoc
show_fixes [] = empty
- show_fixes (f:fs) = sep [ptext SLIT("Possible fix:"),
- nest 2 (vcat (f : map (ptext SLIT("or") <+>) fs))]
+ show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"),
+ nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
+addTopAmbigErrs :: [Inst] -> TcRn ()
addTopAmbigErrs dicts
-- Divide into groups that share a common set of ambiguous tyvars
= ifErrsM (return ()) $ -- Only report ambiguity if no other errors happened
cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
report :: [(Inst,[TcTyVar])] -> TcM ()
- report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
- = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
+ report pairs@((inst,tvs) : _) = do -- The pairs share a common set of ambiguous tyvars
+ (tidy_env, mono_msg) <- mkMonomorphismMsg tidy_env tvs
setSrcSpan (instSpan inst) $
-- the location of the first one will do for the err message
- addErrTcM (tidy_env, msg $$ mono_msg)
+ addErrTcM (tidy_env, msg $$ mono_msg)
where
dicts = map fst pairs
msg = sep [text "Ambiguous type variable" <> plural tvs <+>
; return (tidy_env, mk_msg dflags docs) }
where
mk_msg _ _ | any isRuntimeUnk inst_tvs
- = vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
+ = 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)")
+ 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 dflags docs
- = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
+ = 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 :: DynFlags -> SDoc
monomorphism_fix dflags
- = ptext SLIT("Probable fix:") <+> vcat
- [ptext SLIT("give these definition(s) an explicit type signature"),
+ = 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"
+ then ptext (sLit "or use -XNoMonomorphismRestriction")
+ else empty] -- Only suggest adding "-XNoMonomorphismRestriction"
-- if it is not already set!
-warnDefault ups default_ty
- = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
+warnDefault :: [(Inst, Class, Var)] -> Type -> TcM ()
+warnDefault ups default_ty = do
+ warn_flag <- doptM Opt_WarnTypeDefaults
addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
where
dicts = [d | (d,_,_) <- ups]
-- Tidy them first
(_, tidy_dicts) = tidyInsts dicts
- warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
+ warn_msg = vcat [ptext (sLit "Defaulting the following constraint(s) to type") <+>
quotes (ppr default_ty),
pprDictsInFull tidy_dicts]
+reduceDepthErr :: Int -> [Inst] -> SDoc
reduceDepthErr n stack
- = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
- ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
+ = vcat [ptext (sLit "Context reduction stack overflow; size =") <+> int n,
+ ptext (sLit "Use -fcontext-stack=N to increase stack size to N"),
nest 4 (pprStack stack)]
+pprStack :: [Inst] -> SDoc
pprStack stack = vcat (map pprInstInFull stack)
\end{code}
projects / ghc-hetmet.git / blobdiff