X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=a5ce732331a579e9cf480b25722c0a9503a71aed;hp=324bda9567511e1a73fafe19ec40c8f42849cae5;hb=30c122df62ec75f9ed7f392f24c2925675bf1d06;hpb=4226903dd2bd0a08e1b7e10547a57588e8371e78 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 324bda9..a5ce732 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 @@ -65,7 +64,9 @@ import Util import UniqSet import SrcLoc import DynFlags +import FastString +import Control.Monad import Data.List \end{code} @@ -921,17 +922,15 @@ tcSimplifyCheck loc qtvs givens wanteds ----------------------------------------------------------- -- tcSimplifyCheckPat is used for existential pattern match tcSimplifyCheckPat :: InstLoc - -> [CoVar] -> [TcTyVar] -- Quantify over these -> [Inst] -- Given -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings -tcSimplifyCheckPat loc co_vars 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 emptyRefinement - givens irreds + ; implic_bind <- bindIrredsR loc qtvs givens irreds ; return (binds `unionBags` implic_bind) } ----------------------------------------------------------- @@ -939,14 +938,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 +953,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 +964,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 +983,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 +998,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 } @@ -1664,8 +1659,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] } @@ -1688,7 +1681,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 } @@ -1696,7 +1688,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 } @@ -1764,12 +1756,12 @@ reduceContext env wanteds ; let givens = red_givens env (given_eqs0, given_dicts0) = partition isEqInst givens (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds - (wanted_implics0, wanted_dicts0) = partition isImplicInst wanted_non_eqs + (wanted_implics0, wanted_dicts) = partition isImplicInst wanted_non_eqs -- We want to add as wanted equalities those that (transitively) -- occur in superclass contexts of wanted class constraints. -- See Note [Ancestor Equalities] - ; ancestor_eqs <- ancestorEqualities wanted_dicts0 + ; ancestor_eqs <- ancestorEqualities wanted_dicts ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs @@ -1782,72 +1774,59 @@ 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 - -- 7. Normalise the *wanted* *dictionary* constraints - -- wrt. the toplevel and given equations - -- NB: normalisation includes zonking as part of what it does - -- so it's important to do it after any unifications - -- that happened as a result of the addGivens - ; (wanted_dicts,normalise_binds1) <- normaliseWantedDicts given_eqs wanted_dicts0 - -- 6. Solve the *wanted* *dictionary* constraints (not implications) -- This may expose some further equational constraints... ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state) - ; (dict_binds, bound_dicts, dict_irreds) <- extractResults avails wanted_dicts + ; (dict_binds, bound_dicts, dict_irreds) + <- extractResults avails wanted_dicts ; traceTc $ text "reduceContext extractresults" <+> vcat - [ppr avails,ppr wanted_dicts,ppr dict_binds] - - -- *** ToDo: what to do with the "extra_eqs"? For the - -- moment I'm simply discarding them, which is probably wrong + [ppr avails, ppr wanted_dicts, ppr dict_binds] -- Solve the wanted *implications*. In doing so, we can provide -- as "given" all the dicts that were originally given, -- *or* for which we now have bindings, -- *or* which are now irreds - ; let implic_env = env { red_givens = givens ++ bound_dicts ++ dict_irreds } - ; (implic_binds_s, implic_irreds_s) <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0 + ; let implic_env = env { red_givens = givens ++ bound_dicts + ++ dict_irreds } + ; (implic_binds_s, implic_irreds_s) + <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0 ; let implic_binds = unionManyBags implic_binds_s implic_irreds = concat implic_irreds_s - -- 3. Solve the *wanted* *equation* constraints - ; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs - - -- 4. Normalise the *wanted* equality constraints with respect to - -- each other - ; eq_irreds <- normaliseWantedEqs eq_irreds0 + -- Normalise the wanted equality constraints + ; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs) - -- 8. Substitute the wanted *equations* in the wanted *dictionaries* + -- Normalise the wanted dictionaries ; let irreds = dict_irreds ++ implic_irreds - ; (norm_irreds, normalise_binds2) <- substEqInDictInsts True {-wanted-} - eq_irreds irreds + eqs = eq_irreds ++ given_eqs + ; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds - -- 9. eliminate the artificial skolem constants introduced in 1. --- ; eliminate_skolems - - -- Figure out whether we should go round again - -- My current plan is to see if any of the mutable tyvars in - -- givens or irreds has been filled in by improvement. - -- If so, there is merit in going around again, because - -- we may make further progress + -- Figure out whether we should go round again. We do so in either + -- two cases: + -- (1) If any of the mutable tyvars in givens or irreds has been + -- filled in by improvement, there is merit in going around + -- again, because we may make further progress. + -- (2) If we managed to normalise any dicts, there is merit in going + -- around gain, because reduceList may be able to get further. -- - -- ToDo: is it only mutable stuff? We may have exposed new + -- ToDo: We may have exposed new -- equality constraints and should probably go round again -- then as well. But currently we are dropping them on the -- floor anyway. ; let all_irreds = norm_irreds ++ eq_irreds - ; improved <- anyM isFilledMetaTyVar $ varSetElems $ - tyVarsOfInsts (givens ++ all_irreds) + ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $ + tyVarsOfInsts (givens ++ all_irreds) + ; let improvedDicts = not $ isEmptyBag normalise_binds + improved = improvedMetaTy || improvedDicts -- The old plan (fragile) -- improveed = availsImproved avails @@ -1872,8 +1851,7 @@ reduceContext env wanteds ])) ; return (improved, - given_binds `unionBags` normalise_binds1 - `unionBags` normalise_binds2 + given_binds `unionBags` normalise_binds `unionBags` dict_binds `unionBags` implic_binds, all_irreds, @@ -1929,12 +1907,9 @@ reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state)) ; dopts <- getDOpts -#ifdef DEBUG - ; if n > 8 then + ; when (debugIsOn && (n > 8)) $ do dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n) 2 (ifPprDebug (nest 2 (pprStack stk)))) - else return () -#endif ; if n >= ctxtStkDepth dopts then failWithTc (reduceDepthErr n stk) else @@ -2117,13 +2092,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) @@ -2149,27 +2121,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 @@ -2198,11 +2163,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! @@ -2446,46 +2412,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 ) @@ -2998,14 +2926,13 @@ report_no_instances tidy_env mb_what insts | not (isClassDict wanted) = Left wanted | otherwise = case lookupInstEnv inst_envs clas tys of + ([], _) -> Left wanted -- No match -- The case of exactly one match and no unifiers means a -- successful lookup. That can't happen here, because dicts -- only end up here if they didn't match in Inst.lookupInst -#ifdef DEBUG - ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted) -#endif - ([], _) -> Left wanted -- No match - res -> Right (mk_overlap_msg wanted res) + ([m],[]) + | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted) + res -> Right (mk_overlap_msg wanted res) where (clas,tys) = getDictClassTys wanted