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
-----------------------------------------
-Choosing Q
-~~~~~~~~~~
+Note [Choosing which variables to quantify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here's a good way to choose Q:
Q = grow( fv(T), C ) \ oclose( fv(G), C )
:: 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
- -- Remove redundant superclasses from 'bound'
- -- The 'Stop' try_me result does not do so,
- -- see Note [No superclasses for Stop]
+ -- To make types simple, reduce as much as possible
+ ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$
+ ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
; let try_me inst = ReduceMe AddSCs
- ; (binds2, irreds) <- checkLoop (mkRedEnv doc try_me []) bound
+ red_env = mkRedEnv doc try_me []
+ ; (irreds1, binds1) <- checkLoop red_env bound
+
+ -- Note [Inference and implication constraints]
+ -- By putting extra_dicts first, we make them available
+ -- to solve the implication constraints
+ ; let extra_dicts = getImplicWanteds qtvs irreds1
+ ; (irreds2, binds2) <- if null extra_dicts
+ then return (irreds1, emptyBag)
+ else do { extra_dicts' <- mapM cloneDict extra_dicts
+ ; checkLoop red_env (extra_dicts' ++ 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
+
+ -- 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.
+
+getImplicWanteds :: TcTyVarSet -> [Inst] -> [Inst]
+-- See Note [Inference and implication constraints]
+-- Find the wanted constraints in implication constraints that mention the
+-- quantified type variables, and are not bound by forall's in the constraint itself
+-- Returns only Dicts
+getImplicWanteds qtvs implics
+ = concatMap get implics
+ where
+ get d@(Dict {}) | tyVarsOfInst d `intersectsVarSet` qtvs = [d]
+ | otherwise = []
+ get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+ = [ d | let tv_set = mkVarSet tvs
+ , d <- getImplicWanteds qtvs wanteds
+ , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
+\end{code}
+
+Note [Inference and implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We can't (or at least don't) abstract over implications. But we might
+have an implication constraint (perhaps arising from a nested pattern
+match) like
+ C a => D a
+when we are now trying to quantify over 'a'. Our best approximation
+is to make (D a) part of the inferred context, so we can use that to
+discharge the implication. Hence getImplicWanteds.
+
+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) <- 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
+
+ ; 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]
-> [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) <- innerCheckLoop 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) <- innerCheckLoop 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,
-----------------------------------------------------------
topCheckLoop :: SDoc
-> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
+ -> TcM ([Inst], TcDictBinds)
topCheckLoop doc wanteds
= checkLoop (mkRedEnv doc try_me []) wanteds
innerCheckLoop :: InstLoc
-> [Inst] -- Given
-> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
+ -> TcM ([Inst], TcDictBinds)
innerCheckLoop inst_loc givens wanteds
= checkLoop env wanteds
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
-----------------------------------------------------------
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
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 }
-> [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}
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 }
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 binding
; (binds, irreds) <- extractResults avails wanteds
+ ; traceTc (text "reduceImplication result" <+> vcat
+ [ ppr irreds, 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
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.
; 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
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 TcId -- 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 (IsIrred x) = text "Irred" <+> ppr x
pprAvail (Given x) = text "Given" <+> ppr x
pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
Nothing -> pprTrace "Urk: extractResults" (ppr w) $
go avails binds irreds ws
- Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
-
Just (Given id)
- | id == instToId w
- -> go avails binds irreds ws
+ | 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 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 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
+ addAvailAndSCs want_scs avails irred (IsIrred (instToId irred))
addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
addAvailAndSCs want_scs avails inst avail
= do { wanteds <- mapM zonkInst wanteds
; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
- ; (binds1, irreds1) <- topCheckLoop doc wanteds
+ ; (irreds1, binds1) <- topCheckLoop doc wanteds
; if null irreds1 then
return binds1
-- 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
+ ; dflags <- getDOpts
+ ; disambiguate interactive dflags irreds1 -- Does unification
+ -- hence try again
- -- Deal with implicit parameter
+ -- Deal with implicit parameters
+ ; (irreds2, binds2) <- topCheckLoop doc irreds1
; let (bad_ips, non_ips) = partition isIPDict irreds2
(ambigs, others) = partition isTyVarDict non_ips
@void@.
\begin{code}
-disambiguate :: Bool -> [Inst] -> TcM ()
+disambiguate :: Bool -> DynFlags -> [Inst] -> TcM ()
-- Just does unification to fix the default types
-- The Insts are assumed to be pre-zonked
-disambiguate extended_defaulting insts
+disambiguate interactive dflags insts
| null defaultable_groups
- = return ()
+ = do { traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ ; return () }
| 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] }
+ ; default_tys <- getDefaultTys extended_defaulting ovl_strings
+
+ ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
; mapM_ (disambigGroup default_tys) defaultable_groups }
where
+ extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
+ ovl_strings = dopt Opt_OverloadedStrings dflags
+
unaries :: [(Inst,Class, TcTyVar)] -- (C tv) constraints
bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
(unaries, bad_tvs) = getDefaultableDicts insts
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 = []
+
+-----------------------
+getDefaultableDicts :: [Inst] -> ([(Inst, Class, TcTyVar)], TcTyVarSet)
+-- Look for free dicts of the form (C tv), even inside implications
+-- *and* the set of tyvars mentioned by all *other* constaints
+-- This disgustingly ad-hoc function is solely to support defaulting
+getDefaultableDicts insts
+ = (concat ps, unionVarSets tvs)
+ where
+ (ps, tvs) = mapAndUnzip get insts
+ get d@(Dict {tci_pred = ClassP cls [ty]})
+ | Just tv <- tcGetTyVar_maybe ty = ([(d,cls,tv)], emptyVarSet)
+ | otherwise = ([], tyVarsOfType ty)
+ get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+ = ([ up | up@(_,_,tv) <- ups, not (tv `elemVarSet` tv_set)],
+ ftvs `minusVarSet` tv_set)
+ where
+ tv_set = mkVarSet tvs
+ (ups, ftvs) = getDefaultableDicts wanteds
+ get inst = ([], tyVarsOfInst inst)
\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, _) <- topCheckLoop doc wanteds
+
+ ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+ simpl_theta = substTheta rev_env (map dictPred irreds)
+ -- This reverse-mapping is a pain, but the result
+ -- should mention the original TyVars not TcTyVars
+
+ -- NB: the caller will further check the tv_dicts for
+ -- legal instance-declaration form
+
+ ; return simpl_theta }
where
doc = ptext SLIT("deriving classes for a data type")
\end{code}
-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)
-
-We nevertheless insist that each predicate meets 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)).
-
@tcSimplifyDefault@ just checks class-type constraints, essentially;
tcSimplifyDefault theta
= newDictBndrsO DefaultOrigin theta `thenM` \ wanteds ->
- topCheckLoop doc wanteds `thenM` \ (_, irreds) ->
+ topCheckLoop doc wanteds `thenM` \ (irreds, _) ->
addNoInstanceErrs irreds `thenM_`
if null irreds then
returnM ()
addTopIPErrs bndrs []
= return ()
addTopIPErrs bndrs ips
- = addErrTcM (tidy_env, mk_msg tidy_ips)
+ = do { dflags <- getDOpts
+ ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
where
(tidy_env, tidy_ips) = tidyInsts ips
- mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
- nest 2 (ptext SLIT("the monomorphic top-level binding")
+ mk_msg dflags ips
+ = vcat [sep [ptext SLIT("Implicit parameters escape from"),
+ nest 2 (ptext SLIT("the monomorphic top-level binding")
<> plural bndrs <+> ptext SLIT("of")
<+> pprBinders bndrs <> colon)],
- nest 2 (vcat (map ppr_ip ips)),
- monomorphism_fix]
+ nest 2 (vcat (map ppr_ip ips)),
+ monomorphism_fix dflags]
ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
topIPErrs :: [Inst] -> TcM ()
quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
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