X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=911e2ff12d8a7f6c4d7a86da0040bb0ce6d19dbd;hb=0560e796f1d813582e066a5f2bec2684c71df44d;hp=94772a6d3642c4a7d7cd9ad698cc98d1f8dd68e5;hpb=5adfdfb259415ca99d67d3c8b9e5df68cb736326;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 94772a6..911e2ff 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 -[NO TYVARS] + -- 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] +~~~~~~~~~~~~~~~~~~~~~~~~~ +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,26 +823,37 @@ 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 + -- 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 @@ -824,7 +863,8 @@ bindIrreds loc co_vars reft qtvs givens 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 } @@ -837,6 +877,8 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement -- 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 @@ -870,8 +912,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 +920,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 +964,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' + ; (improved, binds, irreds) <- reduceContext env wanteds' - ; ASSERT( null _frees ) - - 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 +1056,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 +1175,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 +1183,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 +1194,40 @@ 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') - `minusVarSet` constrained_tvs' - in - traceTc (text "tcSimplifyRestricted" <+> vcat [ - pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts', + ; 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 -- 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 +1239,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 +1392,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 +1406,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 +1452,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 +1467,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 +1525,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 +1546,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 +1565,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 +1574,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 +1651,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 +1721,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 +1835,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 +1893,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 +1923,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 +1946,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 +1994,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 +2060,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 +2073,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 +2199,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 @@ -2169,10 +2207,9 @@ tc_simplify_top doc interactive wanteds -- 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 + ; (irreds2, binds2) <- topCheckLoop doc irreds1 -- Deal with implicit parameter ; let (bad_ips, non_ips) = partition isIPDict irreds2 @@ -2219,24 +2256,23 @@ Since we're not using the result of @foo@, the result if (presumably) @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 @@ -2248,21 +2284,26 @@ disambiguate extended_defaulting 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) @@ -2287,8 +2328,43 @@ disambigGroup default_tys dicts -- After this we can't fail ; warnDefault dicts default_ty ; unifyType default_ty (mkTyVarTy tyvar) } + + +getDefaultTys :: Bool -> Bool -> TcM [Type] +getDefaultTys extended_deflts ovl_strings + = do { mb_defaults <- getDeclaredDefaultTys + ; case mb_defaults of { + Just tys -> return tys ; -- User-supplied defaults + Nothing -> do + + -- No use-supplied default + -- Use [Integer, Double], plus modifications + { integer_ty <- tcMetaTy integerTyConName + ; checkWiredInTyCon doubleTyCon + ; string_ty <- tcMetaTy stringTyConName + ; return (opt_deflt extended_deflts unitTy + -- Note [Default unitTy] + ++ + [integer_ty,doubleTy] + ++ + opt_deflt ovl_strings string_ty) } } } + where + opt_deflt True ty = [ty] + opt_deflt False ty = [] \end{code} +Note [Default unitTy] +~~~~~~~~~~~~~~~~~~~~~ +In interative mode (or with -fextended-default-rules) we add () as the first type we +try when defaulting. This has very little real impact, except in the following case. +Consider: + Text.Printf.printf "hello" +This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't +want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to +default the 'a' to (), rather than to Integer (which is what would otherwise happen; +and then GHCi doesn't attempt to print the (). So in interactive mode, we add +() to the list of defaulting types. See Trac #1200. + Note [Avoiding spurious errors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When doing the unification for defaulting, we check for skolem @@ -2321,78 +2397,34 @@ 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) - -- 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; @@ -2405,7 +2437,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 +2493,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 +2675,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"),