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
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
- = inferLoop doc (varSetElems tau_tvs)
- wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
-
- extendLIEs frees `thenM_`
- returnM (qtvs, binds, map instToId irreds)
-
-inferLoop doc tau_tvs wanteds
- = -- Step 1
- zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
- mappM zonkInst wanteds `thenM` \ wanteds' ->
- tcGetGlobalTyVars `thenM` \ gbl_tvs ->
- let
- preds = fdPredsOfInsts wanteds'
- qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
-
- try_me inst
- | isFreeWhenInferring qtvs inst = Free
- | isClassDict inst = Irred -- Dicts
- | otherwise = ReduceMe NoSCs -- Lits and Methods
- env = mkRedEnv doc try_me []
- in
- traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
- ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
- -- Step 2
- reduceContext env wanteds' `thenM` \ (improved, frees, binds, irreds) ->
-
- -- Step 3
- if not improved then
- returnM (varSetElems qtvs, frees, binds, irreds)
- else
- -- If improvement did some unification, we go round again. There
- -- are two subtleties:
- -- a) 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 example [LOOP]
- --
- -- b) It's also essential to re-process frees, because unification
- -- might mean that a type variable that looked free isn't now.
- --
- -- Hence the (irreds ++ frees)
-
- -- However, NOTICE that when we are done, we might have some bindings, but
- -- the final qtvs might be empty. See [NO TYVARS] below.
-
- inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
- returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
+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 wanted'
+ qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
+ (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
+ ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound))
+ ; extendLIEs free
+
+ -- To make types simple, reduce as much as possible
+ ; let try_me inst = ReduceMe AddSCs
+ ; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound
+
+ ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
+
+ -- We can't abstract over implications
+ ; let (dicts, implics) = partition isDict irreds
+ ; loc <- getInstLoc (ImplicOrigin doc)
+ ; implic_bind <- bindIrreds loc qtvs' dicts implics
+
+ ; return (qtvs', dicts, binds `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.
\end{code}
-Example [LOOP]
+\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
- class If b t e r | b t e -> r
- instance If T t e t
- instance If F t e e
- class Lte a b c | a b -> c where lte :: a -> b -> c
- instance Lte Z b T
- instance (Lte a b l,If l b a c) => Max a b c
+tcSimplifyInferCheck loc tau_tvs givens wanteds
+ = do { (irreds, binds) <- innerCheckLoop loc givens wanteds
-Wanted: Max Z (S x) y
+ -- 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
-Then we'll reduce using the Max instance to:
- (Lte Z (S x) l, If l (S x) Z y)
-and improve by binding l->T, after which we can do some reduction
-on both the Lte and If constraints. What we *can't* do is start again
-with (Max Z (S x) y)!
+ ; qtvs' <- zonkQuantifiedTyVars qtvs
+
+ -- Now we are back to normal (c.f. tcSimplCheck)
+ ; implic_bind <- bindIrreds loc qtvs' givens irreds
-[NO TYVARS]
+ ; return (qtvs', binds `unionBags` implic_bind) }
+\end{code}
+Note [Squashing methods]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Be careful if you want to float methods more:
+ truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
+From an application (truncate f i) we get
+ t1 = truncate at f
+ t2 = t1 at i
+If we have also have a second occurrence of truncate, we get
+ t3 = truncate at f
+ t4 = t3 at i
+When simplifying with i,f free, we might still notice that
+t1=t3; but alas, the binding for t2 (which mentions t1)
+may continue to float out!
+
+
+Note [NO TYVARS]
+~~~~~~~~~~~~~~~~~
class Y a b | a -> b where
y :: a -> X b
\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 AddSCs 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 AddSCs 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
-- partition the 'wanteds' by their qtvs, thereby trimming irreds
-----------------------------------------------------------
topCheckLoop :: SDoc
-> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
+ -> TcM ([Inst], TcDictBinds)
topCheckLoop doc wanteds
= checkLoop (mkRedEnv doc try_me []) wanteds
try_me inst = ReduceMe AddSCs
-----------------------------------------------------------
-innerCheckLoop :: InstLoc -> WantSCs
+innerCheckLoop :: InstLoc
-> [Inst] -- Given
-> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
+ -> TcM ([Inst], TcDictBinds)
-innerCheckLoop inst_loc want_scs givens wanteds
+innerCheckLoop inst_loc givens wanteds
= checkLoop env wanteds
where
env = mkRedEnv (pprInstLoc inst_loc) try_me givens
- try_me inst | isMethodOrLit inst = ReduceMe want_scs
- | otherwise = Irred
+ try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ | otherwise = Stop
-- When checking against a given signature
-- we MUST be very gentle: Note [Check gently]
\end{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
checkLoop env wanteds
= do { -- Givens are skolems, so no need to zonk them
wanteds' <- mappM zonkInst wanteds
- ; (improved, _frees, binds, irreds) <- reduceContext env wanteds'
-
- ; ASSERT( null _frees )
+ ; (improved, binds, irreds) <- reduceContext env wanteds'
- if not improved then
- return (binds, irreds)
+ ; if not improved then
+ return (irreds, binds)
else do
- { (binds1, irreds1) <- checkLoop env irreds
- ; return (binds `unionBags` binds1, irreds1) } }
+ -- 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]
+~~~~~~~~~~~
+ class If b t e r | b t e -> r
+ instance If T t e t
+ instance If F t e e
+ class Lte a b c | a b -> c where lte :: a -> b -> c
+ instance Lte Z b T
+ instance (Lte a b l,If l b a c) => Max a b c
-\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 AddSCs givens wanteds
+Wanted: Max Z (S x) y
- -- 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
+Then we'll reduce using the Max instance to:
+ (Lte Z (S x) l, If l (S x) Z y)
+and improve by binding l->T, after which we can do some reduction
+on both the Lte and If constraints. What we *can't* do is start again
+with (Max Z (S x) y)!
- -- 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, _frees, _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')
+ ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+ ; gbl_tvs' <- tcGetGlobalTyVars
+ ; constrained_dicts' <- mappM zonkInst 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 [
- pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts',
+ ; 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
-- set of type variables to quantify over.
--
- -- We quantify only over constraints that are captured by qtvs';
+ -- We quantify only over constraints that are captured by qtvs;
-- these will just be a subset of non-dicts. This in contrast
-- to normal inference (using isFreeWhenInferring) in which we quantify over
-- all *non-inheritable* constraints too. This implements choice
--
-- 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) = Free
- | otherwise = ReduceMe AddSCs
- env = mkNoImproveRedEnv doc try_me
- in
- reduceContext env wanteds' `thenM` \ (_imp, frees, binds, irreds) ->
- ASSERT( null irreds )
+ ; 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 frees `thenM_`
- returnM (varSetElems qtvs', binds)
- else
- let
- (non_ips, bad_ips) = partition isClassDict frees
- 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}
-- Unusually for checking, we *must* zonk the given_ips
; let env = mkRedEnv doc try_me given_ips'
- ; (improved, _frees, binds, irreds) <- reduceContext env wanteds'
+ ; (improved, binds, irreds) <- reduceContext env wanteds'
; if not improved then
ASSERT( all is_free irreds )
is_free inst = isFreeWrtIPs ip_set inst
-- Simplify any methods that mention the implicit parameter
- try_me inst | is_free inst = Irred
+ try_me inst | is_free inst = Stop
| otherwise = ReduceMe NoSCs
\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 }
-- so it's worth building a set, so that
-- lookup (in isMethodFor) is faster
try_me inst | isMethod inst = ReduceMe NoSCs
- | otherwise = Irred
+ | otherwise = Stop
\end{code}
-- message of any kind.
-- It might be quite legitimate such as (Eq a)!
- | Irred -- Return as irreducible unless it can
+ | Stop -- Return as irreducible unless it can
-- be reduced to a constant in one step
-
- | Free -- Return as free
+ -- Do not add superclasses; see
data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
-- of a predicate when adding it to the avails
reduceContext :: RedEnv
-> [Inst] -- Wanted
-> TcM (ImprovementDone,
- [Inst], -- Free
TcDictBinds, -- Dictionary bindings
[Inst]) -- Irreducible
; avails <- reduceList env wanteds init_state
; let improved = availsImproved avails
- ; (binds, irreds, frees) <- extractResults avails wanteds
+ ; (binds, irreds) <- extractResults avails wanteds
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
text "wanted" <+> ppr wanteds,
text "----",
text "avails" <+> pprAvails avails,
- text "frees" <+> ppr frees,
text "improved =" <+> ppr improved,
text "----------------------"
]))
- ; return (improved, frees, binds, irreds) }
+ ; return (improved, binds, irreds) }
tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
tcImproveOne avails inst
| otherwise
= case red_try_me env wanted of {
- Free -> try_simple addFree -- It's free so just chuck it upstairs
- ; Irred -> try_simple (addIrred AddSCs) -- Assume want superclasses
+ ; 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) ->
in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
becuase it lost legitimate superclass sharing, and it still didn't do the job:
I found a very obscure program (now tcrun021) in which improvement meant the
-simplifier got two bites a the cherry... so something seemed to be an Irred
+simplifier got two bites a the cherry... so something seemed to be an Stop
first time, but reducible next time.
Now we implement the Right Solution, which is to check for loops directly
, 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)
- ; (binds, irreds, _frees) <- extractResults avails wanteds
+ -- Extract the binding
+ ; (binds, irreds) <- extractResults avails wanteds
-- We always discard the extra avails we've generated;
-- but we remember if we have done any (global) improvement
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
- = IsFree -- Used for free Insts
- | 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 IsFree = text "Free"
pprAvail IsIrred = text "Irred"
pprAvail (Given x) = text "Given" <+> ppr x
pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
extractResults :: Avails
-> [Inst] -- Wanted
-> TcM ( TcDictBinds, -- Bindings
- [Inst], -- Irreducible ones
- [Inst]) -- Free ones
+ [Inst]) -- Irreducible ones
extractResults (Avails _ avails) wanteds
- = go avails emptyBag [] [] wanteds
+ = go avails emptyBag [] wanteds
where
- go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] -> [Inst]
- -> TcM (TcDictBinds, [Inst], [Inst])
- go avails binds irreds frees []
- = returnM (binds, irreds, frees)
+ go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
+ -> TcM (TcDictBinds, [Inst])
+ go avails binds irreds []
+ = returnM (binds, irreds)
- go avails binds irreds frees (w:ws)
+ go avails binds irreds (w:ws)
= case findAvailEnv avails w of
Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds frees ws
+ go avails binds irreds ws
- Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
- Just IsIrred -> go (add_given avails w) binds (w:irreds) frees ws
+ Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
- Just (Given id) -> go avails new_binds irreds frees ws
- where
- new_binds | id == instToId w = binds
- | otherwise = addBind binds w (L (instSpan w) (HsVar id))
+ Just (Given id)
+ | id == instToId w
+ -> go avails binds irreds ws
-- The sought Id can be one of the givens, via a superclass chain
-- and then we definitely don't want to generate an x=x binding!
- Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
+ | otherwise
+ -> go avails (addBind binds w (nlHsVar id)) irreds ws
+
+ Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
where
new_binds = addBind binds w rhs
add_given avails w = extendAvailEnv avails w (Given (instToId w))
- add_free avails w | isMethod w = avails
- | otherwise = add_given avails w
- -- NB: Hack alert!
- -- Do *not* replace Free by Given if it's a method.
- -- The following situation shows why this is bad:
- -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
- -- From an application (truncate f i) we get
- -- t1 = truncate at f
- -- t2 = t1 at i
- -- If we have also have a second occurrence of truncate, we get
- -- t3 = truncate at f
- -- t4 = t3 at i
- -- When simplifying with i,f free, we might still notice that
- -- t1=t3; but alas, the binding for t2 (which mentions t1)
- -- will continue to float out!
-
-addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst)
+addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst)
(VarBind (instToId inst) rhs))
-instSpan wanted = instLocSpan (instLoc wanted)
\end{code}
-\begin{code}
--------------------------
-addFree :: Avails -> Inst -> TcM Avails
- -- When an Inst is tossed upstairs as 'free' we nevertheless add it
- -- to avails, so that any other equal Insts will be commoned up right
- -- here rather than also being tossed upstairs. This is really just
- -- an optimisation, and perhaps it is more trouble that it is worth,
- -- as the following comments show!
- --
- -- NB: do *not* add superclasses. If we have
- -- df::Floating a
- -- dn::Num a
- -- but a is not bound here, then we *don't* want to derive
- -- dn from df here lest we lose sharing.
- --
-addFree avails free = extendAvails avails free IsFree
+Note [No superclasses for Stop]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
+add it to avails, so that any other equal Insts will be commoned up
+right here. However, we do *not* add superclasses. If we have
+ df::Floating a
+ dn::Num a
+but a is not bound here, then we *don't* want to derive dn from df
+here lest we lose sharing.
+\begin{code}
addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
addWanted want_scs avails wanted rhs_expr wanteds
= addAvailAndSCs want_scs avails wanted avail
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
= 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
; extended_default <- if interactive then return True
else doptM Opt_ExtendedDefaultRules
; disambiguate extended_default irreds1 -- Does unification
- ; (binds2, irreds2) <- topCheckLoop doc irreds1
+ ; (irreds2, binds2) <- topCheckLoop doc irreds1
-- Deal with implicit parameter
; let (bad_ips, non_ips) = partition isIPDict irreds2
-- The Insts are assumed to be pre-zonked
disambiguate extended_defaulting 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
do { integer_ty <- tcMetaTy integerTyConName
; checkWiredInTyCon doubleTyCon
; return [integer_ty, doubleTy] }
+ ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
; mapM_ (disambigGroup default_tys) defaultable_groups }
where
unaries :: [(Inst,Class, TcTyVar)] -- (C tv) constraints
defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
defaultable_group ds@((_,_,tv):_)
- = not (isSkolemTyVar tv) -- Note [Avoiding spurious errors]
+ = not (isImmutableTyVar tv) -- Note [Avoiding spurious errors]
&& not (tv `elemVarSet` bad_tvs)
&& defaultable_classes [c | (_,c,_) <- ds]
defaultable_group [] = panic "defaultable_group"
\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)
+ ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
+ ; (irreds, _) <- topCheckLoop doc wanteds
+
+ ; let (dicts, non_dicts) = partition isDict irreds
+ -- Exclude implication consraints
+ ; addNoInstanceErrs non_dicts -- I'm not sure if these can really happen
+
+ ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+ simpl_theta = substTheta rev_env (map dictPred dicts)
-- 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)
+
+ ; return simpl_theta }
where
doc = ptext SLIT("deriving classes for a data type")
\end{code}
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 ()
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")
+ 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]
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