X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=342114b9fbb04e3ab9316409ecab54c8bec2d0fb;hp=94772a6d3642c4a7d7cd9ad698cc98d1f8dd68e5;hb=84923cc7de2a93c22a2f72daf9ac863959efae13;hpb=5adfdfb259415ca99d67d3c8b9e5df68cb736326 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 94772a6..342114b 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -15,7 +15,7 @@ module TcSimplify ( tcSimplifyBracket, tcSimplifyCheckPat, tcSimplifyDeriv, tcSimplifyDefault, - bindInstsOfLocalFuns + bindInstsOfLocalFuns, bindIrreds, ) where #include "HsVersions.h" @@ -28,11 +28,10 @@ import Inst import TcEnv import InstEnv import TcGadt -import TcMType import TcType +import TcMType import TcIface import Var -import TyCon import Name import NameSet import Class @@ -398,8 +397,8 @@ When m is later unified with [], we can solve both constraints. Notes on implicit parameters -------------------------------------- -Question 1: can we "inherit" implicit parameters -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Inheriting implicit parameters] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: f x = (x::Int) + ?y @@ -424,6 +423,21 @@ BOTTOM LINE: when *inferring types* you *must* quantify 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 @@ -642,83 +656,98 @@ tcSimplifyInfer :: 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 @@ -743,9 +772,9 @@ The net effect of [NO TYVARS] \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 @@ -780,10 +809,9 @@ tcSimplifyCheck :: InstLoc -> [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) } ----------------------------------------------------------- @@ -795,21 +823,31 @@ tcSimplifyCheckPat :: InstLoc -> [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 @@ -870,8 +908,7 @@ makeImplicationBind loc all_tvs reft ----------------------------------------------------------- topCheckLoop :: SDoc -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible + -> TcM ([Inst], TcDictBinds) topCheckLoop doc wanteds = checkLoop (mkRedEnv doc try_me []) wanteds @@ -879,19 +916,18 @@ topCheckLoop doc 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} @@ -924,66 +960,45 @@ with topCheckLooop. ----------------------------------------------------------- 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} %************************************************************************ @@ -1037,7 +1052,7 @@ tcSimplifySuperClasses -> [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 } @@ -1156,7 +1171,7 @@ tcSimplifyRestricted -- Used for restricted binding groups -> [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. @@ -1164,7 +1179,7 @@ tcSimplifyRestricted -- Used for restricted binding groups 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 @@ -1175,29 +1190,27 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- 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 @@ -1209,27 +1222,23 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- -- 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} @@ -1366,7 +1375,7 @@ tcSimplifyIPs given_ips wanteds -- 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 ) @@ -1380,7 +1389,7 @@ tcSimplifyIPs given_ips wanteds 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} @@ -1426,7 +1435,7 @@ bindInstsOfLocalFuns wanteds local_ids 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 } @@ -1441,7 +1450,7 @@ bindInstsOfLocalFuns wanteds local_ids -- 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} @@ -1499,10 +1508,9 @@ data WhatToDo -- 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 @@ -1521,7 +1529,6 @@ data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses reduceContext :: RedEnv -> [Inst] -- Wanted -> TcM (ImprovementDone, - [Inst], -- Free TcDictBinds, -- Dictionary bindings [Inst]) -- Irreducible @@ -1541,7 +1548,7 @@ reduceContext env wanteds ; 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 "----------------------", @@ -1550,12 +1557,11 @@ reduceContext env wanteds 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 @@ -1628,8 +1634,7 @@ reduce env wanted avails | 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) -> @@ -1699,7 +1704,7 @@ At first I had a gross hack, whereby I simply did not add superclass constraints 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 @@ -1813,11 +1818,13 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc , 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 @@ -1869,6 +1876,20 @@ We can satisfy the (C Int) from the superclass of D, so we don't want 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 @@ -1885,8 +1906,7 @@ type ImprovementDone = Bool -- True <=> some unification has happened 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 @@ -1909,7 +1929,6 @@ instance Outputable AvailHow where ------------------------- 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) @@ -1958,77 +1977,54 @@ dependency analyser can sort them out later 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 @@ -2047,7 +2043,9 @@ addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails addRefinedGiven reft (refined_givens, avails) given | isDict given -- We sometimes have 'given' methods, but they -- are always optional, so we can drop them - , 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)) @@ -2058,7 +2056,30 @@ addRefinedGiven reft (refined_givens, avails) 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 -> )... + +From the case (where x::T ty) we'll get an implication constraint + forall b. (Eq ty, Ord b) => +Now suppose itself has an implication constraint +of form + forall c. => +Then, we can certainly apply the refinement 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 @@ -2161,7 +2182,7 @@ tc_simplify_top doc interactive wanteds = 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 @@ -2172,7 +2193,7 @@ tc_simplify_top doc interactive wanteds ; 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 @@ -2224,7 +2245,8 @@ disambiguate :: Bool -> [Inst] -> TcM () -- 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 @@ -2235,6 +2257,7 @@ disambiguate extended_defaulting insts 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 @@ -2248,7 +2271,7 @@ disambiguate extended_defaulting insts 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" @@ -2321,55 +2344,31 @@ instance declarations. \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} @@ -2405,7 +2404,7 @@ tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it 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 () @@ -2461,7 +2460,8 @@ addTopIPErrs bndrs 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") + 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] @@ -2642,12 +2642,6 @@ warnDefault ups default_ty 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"),