tcSimplifyBracket, tcSimplifyCheckPat,
tcSimplifyDeriv, tcSimplifyDefault,
- bindInstsOfLocalFuns
+ bindInstsOfLocalFuns, bindIrreds,
) where
#include "HsVersions.h"
import TcEnv
import InstEnv
import TcGadt
-import TcMType
import TcType
+import TcMType
import TcIface
import Var
-import TyCon
import Name
import NameSet
import Class
import FiniteMap
import Bag
import Outputable
+import Maybes
import ListSetOps
import Util
import SrcLoc
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
Notes on implicit parameters
--------------------------------------
-Question 1: can we "inherit" implicit parameters
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Inheriting implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
f x = (x::Int) + ?y
over implicit parameters. See the predicate isFreeWhenInferring.
+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
+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'.
+
+
Question 2: type signatures
~~~~~~~~~~~~~~~~~~~~~~~~~~~
BUT WATCH OUT: When you supply a type signature, we can't force you
:: SDoc
-> TcTyVarSet -- fv(T); type vars
-> [Inst] -- Wanted
- -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
- TcDictBinds, -- Bindings
- [TcId]) -- Dict Ids that must be bound here (zonked)
+ -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified)
+ [Inst], -- Dict Ids that must be bound here (zonked)
+ TcDictBinds) -- Bindings
-- Any free (escaping) Insts are tossed into the environment
\end{code}
\begin{code}
-tcSimplifyInfer doc tau_tvs wanted_lie
- = do { let try_me inst | isDict inst = Stop -- Dicts
- | otherwise = ReduceMe NoSCs -- Lits, Methods,
- -- and impliciation constraints
- -- In an effort to make the inferred types simple, we try
- -- to squeeze out implication constraints if we can.
- -- See Note [Squashing methods]
-
- ; (binds1, irreds) <- checkLoop (mkRedEnv doc try_me []) wanted_lie
-
- ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+tcSimplifyInfer doc tau_tvs wanted
+ = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+ ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars
; gbl_tvs <- tcGetGlobalTyVars
- ; let preds = fdPredsOfInsts irreds
+ ; let preds = fdPredsOfInsts wanted'
qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
- (free, bound) = partition (isFreeWhenInferring qtvs) irreds
+ -- 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
+
+ -- 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))
+ ; (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
- -- Remove redundant superclasses from 'bound'
- -- The 'Stop' try_me result does not do so,
- -- see Note [No superclasses for Stop]
- ; let try_me inst = ReduceMe AddSCs
- ; (binds2, irreds) <- checkLoop (mkRedEnv doc try_me []) bound
+ -- 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
+
+ -- We can't abstract over any remaining unsolved
+ -- implications so instead just float them outwards. Ugh.
+ ; let (q_dicts, implics) = partition isDict irreds3
+ ; loc <- getInstLoc (ImplicOrigin doc)
+ ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics
- ; extendLIEs free
- ; return (varSetElems qtvs, binds1 `unionBags` binds2, map instToId irreds) }
+ ; return (qtvs2, 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 other = pprPanic "approximateImplications" (ppr other)
+\end{code}
+
+Note [Inference and implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have a wanted implication constraint (perhaps arising from
+a nested pattern match) like
+ C a => D [a]
+and we are now trying to quantify over 'a' when inferring the type for
+a function. In principle it's possible that there might be an instance
+ instance (C a, E a) => D [a]
+so the context (E a) would suffice. The Right Thing is to abstract over
+the implication constraint, but we don't do that (a) because it'll be
+surprising to programmers and (b) because we don't have the machinery to deal
+with 'given' implications.
+
+So our best approximation is to make (D [a]) part of the inferred
+context, so we can use that to discharge the implication. Hence
+the strange function get_dictsin approximateImplications.
+
+The common cases are more clear-cut, when we have things like
+ forall a. C a => C b
+Here, abstracting over (C b) is not an approximation at all -- but see
+Note [Freeness and implications].
+
+See Trac #1430 and test tc228.
+
+
+\begin{code}
+-----------------------------------------------------------
+-- tcSimplifyInferCheck is used when we know the constraints we are to simplify
+-- against, but we don't know the type variables over which we are going to quantify.
+-- This happens when we have a type signature for a mutually recursive group
+tcSimplifyInferCheck
+ :: InstLoc
+ -> TcTyVarSet -- fv(T)
+ -> [Inst] -- Given
+ -> [Inst] -- Wanted
+ -> TcM ([TyVar], -- Fully zonked, and quantified
+ TcDictBinds) -- Bindings
+
+tcSimplifyInferCheck loc tau_tvs givens wanteds
+ = do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
+
+ -- Figure out which type variables to quantify over
+ -- You might think it should just be the signature tyvars,
+ -- but in bizarre cases you can get extra ones
+ -- f :: forall a. Num a => a -> a
+ -- f x = fst (g (x, head [])) + 1
+ -- g a b = (b,a)
+ -- Here we infer g :: forall a b. a -> b -> (b,a)
+ -- We don't want g to be monomorphic in b just because
+ -- f isn't quantified over b.
+ ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
+ ; all_tvs <- zonkTcTyVarsAndFV all_tvs
+ ; gbl_tvs <- tcGetGlobalTyVars
+ ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs)
+ -- We could close gbl_tvs, but its not necessary for
+ -- soundness, and it'll only affect which tyvars, not which
+ -- dictionaries, we quantify over
+
+ ; qtvs' <- zonkQuantifiedTyVars qtvs
+
+ -- Now we are back to normal (c.f. tcSimplCheck)
+ ; implic_bind <- bindIrreds loc qtvs' givens irreds
+
+ ; return (qtvs', binds `unionBags` implic_bind) }
\end{code}
Note [Squashing methods]
\begin{code}
isFreeWhenInferring :: TyVarSet -> Inst -> Bool
isFreeWhenInferring qtvs inst
- = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
- && isInheritableInst inst -- And no implicit parameter involved
- -- (see "Notes on implicit parameters")
+ = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
+ && isInheritableInst inst -- and no implicit parameter involved
+ -- see Note [Inheriting implicit parameters]
{- No longer used (with implication constraints)
isFreeWhenChecking :: TyVarSet -- Quantified tyvars
-> [Inst] -- Wanted
-> TcM TcDictBinds -- Bindings
tcSimplifyCheck loc qtvs givens wanteds
- = ASSERT( all isSkolemTyVar qtvs )
- do { (binds, irreds) <- innerCheckLoop loc givens wanteds
- ; implic_bind <- bindIrreds loc [] emptyRefinement
- qtvs givens irreds
+ = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
+ do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
+ ; implic_bind <- bindIrreds loc qtvs givens irreds
; return (binds `unionBags` implic_bind) }
-----------------------------------------------------------
-> [Inst] -- Wanted
-> TcM TcDictBinds -- Bindings
tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
- = ASSERT( all isSkolemTyVar qtvs )
- do { (binds, irreds) <- innerCheckLoop loc givens wanteds
- ; implic_bind <- bindIrreds loc co_vars reft
- qtvs givens irreds
+ = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
+ do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
+ ; implic_bind <- bindIrredsR loc qtvs co_vars reft
+ givens irreds
; return (binds `unionBags` implic_bind) }
-----------------------------------------------------------
-bindIrreds :: InstLoc -> [CoVar] -> Refinement
- -> [TcTyVar] -> [Inst] -> [Inst]
- -> TcM TcDictBinds
+bindIrreds :: InstLoc -> [TcTyVar]
+ -> [Inst] -> [Inst]
+ -> TcM TcDictBinds
+bindIrreds loc qtvs givens irreds
+ = bindIrredsR loc qtvs [] emptyRefinement givens irreds
+
+bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar]
+ -> Refinement -> [Inst] -> [Inst]
+ -> TcM TcDictBinds
-- Make a binding that binds 'irreds', by generating an implication
-- constraint for them, *and* throwing the constraint into the LIE
-bindIrreds loc co_vars reft qtvs givens irreds
+bindIrredsR loc qtvs co_vars reft givens irreds
+ | null irreds
+ = return emptyBag
+ | otherwise
= do { let givens' = filter isDict givens
-- The givens can include methods
+ -- See Note [Pruning the givens in an implication constraint]
- -- If there are no 'givens', then it's safe to
+ -- If there are no 'givens' *and* the refinement is empty
+ -- (the refinement is like more givens), then it's safe to
-- partition the 'wanteds' by their qtvs, thereby trimming irreds
-- See Note [Freeness and implications]
- ; irreds' <- if null givens'
+ ; irreds' <- if null givens' && isEmptyRefinement reft
then do
{ let qtv_set = mkVarSet qtvs
(frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
; let all_tvs = qtvs ++ co_vars -- Abstract over all these
; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
- -- This call does the real work
+ -- This call does the real work
+ -- If irreds' is empty, it does something sensible
; extendLIEs implics
; return bind }
-- 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
--
-- This binding must line up the 'rhs' in reduceImplication
makeImplicationBind loc all_tvs reft
| otherwise -- Otherwise we must generate a binding
= do { uniq <- newUnique
; span <- getSrcSpanM
- ; let name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span)
+ ; let name = mkInternalName uniq (mkVarOcc "ic") span
implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
tci_tyvars = all_tvs,
tci_given = givens,
return ([implic_inst], unitBag (L span bind)) }
-----------------------------------------------------------
-topCheckLoop :: SDoc
+tryHardCheckLoop :: SDoc
-> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
+ -> TcM ([Inst], TcDictBinds)
-topCheckLoop doc wanteds
+tryHardCheckLoop doc wanteds
= checkLoop (mkRedEnv doc try_me []) wanteds
where
try_me inst = ReduceMe AddSCs
+ -- Here's the try-hard bit
-----------------------------------------------------------
-innerCheckLoop :: InstLoc
+gentleCheckLoop :: InstLoc
-> [Inst] -- Given
-> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
+ -> TcM ([Inst], TcDictBinds)
-innerCheckLoop inst_loc givens wanteds
+gentleCheckLoop inst_loc givens wanteds
= checkLoop env wanteds
where
env = mkRedEnv (pprInstLoc inst_loc) try_me givens
Hence we have a dictionary for Show [a] available; and indeed we
need it. We are going to build an implication contraint
forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledge (Show b)
+Later, we will solve this constraint using the knowledg e(Show b)
But we MUST NOT reduce (Show [a]) to (Show a), else the whole
thing becomes insoluble. So we simplify gently (get rid of literals
and methods only, plus common up equal things), deferring the real
work until top level, when we solve the implication constraint
-with topCheckLooop.
+with tryHardCheckLooop.
\begin{code}
-----------------------------------------------------------
checkLoop :: RedEnv
-> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
--- Precondition: the try_me never returns Free
--- givens are completely rigid
+ -> 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
; (improved, binds, irreds) <- reduceContext env wanteds'
; if not improved then
- return (binds, irreds)
+ return (irreds, binds)
else do
-- If improvement did some unification, we go round again.
-- 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, irreds1) <- checkLoop env irreds
- ; return (binds `unionBags` binds1, irreds1) } }
+ { (irreds1, binds1) <- checkLoop env irreds
+ ; return (irreds1, binds `unionBags` binds1) } }
\end{code}
Note [LOOP]
with (Max Z (S x) y)!
-\begin{code}
------------------------------------------------------------
--- tcSimplifyInferCheck is used when we know the constraints we are to simplify
--- against, but we don't know the type variables over which we are going to quantify.
--- This happens when we have a type signature for a mutually recursive group
-tcSimplifyInferCheck
- :: InstLoc
- -> TcTyVarSet -- fv(T)
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM ([TcTyVar], -- Variables over which to quantify
- TcDictBinds) -- Bindings
-
-tcSimplifyInferCheck loc tau_tvs givens wanteds
- = do { (binds, irreds) <- innerCheckLoop loc givens wanteds
-
- -- Figure out which type variables to quantify over
- -- You might think it should just be the signature tyvars,
- -- but in bizarre cases you can get extra ones
- -- f :: forall a. Num a => a -> a
- -- f x = fst (g (x, head [])) + 1
- -- g a b = (b,a)
- -- Here we infer g :: forall a b. a -> b -> (b,a)
- -- We don't want g to be monomorphic in b just because
- -- f isn't quantified over b.
- ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
- ; all_tvs <- zonkTcTyVarsAndFV all_tvs
- ; gbl_tvs <- tcGetGlobalTyVars
- ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs)
- -- We could close gbl_tvs, but its not necessary for
- -- soundness, and it'll only affect which tyvars, not which
- -- dictionaries, we quantify over
-
- -- Now we are back to normal (c.f. tcSimplCheck)
- ; implic_bind <- bindIrreds loc [] emptyRefinement
- qtvs givens irreds
- ; return (qtvs, binds `unionBags` implic_bind) }
-\end{code}
-
%************************************************************************
%* *
-> [Inst] -- Wanted
-> TcM TcDictBinds
tcSimplifySuperClasses loc givens sc_wanteds
- = do { (binds1, irreds) <- checkLoop env sc_wanteds
+ = do { (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}
-> [Name] -- Things bound in this group
-> TcTyVarSet -- Free in the type of the RHSs
-> [Inst] -- Free in the RHSs
- -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
+ -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified)
TcDictBinds) -- Bindings
-- tcSimpifyRestricted returns no constraints to
-- quantify over; by definition there are none.
tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
-- Zonk everything in sight
- = mappM zonkInst wanteds `thenM` \ wanteds' ->
+ = do { wanteds' <- mappM zonkInst 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)
- in
- reduceContext env wanteds' `thenM` \ (_imp, _binds, constrained_dicts) ->
+ ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
+ ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
-- Next, figure out the tyvars we will quantify over
- zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
- tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
- mappM zonkInst constrained_dicts `thenM` \ constrained_dicts' ->
- let
- constrained_tvs' = tyVarsOfInsts constrained_dicts'
- qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
- `minusVarSet` constrained_tvs'
- in
- traceTc (text "tcSimplifyRestricted" <+> vcat [
+ ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+ ; gbl_tvs' <- tcGetGlobalTyVars
+ ; constrained_dicts' <- mappM zonkInst constrained_dicts
+
+ ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
+ -- As in tcSimplifyInfer
+
+ -- Do not quantify over constrained type variables:
+ -- this is the monomorphism restriction
+ constrained_tvs' = tyVarsOfInsts constrained_dicts'
+ qtvs = qtvs1 `minusVarSet` constrained_tvs'
+ pp_bndrs = pprWithCommas (quotes . ppr) bndrs
+
+ -- 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])
+
+ ; traceTc (text "tcSimplifyRestricted" <+> vcat [
pprInsts wanteds, pprInsts constrained_dicts',
ppr _binds,
- ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) `thenM_`
+ ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
-- The first step may have squashed more methods than
-- necessary, so try again, this time more gently, knowing the exact
--
-- At top level, we *do* squash methods becuase we want to
-- expose implicit parameters to the test that follows
- let
- is_nested_group = isNotTopLevel top_lvl
- try_me inst | isFreeWrtTyVars qtvs inst,
- (is_nested_group || isDict inst) = Stop
- | otherwise = ReduceMe AddSCs
- env = mkNoImproveRedEnv doc try_me
- in
- reduceContext env wanteds' `thenM` \ (_imp, binds, irreds) ->
- ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
+ ; let is_nested_group = isNotTopLevel top_lvl
+ try_me inst | isFreeWrtTyVars qtvs inst,
+ (is_nested_group || isDict inst) = Stop
+ | otherwise = ReduceMe AddSCs
+ env = mkNoImproveRedEnv doc try_me
+ ; (_imp, binds, irreds) <- reduceContext env wanteds'
-- See "Notes on implicit parameters, Question 4: top level"
- if is_nested_group then
- extendLIEs irreds `thenM_`
- returnM (varSetElems qtvs, binds)
- else
- let
- (non_ips, bad_ips) = partition isClassDict irreds
- in
- addTopIPErrs bndrs bad_ips `thenM_`
- extendLIEs non_ips `thenM_`
- returnM (varSetElems qtvs, binds)
+ ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
+ if is_nested_group then
+ extendLIEs irreds
+ else do { let (bad_ips, non_ips) = partition isIPDict irreds
+ ; addTopIPErrs bndrs bad_ips
+ ; extendLIEs non_ips }
+
+ ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
+ ; return (qtvs', binds) }
\end{code}
-- 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 (addBind binds (instToId 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"
returnM emptyLHsBinds
| otherwise
- = do { (binds, irreds) <- checkLoop env for_me
+ = do { (irreds, binds) <- checkLoop env for_me
; extendLIEs not_for_me
; extendLIEs irreds
; return binds }
; init_state <- foldlM addGiven emptyAvails (red_givens env)
-- Do the real work
- ; avails <- reduceList env wanteds init_state
+ -- 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
text "----",
text "avails" <+> pprAvails avails,
text "improved =" <+> ppr improved,
+ text "irreds = " <+> ppr irreds,
text "----------------------"
]))
, red_try_me = try_me }
; traceTc (text "reduceImplication" <+> vcat
- [ ppr (red_givens env), ppr extra_givens, ppr reft, ppr wanteds ])
+ [ ppr orig_avails,
+ ppr (red_givens env), ppr extra_givens,
+ ppr reft, ppr wanteds, ppr avails ])
; avails <- reduceList env' wanteds avails
- -- Extract the binding (no frees, because try_me never says Free)
+ -- Extract the results
+ -- Note [Reducing implication constraints]
; (binds, irreds) <- extractResults avails wanteds
-
+ ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds
+
+ ; traceTc (text "reduceImplication result" <+> vcat
+ [ ppr outer, ppr inner, ppr binds])
+
-- We always discard the extra avails we've generated;
-- but we remember if we have done any (global) improvement
; let ret_avails = updateImprovement orig_avails avails
- ; if isEmptyLHsBinds binds then -- No progress
+ ; if isEmptyLHsBinds binds && null outer then -- No progress
return (ret_avails, NoInstance)
else do
- { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
- -- 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.
+ { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens inner
; let dict_ids = map instToId extra_givens
co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
rhs = mkHsWrap co payload
loc = instLocSpan inst_loc
- payload | isSingleton wanteds = HsVar (instToId (head wanteds))
+ payload | [wanted] <- wanteds = HsVar (instToId wanted)
| otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
- -- If there are any irreds, we back off and return NoInstance
- ; return (ret_avails, GenInst implic_insts (L loc rhs))
+ ; return (ret_avails, GenInst (implic_insts ++ outer) (L loc rhs))
} }
\end{code}
+Note [Reducing implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are trying to simplify
+ (Ord a, forall b. C a b => (W [a] b, D c b))
+where
+ instance (C a b, Ord a) => W [a] b
+When solving the implication constraint, we'll start with
+ Ord a -> Irred
+in the Avails. Then we add (C a b -> Given) and solve. Extracting
+the results gives us a binding for the (W [a] b), with an Irred of
+(Ord a, D c b). Now, the (Ord a) comes from "outside" the implication,
+but the (D d b) is from "inside". So we want to generate a Rhs binding
+like this
+
+ ic = /\b \dc:C a b). (df a b dc do, ic' b dc)
+ depending on
+ do :: Ord a
+ ic' :: forall b. C a b => D c b
+
+The 'depending on' part of the Rhs is important, because it drives
+the extractResults code.
+
+The "inside" and "outside" distinction is what's going on with 'inner' and
+'outer' in reduceImplication
+
+
Note [Freeness and implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's hard to say when an implication constraint can be floated out. Consider
to float the (C Int) out, even though it mentions no type variable in
the constraints!
+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.
+
+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
+advantage of that at the moment.
+
+If you do, BE CAREFUL of wobbly type variables.
+
+
%************************************************************************
%* *
Avails and AvailHow: the pool of evidence
type AvailEnv = FiniteMap Inst AvailHow
data AvailHow
- = IsIrred -- Used for irreducible dictionaries,
+ = IsIrred -- Used for irreducible dictionaries,
-- which are going to be lambda bound
| Given TcId -- Used for dictionaries for which we have a binding
pprAvail :: AvailHow -> SDoc
pprAvail IsIrred = text "Irred"
pprAvail (Given x) = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Rhs rhs bs) = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
-------------------------
extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
go avails binds irreds (w:ws)
= 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
+ Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+ go avails binds irreds ws
Just (Given id)
- | id == instToId w
- -> go avails binds irreds ws
+ | 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!
- | otherwise
- -> go avails (addBind binds w (nlHsVar id)) irreds ws
+ Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
+ -- The add_given handles the case where we want (Ord a, Eq a), and we
+ -- don't want to emit *two* Irreds for Ord a, one via the superclass chain
+ -- This showed up in a dupliated Ord constraint in the error message for
+ -- test tcfail043
Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
- where
- new_binds = addBind binds w rhs
- where
- w_span = instSpan w
- w_id = instToId w
+ where
+ new_binds = addBind binds w_id rhs
+ where
+ w_id = instToId w
add_given avails w = extendAvailEnv avails w (Given (instToId w))
+ -- Don't add the same binding twice
-addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst)
- (VarBind (instToId inst) rhs))
+addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs))
\end{code}
addRefinedGiven reft (refined_givens, avails) given
| isDict given -- We sometimes have 'given' methods, but they
-- are always optional, so we can drop them
- , Just (co, pred) <- refinePred reft (dictPred given)
+ , 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))
-- 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
-- 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 <- mapM zonkInst wanteds
; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
- ; (binds1, irreds1) <- topCheckLoop doc wanteds
+ ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
+ ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
- ; 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
- ; extended_default <- if interactive then return True
- else doptM Opt_ExtendedDefaultRules
- ; disambiguate extended_default irreds1 -- Does unification
- ; (binds2, irreds2) <- 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 -> [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 extended_defaulting insts
+disambiguate doc interactive dflags insts
+ | null insts
+ = return (insts, emptyBag)
+
| null defaultable_groups
- = return ()
+ = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ ; return (insts, emptyBag) }
+
| otherwise
= do { -- Figure out what default types to use
- mb_defaults <- getDefaultTys
- ; default_tys <- case mb_defaults of
- Just tys -> return tys
- Nothing -> -- No use-supplied default;
- -- use [Integer, Double]
- do { integer_ty <- tcMetaTy integerTyConName
- ; checkWiredInTyCon doubleTyCon
- ; return [integer_ty, doubleTy] }
- ; mapM_ (disambigGroup default_tys) defaultable_groups }
+ 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 }
+
where
- unaries :: [(Inst,Class, TcTyVar)] -- (C tv) constraints
- bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
- (unaries, bad_tvs) = getDefaultableDicts insts
+ 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_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)]]
defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
defaultable_group ds@((_,_,tv):_)
- = not (isSkolemTyVar tv) -- Note [Avoiding spurious errors]
+ = isTyConableTyVar tv -- Note [Avoiding spurious errors]
&& not (tv `elemVarSet` bad_tvs)
&& defaultable_classes [c | (_,c,_) <- ds]
defaultable_group [] = panic "defaultable_group"
defaultable_classes clss
| extended_defaulting = any isInteractiveClass clss
- | otherwise = all isStandardClass clss && any isNumericClass clss
+ | otherwise = all is_std_class clss && (any is_num_class clss)
-- In interactive mode, or with -fextended-default-rules,
-- we default Show a to Show () to avoid graututious errors on "show []"
isInteractiveClass cls
- = isNumericClass cls
- || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
+ = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
+
+ is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
+ -- is_num_class adds IsString to the standard numeric classes,
+ -- when -foverloaded-strings is enabled
+ 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
-- After this we can't fail
; warnDefault dicts default_ty
; unifyType default_ty (mkTyVarTy tyvar) }
+
+
+-----------------------
+getDefaultTys :: Bool -> Bool -> TcM [Type]
+getDefaultTys extended_deflts ovl_strings
+ = do { mb_defaults <- getDeclaredDefaultTys
+ ; case mb_defaults of {
+ Just tys -> return tys ; -- User-supplied defaults
+ Nothing -> do
+
+ -- No use-supplied default
+ -- Use [Integer, Double], plus modifications
+ { integer_ty <- tcMetaTy integerTyConName
+ ; checkWiredInTyCon doubleTyCon
+ ; string_ty <- tcMetaTy stringTyConName
+ ; return (opt_deflt extended_deflts unitTy
+ -- Note [Default unitTy]
+ ++
+ [integer_ty,doubleTy]
+ ++
+ opt_deflt ovl_strings string_ty) } } }
+ where
+ opt_deflt True ty = [ty]
+ opt_deflt False ty = []
\end{code}
+Note [Default unitTy]
+~~~~~~~~~~~~~~~~~~~~~
+In interative mode (or with -fextended-default-rules) 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"
+This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't
+want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to
+default the 'a' to (), rather than to Integer (which is what would otherwise happen;
+and then GHCi doesn't attempt to print the (). So in interactive mode, we add
+() to the list of defaulting types. See Trac #1200.
+
Note [Avoiding spurious errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When doing the unification for defaulting, we check for skolem
\begin{code}
tcSimplifyDeriv :: InstOrigin
- -> TyCon
-> [TyVar]
-> ThetaType -- Wanted
-> 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 tc tyvars theta
- = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
+tcSimplifyDeriv orig tyvars theta
+ = do { (tvs, _, tenv) <- tcInstTyVars tyvars
-- The main loop may do unification, and that may crash if
-- it doesn't see a TcTyVar, so we have to instantiate. Sigh
-- ToDo: what if two of them do get unified?
- newDictBndrsO orig (substTheta tenv theta) `thenM` \ wanteds ->
- topCheckLoop doc wanteds `thenM` \ (_, irreds) ->
-
- doptM Opt_GlasgowExts `thenM` \ gla_exts ->
- doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
- let
- inst_ty = mkTyConApp tc (mkTyVarTys tvs)
- (ok_insts, bad_insts) = partition is_ok_inst irreds
- is_ok_inst inst
- = isDict inst -- Exclude implication consraints
- && (isTyVarClassPred pred || (gla_exts && ok_gla_pred pred))
- where
- pred = dictPred inst
-
- ok_gla_pred pred = null (checkInstTermination [inst_ty] [pred])
- -- See Note [Deriving context]
-
- tv_set = mkVarSet tvs
- simpl_theta = map dictPred ok_insts
- weird_preds = [pred | pred <- simpl_theta
- , not (tyVarsOfPred pred `subVarSet` tv_set)]
-
- -- Check for a bizarre corner case, when the derived instance decl should
- -- have form instance C a b => D (T a) where ...
- -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
- -- of problems; in particular, it's hard to compare solutions for
- -- equality when finding the fixpoint. So I just rule it out for now.
-
- rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
- -- This reverse-mapping is a Royal Pain,
- -- but the result should mention TyVars not TcTyVars
- in
- -- In effect, the bad and wierd insts cover all of the cases that
- -- would make checkValidInstance fail; if it were called right after tcSimplifyDeriv
- -- * wierd_preds ensures unambiguous instances (checkAmbiguity in checkValidInstance)
- -- * ok_gla_pred ensures termination (checkInstTermination in checkValidInstance)
- addNoInstanceErrs bad_insts `thenM_`
- mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
- returnM (substTheta rev_env simpl_theta)
+ ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
+ ; (irreds, _) <- tryHardCheckLoop doc wanteds
+
+ ; let (tv_dicts, others) = partition isTyVarDict irreds
+ ; addNoInstanceErrs others
+
+ ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+ 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
+
+ ; return simpl_theta }
where
doc = ptext SLIT("deriving classes for a data type")
\end{code}
-Note [Deriving context]
-~~~~~~~~~~~~~~~~~~~~~~~
-With -fglasgow-exts, we allow things like (C Int a) in the simplified
-context for a derived instance declaration, because at a use of this
-instance, we might know that a=Bool, and have an instance for (C Int
-Bool)
+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.
-We nevertheless insist that each predicate meets the termination
-conditions. If not, the deriving mechanism generates larger and larger
-constraints. Example:
+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
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)).
-
@tcSimplifyDefault@ just checks class-type constraints, essentially;
tcSimplifyDefault theta
= newDictBndrsO DefaultOrigin theta `thenM` \ wanteds ->
- topCheckLoop doc wanteds `thenM` \ (_, irreds) ->
+ tryHardCheckLoop doc wanteds `thenM` \ (irreds, _) ->
addNoInstanceErrs irreds `thenM_`
if null irreds then
returnM ()
addTopIPErrs bndrs []
= return ()
addTopIPErrs bndrs ips
- = addErrTcM (tidy_env, mk_msg tidy_ips)
+ = do { dflags <- getDOpts
+ ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
where
(tidy_env, tidy_ips) = tidyInsts ips
- mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
- nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
+ 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 ()
(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 instances")])]
where
- ispecs = [ispec | (_, ispec) <- matches]
+ ispecs = [ispec | (ispec, _) <- matches]
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]
+
+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"),
+ 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 ->
quotes (ppr default_ty),
pprDictsInFull tidy_dicts]
--- Used for the ...Thetas variants; all top level
-badDerivedPred pred
- = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
- ptext SLIT("type variables that are not data type parameters"),
- nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
-
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"),
projects / ghc-hetmet.git / blobdiff