X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=adf0f780884c72a9c64caa1240ea2ed136ef7871;hb=ab241c5d6187a93acffc609bdbffdae30ff9b284;hp=23d0b23a07017d46a42ea3ca59ef724fdd9041a6;hpb=f4510d27c5883fe7e8570f4dd49d45a8b0122f2c;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 23d0b23..adf0f78 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 @@ -210,8 +209,8 @@ Notice that ----------------------------------------- -Choosing Q -~~~~~~~~~~ +Note [Choosing which variables to quantify] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Here's a good way to choose Q: Q = grow( fv(T), C ) \ oclose( fv(G), C ) @@ -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,160 @@ 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 + -- See Note [Choosing which variables to quantify] + + -- To maximise sharing, remove from consideration any + -- constraints that don't mention qtvs at all + ; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted' + ; extendLIEs free1 + + -- To make types simple, reduce as much as possible + ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ + ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound)) + ; let try_me inst = ReduceMe AddSCs + red_env = mkRedEnv doc try_me [] + ; (irreds1, binds1) <- checkLoop red_env bound + + -- Note [Inference and implication constraints] + -- By putting extra_dicts first, we make them available + -- to solve the implication constraints + ; let extra_dicts = getImplicWanteds qtvs irreds1 + ; (irreds2, binds2) <- if null extra_dicts + then return (irreds1, emptyBag) + else do { extra_dicts' <- mapM cloneDict extra_dicts + ; checkLoop red_env (extra_dicts' ++ irreds1) } + + -- By now improvment may have taken place, and we must *not* + -- quantify over any variable free in the environment + -- tc137 (function h inside g) is an example + ; gbl_tvs <- tcGetGlobalTyVars + ; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs) + ; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs)) + + -- Do not quantify over constraints that *now* do not + -- mention quantified type variables, because they are + -- simply ambiguous (or might be bound further out). Example: + -- f :: Eq b => a -> (a, b) + -- g x = fst (f x) + -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta) + -- We decide to quantify over 'alpha' alone, but free1 does not include f77 + -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous) + -- constraint (Eq beta), which we dump back into the free set + -- See test tcfail181 + ; let (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2 + ; extendLIEs free3 + + -- We can't abstract over any remaining unsolved + -- implications so instead just float them outwards. Ugh. + ; let (q_dicts, implics) = partition isDict irreds3 + ; loc <- getInstLoc (ImplicOrigin doc) + ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics + + ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) } + -- NB: when we are done, we might have some bindings, but + -- the final qtvs might be empty. See Note [NO TYVARS] below. + +getImplicWanteds :: TcTyVarSet -> [Inst] -> [Inst] +-- See Note [Inference and implication constraints] +-- Find the wanted constraints in implication constraints that mention the +-- quantified type variables, and are not bound by forall's in the constraint itself +-- Returns only Dicts +getImplicWanteds qtvs implics + = concatMap get implics + where + get d@(Dict {}) | tyVarsOfInst d `intersectsVarSet` qtvs = [d] + | otherwise = [] + get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds}) + = [ d | let tv_set = mkVarSet tvs + , d <- getImplicWanteds qtvs wanteds + , not (tyVarsOfInst d `intersectsVarSet` tv_set)] \end{code} -Example [LOOP] +Note [Inference and implication constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We can't (or at least don't) abstract over implications. But we might +have an implication constraint (perhaps arising from a nested pattern +match) like + C a => D a +when we are now trying to quantify over 'a'. Our best approximation +is to make (D a) part of the inferred context, so we can use that to +discharge the implication. Hence getImplicWanteds. - 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 +See Trac #1430 and test tc228. -Wanted: Max Z (S x) y -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)! +\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 -[NO TYVARS] +tcSimplifyInferCheck loc tau_tvs givens wanteds + = do { (irreds, binds) <- innerCheckLoop loc givens wanteds + -- Figure out which type variables to quantify over + -- You might think it should just be the signature tyvars, + -- but in bizarre cases you can get extra ones + -- f :: forall a. Num a => a -> a + -- f x = fst (g (x, head [])) + 1 + -- g a b = (b,a) + -- Here we infer g :: forall a b. a -> b -> (b,a) + -- We don't want g to be monomorphic in b just because + -- f isn't quantified over b. + ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens) + ; all_tvs <- zonkTcTyVarsAndFV all_tvs + ; gbl_tvs <- tcGetGlobalTyVars + ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs) + -- We could close gbl_tvs, but its not necessary for + -- soundness, and it'll only affect which tyvars, not which + -- dictionaries, we quantify over + + ; qtvs' <- zonkQuantifiedTyVars qtvs + + -- Now we are back to normal (c.f. tcSimplCheck) + ; implic_bind <- bindIrreds loc qtvs' givens irreds + + ; return (qtvs', binds `unionBags` implic_bind) } +\end{code} + +Note [Squashing methods] +~~~~~~~~~~~~~~~~~~~~~~~~~ +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 +834,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 +871,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 <- makeImplicationBind 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,53 +885,76 @@ 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 <- makeImplicationBind 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) } ----------------------------------------------------------- -makeImplicationBind :: 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 -makeImplicationBind 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' - then do - { let qtv_set = mkVarSet qtvs - (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds - ; extendLIEs frees - ; return real_irreds } - else - return irreds - - -- If there are no irreds, we are done! - ; if null irreds then - return emptyBag - else do + ; irreds' <- if null givens' && isEmptyRefinement reft + then do + { let qtv_set = mkVarSet qtvs + (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds + ; extendLIEs frees + ; return real_irreds } + else return 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 + -- If irreds' is empty, it does something sensible + ; extendLIEs implics + ; return bind } - -- Otherwise we must generate a binding - -- The binding looks like - -- (ir1, .., irn) = f qtvs givens - -- where f is (evidence for) the new implication constraint - -- - -- This binding must line up the 'rhs' in reduceImplication - { uniq <- newUnique +makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement + -> [Inst] -> [Inst] + -> TcM ([Inst], TcDictBinds) +-- Make a binding that binds 'irreds', by generating an implication +-- constraint for them, *and* throwing the constraint into the LIE +-- 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 + givens -- Guaranteed all Dicts + irreds + | null irreds -- If there are no irreds, we are done + = return ([], emptyBag) + | otherwise -- Otherwise we must generate a binding + = do { uniq <- newUnique ; span <- getSrcSpanM - ; let all_tvs = qtvs ++ co_vars -- Abstract over all these - name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span) + ; let name = mkInternalName uniq (mkVarOcc "ic") span implic_inst = ImplicInst { tci_name = name, tci_reft = reft, tci_tyvars = all_tvs, - tci_given = givens', + tci_given = givens, tci_wanted = irreds, tci_loc = loc } ; let n_irreds = length irreds @@ -849,22 +962,19 @@ makeImplicationBind loc co_vars reft qtvs givens irreds tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids) pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty rhs = L span (mkHsWrap co (HsVar (instToId implic_inst))) - co = mkWpApps (map instToId givens') <.> mkWpTyApps (mkTyVarTys all_tvs) + co = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs) bind | n_irreds==1 = VarBind (head irred_ids) rhs | otherwise = PatBind { pat_lhs = L span pat, pat_rhs = unguardedGRHSs rhs, pat_rhs_ty = tup_ty, bind_fvs = placeHolderNames } ; -- pprTrace "Make implic inst" (ppr implic_inst) $ - extendLIE implic_inst - ; return (unitBag (L span bind)) }} - + return ([implic_inst], unitBag (L span bind)) } ----------------------------------------------------------- topCheckLoop :: SDoc -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible + -> TcM ([Inst], TcDictBinds) topCheckLoop doc wanteds = checkLoop (mkRedEnv doc try_me []) wanteds @@ -872,19 +982,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} @@ -904,7 +1013,7 @@ Inside the pattern match, which binds (a:*, x:a), we know that Hence we have a dictionary for Show [a] available; and indeed we need it. We are going to build an implication contraint forall a. (b~[a]) => Show [a] -Later, we will solve this constraint using the knowledge (Show b) +Later, we will solve this constraint using the knowledg e(Show b) But we MUST NOT reduce (Show [a]) to (Show a), else the whole thing becomes insoluble. So we simplify gently (get rid of literals @@ -917,66 +1026,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 <- makeImplicationBind loc [] emptyRefinement - qtvs givens irreds - ; return (qtvs, binds `unionBags` implic_bind) } -\end{code} %************************************************************************ @@ -1030,7 +1118,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 } @@ -1149,7 +1237,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. @@ -1157,9 +1245,9 @@ 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 + -- 'ReduceMe': Reduce as far as we can. Don't stop at -- dicts; the idea is to get rid of as many type -- variables as possible, and we don't want to stop -- at (say) Monad (ST s), because that reduces @@ -1168,29 +1256,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 reduceMe - 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 @@ -1202,27 +1301,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} @@ -1301,7 +1396,7 @@ tcSimplifyRuleLhs wanteds -- to fromInteger; this looks fragile to me ; lookup_result <- lookupSimpleInst w' ; case lookup_result of - GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws) + GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws) NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w) } \end{code} @@ -1359,7 +1454,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 ) @@ -1373,7 +1468,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} @@ -1419,7 +1514,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 } @@ -1434,7 +1529,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} @@ -1492,13 +1587,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 - -reduceMe :: Inst -> WhatToDo -reduceMe inst = ReduceMe AddSCs + -- 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 @@ -1517,7 +1608,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 @@ -1537,7 +1627,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 "----------------------", @@ -1546,12 +1636,12 @@ reduceContext env wanteds text "wanted" <+> ppr wanteds, text "----", text "avails" <+> pprAvails avails, - text "frees" <+> ppr frees, text "improved =" <+> ppr improved, + text "irreds = " <+> ppr irreds, text "----------------------" ])) - ; return (improved, frees, binds, irreds) } + ; return (improved, binds, irreds) } tcImproveOne :: Avails -> Inst -> TcM ImprovementDone tcImproveOne avails inst @@ -1624,8 +1714,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) -> @@ -1695,7 +1784,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 @@ -1809,28 +1898,36 @@ 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 - ; (binds, irreds, _frees) <- extractResults avails wanteds - -- No frees, because try_me never says Free + ; (binds, irreds) <- extractResults avails wanteds + ; traceTc (text "reduceImplication result" <+> vcat + [ ppr irreds, ppr binds]) + + -- We always discard the extra avails we've generated; + -- but we remember if we have done any (global) improvement + ; let ret_avails = updateImprovement orig_avails avails + + ; if isEmptyLHsBinds binds then -- No progress + return (ret_avails, NoInstance) + else do + { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds + ; let dict_ids = map instToId extra_givens - co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet binds + co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind) rhs = mkHsWrap co payload loc = instLocSpan inst_loc - payload | isSingleton wanteds = HsVar (instToId (head wanteds)) + payload | [wanted] <- wanteds = HsVar (instToId wanted) | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed -- If there are any irreds, we back off and return NoInstance - -- Either way, we discard the extra avails we've generated; - -- but we remember if we have done any (global) improvement - ; let ret_avails = updateImprovement orig_avails avails - ; case irreds of - [] -> return (ret_avails, GenInst [] (L loc rhs)) - other -> return (ret_avails, NoInstance) - } + ; return (ret_avails, GenInst implic_insts (L loc rhs)) + } } \end{code} Note [Freeness and implications] @@ -1858,6 +1955,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 @@ -1874,8 +1985,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 TcId -- Used for irreducible dictionaries, -- which are going to be lambda bound | Given TcId -- Used for dictionaries for which we have a binding @@ -1898,8 +2008,7 @@ instance Outputable AvailHow where ------------------------- pprAvail :: AvailHow -> SDoc -pprAvail IsFree = text "Free" -pprAvail IsIrred = text "Irred" +pprAvail (IsIrred x) = text "Irred" <+> ppr x pprAvail (Given x) = text "Given" <+> ppr x pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs) @@ -1947,77 +2056,59 @@ 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 (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 == w_id -> go avails binds irreds ws + | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws -- The sought Id can be one of the givens, via a superclass chain -- and then we definitely don't want to generate an x=x binding! - Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws) - where - new_binds = addBind binds w rhs + Just (IsIrred id) + | id == w_id -> go (add_given avails w) binds (w:irreds) ws + | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws + -- The add_given handles the case where we want (Ord a, Eq a), and we + -- don't want to emit *two* Irreds for Ord a, one via the superclass chain + -- This showed up in a dupliated Ord constraint in the error message for + -- test tcfail043 + + Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws) + where + new_binds = addBind binds w_id rhs + where + w_id = instToId w add_given avails w = extendAvailEnv avails w (Given (instToId w)) + -- Don't add the same binding twice - 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) - (VarBind (instToId inst) rhs)) -instSpan wanted = instLocSpan (instLoc wanted) +addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs)) \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 @@ -2036,7 +2127,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)) @@ -2047,10 +2140,33 @@ 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 + addAvailAndSCs want_scs avails irred (IsIrred (instToId irred)) addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails addAvailAndSCs want_scs avails inst avail @@ -2150,7 +2266,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 @@ -2158,12 +2274,12 @@ 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 + -- hence try again - -- Deal with implicit parameter + -- Deal with implicit parameters + ; (irreds2, binds2) <- topCheckLoop doc irreds1 ; let (bad_ips, non_ips) = partition isIPDict irreds2 (ambigs, others) = partition isTyVarDict non_ips @@ -2208,24 +2324,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 @@ -2237,22 +2352,28 @@ 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) -> TcM () -- Just does unification, to fix the default types @@ -2276,8 +2397,64 @@ 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 = [] + +----------------------- +getDefaultableDicts :: [Inst] -> ([(Inst, Class, TcTyVar)], TcTyVarSet) +-- Look for free dicts of the form (C tv), even inside implications +-- *and* the set of tyvars mentioned by all *other* constaints +-- This disgustingly ad-hoc function is solely to support defaulting +getDefaultableDicts insts + = (concat ps, unionVarSets tvs) + where + (ps, tvs) = mapAndUnzip get insts + get d@(Dict {tci_pred = ClassP cls [ty]}) + | Just tv <- tcGetTyVar_maybe ty = ([(d,cls,tv)], emptyVarSet) + | otherwise = ([], tyVarsOfType ty) + get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds}) + = ([ up | up@(_,_,tv) <- ups, not (tv `elemVarSet` tv_set)], + ftvs `minusVarSet` tv_set) + where + tv_set = mkVarSet tvs + (ups, ftvs) = getDefaultableDicts wanteds + get inst = ([], tyVarsOfInst inst) \end{code} +Note [Default unitTy] +~~~~~~~~~~~~~~~~~~~~~ +In interative mode (or with -fextended-default-rules) we add () as the first type we +try when defaulting. This has very little real impact, except in the following case. +Consider: + Text.Printf.printf "hello" +This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't +want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to +default the 'a' to (), rather than to Integer (which is what would otherwise happen; +and then GHCi doesn't attempt to print the (). So in interactive mode, we add +() to the list of defaulting types. See Trac #1200. + Note [Avoiding spurious errors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When doing the unification for defaulting, we check for skolem @@ -2310,78 +2487,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; @@ -2394,7 +2527,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 () @@ -2446,14 +2579,17 @@ addTopIPErrs :: [Name] -> [Inst] -> TcM () addTopIPErrs bndrs [] = return () addTopIPErrs bndrs ips - = addErrTcM (tidy_env, mk_msg tidy_ips) + = do { dflags <- getDOpts + ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) } where (tidy_env, tidy_ips) = tidyInsts ips - mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"), - nest 2 (ptext SLIT("the monomorphic top-level binding(s) of") + mk_msg dflags ips + = vcat [sep [ptext SLIT("Implicit parameters escape from"), + nest 2 (ptext SLIT("the monomorphic top-level binding") + <> plural bndrs <+> ptext SLIT("of") <+> pprBinders bndrs <> colon)], - nest 2 (vcat (map ppr_ip ips)), - monomorphism_fix] + nest 2 (vcat (map ppr_ip ips)), + monomorphism_fix dflags] ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip topIPErrs :: [Inst] -> TcM () @@ -2533,7 +2669,7 @@ report_no_instances tidy_env mb_what insts quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))), ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])] where - ispecs = [ispec | (_, ispec) <- matches] + ispecs = [ispec | (ispec, _) <- matches] mk_no_inst_err insts | null insts = empty @@ -2603,21 +2739,35 @@ mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message) -- Try to identify the offending variable -- ASSUMPTION: the Insts are fully zonked mkMonomorphismMsg tidy_env inst_tvs - = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) -> - returnM (tidy_env, mk_msg docs) + = do { dflags <- getDOpts + ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env + ; return (tidy_env, mk_msg dflags docs) } where - mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)") + mk_msg _ _ | any isRuntimeUnk inst_tvs + = vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+> + (pprWithCommas ppr inst_tvs), + ptext SLIT("Use :print or :force to determine these types")] + mk_msg _ [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)") -- This happens in things like -- f x = show (read "foo") -- where monomorphism doesn't play any role - mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"), - nest 2 (vcat docs), - monomorphism_fix - ] -monomorphism_fix :: SDoc -monomorphism_fix = ptext SLIT("Probable fix:") <+> - (ptext SLIT("give these definition(s) an explicit type signature") - $$ ptext SLIT("or use -fno-monomorphism-restriction")) + mk_msg dflags docs + = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"), + nest 2 (vcat docs), + monomorphism_fix dflags] + +isRuntimeUnk :: TcTyVar -> Bool +isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True + | otherwise = False + +monomorphism_fix :: DynFlags -> SDoc +monomorphism_fix dflags + = ptext SLIT("Probable fix:") <+> vcat + [ptext SLIT("give these definition(s) an explicit type signature"), + if dopt Opt_MonomorphismRestriction dflags + then ptext SLIT("or use -fno-monomorphism-restriction") + else empty] -- Only suggest adding "-fno-monomorphism-restriction" + -- if it is not already set! warnDefault ups default_ty = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag -> @@ -2631,12 +2781,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"),