X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=3212e53407c1692288cbd4ab5422372607d6662b;hp=433266ec08ea69cc536c90166f33539987ec4017;hb=288213d7c2c65fa68ca466c1a1a3378e24fa1151;hpb=b6d08641e2757898470a10dfa906084ade8ab835 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 433266e..3212e53 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -36,7 +36,6 @@ import TcRnMonad import Inst import TcEnv import InstEnv -import TcGadt import TcType import TcMType import TcIface @@ -657,7 +656,7 @@ tcSimplifyInfer \begin{code} tcSimplifyInfer doc tau_tvs wanted = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs) - ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars + ; wanted' <- mapM zonkInst wanted -- Zonk before deciding quantified tyvars ; gbl_tvs <- tcGetGlobalTyVars ; let preds1 = fdPredsOfInsts wanted' gbl_tvs1 = oclose preds1 gbl_tvs @@ -726,7 +725,7 @@ tcSimplifyInfer doc tau_tvs wanted -- Prepare equality instances for quantification ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0 - ; q_eqs <- mappM finalizeEqInst q_eqs0 + ; q_eqs <- mapM finalizeEqInst q_eqs0 ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) } -- NB: when we are done, we might have some bindings, but @@ -806,7 +805,7 @@ tcSimplifyInferCheck tcSimplifyInferCheck loc tau_tvs givens wanteds = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds) - ; (irreds, binds) <- gentleCheckLoop loc givens wanteds + ; (irreds, binds) <- gentleCheckLoop loc givens wanteds -- Figure out which type variables to quantify over -- You might think it should just be the signature tyvars, @@ -921,17 +920,15 @@ tcSimplifyCheck loc qtvs givens wanteds ----------------------------------------------------------- -- tcSimplifyCheckPat is used for existential pattern match tcSimplifyCheckPat :: InstLoc - -> [CoVar] -> Refinement -> [TcTyVar] -- Quantify over these -> [Inst] -- Given -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings -tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds +tcSimplifyCheckPat loc qtvs givens wanteds = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) do { traceTc (text "tcSimplifyCheckPat") ; (irreds, binds) <- gentleCheckLoop loc givens wanteds - ; implic_bind <- bindIrredsR loc qtvs co_vars reft - givens irreds + ; implic_bind <- bindIrredsR loc qtvs givens irreds ; return (binds `unionBags` implic_bind) } ----------------------------------------------------------- @@ -939,14 +936,12 @@ bindIrreds :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds bindIrreds loc qtvs givens irreds - = bindIrredsR loc qtvs [] emptyRefinement givens irreds + = bindIrredsR loc qtvs givens irreds -bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar] - -> Refinement -> [Inst] -> [Inst] - -> TcM TcDictBinds +bindIrredsR :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds -- Make a binding that binds 'irreds', by generating an implication -- constraint for them, *and* throwing the constraint into the LIE -bindIrredsR loc qtvs co_vars reft givens irreds +bindIrredsR loc qtvs givens irreds | null irreds = return emptyBag | otherwise @@ -956,11 +951,10 @@ bindIrredsR loc qtvs co_vars reft givens irreds -- There should be no implicadtion constraints -- See Note [Pruning the givens in an implication constraint] - -- If there are no 'givens' *and* the refinement is empty - -- (the refinement is like more givens), then it's safe to + -- If there are no 'givens', then it's safe to -- partition the 'wanteds' by their qtvs, thereby trimming irreds -- See Note [Freeness and implications] - ; irreds' <- if null givens' && isEmptyRefinement reft + ; irreds' <- if null givens' then do { let qtv_set = mkVarSet qtvs (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds @@ -968,15 +962,14 @@ bindIrredsR loc qtvs co_vars reft givens irreds ; 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' + ; (implics, bind) <- makeImplicationBind loc qtvs givens' irreds' -- This call does the real work -- If irreds' is empty, it does something sensible ; extendLIEs implics ; return bind } -makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement +makeImplicationBind :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM ([Inst], TcDictBinds) -- Make a binding that binds 'irreds', by generating an implication @@ -988,7 +981,7 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement -- qtvs includes coercion variables -- -- This binding must line up the 'rhs' in reduceImplication -makeImplicationBind loc all_tvs reft +makeImplicationBind loc all_tvs givens -- Guaranteed all Dicts -- or EqInsts irreds @@ -1003,7 +996,7 @@ makeImplicationBind loc all_tvs reft -- 'givens' must be a simple CoVar. This MUST be cleaned up. ; let name = mkInternalName uniq (mkVarOcc "ic") span - implic_inst = ImplicInst { tci_name = name, tci_reft = reft, + implic_inst = ImplicInst { tci_name = name, tci_tyvars = all_tvs, tci_given = (eq_givens ++ dict_givens), tci_wanted = irreds, tci_loc = loc } @@ -1101,24 +1094,27 @@ checkLoop :: RedEnv -- Postcondition: returned Insts are zonked checkLoop env wanteds - = go env wanteds - where go env wanteds - = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv] + = go env wanteds (return ()) + where go env wanteds elim_skolems + = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv] ; env' <- zonkRedEnv env ; wanteds' <- zonkInsts wanteds - ; (improved, binds, irreds) <- reduceContext env' wanteds' + ; (improved, binds, irreds, elim_more_skolems) + <- reduceContext env' wanteds' + ; let elim_skolems' = elim_skolems >> elim_more_skolems ; if not improved then - return (irreds, binds) + elim_skolems' >> return (irreds, binds) else do -- 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) <- go env' irreds + -- 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) <- go env' irreds elim_skolems' ; return (irreds1, binds `unionBags` binds1) } } \end{code} @@ -1367,7 +1363,9 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- HOWEVER, some unification may take place, if we instantiate -- a method Inst with an equality constraint ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs) - ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds' + ; (_imp, _binds, constrained_dicts, elim_skolems) + <- reduceContext env wanteds' + ; elim_skolems -- Next, figure out the tyvars we will quantify over ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) @@ -1416,7 +1414,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds (is_nested_group || isDict inst) = Stop | otherwise = ReduceMe AddSCs env = mkNoImproveRedEnv doc try_me - ; (_imp, binds, irreds) <- reduceContext env wanteds' + ; (_imp, binds, irreds, elim_skolems) <- reduceContext env wanteds' + ; elim_skolems -- See "Notes on implicit parameters, Question 4: top level" ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured @@ -1565,7 +1564,8 @@ tcSimplifyIPs given_ips wanteds -- Unusually for checking, we *must* zonk the given_ips ; let env = mkRedEnv doc try_me given_ips' - ; (improved, binds, irreds) <- reduceContext env wanteds' + ; (improved, binds, irreds, elim_skolems) <- reduceContext env wanteds' + ; elim_skolems ; if not improved then ASSERT( all is_free irreds ) @@ -1619,10 +1619,10 @@ bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds -- arguably a bug in Match.tidyEqnInfo (see notes there) bindInstsOfLocalFuns wanteds local_ids - | null overloaded_ids + | null overloaded_ids = do -- Common case - = extendLIEs wanteds `thenM_` - returnM emptyLHsBinds + extendLIEs wanteds + return emptyLHsBinds | otherwise = do { (irreds, binds) <- gentleInferLoop doc for_me @@ -1657,8 +1657,6 @@ data RedEnv , red_givens :: [Inst] -- All guaranteed rigid -- Always dicts -- but see Note [Rigidity] - , red_reft :: Refinement -- The refinement to apply to the 'givens' - -- You should think of it as 'given equalities' , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg) -- See Note [RedStack] } @@ -1681,7 +1679,6 @@ mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv mkRedEnv doc try_me givens = RedEnv { red_doc = doc, red_try_me = try_me, red_givens = givens, - red_reft = emptyRefinement, red_stack = (0,[]), red_improve = True } @@ -1689,7 +1686,7 @@ mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv -- Do not do improvement; no givens mkNoImproveRedEnv doc try_me = RedEnv { red_doc = doc, red_try_me = try_me, - red_givens = [], red_reft = emptyRefinement, + red_givens = [], red_stack = (0,[]), red_improve = True } @@ -1710,8 +1707,8 @@ data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses -- Note [SUPER-CLASS LOOP 1] zonkRedEnv :: RedEnv -> TcM RedEnv -zonkRedEnv env - = do { givens' <- mappM zonkInst (red_givens env) +zonkRedEnv env + = do { givens' <- mapM zonkInst (red_givens env) ; return $ env {red_givens = givens'} } \end{code} @@ -1741,7 +1738,8 @@ reduceContext :: RedEnv -> [Inst] -- Wanted -> TcM (ImprovementDone, TcDictBinds, -- Dictionary bindings - [Inst]) -- Irreducible + [Inst], -- Irreducible + TcM ()) -- Undo skolems from SkolemOccurs reduceContext env wanteds = do { traceTc (text "reduceContext" <+> (vcat [ @@ -1774,13 +1772,10 @@ reduceContext env wanteds given_dicts0 -- 5. Build the Avail mapping from "given_dicts" - -- Add dicts refined by the current type refinement ; (init_state, extra_givens) <- getLIE $ do { init_state <- foldlM addGiven emptyAvails given_dicts - ; let reft = red_reft env - ; if isEmptyRefinement reft then return init_state - else foldlM (addRefinedGiven reft) - init_state given_dicts } + ; return init_state + } -- *** ToDo: what to do with the "extra_givens"? For the -- moment I'm simply discarding them, which is probably wrong @@ -1824,7 +1819,7 @@ reduceContext env wanteds eq_irreds irreds -- 9. eliminate the artificial skolem constants introduced in 1. - ; eliminate_skolems +-- ; eliminate_skolems -- Figure out whether we should go round again -- My current plan is to see if any of the mutable tyvars in @@ -1868,7 +1863,8 @@ reduceContext env wanteds `unionBags` normalise_binds2 `unionBags` dict_binds `unionBags` implic_binds, - all_irreds) + all_irreds, + eliminate_skolems) } tcImproveOne :: Avails -> Inst -> TcM ImprovementDone @@ -1893,13 +1889,13 @@ unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))] unifyEqns [] = return False unifyEqns eqns = do { traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) - ; mappM_ unify eqns + ; mapM_ unify eqns ; return True } where unify ((qtvs, pairs), what1, what2) - = addErrCtxtM (mkEqnMsg what1 what2) $ - tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) -> - mapM_ (unif_pr tenv) pairs + = addErrCtxtM (mkEqnMsg what1 what2) $ do + (_, _, tenv) <- tcInstTyVars (varSetElems qtvs) + mapM_ (unif_pr tenv) pairs unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2) pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)] @@ -1918,7 +1914,7 @@ The main context-reduction function is @reduce@. Here's its game plan. \begin{code} reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state - = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state)) + = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state)) ; dopts <- getDOpts #ifdef DEBUG ; if n > 8 then @@ -1940,7 +1936,7 @@ reduce env wanted avails -- It's the same as an existing inst, or a superclass thereof | Just avail <- findAvail avails wanted = do { traceTc (text "reduce: found " <+> ppr wanted) - ; returnM avails + ; return avails } | otherwise @@ -2108,13 +2104,10 @@ reduceImplication :: RedEnv Suppose we are simplifying the constraint forall bs. extras => wanted -in the context of an overall simplification problem with givens 'givens', -and refinment 'reft'. +in the context of an overall simplification problem with givens 'givens'. Note that - * The refinement is often empty - - * The 'extra givens' need not mention any of the quantified type variables + * The 'givens' need not mention any of the quantified type variables e.g. forall {}. Eq a => Eq [a] forall {}. C Int => D (Tree Int) @@ -2140,27 +2133,20 @@ Note that -- reduceImplication env orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc, - tci_tyvars = tvs, tci_reft = reft, + tci_tyvars = tvs, tci_given = extra_givens, tci_wanted = wanteds }) - = do { -- Add refined givens, and the extra givens - -- Todo fix this --- (refined_red_givens,refined_avails) --- <- if isEmptyRefinement reft then return (red_givens env,orig_avails) --- else foldlM (addRefinedGiven reft) ([],orig_avails) (red_givens env) --- Commented out SLPJ Sept 07; see comment with extractLocalResults below - let refined_red_givens = [] - - -- Solve the sub-problem - ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications] + = do { -- Solve the sub-problem + ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications] env' = env { red_givens = extra_givens ++ red_givens env - , red_reft = reft - , red_doc = sep [ptext SLIT("reduceImplication for") <+> ppr name, - nest 2 (parens $ ptext SLIT("within") <+> red_doc env)] + , red_doc = sep [ptext SLIT("reduceImplication for") + <+> ppr name, + nest 2 (parens $ ptext SLIT("within") + <+> red_doc env)] , red_try_me = try_me } ; traceTc (text "reduceImplication" <+> vcat [ ppr (red_givens env), ppr extra_givens, - ppr reft, ppr wanteds]) + ppr wanteds]) ; (irreds, binds) <- checkLoop env' wanteds ; let (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens -- SLPJ Sept 07: I think this is bogus; currently @@ -2189,11 +2175,12 @@ reduceImplication env -- If there are any irreds, we back off and do nothing return (emptyBag, [orig_implic]) else do - { (simpler_implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds - -- This binding is useless if the recursive simplification - -- made no progress; but currently we don't try to optimise that - -- case. After all, we only try hard to reduce at top level, or - -- when inferring types. + { (simpler_implic_insts, bind) + <- makeImplicationBind inst_loc tvs extra_givens irreds + -- This binding is useless if the recursive simplification + -- made no progress; but currently we don't try to optimise that + -- case. After all, we only try hard to reduce at top level, or + -- when inferring types. ; let dict_wanteds = filter (not . isEqInst) wanteds -- TOMDO: given equational constraints bug! @@ -2207,7 +2194,7 @@ reduceImplication env -- it makes no difference co = wrap_inline -- Note [Always inline implication constraints] <.> mkWpTyLams tvs - <.> mkWpTyLams eq_tyvars + <.> mkWpLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind) wrap_inline | null dict_ids = idHsWrapper @@ -2342,7 +2329,7 @@ elemAvails wanted (Avails _ avails) = wanted `elemFM` avails extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails -- Does improvement -extendAvails avails@(Avails imp env) inst avail +extendAvails avails@(Avails imp env) inst avail = do { imp1 <- tcImproveOne avails inst -- Do any improvement ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) } @@ -2437,46 +2424,8 @@ addGiven avails given = addAvailAndSCs AddSCs avails given (Given given) -- No ASSERT( not (given `elemAvails` avails) ) because in an instance -- decl for Ord t we can add both Ord t and Eq t as 'givens', -- so the assert isn't true - -addRefinedGiven :: Refinement -> Avails -> Inst -> TcM Avails -addRefinedGiven reft avails given - | isDict given -- We sometimes have 'given' methods, but they - -- are always optional, so we can drop them - , 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)) - ; addAvailAndSCs AddSCs avails new_given (Rhs rhs [given]) } - -- ToDo: the superclasses of the original given all exist in Avails - -- so we could really just cast them, but it's more awkward to do, - -- and hopefully the optimiser will spot the duplicated work - | otherwise - = return 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 ) @@ -2607,7 +2556,7 @@ tcSimplifyInteractive wanteds -- error message generation for the monomorphism restriction tc_simplify_top doc interactive wanteds = do { dflags <- getDOpts - ; wanteds <- zonkInsts wanteds + ; wanteds <- zonkInsts wanteds ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds)) ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds) @@ -2869,13 +2818,13 @@ whether it worked or not. tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it -> TcM () -tcSimplifyDefault theta - = newDictBndrsO DefaultOrigin theta `thenM` \ wanteds -> - tryHardCheckLoop doc wanteds `thenM` \ (irreds, _) -> - addNoInstanceErrs irreds `thenM_` +tcSimplifyDefault theta = do + wanteds <- newDictBndrsO DefaultOrigin theta + (irreds, _) <- tryHardCheckLoop doc wanteds + addNoInstanceErrs irreds if null irreds then - returnM () - else + return () + else traceTc (ptext SLIT("tcSimplifyDefault failing")) >> failM where doc = ptext SLIT("default declaration") @@ -2901,7 +2850,7 @@ groupErrs :: ([Inst] -> TcM ()) -- Deal with one group groupErrs report_err [] = return () -groupErrs report_err (inst:insts) +groupErrs report_err (inst:insts) = do { do_one (inst:friends) ; groupErrs report_err others } where @@ -3069,11 +3018,11 @@ addTopAmbigErrs dicts cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2 report :: [(Inst,[TcTyVar])] -> TcM () - report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars - = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) -> + report pairs@((inst,tvs) : _) = do -- The pairs share a common set of ambiguous tyvars + (tidy_env, mono_msg) <- mkMonomorphismMsg tidy_env tvs setSrcSpan (instSpan inst) $ -- the location of the first one will do for the err message - addErrTcM (tidy_env, msg $$ mono_msg) + addErrTcM (tidy_env, msg $$ mono_msg) where dicts = map fst pairs msg = sep [text "Ambiguous type variable" <> plural tvs <+> @@ -3115,8 +3064,8 @@ monomorphism_fix dflags else empty] -- Only suggest adding "-fno-monomorphism-restriction" -- if it is not already set! -warnDefault ups default_ty - = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag -> +warnDefault ups default_ty = do + warn_flag <- doptM Opt_WarnTypeDefaults addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg) where dicts = [d | (d,_,_) <- ups]