From e891720545a2f088cc48ad62bad7c5b2ad7d183f Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Sat, 13 Sep 2008 13:36:31 +0000 Subject: [PATCH] Type families: completed the new equality solver - Implements normalisation of class constraints containing synonym family applications or skolems refined by local equalities. - Clean up of TcSimplify.reduceContext by using the new equality solver. - Removed all the now unused code of the old algorithm. - This completes the implementation of the new algorithm, but it is largely untested => many regressions. --- compiler/typecheck/Inst.lhs | 4 +- compiler/typecheck/TcSimplify.lhs | 133 ++-- compiler/typecheck/TcTyFuns.lhs | 1488 +++++++++---------------------------- 3 files changed, 399 insertions(+), 1226 deletions(-) diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index d839aba..aecaf7f 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -513,7 +513,7 @@ Zonking makes sure that the instance types are fully zonked. \begin{code} zonkInst :: Inst -> TcM Inst -zonkInst dict@(Dict { tci_pred = pred}) = do +zonkInst dict@(Dict {tci_pred = pred}) = do new_pred <- zonkTcPredType pred return (dict {tci_pred = new_pred}) @@ -544,7 +544,7 @@ zonkInst eqinst@(EqInst {tci_left = ty1, tci_right = ty2}) (\co -> liftM mkGivenCo $ zonkTcType co) ; ty1' <- zonkTcType ty1 ; ty2' <- zonkTcType ty2 - ; return (eqinst {tci_co = co', tci_left= ty1', tci_right = ty2' }) + ; return (eqinst {tci_co = co', tci_left = ty1', tci_right = ty2' }) } zonkInsts :: [Inst] -> TcRn [Inst] diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index f7d0021..b074437 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -1090,18 +1090,16 @@ checkLoop :: RedEnv -- Postcondition: returned Insts are zonked checkLoop env wanteds - = go env wanteds (return ()) - where go env wanteds elim_skolems + = go env wanteds + where go env wanteds = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv] ; env' <- zonkRedEnv env ; wanteds' <- zonkInsts wanteds - ; (improved, binds, irreds, elim_more_skolems) - <- reduceContext env' wanteds' - ; let elim_skolems' = elim_skolems >> elim_more_skolems + ; (improved, binds, irreds) <- reduceContext env' wanteds' ; if not improved then - elim_skolems' >> return (irreds, binds) + return (irreds, binds) else do -- If improvement did some unification, we go round again. @@ -1110,7 +1108,7 @@ checkLoop env wanteds -- 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' + { (irreds1, binds1) <- go env' irreds ; return (irreds1, binds `unionBags` binds1) } } \end{code} @@ -1359,9 +1357,7 @@ 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 (\_ -> ReduceMe AddSCs) - ; (_imp, _binds, constrained_dicts, elim_skolems) - <- reduceContext env wanteds' - ; elim_skolems + ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds' -- Next, figure out the tyvars we will quantify over ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) @@ -1410,8 +1406,7 @@ 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, elim_skolems) <- reduceContext env wanteds' - ; elim_skolems + ; (_imp, binds, irreds) <- reduceContext env wanteds' -- See "Notes on implicit parameters, Question 4: top level" ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured @@ -1588,8 +1583,7 @@ tcSimplifyIPs given_ips wanteds -- Unusually for checking, we *must* zonk the given_ips ; let env = mkRedEnv doc try_me given_ips' - ; (improved, binds, irreds, elim_skolems) <- reduceContext env wanteds' - ; elim_skolems + ; (improved, binds, irreds) <- reduceContext env wanteds' ; if not improved then ASSERT( all is_free irreds ) @@ -1762,53 +1756,47 @@ reduceContext :: RedEnv -> [Inst] -- Wanted -> TcM (ImprovementDone, TcDictBinds, -- Dictionary bindings - [Inst], -- Irreducible - TcM ()) -- Undo skolems from SkolemOccurs + [Inst]) -- Irreducible -reduceContext env wanteds +reduceContext env wanteds0 = do { traceTc (text "reduceContext" <+> (vcat [ text "----------------------", red_doc env, text "given" <+> ppr (red_givens env), - text "wanted" <+> ppr wanteds, + text "wanted" <+> ppr wanteds0, text "----------------------" ])) - - ; let givens = red_givens env - (given_eqs0, given_dicts0) = partition isEqInst givens - (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds - (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_dicts - ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs + ; ancestor_eqs <- ancestorEqualities wanteds0 ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs - -- 1. Normalise the *given* *equality* constraints - ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0 - - -- 2. Normalise the *given* *dictionary* constraints - -- wrt. the toplevel and given equations - ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs - given_dicts0 - - -- 5. Build the Avail mapping from "given_dicts" + -- Normalise and solve all equality constraints as far as possible + -- and normalise all dictionary constraints wrt to the reduced + -- equalities. The returned wanted constraints include the + -- irreducible wanted equalities. + ; let wanteds = wanteds0 ++ ancestor_eqs + givens = red_givens env + ; (givens', + wanteds', + normalise_binds, + eq_improved) <- tcReduceEqs givens wanteds + + -- Build the Avail mapping from "given_dicts" ; (init_state, _) <- getLIE $ do - { init_state <- foldlM addGiven emptyAvails given_dicts + { init_state <- foldlM addGiven emptyAvails givens' ; return init_state } - -- !!! ToDo: what to do with the "extra_givens"? For the - -- moment I'm simply discarding them, which is probably wrong - - -- 6. Solve the *wanted* *dictionary* constraints (not implications) - -- This may expose some further equational constraints... + -- Solve the *wanted* *dictionary* constraints (not implications) + -- This may expose some further equational constraints... + ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds' ; (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] @@ -1816,21 +1804,29 @@ reduceContext env wanteds -- 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 } + ; let implic_env = env { red_givens = givens ++ bound_dicts ++ + dict_irreds } ; (implic_binds_s, implic_irreds_s) - <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0 + <- mapAndUnzipM (reduceImplication implic_env) wanted_implics ; let implic_binds = unionManyBags implic_binds_s implic_irreds = concat implic_irreds_s - -- Normalise the wanted equality constraints - ; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs) - - -- Normalise the wanted dictionaries - ; let irreds = dict_irreds ++ implic_irreds - eqs = eq_irreds ++ given_eqs - ; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds - + -- Collect all irreducible instances, and determine whether we should + -- go round again. We do so in either of three cases: + -- (1) If dictionary reduction or equality solving led to + -- improvement (i.e., instantiated type variables). + -- (2) If we managed to normalise any dicts, there is merit in going + -- around gain, because reduceList may be able to get further. + -- (3) If we uncovered extra equalities. We will try to solve them + -- in the next iteration. + ; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs + improvedFlexible = availsImproved avails || + eq_improved + improvedDicts = not $ isEmptyBag normalise_binds + extraEqs = (not . null) extra_eqs + improved = improvedFlexible || improvedDicts || extraEqs + +{- Old story -- 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 @@ -1838,31 +1834,18 @@ reduceContext env wanteds -- 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: 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 ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $ tyVarsOfInsts (givens ++ all_irreds) ; let improvedDicts = not $ isEmptyBag normalise_binds improved = improvedMetaTy || improvedDicts - - -- The old plan (fragile) - -- improveed = availsImproved avails - -- || (not $ isEmptyBag normalise_binds1) - -- || (not $ isEmptyBag normalise_binds2) - -- || (any isEqInst irreds) + -} ; traceTc (text "reduceContext end" <+> (vcat [ text "----------------------", red_doc env, text "given" <+> ppr givens, - text "given_eqs" <+> ppr given_eqs, - text "wanted" <+> ppr wanteds, - text "wanted_dicts" <+> ppr wanted_dicts, + text "wanted" <+> ppr wanteds0, text "----", text "avails" <+> pprAvails avails, text "improved =" <+> ppr improved, @@ -1873,11 +1856,9 @@ reduceContext env wanteds ])) ; return (improved, - given_binds `unionBags` normalise_binds - `unionBags` dict_binds - `unionBags` implic_binds, - all_irreds, - eliminate_skolems) + normalise_binds `unionBags` dict_binds + `unionBags` implic_binds, + all_irreds) } tcImproveOne :: Avails -> Inst -> TcM ImprovementDone @@ -2368,8 +2349,8 @@ extendAvails avails@(Avails imp env) inst avail availsInsts :: Avails -> [Inst] availsInsts (Avails _ avails) = keysFM avails -_availsImproved :: Avails -> ImprovementDone -_availsImproved (Avails imp _) = imp +availsImproved :: Avails -> ImprovementDone +availsImproved (Avails imp _) = imp \end{code} Extracting the bindings from a bunch of Avails. diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 188a29e..981845a 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -6,18 +6,13 @@ module TcTyFuns ( -- type normalisation wrt to toplevel equalities only tcNormaliseFamInst, - -- normalisation and solving of equalities - EqConfig, - normaliseEqs, propagateEqs, finaliseEqs, normaliseDicts, + -- instance normalisation wrt to equalities + tcReduceEqs, -- errors misMatchMsg, failWithMisMatch, - -- DEPRECATED: interface for the ICFP'08 algorithm - normaliseGivenEqs, normaliseGivenDicts, - normaliseWantedEqs, normaliseWantedDicts, - - ) where +) where #include "HsVersions.h" @@ -83,7 +78,7 @@ tcUnfoldSynFamInst (TyConApp tycon tys) mkTyConApp coe_tc tys') where tys' = rep_tys ++ restTys - coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst" + coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst" (tyConFamilyCoercion_maybe rep_tc) } where @@ -105,11 +100,128 @@ possible (ie, we treat family instances as a TRS). Also zonk meta variables. -- tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType) tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst +\end{code} + +Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and +apply the normalisation function gives as the first argument to every TyConApp +and every TyVarTy subterm. + + tcGenericNormaliseFamInst fun ty = (co, ty') + then co : ty ~ ty' + +This function is (by way of using smart constructors) careful to ensure that +the returned coercion is exactly IdCo (and not some semantically equivalent, +but syntactically different coercion) whenever (ty' `tcEqType` ty). This +makes it easy for the caller to determine whether the type changed. BUT +even if we return IdCo, ty' may be *syntactically* different from ty due to +unfolded closed type synonyms (by way of tcCoreView). In the interest of +good error messages, callers should discard ty' in favour of ty in this case. -tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType) -tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst +\begin{code} +tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion))) + -- what to do with type functions and tyvars + -> TcType -- old type + -> TcM (CoercionI, TcType) -- (coercion, new type) +tcGenericNormaliseFamInst fun ty + | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty' +tcGenericNormaliseFamInst fun (TyConApp tyCon tys) + = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys + ; let tycon_coi = mkTyConAppCoI tyCon ntys cois + ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args! + ; case maybe_ty_co of + -- a matching family instance exists + Just (ty', co) -> + do { let first_coi = mkTransCoI tycon_coi (ACo co) + ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty' + ; let fix_coi = mkTransCoI first_coi rest_coi + ; return (fix_coi, nty) + } + -- no matching family instance exists + -- we do not do anything + Nothing -> return (tycon_coi, mkTyConApp tyCon ntys) + } +tcGenericNormaliseFamInst fun (AppTy ty1 ty2) + = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1 + ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2 + ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2) + } +tcGenericNormaliseFamInst fun (FunTy ty1 ty2) + = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1 + ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2 + ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2) + } +tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1) + = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1 + ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1) + } +tcGenericNormaliseFamInst fun ty@(TyVarTy tv) + | isTcTyVar tv + = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty) + ; res <- lookupTcTyVar tv + ; case res of + DoneTv _ -> + do { maybe_ty' <- fun ty + ; case maybe_ty' of + Nothing -> return (IdCo, ty) + Just (ty', co1) -> + do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty' + ; return (ACo co1 `mkTransCoI` coi2, ty'') + } + } + IndirectTv ty' -> tcGenericNormaliseFamInst fun ty' + } + | otherwise + = return (IdCo, ty) +tcGenericNormaliseFamInst fun (PredTy predty) + = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty + ; return (coi, PredTy pred') } + +--------------------------------- +tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion))) + -> TcPredType + -> TcM (CoercionI, TcPredType) + +tcGenericNormaliseFamInstPred fun (ClassP cls tys) + = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys + ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys') + } +tcGenericNormaliseFamInstPred fun (IParam ipn ty) + = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty + ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty') + } +tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2) + = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1 + ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2 + ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') } \end{code} + +%************************************************************************ +%* * + Normalisation of instances wrt to equalities +%* * +%************************************************************************ + +\begin{code} +tcReduceEqs :: [Inst] -- locals + -> [Inst] -- wanteds + -> TcM ([Inst], -- normalised locals (w/o equalities) + [Inst], -- normalised wanteds (including equalities) + TcDictBinds, -- bindings for all simplified dictionaries + Bool) -- whether any flexibles where instantiated +tcReduceEqs locals wanteds + = do { let (local_eqs , local_dicts) = partition isEqInst locals + (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds + ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs) + ; eqCfg2 <- normaliseDicts False local_dicts + ; eqCfg3 <- normaliseDicts True wanteds_dicts + ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` eqCfg2 + `unionEqConfig` eqCfg3) + ; finaliseEqsAndDicts eqCfg + } +\end{code} + + %************************************************************************ %* * Equality Configurations @@ -117,17 +229,19 @@ tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst %************************************************************************ We maintain normalised equalities together with the skolems introduced as -intermediates during flattening of equalities. +intermediates during flattening of equalities as well as -!!!TODO: Do we really need to keep track of the skolem variables? They are at -the moment not used in instantiateAndExtract, but it is hard to say until we -know exactly how finalisation will fianlly look like. +!!!TODO: We probably now can do without the skolem set. It's not used during +finalisation in the current code. \begin{code} -- |Configuration of normalised equalities used during solving. -- -data EqConfig = EqConfig { eqs :: [RewriteInst] - , skolems :: TyVarSet +data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities + , locals :: [Inst] -- given dicts + , wanteds :: [Inst] -- wanted dicts + , binds :: TcDictBinds -- bindings + , skolems :: TyVarSet -- flattening skolems } addSkolems :: EqConfig -> TyVarSet -> EqConfig @@ -136,6 +250,24 @@ addSkolems eqCfg newSkolems addEq :: EqConfig -> RewriteInst -> EqConfig addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg} + +unionEqConfig :: EqConfig -> EqConfig -> EqConfig +unionEqConfig eqc1 eqc2 = EqConfig + { eqs = eqs eqc1 ++ eqs eqc2 + , locals = locals eqc1 ++ locals eqc2 + , wanteds = wanteds eqc1 ++ wanteds eqc2 + , binds = binds eqc1 `unionBags` binds eqc2 + , skolems = skolems eqc1 `unionVarSet` skolems eqc2 + } + +emptyEqConfig :: EqConfig +emptyEqConfig = EqConfig + { eqs = [] + , locals = [] + , wanteds = [] + , binds = emptyBag + , skolems = emptyVarSet + } \end{code} The set of operations on an equality configuration. We obtain the initialise @@ -143,9 +275,6 @@ configuration by normalisation ('normaliseEqs'), solve the equalities by propagation ('propagateEqs'), and eventually finalise the configuration when no further propoagation is possible. -!!!TODO: Eventually, normalisation of dictionaries and dictionary -simplification should be included in propagation. - \begin{code} -- |Turn a set of equalities into an equality configuration for solving. -- @@ -154,9 +283,27 @@ simplification should be included in propagation. normaliseEqs :: [Inst] -> TcM EqConfig normaliseEqs eqs = do { (eqss, skolemss) <- mapAndUnzipM normEqInst eqs - ; return $ EqConfig { eqs = concat eqss - , skolems = unionVarSets skolemss - } + ; return $ emptyEqConfig { eqs = concat eqss + , skolems = unionVarSets skolemss + } + } + +-- |Flatten the type arguments of all dictionaries, returning the result as a +-- equality configuration. The dictionaries go into the 'wanted' component if +-- the second argument is 'True'. +-- +-- Precondition: The Insts are zonked. +-- +normaliseDicts :: Bool -> [Inst] -> TcM EqConfig +normaliseDicts isWanted insts + = do { (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted) + insts + ; return $ emptyEqConfig { eqs = concat eqss + , locals = if isWanted then [] else insts' + , wanteds = if isWanted then insts' else [] + , binds = unionManyBags bindss + , skolems = unionVarSets skolemss + } } -- |Solves the equalities as far as possible by applying propagation rules. @@ -165,23 +312,27 @@ propagateEqs :: EqConfig -> TcM EqConfig propagateEqs eqCfg@(EqConfig {eqs = todoEqs}) = propagate todoEqs (eqCfg {eqs = []}) --- |Finalise a set of equalities after propagation. The Boolean value is --- `True' iff any flexible variables, except those introduced by flattening --- (i.e., those in the `skolems' component of the argument) where instantiated. --- The returned set of instances are all residual wanteds. +-- |Finalise a set of equalities and associated dictionaries after +-- propagation. The returned Boolean value is `True' iff any flexible +-- variables, except those introduced by flattening (i.e., those in the +-- `skolems' component of the argument) where instantiated. The first returned +-- set of instances are the locals (without equalities) and the second set are +-- all residual wanteds, including equalities. -- -finaliseEqs :: EqConfig -> TcM ([Inst], Bool) -finaliseEqs (EqConfig {eqs = eqs, skolems = skolems}) - = do { eqs' <- substitute eqs - ; instantiateAndExtract eqs' skolems +finaliseEqsAndDicts :: EqConfig + -> TcM ([Inst], [Inst], TcDictBinds, Bool) +finaliseEqsAndDicts (EqConfig { eqs = eqs + , locals = locals + , wanteds = wanteds + , binds = binds + }) + = do { (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds + ; (eqs'', improved) <- instantiateAndExtract eqs' + ; return (locals', + eqs'' ++ wanteds', + subst_binds `unionBags` binds, + improved) } - --- |Normalise a set of class instances under a given equality configuration. --- Both the class instances and the equality configuration may change. The --- function returns 'Nothing' if neither changes. --- -normaliseDicts :: EqConfig -> [Inst] -> TcM (Maybe (EqConfig, [Inst])) -normaliseDicts = error "TcTyFuns.normaliseDicts" \end{code} @@ -253,10 +404,20 @@ rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args}) \end{code} The following functions turn an arbitrary equality into a set of normal -equalities. +equalities. This implements the WFlat and LFlat rules of the paper in one +sweep. However, we use flexible variables for both locals and wanteds, and +avoid to carry around the unflattening substitution \Sigma (for locals) by +already updating the skolems for locals with the family application that they +represent - i.e., they will turn into that family application on the next +zonking (which only happens after finalisation). + +In a corresponding manner, normDict normalises class dictionaries by +extracting any synonym family applications and generation appropriate normal +equalities. \begin{code} normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet) +-- Normalise one equality. normEqInst inst = ASSERT( isEqInst inst ) go ty1 ty2 (eqInstCoercion inst) @@ -313,6 +474,21 @@ normEqInst inst unionVarSets (ty2_skolems:args_skolemss)) } +normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet) +-- Normalise one dictionary or IP constraint. +normDict isWanted inst@(Dict {tci_pred = ClassP clas args}) + = do { (args', cargs, args_eqss, args_skolemss) + <- mapAndUnzip4M (flattenType inst) args + ; let rewriteCo = PredTy $ ClassP clas cargs + eqs = concat args_eqss + pred' = ClassP clas args' + ; (inst', bind, eqs') <- mkDictBind inst isWanted rewriteCo pred' eqs + ; return (inst', eqs', bind, unionVarSets args_skolemss) + } +normDict isWanted inst + = return (inst, [], emptyBag, emptyVarSet) +-- !!!TODO: Still need to normalise IP constraints. + checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst] -- Performs the occurs check, decomposition, and proper orientation -- (returns a singleton, or an empty list in case of a trivial equality) @@ -397,7 +573,8 @@ flattenType inst ty -- look through synonyms go ty | Just ty' <- tcView ty = go ty' - -- type family application => flatten to "id :: F t1'..tn' ~ alpha" + -- type family application + -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh) go ty@(TyConApp con args) | isOpenSynTyCon con = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args @@ -457,21 +634,74 @@ flattenType inst ty adjustCoercions :: EqInstCo -- coercion of original equality -> Coercion -- coercion witnessing the rewrite - -> (Type, Type) -- type sof flattened equality + -> (Type, Type) -- types of flattened equality -> [RewriteInst] -- equalities from flattening -> TcM (EqInstCo, -- coercion for flattened equality [RewriteInst]) -- final equalities from flattening -- Depending on whether we flattened a local or wanted equality, that equality's --- coercion and that of the new ones are adjusted +-- coercion and that of the new equalities produced during flattening are +-- adjusted . adjustCoercions co rewriteCo eqTys all_eqs + + -- wanted => generate a fresh coercion variable for the flattened equality | isWantedCo co = do { co' <- mkRightTransEqInstCo co rewriteCo eqTys ; return (co', all_eqs) } + + -- local => turn all new equalities into locals and update (but not zonk) + -- the skolem | otherwise - = return (co, map wantedToLocal all_eqs) + = do { all_eqs' <- mapM wantedToLocal all_eqs + ; return (co, all_eqs') + } + +mkDictBind :: Inst -- original instance + -> Bool -- is this a wanted contraint? + -> Coercion -- coercion witnessing the rewrite + -> PredType -- coerced predicate + -> [RewriteInst] -- equalities from flattening + -> TcM (Inst, -- new inst + TcDictBinds, -- binding for coerced dictionary + [RewriteInst]) -- final equalities from flattening +mkDictBind dict _isWanted _rewriteCo _pred [] + = return (dict, emptyBag, []) -- don't generate binding for an id coercion +mkDictBind dict isWanted rewriteCo pred eqs + = do { dict' <- newDictBndr loc pred + -- relate the old inst to the new one + -- target_dict = source_dict `cast` st_co + ; let (target_dict, source_dict, st_co) + | isWanted = (dict, dict', mkSymCoercion rewriteCo) + | otherwise = (dict', dict, rewriteCo) + -- we have + -- co :: dict ~ dict' + -- hence, if isWanted + -- dict = dict' `cast` sym co + -- else + -- dict' = dict `cast` co + expr = HsVar $ instToId source_dict + cast_expr = HsWrap (WpCast st_co) expr + rhs = L (instLocSpan loc) cast_expr + binds = instToDictBind target_dict rhs + ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs + ; return (dict', binds, eqs') + } where - wantedToLocal eq = eq {rwi_co = mkGivenCo (rwi_right eq)} + loc = tci_loc dict + +-- gamma :: Fam args ~ alpha +-- => alpha :: Fam args ~ alpha, with alpha := Fam args +-- (the update of alpha will not be apparent during propagation, as we +-- never follow the indirections of meta variables; it will be revealed +-- when the equality is zonked) +wantedToLocal :: RewriteInst -> TcM RewriteInst +wantedToLocal eq@(RewriteFam {rwi_fam = fam, + rwi_args = args, + rwi_right = alphaTy@(TyVarTy alpha)}) + = do { writeMetaTyVar alpha (mkTyConApp fam args) + ; return $ eq {rwi_co = mkGivenCo alphaTy} + } +wantedToLocal _ = panic "TcTyFuns.wantedToLocal" \end{code} @@ -698,32 +928,57 @@ applySubstVarFam _ _ = return Nothing %************************************************************************ Exhaustive substitution of all variable equalities of the form co :: x ~ t -(both local and wanted) into the left-hand sides all other equalities. This +(both local and wanted) into the left-hand sides of all other equalities. This may lead to recursive equalities; i.e., (1) we need to apply the substitution implied by one variable equality exhaustively before turning to the next and (2) we need an occurs check. -NB: Gievn that we apply the substitution corresponding to a single equality +We also apply the same substitutions to the local and wanted class and IP +dictionaries. + +NB: Given that we apply the substitution corresponding to a single equality exhaustively, before turning to the next, and because we eliminate recursive -eqaulities, all opportunities for subtitution will have been exhausted after +equalities, all opportunities for subtitution will have been exhausted after we have considered each equality once. \begin{code} -substitute :: [RewriteInst] -> TcM [RewriteInst] -substitute eqs = subst eqs [] +substitute :: [RewriteInst] -- equalities + -> [Inst] -- local class dictionaries + -> [Inst] -- wanted class dictionaries + -> TcM ([RewriteInst], -- equalities after substitution + TcDictBinds, -- all newly generated dictionary bindings + [Inst], -- local dictionaries after substitution + [Inst]) -- wanted dictionaries after substitution +substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds where - subst [] res = return res - subst (eq:eqs) res - = do { eqs' <- mapM (substOne eq) eqs - ; res' <- mapM (substOne eq) res - ; subst eqs' (eq:res') + subst [] res binds locals wanteds + = return (res, binds, locals, wanteds) + subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs) + res binds locals wanteds + = do { let coSubst = zipOpenTvSubst [tv] [eqInstCoType co] + tySubst = zipOpenTvSubst [tv] [ty] + ; eqs' <- mapM (substEq eq coSubst tySubst) eqs + ; res' <- mapM (substEq eq coSubst tySubst) res + ; (lbinds, locals') <- mapAndUnzipM + (substDict eq coSubst tySubst False) + locals + ; (wbinds, wanteds') <- mapAndUnzipM + (substDict eq coSubst tySubst True) + wanteds + ; let binds' = unionManyBags $ binds : lbinds ++ wbinds + ; subst eqs' (eq:res') binds' locals' wanteds' } - - -- apply [ty/tv] to left-hand side of eq2 - substOne (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) eq2 - = do { let co1Subst = mkSymCoercion $ - substTyWith [tv] [eqInstCoType co] (rwi_right eq2) - right2' = substTyWith [tv] [ty] (rwi_right eq2) + subst (eq:eqs) res binds locals wanteds + = subst eqs (eq:res) binds locals wanteds + + -- We have, co :: tv ~ ty + -- => apply [ty/tv] to right-hand side of eq2 + -- (but only if tv actually occurs in the right-hand side of eq2) + substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) + coSubst tySubst eq2 + | tv `elemVarSet` tyVarsOfType (rwi_right eq2) + = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2) + right2' = substTy tySubst (rwi_right eq2) left2 = case eq2 of RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2 RewriteFam {rwi_fam = fam, @@ -735,9 +990,28 @@ substitute eqs = subst eqs [] _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'} } - -- changed - substOne _ eq2 + -- unchanged + substEq _ _ _ eq2 = return eq2 + + -- We have, co :: tv ~ ty + -- => apply [ty/tv] to dictionary predicate + -- (but only if tv actually occurs in the predicate) + substDict (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) + coSubst tySubst isWanted dict + | isClassDict dict + , tv `elemVarSet` tyVarsOfPred (tci_pred dict) + = do { let co1Subst = mkSymCoercion $ + PredTy (substPred coSubst (tci_pred dict)) + pred' = substPred tySubst (tci_pred dict) + ; (dict', binds, _) <- mkDictBind dict isWanted co1Subst pred' [] + ; return (binds, dict') + } + + -- unchanged + substDict _ _ _ _ dict + = return (emptyBag, dict) +-- !!!TODO: Still need to substitute into IP constraints. \end{code} For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~ @@ -746,8 +1020,8 @@ Return all remaining wanted equalities. The Boolean result component is True if at least one instantiation of a flexible was performed. \begin{code} -instantiateAndExtract :: [RewriteInst] -> TyVarSet -> TcM ([Inst], Bool) -instantiateAndExtract eqs _skolems +instantiateAndExtract :: [RewriteInst] -> TcM ([Inst], Bool) +instantiateAndExtract eqs = do { let wanteds = filter (isWantedCo . rwi_co) eqs ; wanteds' <- mapM inst wanteds ; let residuals = catMaybes wanteds' @@ -775,9 +1049,9 @@ instantiateAndExtract eqs _skolems } where -- meta variable has been filled already - -- => panic (all equalities should have been zonked on normalisation) + -- => ignore (must be a skolem that was introduced by flattening locals) uMeta _swapped _tv (IndirectTv _) _ty _cotv - = panic "TcTyFuns.uMeta: expected zonked equalities" + = return Nothing -- type variable meets type variable -- => check that tv2 hasn't been updated yet and choose which to update @@ -873,1088 +1147,6 @@ instantiateAndExtract eqs _skolems \end{code} - -==================== CODE FOR THE OLD ICFP'08 ALGORITHM ====================== - -An elementary rewrite is a properly oriented equality with associated coercion -that has one of the following two forms: - -(1) co :: F t1..tn ~ t -(2) co :: a ~ t , where t /= F t1..tn and a is a skolem tyvar - -NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a -reqrite rule. Instead, such equalities are solved by unification. This is -essential; cf Note [skolemOccurs loop]. - -The following functions takes an equality instance and turns it into an -elementary rewrite if possible. - -\begin{code} -data Rewrite = Rewrite TcType -- lhs of rewrite rule - TcType -- rhs of rewrite rule - TcType -- coercion witnessing the rewrite rule - -eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool) - -- True iff rewrite swapped equality -eqInstToRewrite inst - = ASSERT( isEqInst inst ) - go ty1 ty2 (eqInstType inst) - where - (ty1,ty2) = eqInstTys inst - - -- look through synonyms - go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co - go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co - - -- left-to-right rule with type family head - go ty1@(TyConApp con _) ty2 co - | isOpenSynTyCon con - = Just (Rewrite ty1 ty2 co, False) -- not swapped - - -- left-to-right rule with type variable head - go ty1@(TyVarTy tv) ty2 co - | isSkolemTyVar tv - = Just (Rewrite ty1 ty2 co, False) -- not swapped - - -- right-to-left rule with type family head, only after - -- having checked whether we can work left-to-right - go ty1 ty2@(TyConApp con _) co - | isOpenSynTyCon con - = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped - - -- right-to-left rule with type variable head, only after - -- having checked whether we can work left-to-right - go ty1 ty2@(TyVarTy tv) co - | isSkolemTyVar tv - = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped - - -- this equality is not a rewrite rule => ignore - go _ _ _ = Nothing -\end{code} - -Normalise a type relative to an elementary rewrite implied by an EqInst or an -explicitly given elementary rewrite. - -\begin{code} --- Rewrite by EqInst --- Precondition: the EqInst passes the occurs check -tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType) -tcEqInstNormaliseFamInst inst ty - = case eqInstToRewrite inst of - Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty - Nothing -> return (IdCo, ty) - --- Rewrite by equality rewrite rule -tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite - -> TcType -- type to rewrite - -> TcM (CoercionI, -- witnessing coercion - TcType) -- rewritten type -tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty - = tcGenericNormaliseFamInst matchEqRule ty - where - matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co) - | otherwise = return $ Nothing -\end{code} - -Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and -apply the normalisation function gives as the first argument to every TyConApp -and every TyVarTy subterm. - - tcGenericNormaliseFamInst fun ty = (co, ty') - then co : ty ~ ty' - -This function is (by way of using smart constructors) careful to ensure that -the returned coercion is exactly IdCo (and not some semantically equivalent, -but syntactically different coercion) whenever (ty' `tcEqType` ty). This -makes it easy for the caller to determine whether the type changed. BUT -even if we return IdCo, ty' may be *syntactically* different from ty due to -unfolded closed type synonyms (by way of tcCoreView). In the interest of -good error messages, callers should discard ty' in favour of ty in this case. - -\begin{code} -tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion))) - -- what to do with type functions and tyvars - -> TcType -- old type - -> TcM (CoercionI, TcType) -- (coercion, new type) -tcGenericNormaliseFamInst fun ty - | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty' -tcGenericNormaliseFamInst fun (TyConApp tyCon tys) - = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys - ; let tycon_coi = mkTyConAppCoI tyCon ntys cois - ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args! - ; case maybe_ty_co of - -- a matching family instance exists - Just (ty', co) -> - do { let first_coi = mkTransCoI tycon_coi (ACo co) - ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty' - ; let fix_coi = mkTransCoI first_coi rest_coi - ; return (fix_coi, nty) - } - -- no matching family instance exists - -- we do not do anything - Nothing -> return (tycon_coi, mkTyConApp tyCon ntys) - } -tcGenericNormaliseFamInst fun (AppTy ty1 ty2) - = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1 - ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2 - ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2) - } -tcGenericNormaliseFamInst fun (FunTy ty1 ty2) - = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1 - ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2 - ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2) - } -tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1) - = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1 - ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1) - } -tcGenericNormaliseFamInst fun ty@(TyVarTy tv) - | isTcTyVar tv - = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty) - ; res <- lookupTcTyVar tv - ; case res of - DoneTv _ -> - do { maybe_ty' <- fun ty - ; case maybe_ty' of - Nothing -> return (IdCo, ty) - Just (ty', co1) -> - do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty' - ; return (ACo co1 `mkTransCoI` coi2, ty'') - } - } - IndirectTv ty' -> tcGenericNormaliseFamInst fun ty' - } - | otherwise - = return (IdCo, ty) -tcGenericNormaliseFamInst fun (PredTy predty) - = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty - ; return (coi, PredTy pred') } - ---------------------------------- -tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion))) - -> TcPredType - -> TcM (CoercionI, TcPredType) - -tcGenericNormaliseFamInstPred fun (ClassP cls tys) - = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys - ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys') - } -tcGenericNormaliseFamInstPred fun (IParam ipn ty) - = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty - ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty') - } -tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2) - = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1 - ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2 - ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') } -\end{code} - - -%************************************************************************ -%* * -\section{Normalisation of equality constraints} -%* * -%************************************************************************ - -Note [Inconsistencies in equality constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We guarantee that we raise an error if we discover any inconsistencies (i.e., -equalities that if presented to the unifer in TcUnify would result in an -error) during normalisation of wanted constraints. This is especially so that -we don't solve wanted constraints under an inconsistent given set. In -particular, we don't want to permit signatures, such as - - bad :: (Int ~ Bool => Int) -> a -> a - -\begin{code} -normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ()) -normaliseGivenEqs givens - = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens) - ; (result, deSkolem) <- - rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs)) - [ ("(ZONK)", dontRerun $ zonkInsts) - , ("(TRIVIAL)", dontRerun $ trivialRule) - , ("(DECOMP)", decompRule) - , ("(TOP)", topRule) - , ("(SUBST)", substRule) -- incl. occurs check - ] givens - ; traceTc (text "normaliseGivenEqs ->" <+> ppr result) - ; return (result, deSkolem) - } -\end{code} - -\begin{code} -normaliseWantedEqs :: [Inst] -- givens - -> [Inst] -- wanteds - -> TcM [Inst] -- irreducible wanteds -normaliseWantedEqs givens wanteds - = do { traceTc $ text "normaliseWantedEqs <-" <+> ppr wanteds - <+> text "with" <+> ppr givens - ; result <- liftM fst $ rewriteToFixedPoint Nothing - [ ("(ZONK)", dontRerun $ zonkInsts) - , ("(TRIVIAL)", dontRerun $ trivialRule) - , ("(DECOMP)", decompRule) - , ("(TOP)", topRule) - , ("(GIVEN)", substGivens givens) -- incl. occurs check - , ("(UNIFY)", unifyMetaRule) -- incl. occurs check - , ("(SUBST)", substRule) -- incl. occurs check - ] wanteds - ; traceTc (text "normaliseWantedEqs ->" <+> ppr result) - ; return result - } - where - -- Use `substInst' with every given on all the wanteds. - substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool) - substGivens [] wanteds = return (wanteds, False) - substGivens (g:gs) wanteds - = do { (wanteds1, changed1) <- substGivens gs wanteds - ; (wanteds2, changed2) <- substInst g wanteds1 - ; return (wanteds2, changed1 || changed2) - } -\end{code} - - -%************************************************************************ -%* * -\section{Normalisation of non-equality dictionaries} -%* * -%************************************************************************ - -\begin{code} -normaliseGivenDicts, normaliseWantedDicts - :: [Inst] -- given equations - -> [Inst] -- dictionaries - -> TcM ([Inst],TcDictBinds) - -normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False -normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True - -normalise_dicts - :: [Inst] -- given equations - -> [Inst] -- dictionaries - -> Bool -- True <=> the dicts are wanted - -- Fals <=> they are given - -> TcM ([Inst],TcDictBinds) -normalise_dicts given_eqs dicts is_wanted - = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-" - | otherwise = "normaliseGivenDicts <-" - in - text name <+> ppr dicts <+> - text "with" <+> ppr given_eqs - ; (dicts0, binds0) <- normaliseInsts is_wanted dicts - ; (dicts1, binds1) <- substEqInDictInsts is_wanted given_eqs dicts0 - ; let binds01 = binds0 `unionBags` binds1 - ; if isEmptyBag binds1 - then return (dicts1, binds01) - else do { (dicts2, binds2) <- - normalise_dicts given_eqs dicts1 is_wanted - ; return (dicts2, binds01 `unionBags` binds2) } } -\end{code} - - -%************************************************************************ -%* * -\section{Normalisation rules and iterative rule application} -%* * -%************************************************************************ - -We have three kinds of normalising rewrite rules: - -(1) Normalisation rules that rewrite a set of insts and return a flag indicating - whether any changes occurred during rewriting that necessitate re-running - the current rule set. - -(2) Precondition rules that rewrite a set of insts and return a monadic action - that reverts the effect of preconditioning. - -(3) Idempotent normalisation rules that never require re-running the rule set. - -\begin{code} -type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run -type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable -type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run - -type NamedRule = (String, RewriteRule) -- rule with description -type NamedPreRule = (String, PrecondRule) -- precond with desc -\end{code} - -Template lifting idempotent rules to full rules (which can be put into a rule -set). - -\begin{code} -dontRerun :: IdemRewriteRule -> RewriteRule -dontRerun rule insts = liftM addFalse $ rule insts - where - addFalse x = (x, False) -\end{code} - -The following function applies a set of rewrite rules until a fixed point is -reached; i.e., none of the `RewriteRule's require re-running the rule set. -Optionally, there may be a pre-conditing rule that is applied before any other -rules are applied and before the rule set is re-run. - -The result is the set of rewritten (i.e., normalised) insts and, in case of a -pre-conditing rule, a monadic action that reverts the effects of -pre-conditioning - specifically, this is removing introduced skolems. - -\begin{code} -rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule - -> [NamedRule] -- rule set - -> [Inst] -- insts to rewrite - -> TcM ([Inst], TcM ()) -rewriteToFixedPoint precondRule rules insts - = completeRewrite (return ()) precondRule insts - where - completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst] - -> TcM ([Inst], TcM ()) - completeRewrite dePrecond (Just (precondName, precond)) insts - = do { traceTc $ text precondName <+> text " <- " <+> ppr insts - ; (insts', dePrecond') <- precond insts - ; traceTc $ text precondName <+> text " -> " <+> ppr insts' - ; tryRules (dePrecond >> dePrecond') rules insts' - } - completeRewrite dePrecond Nothing insts - = tryRules dePrecond rules insts - - tryRules dePrecond _ [] = return ([] , dePrecond) - tryRules dePrecond [] insts = return (insts, dePrecond) - tryRules dePrecond ((name, rule):rules) insts - = do { traceTc $ text name <+> text " <- " <+> ppr insts - ; (insts', rerun) <- rule insts - ; traceTc $ text name <+> text " -> " <+> ppr insts' - ; if rerun then completeRewrite dePrecond precondRule insts' - else tryRules dePrecond rules insts' - } -\end{code} - - -%************************************************************************ -%* * -\section{Different forms of Inst rewrite rules} -%* * -%************************************************************************ - -Splitting of non-terminating given constraints: skolemOccurs -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -This is a preconditioning rule exclusively applied to given constraints. -Moreover, its rewriting is only temporary, as it is undone by way of -side-effecting mutable type variables after simplification and constraint -entailment has been completed. - -This version is an (attempt at, yet unproven, an) *unflattened* version of -the SubstL-Ev completion rule. - -The above rule is essential to catch non-terminating rules that cannot be -oriented properly, like - - F a ~ [G (F a)] - or even - a ~ [G a] , where a is a skolem tyvar - -The left-to-right orientiation is not suitable because it does not -terminate. The right-to-left orientation is not suitable because it -does not have a type-function on the left. This is undesirable because -it would hide information. E.g. assume - - instance C [x] - -then rewriting C [G (F a)] to C (F a) is bad because we cannot now -see that the C [x] instance applies. - -The rule also caters for badly-oriented rules of the form: - - F a ~ G (F a) - -for which other solutions are possible, but this one will do too. - -It's behavior is: - - co : ty1 ~ ty2{F ty1} - >--> - co : ty1 ~ ty2{b} - sym (F co) : F ty2{b} ~ b - where b is a fresh skolem variable - -We also cater for the symmetric situation *if* the rule cannot be used as a -left-to-right rewrite rule. - -We also return an action (b := ty1) which is used to eliminate b -after the dust of normalisation with the completed rewrite system -has settled. - -A subtle point of this transformation is that both coercions in the results -are strictly speaking incorrect. However, they are correct again after the -action {B := ty1} has removed the skolem again. This happens immediately -after constraint entailment has been checked; ie, code outside of the -simplification and entailment checking framework will never see these -temporarily incorrect coercions. - -NB: We perform this transformation for multiple occurences of ty1 under one - or multiple family applications on the left-hand side at once (ie, the - rule doesn't need to be applied multiple times at a single inst). As a - result we can get two or more insts back. - -Note [skolemOccurs loop] -~~~~~~~~~~~~~~~~~~~~~~~~ -You might think that under - - type family F a - type instance F [a] = [F a] - -a signature such as - - foo :: (F [a] ~ a) => a - -will get us into a loop. However, this is *not* the case. Here is why: - - F [a] ~ a - - -->(TOP) - - [F a] ~ a - - -->(SkolemOccurs) - - [b] ~ a - F [b] ~ b , with b := F a - - -->(TOP) - - [b] ~ a - [F b] ~ b , with b := F a - -At this point (SkolemOccurs) does *not* apply anymore, as - - [F b] ~ b - -is not used as a rewrite rule. The variable b is not a skolem (cf -eqInstToRewrite). - -(The regression test indexed-types/should_compile/Simple20 checks that the -described property of the system does not change.) - -\begin{code} -skolemOccurs :: PrecondRule -skolemOccurs insts - = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts - ; return (concat instss, sequence_ undoSkolems) - } - where - oneSkolemOccurs inst - = ASSERT( isEqInst inst ) - case eqInstToRewrite inst of - Just (rewrite, swapped) -> breakRecursion rewrite swapped - Nothing -> return ([inst], return ()) - where - -- inst is an elementary rewrite rule, check whether we need to break - -- it up - breakRecursion (Rewrite pat body _) swapped - - -- skolemOccurs does not apply, leave as is - | null tysToLiftOut - = do { traceTc $ text "oneSkolemOccurs: no tys to lift out" - ; return ([inst], return ()) - } - - -- recursive occurence of pat in body under a type family application - | otherwise - = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut - ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut - ; let skTvs_tysTLO = zip skTvs tysToLiftOut - insertSkolems = return . replace skTvs_tysTLO - ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body - ; inst' <- if swapped then mkEqInst (EqPred body' pat) co - else mkEqInst (EqPred pat body') co - -- ensure to reconstruct the inst in the - -- original orientation - ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst' - ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst') - skTvs_tysTLO - ; return (inst':insts, sequence_ undoSk) - } - where - co = eqInstCoercion inst - - -- all subtypes that are (1) type family instances and (2) contain - -- the lhs type as part of the type arguments of the type family - -- constructor - tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body - , any (pat `tcPartOfType`) tys] - - replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion) - replace [] _ = Nothing - replace ((skTv, tyTLO):rest) ty - | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined) - | otherwise = replace rest ty - - -- create the EqInst for the equality determining the skolem and a - -- TcM action undoing the skolem introduction - mkSkolemInst inst' (skTv, tyTLO) - = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO - ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv)) - (mkGivenCo $ mkSymCoercion (fromACo co)) - -- co /= IdCo due to construction of inst' - ; return (inst, writeMetaTyVar skTv tyTLO) - } -\end{code} - - -Removal of trivial equalities: trivialRule -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The following rules exploits the reflexivity of equality: - - (Trivial) - g1 : t ~ t - >--> - g1 := t - -\begin{code} -trivialRule :: IdemRewriteRule -trivialRule insts - = liftM catMaybes $ mapM trivial insts - where - trivial inst - | ASSERT( isEqInst inst ) - ty1 `tcEqType` ty2 - = do { eitherEqInst inst - (\cotv -> writeMetaTyVar cotv ty1) - (\_ -> return ()) - ; return Nothing - } - | otherwise - = return $ Just inst - where - (ty1,ty2) = eqInstTys inst -\end{code} - - -Decomposition of data type constructors: decompRule -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Whenever, the same *data* constructors occurs on both sides of an equality, we -can decompose as in standard unification. - - (Decomp) - g1 : T cs ~ T ds - >--> - g21 : c1 ~ d1, ..., g2n : cn ~ dn - g1 := T g2s - -Works also for the case where T is actually an application of a type family -constructor to a set of types, provided the applications on both sides of the -~ are identical; see also Note [OpenSynTyCon app] in TcUnify. - -We guarantee to raise an error for any inconsistent equalities; -cf Note [Inconsistencies in equality constraints]. - -\begin{code} -decompRule :: RewriteRule -decompRule insts - = do { (insts, changed) <- mapAndUnzipM decomp insts - ; return (concat insts, or changed) - } - where - decomp inst - = ASSERT( isEqInst inst ) - go ty1 ty2 - where - (ty1,ty2) = eqInstTys inst - go ty1 ty2 - | Just ty1' <- tcView ty1 = go ty1' ty2 - | Just ty2' <- tcView ty2 = go ty1 ty2' - - go (TyConApp con1 tys1) (TyConApp con2 tys2) - | con1 == con2 && identicalHead - = mkArgInsts (mkTyConApp con1) tys1 tys2 - - | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2) - -- not matching data constructors (of any flavour) are bad news - = eqInstMisMatch inst - where - n = tyConArity con1 - (idxTys1, _) = splitAt n tys1 - (idxTys2, _) = splitAt n tys2 - identicalHead = not (isOpenSynTyCon con1) || - idxTys1 `tcEqTypes` idxTys2 - - go (FunTy fun1 arg1) (FunTy fun2 arg2) - = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1] - [fun2, arg2] - - -- Applications need a bit of care! - -- They can match FunTy and TyConApp, so use splitAppTy_maybe - go (AppTy s1 t1) ty2 - | Just (s2, t2) <- tcSplitAppTy_maybe ty2 - = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2] - - -- Symmetric case - go ty1 (AppTy s2 t2) - | Just (s1, t1) <- tcSplitAppTy_maybe ty1 - = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2] - - -- We already covered all the consistent cases of rigid types on both - -- sides; so, if we see two rigid types here, we discovered an - -- inconsistency. - go ty1 ty2 - | isRigid ty1 && isRigid ty2 - = eqInstMisMatch inst - - -- We can neither assert consistency nor inconsistency => defer - go _ _ = return ([inst], False) - - isRigid (TyConApp con _) = not (isOpenSynTyCon con) - isRigid (FunTy _ _) = True - isRigid (AppTy _ _) = True - isRigid _ = False - - -- Create insts for matching argument positions (ie, the bit after - -- '>-->' in the rule description above) - mkArgInsts con tys1 tys2 - = do { cos <- eitherEqInst inst - -- old_co := Con1 cos - (\old_covar -> - do { cotvs <- zipWithM newMetaCoVar tys1 tys2 - ; let cos = map mkTyVarTy cotvs - ; writeMetaTyVar old_covar (con cos) - ; return $ map mkWantedCo cotvs - }) - -- co_i := Con_i old_co - (\old_co -> - return $ map mkGivenCo $ - mkRightCoercions (length tys1) old_co) - ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos - ; traceTc (text "decomp identicalHead" <+> ppr insts) - ; return (insts, not $ null insts) - } -\end{code} - - -Rewriting with type instances: topRule -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We use (toplevel) type instances to normalise both sides of equalities. - - (Top) - g1 : t ~ s - >--> co1 :: t ~ t' / co2 :: s ~ s' - g2 : t' ~ s' - g1 := co1 * g2 * sym co2 - -\begin{code} -topRule :: RewriteRule -topRule insts - = do { (insts, changed) <- mapAndUnzipM top insts - ; return (insts, or changed) - } - where - top inst - = ASSERT( isEqInst inst ) - do { (coi1, ty1') <- tcNormaliseFamInst ty1 - ; (coi2, ty2') <- tcNormaliseFamInst ty2 - ; case (coi1, coi2) of - (IdCo, IdCo) -> return (inst, False) - _ -> - do { wg_co <- - eitherEqInst inst - -- old_co = co1 * new_co * sym co2 - (\old_covar -> - do { new_cotv <- newMetaCoVar ty1' ty2' - ; let new_co = mkTyVarTy new_cotv - old_coi = coi1 `mkTransCoI` - ACo new_co `mkTransCoI` - (mkSymCoI coi2) - ; writeMetaTyVar old_covar (fromACo old_coi) - ; return $ mkWantedCo new_cotv - }) - -- new_co = sym co1 * old_co * co2 - (\old_co -> - return $ - mkGivenCo $ - fromACo $ - mkSymCoI coi1 `mkTransCoI` - ACo old_co `mkTransCoI` coi2) - ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co - ; return (new_inst, True) - } - } - where - (ty1,ty2) = eqInstTys inst -\end{code} - - -Rewriting with equalities: substRule -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -From a set of insts, use all insts that can be read as rewrite rules to -rewrite the types in all other insts. - - (Subst) - g : F c ~ t, - forall g1 : s1{F c} ~ s2{F c} - >--> - g2 : s1{t} ~ s2{t} - g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g} - -Alternatively, the rewrite rule may have the form (g : a ~ t). - -To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a), -where t is neither a variable nor a type family application, we use them for -rewriting from right-to-left. However, it is crucial to only apply rules -from right-to-left if they cannot be used left-to-right. - -The workhorse is substInst, which performs an occurs check before actually -using an equality for rewriting. If the type pattern occurs in the type we -substitute for the pattern, normalisation would diverge. - -\begin{code} -substRule :: RewriteRule -substRule insts = tryAllInsts insts [] - where - -- for every inst check whether it can be used to rewrite the others - -- (we make an effort to keep the insts in order; it makes debugging - -- easier) - tryAllInsts [] triedInsts = return (reverse triedInsts, False) - tryAllInsts (inst:insts) triedInsts - = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts) - ; if changed then return (insertAt (length triedInsts) inst insts', - True) - else tryAllInsts insts (inst:triedInsts) - } - where - insertAt n x xs = let (xs1, xs2) = splitAt n xs - in xs1 ++ [x] ++ xs2 - --- Use the given inst as a rewrite rule to normalise the insts in the second --- argument. Don't do anything if the inst cannot be used as a rewrite rule, --- but do apply it right-to-left, if possible, and if it cannot be used --- left-to-right. --- -substInst :: Inst -> [Inst] -> TcM ([Inst], Bool) -substInst inst insts - = case eqInstToRewrite inst of - Just (rewrite, _) -> substEquality rewrite insts - Nothing -> return (insts, False) - where - substEquality :: Rewrite -- elementary rewrite - -> [Inst] -- insts to rewrite - -> TcM ([Inst], Bool) - substEquality eqRule@(Rewrite pat rhs _) insts - | pat `tcPartOfType` rhs -- occurs check! - = occurCheckErr pat rhs - | otherwise - = do { (insts', changed) <- mapAndUnzipM substOne insts - ; return (insts', or changed) - } - where - substOne inst - = ASSERT( isEqInst inst ) - do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1 - ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2 - ; case (coi1, coi2) of - (IdCo, IdCo) -> return (inst, False) - _ -> - do { gw_co <- - eitherEqInst inst - -- old_co := co1 * new_co * sym co2 - (\old_covar -> - do { new_cotv <- newMetaCoVar ty1' ty2' - ; let new_co = mkTyVarTy new_cotv - old_coi = coi1 `mkTransCoI` - ACo new_co `mkTransCoI` - (mkSymCoI coi2) - ; writeMetaTyVar old_covar (fromACo old_coi) - ; return $ mkWantedCo new_cotv - }) - -- new_co := sym co1 * old_co * co2 - (\old_co -> - return $ - mkGivenCo $ - fromACo $ - mkSymCoI coi1 `mkTransCoI` - ACo old_co `mkTransCoI` coi2) - ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co - ; return (new_inst, True) - } - } - where - (ty1,ty2) = eqInstTys inst -\end{code} - - -Instantiate meta variables: unifyMetaRule -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If an equality equates a meta type variable with a type, we simply instantiate -the meta variable. - - (UnifyMeta) - g : alpha ~ t - >--> - alpha := t - g := t - -Meta variables can only appear in wanted constraints, and this rule should -only be applied to wanted constraints. We also know that t definitely is -distinct from alpha (as the trivialRule) has been run on the insts beforehand. - -NB: We cannot assume that meta tyvars are empty. They may have been updated -by another inst in the currently processed wanted list. We need to be very -careful when updateing type variables (see TcUnify.uUnfilledVar), but at least -we know that we have no boxes. It's unclear that it would be an advantage to -common up the code in TcUnify and the code below. Firstly, we don't want -calls to TcUnify.defer_unification here, and secondly, TcUnify import the -current module, so we would have to move everything here (Yuk!) or to -TcMType. Besides, the code here is much simpler due to the lack of boxes. - -\begin{code} -unifyMetaRule :: RewriteRule -unifyMetaRule insts - = do { (insts', changed) <- mapAndUnzipM unifyMeta insts - ; return (concat insts', or changed) - } - where - unifyMeta inst - = ASSERT( isEqInst inst ) - go ty1 ty2 - (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst) - where - (ty1,ty2) = eqInstTys inst - go ty1 ty2 cotv - | Just ty1' <- tcView ty1 = go ty1' ty2 cotv - | Just ty2' <- tcView ty2 = go ty1 ty2' cotv - - | TyVarTy tv1 <- ty1 - , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1 - ; uMeta False tv1 lookupTV ty2 cotv - } - | TyVarTy tv2 <- ty2 - , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2 - ; uMeta True tv2 lookupTV ty1 cotv - } - | otherwise = return ([inst], False) - - -- meta variable has been filled already - -- => ignore this inst (we'll come around again, after zonking) - uMeta _swapped _tv (IndirectTv _) _ty _cotv - = return ([inst], False) - - -- type variable meets type variable - -- => check that tv2 hasn't been updated yet and choose which to update - uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv - | tv1 == tv2 - = return ([inst], False) -- The two types are already identical - - | otherwise - = do { lookupTV2 <- lookupTcTyVar tv2 - ; case lookupTV2 of - IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv - DoneTv details2 -> uMetaVar swapped tv1 details1 tv2 details2 cotv - } - - ------ Beyond this point we know that ty2 is not a type variable - - -- signature skolem meets non-variable type - -- => cannot update! - uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv - = return ([inst], False) - - -- updatable meta variable meets non-variable type - -- => occurs check, monotype check, and kinds match check, then update - uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv - = do { mb_ty' <- checkTauTvUpdate tv non_tv_ty -- occurs + monotype check - ; case mb_ty' of - Nothing -> return ([inst], False) -- tv occurs in faminst - Just ty' -> - do { checkUpdateMeta swapped tv ref ty' -- update meta var - ; writeMetaTyVar cotv ty' -- update co var - ; return ([], True) - } - } - - uMeta _ _ _ _ _ = panic "uMeta" - - -- uMetaVar: unify two type variables - -- meta variable meets skolem - -- => just update - uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv - = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2) - ; writeMetaTyVar cotv (mkTyVarTy tv2) - ; return ([], True) - } - - -- meta variable meets meta variable - -- => be clever about which of the two to update - -- (from TcUnify.uUnfilledVars minus boxy stuff) - uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv - = do { case (info1, info2) of - -- Avoid SigTvs if poss - (SigTv _, _ ) | k1_sub_k2 -> update_tv2 - (_, SigTv _) | k2_sub_k1 -> update_tv1 - - (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1 - then update_tv1 -- Same kinds - else update_tv2 - | k2_sub_k1 -> update_tv1 - | otherwise -> kind_err - -- Update the variable with least kind info - -- See notes on type inference in Kind.lhs - -- The "nicer to" part only applies if the two kinds are the same, - -- so we can choose which to do. - - ; writeMetaTyVar cotv (mkTyVarTy tv2) - ; return ([], True) - } - where - -- Kinds should be guaranteed ok at this point - update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2) - update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1) - - kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $ - unifyKindMisMatch k1 k2 - - k1 = tyVarKind tv1 - k2 = tyVarKind tv2 - k1_sub_k2 = k1 `isSubKind` k2 - k2_sub_k1 = k2 `isSubKind` k1 - - nicer_to_update_tv1 = isSystemName (Var.varName tv1) - -- Try to update sys-y type variables in preference to ones - -- gotten (say) by instantiating a polymorphic function with - -- a user-written type sig - - uMetaVar _ _ _ _ _ _ = panic "uMetaVar" -\end{code} - - -%************************************************************************ -%* * -\section{Normalisation of Insts} -%* * -%************************************************************************ - -Normalises a set of dictionaries relative to a set of given equalities (which -are interpreted as rewrite rules). We only consider given equalities of the -form - - F ts ~ t or a ~ t - -where F is a type family. - -\begin{code} -substEqInDictInsts :: Bool -- whether the *dictionaries* are wanted/given - -> [Inst] -- given equalities (used as rewrite rules) - -> [Inst] -- dictinaries to be normalised - -> TcM ([Inst], TcDictBinds) -substEqInDictInsts isWanted eqInsts dictInsts - = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts) - ; dictInsts' <- - foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts - ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts') - ; return dictInsts' - } - where - -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting - rewriteWithOneEquality (dictInsts, dictBinds) - eqInst@(EqInst {tci_left = pattern, - tci_right = target}) - | isOpenSynTyConApp pattern || isTyVarTy pattern - = do { (dictInsts', moreDictBinds) <- - genericNormaliseInsts isWanted applyThisEq dictInsts - ; return (dictInsts', dictBinds `unionBags` moreDictBinds) - } - where - applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult) - - -- rewrite in case of an exact match - matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst) - | otherwise = Nothing - - -- (2) Given equality has the wrong form: ignore - rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule - = return (dictInsts, dictBinds) -\end{code} - - -Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level -type-function equations, where - - (norm_insts, binds) = normaliseInsts is_wanted insts - -If 'is_wanted' - = True, (binds + norm_insts) defines insts (wanteds) - = False, (binds + insts) defines norm_insts (givens) - -Ie, in the case of normalising wanted dictionaries, we use the normalised -dictionaries to define the originally wanted ones. However, in the case of -given dictionaries, we use the originally given ones to define the normalised -ones. - -\begin{code} -normaliseInsts :: Bool -- True <=> wanted insts - -> [Inst] -- wanted or given insts - -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings -normaliseInsts isWanted insts - = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts - -genericNormaliseInsts :: Bool -- True <=> wanted insts - -> (TcPredType -> TcM (CoercionI, TcPredType)) - -- how to normalise - -> [Inst] -- wanted or given insts - -> TcM ([Inst], TcDictBinds) -- normalised insts & binds -genericNormaliseInsts isWanted fun insts - = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts - ; return (insts', unionManyBags binds) - } - where - normaliseOneInst isWanted fun - dict@(Dict {tci_pred = pred, - tci_loc = loc}) - = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict - ; (coi, pred') <- fun pred - - ; case coi of - IdCo -> - do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict - ; return (dict, emptyBag) - } - -- don't use pred' in this case; otherwise, we get - -- more unfolded closed type synonyms in error messages - ACo co -> - do { -- an inst for the new pred - ; dict' <- newDictBndr loc pred' - -- relate the old inst to the new one - -- target_dict = source_dict `cast` st_co - ; let (target_dict, source_dict, st_co) - | isWanted = (dict, dict', mkSymCoercion co) - | otherwise = (dict', dict, co) - -- we have - -- co :: dict ~ dict' - -- hence, if isWanted - -- dict = dict' `cast` sym co - -- else - -- dict' = dict `cast` co - expr = HsVar $ instToId source_dict - cast_expr = HsWrap (WpCast st_co) expr - rhs = L (instLocSpan loc) cast_expr - binds = instToDictBind target_dict rhs - -- return the new inst - ; traceTc $ let name | isWanted - = "genericNormaliseInst (wanted) ->" - | otherwise - = "genericNormaliseInst (given) ->" - in - text name <+> ppr dict' <+> - text "with" <+> ppr binds - ; return (dict', binds) - } - } - - -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst?? - normaliseOneInst _isWanted _fun inst - = do { inst' <- zonkInst inst - ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+> - ppr inst - ; return (inst', emptyBag) - } -\end{code} - - %************************************************************************ %* * \section{Errors} -- 1.7.10.4