From: simonpj@microsoft.com Date: Mon, 13 Sep 2010 10:34:26 +0000 (+0000) Subject: Remove two old junk files X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;h=12864264ace606f45b238ec07cbdc724f654b213;p=ghc-hetmet.git Remove two old junk files --- diff --git a/compiler/typecheck/TcTyFuns.lhs-old b/compiler/typecheck/TcTyFuns.lhs-old deleted file mode 100644 index aa038af..0000000 --- a/compiler/typecheck/TcTyFuns.lhs-old +++ /dev/null @@ -1,1685 +0,0 @@ -Normalisation of type terms relative to type instances as well as -normalisation and entailment checking of equality constraints. - -\begin{code} -module TcTyFuns ( - -- type normalisation wrt to toplevel equalities only - tcNormaliseFamInst, - - -- instance normalisation wrt to equalities - tcReduceEqs, - - -- errors - misMatchMsg, failWithMisMatch, - -) where - - -#include "HsVersions.h" - ---friends -import TcRnMonad -import TcEnv -import Inst -import TcType -import TcMType - --- GHC -import Coercion -import Type -import TypeRep ( Type(..) ) -import TyCon -import HsSyn -import VarEnv -import VarSet -import Var -import Name -import Bag -import Outputable -import SrcLoc ( Located(..) ) -import Maybes -import FastString - --- standard -import Data.List -import Control.Monad -\end{code} - - -%************************************************************************ -%* * - Normalisation of types wrt toplevel equality schemata -%* * -%************************************************************************ - -Unfold a single synonym family instance and yield the witnessing coercion. -Return 'Nothing' if the given type is either not synonym family instance -or is a synonym family instance that has no matching instance declaration. -(Applies only if the type family application is outermost.) - -For example, if we have - - :Co:R42T a :: T [a] ~ :R42T a - -then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int). - -\begin{code} -tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion)) -tcUnfoldSynFamInst (TyConApp tycon tys) - | not (isSynFamilyTyCon tycon) -- unfold *only* _synonym_ family instances - = return Nothing - | otherwise - = do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst - ; maybeFamInst <- tcLookupFamInst tycon tys - ; case maybeFamInst of - Nothing -> return Nothing - Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys, - mkTyConApp coe_tc rep_tys) - where - coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst" - (tyConFamilyCoercion_maybe rep_tc) - } -tcUnfoldSynFamInst _other = return Nothing -\end{code} - -Normalise 'Type's and 'PredType's by unfolding type family applications where -possible (ie, we treat family instances as a TRS). Also zonk meta variables. - - tcNormaliseFamInst ty = (co, ty') - then co : ty ~ ty' - -\begin{code} --- |Normalise the given type as far as possible with toplevel equalities. --- This results in a coercion witnessing the type equality, in addition to the --- normalised type. --- -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. - -\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 -%* * -%************************************************************************ - -Given a set of given, local constraints and a set of wanted constraints, -simplify the wanted equalities as far as possible and normalise both local and -wanted dictionaries with respect to the equalities. - -In addition to the normalised local dictionaries and simplified wanteds, the -function yields bindings for instantiated meta variables (due to solving -equality constraints) and dictionary bindings (due to simplifying class -constraints). The bag of type variable bindings only contains bindings for -non-local variables - i.e., type variables other than those newly created by -the present function. Consequently, type improvement took place iff the bag -of bindings contains any bindings for proper type variables (not just covars). -The solver does not instantiate any non-local variables; i.e., the bindings -must be executed by the caller. - -All incoming constraints are assumed to be zonked already. All outgoing -constraints will be zonked again. - -NB: The solver only has local effects that cannot be observed from outside. - In particular, it can be executed twice on the same constraint set with - the same result (modulo generated variables names). - -\begin{code} -tcReduceEqs :: [Inst] -- locals - -> [Inst] -- wanteds - -> TcM ([Inst], -- normalised locals (w/o equalities) - [Inst], -- normalised wanteds (including equalities) - TcTyVarBinds, -- bindings for meta type variables - TcDictBinds) -- bindings for all simplified dictionaries -tcReduceEqs locals wanteds - = do { ((locals, wanteds, dictBinds), tyBinds) <- getTcTyVarBinds $ - 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 freeFlexibles eqCfg - } - -- execute type bindings of skolem flexibles... - ; tyBinds_pruned <- pruneTyBinds tyBinds freeFlexibles - -- ...and zonk the constraints to propagate the bindings - ; locals_z <- zonkInsts locals - ; wanteds_z <- zonkInsts wanteds - ; return (locals_z, wanteds_z, tyBinds_pruned, dictBinds) - } - where - -- unification variables that appear in the environment and may not be - -- instantiated - this includes coercion variables - freeFlexibles = tcTyVarsOfInsts locals `unionVarSet` - tcTyVarsOfInsts wanteds - - pruneTyBinds tybinds freeFlexibles - = do { let tybinds' = bagToList tybinds - (skolem_tybinds, env_tybinds) = partition isSkolem tybinds' - ; execTcTyVarBinds (listToBag skolem_tybinds) - ; return $ listToBag env_tybinds - } - where - isSkolem (TcTyVarBind tv _ ) = not (tv `elemVarSet` freeFlexibles) -\end{code} - - -%************************************************************************ -%* * - Equality Configurations -%* * -%************************************************************************ - -We maintain normalised equalities together with the skolems introduced as -intermediates during flattening of equalities as well as - -\begin{code} --- |Configuration of normalised equalities used during solving. --- -data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities - , locals :: [Inst] -- given dicts - , wanteds :: [Inst] -- wanted dicts - , binds :: TcDictBinds -- bindings - } - -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 - } - -emptyEqConfig :: EqConfig -emptyEqConfig = EqConfig - { eqs = [] - , locals = [] - , wanteds = [] - , binds = emptyBag - } - -instance Outputable EqConfig where - ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds}) - = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds] -\end{code} - -The set of operations on an equality configuration. We obtain the initialise -configuration by normalisation ('normaliseEqs'), solve the equalities by -propagation ('propagateEqs'), and eventually finalise the configuration when -no further propoagation is possible. - -\begin{code} --- |Turn a set of equalities into an equality configuration for solving. --- --- Precondition: The Insts are zonked. --- -normaliseEqs :: [Inst] -> TcM EqConfig -normaliseEqs eqs - = do { WARNM2( anyM wantedEqInstIsUnsolved eqs, ppr eqs ) - ; traceTc $ ptext (sLit "Entering normaliseEqs") - - ; eqss <- mapM normEqInst eqs - ; return $ emptyEqConfig { eqs = concat eqss } - } - --- |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 { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+> - ptext (if isWanted then sLit "[Wanted] for" - else sLit "[Local] for")) - 4 (ppr insts) - - ; (insts', eqss, bindss) <- mapAndUnzip3M (normDict isWanted) insts - - ; traceTc $ hang (ptext (sLit "normaliseDicts returns")) - 4 (ppr insts' $$ ppr eqss) - ; return $ emptyEqConfig { eqs = concat eqss - , locals = if isWanted then [] else insts' - , wanteds = if isWanted then insts' else [] - , binds = unionManyBags bindss - } - } - --- |Solves the equalities as far as possible by applying propagation rules. --- -propagateEqs :: EqConfig -> TcM EqConfig -propagateEqs eqCfg@(EqConfig {eqs = todoEqs}) - = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:")) - 4 (ppr eqCfg) - - ; propagate todoEqs (eqCfg {eqs = []}) - } - --- |Finalise a set of equalities and associated dictionaries after --- propagation. The first returned set of instances are the locals (without --- equalities) and the second set are all residual wanteds, including --- equalities. In addition, we return all generated dictionary bindings. --- -finaliseEqsAndDicts :: TcTyVarSet -> EqConfig - -> TcM ([Inst], [Inst], TcDictBinds) -finaliseEqsAndDicts freeFlexibles (EqConfig { eqs = eqs - , locals = locals - , wanteds = wanteds - , binds = binds - }) - = do { traceTc $ ptext (sLit "finaliseEqsAndDicts") - - ; (eqs', subst_binds, locals', wanteds') - <- substitute eqs locals wanteds checkingMode freeFlexibles - ; eqs'' <- bindAndExtract eqs' checkingMode freeFlexibles - ; let final_binds = subst_binds `unionBags` binds - - -- Assert that all cotvs of wanted equalities are still unfilled, and - -- zonk all final insts, to make any improvement visible - ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' ) - ; zonked_locals <- zonkInsts locals' - ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds') - ; return (zonked_locals, zonked_wanteds, final_binds) - } - where - checkingMode = length eqs > length wanteds || not (null locals) - -- no local equalities or dicts => checking mode -\end{code} - - -%************************************************************************ -%* * - Normalisation of equalities -%* * -%************************************************************************ - -A normal equality is a properly oriented equality with associated coercion -that contains at most one family equality (in its left-hand side) is oriented -such that it may be used as a rewrite rule. It has one of the following two -forms: - -(1) co :: F t1..tn ~ t (family equalities) -(2) co :: x ~ t (variable equalities) - -Variable equalities fall again in two classes: - -(2a) co :: x ~ t, where t is *not* a variable, or -(2b) co :: x ~ y, where x > y. - -The types t, t1, ..., tn may not contain any occurrences of synonym -families. Moreover, in Forms (2) & (3), the left-hand side may not occur in -the right-hand side, and the relation x > y is an (nearly) arbitrary, but -total order on type variables. The only restriction that we impose on that -order is that for x > y, we are happy to instantiate x with y taking into -account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars). - -\begin{code} -data RewriteInst - = RewriteVar -- Form (2) above - { rwi_var :: TyVar -- may be rigid or flexible - , rwi_right :: TcType -- contains no synonym family applications - , rwi_co :: EqInstCo -- the wanted or given coercion - , rwi_loc :: InstLoc - , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst) - , rwi_swapped :: Bool -- swapped orientation of original EqInst - } - | RewriteFam -- Forms (1) above - { rwi_fam :: TyCon -- synonym family tycon - , rwi_args :: [Type] -- contain no synonym family applications - , rwi_right :: TcType -- contains no synonym family applications - , rwi_co :: EqInstCo -- the wanted or given coercion - , rwi_loc :: InstLoc - , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst) - , rwi_swapped :: Bool -- swapped orientation of original EqInst - } - -isWantedRewriteInst :: RewriteInst -> Bool -isWantedRewriteInst = isWantedCo . rwi_co - -isRewriteVar :: RewriteInst -> Bool -isRewriteVar (RewriteVar {}) = True -isRewriteVar _ = False - -tyVarsOfRewriteInst :: RewriteInst -> TyVarSet -tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty}) - = unitVarSet tv `unionVarSet` tyVarsOfType ty -tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty}) - = tyVarsOfTypes args `unionVarSet` tyVarsOfType ty - -rewriteInstToInst :: RewriteInst -> TcM Inst -rewriteInstToInst eq@(RewriteVar {rwi_var = tv}) - = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq) -rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args}) - = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq) - --- Derive an EqInst based from a RewriteInst, possibly swapping the types --- around. --- -deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst -deriveEqInst rewrite ty1 ty2 co - = do { co_adjusted <- if not swapped then return co - else mkSymEqInstCo co (ty2, ty1) - ; return $ EqInst - { tci_left = left - , tci_right = right - , tci_co = co_adjusted - , tci_loc = rwi_loc rewrite - , tci_name = rwi_name rewrite - } - } - where - swapped = rwi_swapped rewrite - (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1) - -instance Outputable RewriteInst where - ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co}) - = hsep [ pprEqInstCo co <+> text "::" - , ppr (mkTyConApp fam args) - , text "~>" - , ppr rhs - ] - ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co}) - = hsep [ pprEqInstCo co <+> text "::" - , ppr tv - , text "~>" - , ppr rhs - ] - -pprEqInstCo :: EqInstCo -> SDoc -pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv -pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co -\end{code} - -The following functions turn an arbitrary equality into a set of normal -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. - -Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...), -we drop that equality and raise an error if it is a wanted or a warning if it -is a local. - -\begin{code} -normEqInst :: Inst -> TcM [RewriteInst] --- Normalise one equality. -normEqInst inst - = ASSERT( isEqInst inst ) - do { traceTc $ ptext (sLit "normEqInst of ") <+> - pprEqInstCo co <+> text "::" <+> - ppr ty1 <+> text "~" <+> ppr ty2 - ; res <- go ty1 ty2 co - - ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res - ; return res - } - where - (ty1, ty2) = eqInstTys inst - co = eqInstCoercion 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 args) ty2 co - | isSynFamilyTyConApp ty1 -- only if not oversaturated - = mkRewriteFam False con args ty2 co - - -- right-to-left rule with type family head - go ty1 ty2@(TyConApp con args) co - | isSynFamilyTyConApp ty2 -- only if not oversaturated - = do { co' <- mkSymEqInstCo co (ty2, ty1) - ; mkRewriteFam True con args ty1 co' - } - - -- no outermost family - go ty1 ty2 co - = do { (ty1', co1, ty1_eqs) <- flattenType inst ty1 - ; (ty2', co2, ty2_eqs) <- flattenType inst ty2 - ; let ty12_eqs = ty1_eqs ++ ty2_eqs - sym_co2 = mkSymCoercion co2 - eqTys = (ty1', ty2') - ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs - ; eqs <- checkOrientation ty1' ty2' co' inst - ; if isLoopyEquality eqs ty12_eqs' - then do { if isWantedCo (tci_co inst) - then - addErrCtxt (ptext (sLit "Rejecting loopy equality")) $ - eqInstMisMatch inst - else - warnDroppingLoopyEquality ty1 ty2 - ; return ([]) -- drop the equality - } - else - return (eqs ++ ty12_eqs') - } - - mkRewriteFam swapped con args ty2 co - = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args - ; (ty2', co2, ty2_eqs) <- flattenType inst ty2 - ; let co1 = mkTyConApp con cargs - sym_co2 = mkSymCoercion co2 - all_eqs = concat args_eqss ++ ty2_eqs - eqTys = (mkTyConApp con args', ty2') - ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs - ; let thisRewriteFam = RewriteFam - { rwi_fam = con - , rwi_args = args' - , rwi_right = ty2' - , rwi_co = co' - , rwi_loc = tci_loc inst - , rwi_name = tci_name inst - , rwi_swapped = swapped - } - ; return $ thisRewriteFam : all_eqs' - } - - -- If the original equality has the form a ~ T .. (F ...a...) ..., we will - -- have a variable equality with 'a' on the lhs as the first equality. - -- Then, check whether 'a' occurs in the lhs of any family equality - -- generated by flattening. - isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs = any inRewriteFam eqs - where - inRewriteFam (RewriteFam {rwi_args = args}) - = tv `elemVarSet` tyVarsOfTypes args - inRewriteFam _ = False - isLoopyEquality _ _ = False - -normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds) --- Normalise one dictionary or IP constraint. -normDict isWanted inst@(Dict {tci_pred = ClassP clas args}) - = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args - ; let rewriteCo = PredTy $ ClassP clas cargs - eqs = concat args_eqss - pred' = ClassP clas args' - ; if null eqs - then -- don't generate a binding if there is nothing to flatten - return (inst, [], emptyBag) - else do { - ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred' - ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs - ; return (inst', eqs', bind) - }} -normDict _isWanted inst - = return (inst, [], emptyBag) --- !!!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) --- NB: We cannot assume that the two types already have outermost type --- synonyms expanded due to the recursion in the case of type applications. -checkOrientation ty1 ty2 co inst - = go ty1 ty2 - where - -- look through synonyms - go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 - go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' - - -- identical types => trivial - go ty1 ty2 - | ty1 `tcEqType` ty2 - = do { mkIdEqInstCo co ty1 - ; return [] - } - - -- two tvs (distinct tvs, due to previous equation) - go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2) - = do { isBigger <- tv1 `tvIsBigger` tv2 - ; if isBigger -- left greater - then mkRewriteVar False tv1 ty2 co -- => unchanged - else do { co' <- mkSymEqInstCo co (ty2, ty1) -- right greater - ; mkRewriteVar True tv2 ty1 co' -- => swap - } - } - - -- only lhs is a tv => unchanged - go ty1@(TyVarTy tv1) ty2 - | ty1 `tcPartOfType` ty2 -- occurs check! - = occurCheckErr ty1 ty2 - | otherwise - = mkRewriteVar False tv1 ty2 co - - -- only rhs is a tv => swap - go ty1 ty2@(TyVarTy tv2) - | ty2 `tcPartOfType` ty1 -- occurs check! - = occurCheckErr ty2 ty1 - | otherwise - = do { co' <- mkSymEqInstCo co (ty2, ty1) - ; mkRewriteVar True tv2 ty1 co' - } - - -- data type constructor application => decompose - -- NB: Special cased for efficiency - could be handled as type application - go (TyConApp con1 args1) (TyConApp con2 args2) - | con1 == con2 - && isInjectiveTyCon con1 -- don't match family synonym apps - = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2) - ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst) - args1 args2 co_args - ; return $ concat eqss - } - - -- function type => decompose - -- NB: Special cased for efficiency - could be handled as type application - go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r) - = do { (co_l, co_r) <- mkFunEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r) - ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst - ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst - ; return $ eqs_l ++ eqs_r - } - - -- type applications => decompose - go ty1 ty2 - | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps - , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2 - = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r) - ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst - ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst - ; return $ eqs_l ++ eqs_r - } - - -- inconsistency => type error - go ty1 ty2 - = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) ) - eqInstMisMatch inst - - mkRewriteVar swapped tv ty co = return [RewriteVar - { rwi_var = tv - , rwi_right = ty - , rwi_co = co - , rwi_loc = tci_loc inst - , rwi_name = tci_name inst - , rwi_swapped = swapped - }] - - -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2 - tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool - tvIsBigger tv1 tv2 - = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2) - where - isBigger tv1 (SkolemTv _) tv2 (SkolemTv _) - = return $ tv1 > tv2 - isBigger _ (MetaTv _ _) _ (SkolemTv _) - = return True - isBigger _ (SkolemTv _) _ (MetaTv _ _) - = return False - isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _) - -- meta variable meets meta variable - -- => be clever about which of the two to update - -- (from TcUnify.uUnfilledVars minus boxy stuff) - = case (info1, info2) of - -- Avoid SigTvs if poss - (SigTv _, SigTv _) -> return $ tv1 > tv2 - (SigTv _, _ ) | k1_sub_k2 -> return False - (_, SigTv _) | k2_sub_k1 -> return True - - (_, _) - | k1_sub_k2 && - k2_sub_k1 - -> case (nicer_to_update tv1, nicer_to_update tv2) of - (True, False) -> return True - (False, True) -> return False - _ -> return $ tv1 > tv2 - | k1_sub_k2 -> return False - | k2_sub_k1 -> return True - | otherwise -> kind_err >> return True - -- 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. - where - kind_err = addErrCtxtM (unifyKindCtxt False 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 tv = isSystemName (Var.varName tv) - -- Try to update sys-y type variables in preference to ones - -- gotten (say) by instantiating a polymorphic function with - -- a user-written type sig - -flattenType :: Inst -- context to get location & name - -> Type -- the type to flatten - -> TcM (Type, -- the flattened type - Coercion, -- coercion witness of flattening wanteds - [RewriteInst]) -- extra equalities --- Removes all family synonyms from a type by moving them into extra equalities -flattenType inst ty = go ty - where - -- look through synonyms - go ty | Just ty' <- tcView ty - = do { (ty_flat, co, eqs) <- go ty' - ; if null eqs - then -- unchanged, keep the old type with folded synonyms - return (ty, ty, []) - else - return (ty_flat, co, eqs) - } - - -- type variable => nothing to do - go ty@(TyVarTy _) - = return (ty, ty, []) - - -- type family application & family arity matches number of args - -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh) - go ty@(TyConApp con args) - | isSynFamilyTyConApp ty -- only if not oversaturated - = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args - ; alpha <- newFlexiTyVar (typeKind ty) - ; let alphaTy = mkTyVarTy alpha - ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy - ; let thisRewriteFam = RewriteFam - { rwi_fam = con - , rwi_args = args' - , rwi_right = alphaTy - , rwi_co = mkWantedCo cotv - , rwi_loc = tci_loc inst - , rwi_name = tci_name inst - , rwi_swapped = True - } - ; return (alphaTy, - mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv, - thisRewriteFam : concat args_eqss) - } - - -- datatype constructor application => flatten subtypes - -- NB: Special cased for efficiency - could be handled as type application - go ty@(TyConApp con args) - | not (isSynFamilyTyCon con) -- don't match oversaturated family apps - = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args - ; let args_eqs = concat args_eqss - ; if null args_eqs - then -- unchanged, keep the old type with folded synonyms - return (ty, ty, []) - else - return (mkTyConApp con args', - mkTyConApp con cargs, - args_eqs) - } - - -- function type => flatten subtypes - -- NB: Special cased for efficiency - could be handled as type application - go ty@(FunTy ty_l ty_r) - = do { (ty_l', co_l, eqs_l) <- go ty_l - ; (ty_r', co_r, eqs_r) <- go ty_r - ; if null eqs_l && null eqs_r - then -- unchanged, keep the old type with folded synonyms - return (ty, ty, []) - else - return (mkFunTy ty_l' ty_r', - mkFunTy co_l co_r, - eqs_l ++ eqs_r) - } - - -- type application => flatten subtypes - go ty - | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty - -- need to use the smart split as ty may be an - -- oversaturated family application - = do { (ty_l', co_l, eqs_l) <- go ty_l - ; (ty_r', co_r, eqs_r) <- go ty_r - ; if null eqs_l && null eqs_r - then -- unchanged, keep the old type with folded synonyms - return (ty, ty, []) - else - return (mkAppTy ty_l' ty_r', - mkAppTy co_l co_r, - eqs_l ++ eqs_r) - } - - -- forall type => panic if the body contains a type family - -- !!!TODO: As long as the family does not contain a quantified variable - -- we might pull it out, but what if it does contain a quantified - -- variable??? - go ty@(ForAllTy _ body) - | null (tyFamInsts body) - = return (ty, ty, []) - | otherwise - = panic "TcTyFuns.flattenType: synonym family in a rank-n type" - - -- predicate type => handle like a datatype constructor application - go (PredTy (ClassP cls tys)) - = do { (tys', ctys, tys_eqss) <- mapAndUnzip3M go tys - ; let tys_eqs = concat tys_eqss - ; if null tys_eqs - then -- unchanged, keep the old type with folded synonyms - return (ty, ty, []) - else - return (PredTy (ClassP cls tys'), - PredTy (ClassP cls ctys), - tys_eqs) - } - - -- implicit parameter => flatten subtype - go ty@(PredTy (IParam ipn ity)) - = do { (ity', co, eqs) <- go ity - ; if null eqs - then return (ty, ty, []) - else return (PredTy (IParam ipn ity'), - PredTy (IParam ipn co), - eqs) - } - - -- we should never see a equality - go (PredTy (EqPred _ _)) - = panic "TcTyFuns.flattenType: malformed type" - - go _ = panic "TcTyFuns: suppress bogus warning" - -adjustCoercions :: EqInstCo -- coercion of original equality - -> Coercion -- coercion witnessing the left rewrite - -> Coercion -- coercion witnessing the right rewrite - -> (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 equalities produced during flattening are --- adjusted . -adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs - -- wanted => generate a fresh coercion variable for the flattened equality - = do { cotv' <- newMetaCoVar ty_l ty_r - ; bindMetaTyVar cotv $ - (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2) - ; return (Left cotv', all_eqs) - } - -adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs - -- local => turn all new equalities into locals and update (but not zonk) - -- the skolem - = 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 - -> TcM (Inst, -- new inst - TcDictBinds) -- binding for coerced dictionary -mkDictBind dict isWanted rewriteCo pred - = do { dict' <- newCtGiven 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 - ; return (dict', binds) - } - where - loc = tci_loc dict - --- gamma ::^l Fam args ~ alpha --- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := 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) --- --- NB: It's crucial to update *both* alpha and gamma, as gamma may already --- have escaped into some other coercions during normalisation. --- --- We do actually update alpha and gamma by side effect (instead of --- only remembering the binding with `bindMetaTyVar', as we do for all --- other tyvars). We can do this as the side effects are strictly --- *local*; we know that both alpha and gamma were just a moment ago --- introduced by normalisation. --- -wantedToLocal :: RewriteInst -> TcM RewriteInst -wantedToLocal eq@(RewriteFam {rwi_fam = fam, - rwi_args = args, - rwi_right = TyVarTy alpha, - rwi_co = Left gamma}) - = do { writeMetaTyVar alpha (mkTyConApp fam args) - ; writeMetaTyVar gamma (mkTyConApp fam args) - ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma} - } -wantedToLocal _ = panic "TcTyFuns.wantedToLocal" -\end{code} - - -%************************************************************************ -%* * - Propagation of equalities -%* * -%************************************************************************ - -Apply the propagation rules exhaustively. - -\begin{code} -propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig -propagate [] eqCfg = return eqCfg -propagate (eq:eqs) eqCfg - = do { optEqs <- applyTop eq - ; case optEqs of - - -- Top applied to 'eq' => retry with new equalities - Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg - - -- Top doesn't apply => try subst rules with all other - -- equalities, after that 'eq' can go into the residual list - Nothing -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg - ; propagate eqs' (eqCfg' `addEq` eq) - } - } - -applySubstRules :: RewriteInst -- currently considered eq - -> [RewriteInst] -- todo eqs list - -> EqConfig -- residual - -> TcM ([RewriteInst], EqConfig) -- new todo & residual -applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs}) - = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs - ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs - ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t, - eqConfig {eqs = unchangedEqs_r}) - } - -mapSubstRules :: RewriteInst -- try substituting this equality - -> [RewriteInst] -- into these equalities - -> TcM ([RewriteInst], [RewriteInst]) -mapSubstRules eq eqs - = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs - ; return (concat newEqss, concat unchangedEqss) - } - where - substRules eq1 eq2 - = do {traceTc $ hang (ptext (sLit "Trying subst rules with")) - 4 (ppr eq1 $$ ppr eq2) - - -- try the SubstFam rule - ; optEqs <- applySubstFam eq1 eq2 - ; case optEqs of - Just eqs -> return (eqs, []) - Nothing -> do - { -- try the SubstVarVar rule - optEqs <- applySubstVarVar eq1 eq2 - ; case optEqs of - Just eqs -> return (eqs, []) - Nothing -> do - { -- try the SubstVarFam rule - optEqs <- applySubstVarFam eq1 eq2 - ; case optEqs of - Just eq -> return ([eq], []) - Nothing -> return ([], [eq2]) - -- if no rule matches, we return the equlity we tried to - -- substitute into unchanged - }}} -\end{code} - -Attempt to apply the Top rule. The rule is - - co :: F t1..tn ~ t - =(Top)=> - co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co' - -where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1. - -Returns Nothing if the rule could not be applied. Otherwise, the resulting -equality is normalised and a list of the normal equalities is returned. - -\begin{code} -applyTop :: RewriteInst -> TcM (Maybe [RewriteInst]) - -applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args}) - = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args) - ; case optTyCo of - Nothing -> return Nothing - Just (lhs, rewrite_co) - -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs) - ; eq' <- deriveEqInst eq lhs rhs co' - ; liftM Just $ normEqInst eq' - } - } - where - co = rwi_co eq - rhs = rwi_right eq - -applyTop _ = return Nothing -\end{code} - -Attempt to apply the SubstFam rule. The rule is - - co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s - =(SubstFam)=> - co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2' - -where co1 may be a wanted only if co2 is a wanted, too. - -Returns Nothing if the rule could not be applied. Otherwise, the equality -co2' is normalised and a list of the normal equalities is returned. (The -equality co1 is not returned as it remain unaltered.) - -\begin{code} -applySubstFam :: RewriteInst - -> RewriteInst - -> TcM (Maybe ([RewriteInst])) -applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1}) - eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2}) - - -- rule matches => rewrite - | fam1 == fam2 && tcEqTypes args1 args2 && - (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1)) - = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs) - ; eq2' <- deriveEqInst eq2 lhs rhs co2' - ; liftM Just $ normEqInst eq2' - } - - -- rule would match with eq1 and eq2 swapped => put eq2 into todo list - | fam1 == fam2 && tcEqTypes args1 args2 && - (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2)) - = return $ Just [eq2] - - where - lhs = rwi_right eq1 - rhs = rwi_right eq2 - co1 = eqInstCoType (rwi_co eq1) - co2 = rwi_co eq2 - -applySubstFam _ _ = return Nothing -\end{code} - -Attempt to apply the SubstVarVar rule. The rule is - - co1 :: x ~ t & co2 :: x ~ s - =(SubstVarVar)=> - co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2' - -where co1 may be a wanted only if co2 is a wanted, too. - -Returns Nothing if the rule could not be applied. Otherwise, the equality -co2' is normalised and a list of the normal equalities is returned. (The -equality co1 is not returned as it remain unaltered.) - -\begin{code} -applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst]) -applySubstVarVar eq1@(RewriteVar {rwi_var = tv1}) - eq2@(RewriteVar {rwi_var = tv2}) - - -- rule matches => rewrite - | tv1 == tv2 && - (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1)) - = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs) - ; eq2' <- deriveEqInst eq2 lhs rhs co2' - ; liftM Just $ normEqInst eq2' - } - - -- rule would match with eq1 and eq2 swapped => put eq2 into todo list - | tv1 == tv2 && - (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2)) - = return $ Just [eq2] - - where - lhs = rwi_right eq1 - rhs = rwi_right eq2 - co1 = eqInstCoType (rwi_co eq1) - co2 = rwi_co eq2 - -applySubstVarVar _ _ = return Nothing -\end{code} - -Attempt to apply the SubstVarFam rule. The rule is - - co1 :: x ~ t & co2 :: F s1..sn ~ s - =(SubstVarFam)=> - co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s - with co2 = [co1/x](F s1..sn) |> co2' - -where x occurs in F s1..sn. (co1 may be local or wanted.) - -Returns Nothing if the rule could not be applied. Otherwise, the equality -co2' is returned. (The equality co1 is not returned as it remain unaltered.) - -\begin{code} -applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst) - - -- rule matches => rewrite -applySubstVarFam eq1@(RewriteVar {rwi_var = tv1}) - eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2}) - | tv1 `elemVarSet` tyVarsOfTypes args2 - = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2) - args2' = substTysWith [tv1] [rhs1] args2 - lhs2 = mkTyConApp fam2 args2' - ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2) - ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'}) - } - where - rhs1 = rwi_right eq1 - rhs2 = rwi_right eq2 - co1 = eqInstCoType (rwi_co eq1) - co2 = rwi_co eq2 - - -- rule would match with eq1 and eq2 swapped => put eq2 into todo list -applySubstVarFam (RewriteFam {rwi_args = args1}) - eq2@(RewriteVar {rwi_var = tv2}) - | tv2 `elemVarSet` tyVarsOfTypes args1 - = return $ Just eq2 - -applySubstVarFam _ _ = return Nothing -\end{code} - - -%************************************************************************ -%* * - Finalisation of equalities -%* * -%************************************************************************ - -Exhaustive substitution of all variable equalities of the form co :: x ~ t -(both local and wanted) into the right-hand sides of all other equalities and -of family equalities of the form co :: F t1..tn ~ alpha into both sides of all -other *family* equalities. This may lead to recursive equalities; i.e., (1) -we need to apply the substitution implied by one equality exhaustively before -turning to the next and (2) we need an occurs check. - -We also apply the same substitutions to the local and wanted class and IP -dictionaries. - -We perform the substitutions in two steps: - - Step A: Substitute variable equalities into the right-hand sides of all - other equalities (but wanted only into wanteds) and into class and IP - constraints (again wanteds only into wanteds). - - Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where - 'alpha' is a skolem flexible (i.e., not free in the environment), - into the right-hand sides of all wanted variable equalities and into - both sides of all wanted family equalities. - - Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~ - alpha' into the right-hand sides of all wanted variable equalities - and into both sides of all wanted family equalities. - -In inference mode, we do not substitute into variable equalities in Steps B & C. - -The treatment of flexibles in wanteds is quite subtle. We absolutely want to -substitute variable equalities first; e.g., consider - - F s ~ alpha, alpha ~ t - -If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead. -This would be bad as `F s' is less useful, eg, as an argument to a class -constraint. - -The restriction on substituting locals is necessary due to examples, such as - - F delta ~ alpha, F alpha ~ delta, - -where `alpha' is a skolem flexible and `delta' a environment flexible. We need -to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise, -we may wrongly claim to having performed an improvement, which can lead to -non-termination of the combined class-family solver. - -We do also substitute flexibles, as in `alpha ~ t' into class constraints. -When `alpha' is later instantiated, we'd get the same effect, but in the -meantime the class constraint would miss some information, which would be a -problem in an integrated equality-class solver. - -NB: -* Given that we apply the substitution corresponding to a single equality - exhaustively, before turning to the next, and because we eliminate recursive - equalities, all opportunities for subtitution will have been exhausted after - we have considered each equality once. - -\begin{code} -substitute :: [RewriteInst] -- equalities - -> [Inst] -- local class dictionaries - -> [Inst] -- wanted class dictionaries - -> Bool -- True ~ checking mode; False ~ inference - -> TyVarSet -- flexibles free in the environment - -> 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 checkingMode freeFlexibles - = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by - -- sorting the equalities appropriately: first all variable, then all - -- family/skolem, and then the remaining family equalities. - let (var_eqs, fam_eqs) = partition isRewriteVar eqs - (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs - in - subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds - where - isFamSkolemEq (RewriteFam {rwi_right = ty}) - | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles) - isFamSkolemEq _ = False - - subst [] res binds locals wanteds - = return (res, binds, locals, wanteds) - - -- co :: x ~ t - subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs) - res binds locals wanteds - = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+> - ppr eq - - -- create the substitution - ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co] - tySubst = zipOpenTvSubst [tv] [ty] - - -- substitute into all other equalities - ; eqs' <- mapM (substEq eq coSubst tySubst) eqs - ; res' <- mapM (substEq eq coSubst tySubst) res - - -- only substitute local equalities into local dictionaries - ; (lbinds, locals') <- if not (isWantedCo co) - then - mapAndUnzipM - (substDict eq coSubst tySubst False) - locals - else - return ([], locals) - - -- substitute all equalities into wanteds dictionaries - ; (wbinds, wanteds') <- mapAndUnzipM - (substDict eq coSubst tySubst True) - wanteds - - ; let binds' = unionManyBags $ binds : lbinds ++ wbinds - ; subst eqs' (eq:res') binds' locals' wanteds' - } - - -- co ::^w F t1..tn ~ alpha - subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty, - rwi_co = co}):eqs) - res binds locals wanteds - | Just tv <- tcGetTyVar_maybe ty - , isMetaTyVar tv - , isWantedCo co - = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+> - ppr eq - - -- create the substitution - ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co] - tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args] - - -- substitute into other wanted equalities (`substEq' makes sure - -- that we only substitute into wanteds) - ; eqs' <- mapM (substEq eq coSubst tySubst) eqs - ; res' <- mapM (substEq eq coSubst tySubst) res - - ; subst eqs' (eq:res') binds locals wanteds - } - - 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 - -- and if eq2 is a local, co :: tv ~ ty needs to be a local, too) - substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) - coSubst tySubst eq2 - | tv `elemVarSet` tyVarsOfType (rwi_right eq2) - && (isWantedRewriteInst eq2 || not (isWantedCo co)) - = 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, - rwi_args = args} ->mkTyConApp fam args - ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2') - ; case eq2 of - RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty - -> occurCheckErr left2 right2' - _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'} - } - - -- We have, co ::^w F t1..tn ~ tv - -- => apply [F t1..tn/tv] to eq2 - -- (but only if tv actually occurs in eq2 - -- and eq2 is a wanted equality - -- and we are either in checking mode or eq2 is a family equality) - substEq (RewriteFam {rwi_args = args, rwi_right = ty}) - coSubst tySubst eq2 - | Just tv <- tcGetTyVar_maybe ty - , tv `elemVarSet` tyVarsOfRewriteInst eq2 - , isWantedRewriteInst eq2 - , checkingMode || not (isRewriteVar eq2) - = do { -- substitute into the right-hand side - ; 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, - rwi_args = args} -> mkTyConApp fam args - ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2') - ; case eq2 of - RewriteVar {rwi_var = tv2} - -- variable equality: perform an occurs check - | tv2 `elemVarSet` tyVarsOfTypes args - -> occurCheckErr left2 right2' - | otherwise - -> return $ eq2 {rwi_right = right2', rwi_co = co2'} - RewriteFam {rwi_fam = fam} - -- family equality: substitute also into the left-hand side - -> do { let co1Subst = substTy coSubst left2 - args2' = substTys tySubst (rwi_args eq2) - left2' = mkTyConApp fam args2' - ; co2'' <- mkRightTransEqInstCo co2' co1Subst - (left2', right2') - ; return $ eq2 {rwi_args = args2', rwi_right = right2', - rwi_co = co2''} - } - } - - -- 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}) coSubst tySubst isWanted dict - | isClassDict dict - , tv `elemVarSet` tyVarsOfPred (tci_pred dict) - = do { let co1Subst = 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 ~ -alpha, we record a binding of alpha with t or a, respectively, and for co := -id. We do the same for equalities of the form co :: F t1..tn ~ alpha unless -we are in inference mode and alpha appears in the environment - i.e., it is -not a flexible introduced by flattening locals or it is local, but was -propagated into the environment by the instantiation of a variable equality. - -We proceed in two phases: (1) first we consider all variable equalities and then -(2) we consider all family equalities. The two phase structure is required as -the recorded variable equalities determine which skolems flexibles escape, and -hence, which family equalities may be recorded as bindings. - -We return all wanted equalities for which we did not generate a binding. -(These can be skolem variable equalities, cyclic variable equalities, and -family equalities.) - -We don't update any meta variables. Instead, instantiation simply implies -putting a type variable binding into the binding pool of TcM. - -NB: - * We may encounter filled flexibles due to the instant filling of local - skolems in local-given constraints during flattening. - * Be careful with SigTVs. They can only be instantiated with other SigTVs or - rigid skolems. - -\begin{code} -bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst] -bindAndExtract eqs checkingMode freeFlexibles - = do { traceTc $ hang (ptext (sLit "bindAndExtract:")) - 4 (ppr eqs $$ ppr freeFlexibles) - ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs) - ; escapingSkolems <- getEscapingSkolems - ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems - ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1 - ; mapM rewriteInstToInst residuals2 - } - where - -- NB: we don't have to transitively chase the relation as the substitution - -- process applied before generating the bindings was exhaustive - getEscapingSkolems - = do { tybinds_rel <- getTcTyVarBindsRelation - ; return (unionVarSets . map snd . filter isFree $ tybinds_rel) - } - where - isFree (tv, _) = tv `elemVarSet` freeFlexibles - - -- co :: alpha ~ t or co :: a ~ alpha - instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co}) - = do { flexi_tv1 <- isFlexible tv1 - ; maybe_flexi_tv2 <- isFlexibleTy ty2 - ; case (flexi_tv1, maybe_flexi_tv2) of - (True, Just tv2) - | isSigTyVar tv1 && isSigTyVar tv2 - -> -- co :: alpha ~ beta, where both a SigTvs - doInst (rwi_swapped eq) tv1 ty2 co eq - (True, Nothing) - | Just tv2 <- tcGetTyVar_maybe ty2 - , isSigTyVar tv1 - , isSkolemTyVar tv2 - -> -- co :: alpha ~ a, where alpha is a SigTv - doInst (rwi_swapped eq) tv1 ty2 co eq - (True, _) - | not (isSigTyVar tv1) - -> -- co :: alpha ~ t, where alpha is not a SigTv - doInst (rwi_swapped eq) tv1 ty2 co eq - (False, Just tv2) - | isSigTyVar tv2 - , isSkolemTyVar tv1 - -> -- co :: a ~ alpha, where alpha is a SigTv - doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq - | not (isSigTyVar tv2) - -> -- co :: a ~ alpha, where alpha is not a SigTv - -- ('a' may be filled) - doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq - _ -> return $ Just eq - } - instVarEq eq = return $ Just eq - - -- co :: F args ~ alpha, - -- and we are either in checking mode or alpha is a skolem flexible that - -- doesn't escape - instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args, - rwi_right = ty2, rwi_co = co}) - | Just tv2 <- tcGetTyVar_maybe ty2 - , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles) - = do { flexi_tv2 <- isFlexible tv2 - ; if flexi_tv2 - then - doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq - else - return $ Just eq - } - instFamEq _ eq = return $ Just eq - - -- tv is a meta var, but not a SigTV and not filled - isFlexible tv - | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv - | otherwise = return False - - -- type is a tv that is a meta var, but not a SigTV and not filled - isFlexibleTy ty - | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv - ; if flexi then return $ Just tv - else return Nothing - } - | otherwise = return Nothing - - doInst _swapped _tv _ty (Right ty) _eq - = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty) - doInst swapped tv ty (Left cotv) eq - = do { lookupTV <- lookupTcTyVar tv - ; bMeta swapped tv lookupTV ty cotv - } - where - -- Try to create a binding for a meta variable. There is *no* need to - -- consider reorienting the underlying equality; `checkOrientation' - -- makes sure that we get variable-variable equalities only in the - -- appropriate orientation. - -- - bMeta :: Bool -- is this a swapped equality? - -> TcTyVar -- tyvar to instantiate - -> LookupTyVarResult -- lookup result of that tyvar - -> TcType -- to to instantiate tyvar with - -> TcTyVar -- coercion tyvar of current equality - -> TcM (Maybe RewriteInst) -- returns the original equality if - -- the tyvar could not be instantiated, - -- and hence, the equality must be kept - - -- meta variable has been filled already - -- => this should never happen due to the use of `isFlexible' above - bMeta _swapped tv (IndirectTv fill_ty) ty _cotv - = pprPanic "TcTyFuns.bMeta" $ - ptext (sLit "flexible") <+> ppr tv <+> - ptext (sLit "already filled with") <+> ppr fill_ty <+> - ptext (sLit "meant to fill with") <+> ppr ty - - -- type variable meets type variable - -- => `checkOrientation' already ensures that it is fine to instantiate - -- tv1 with tv2, but chase tv2's instantiations if necessary, so that - -- we eventually can perform a kinds check in bMetaInst - -- NB: tv's instantiations won't alter the orientation in which we - -- want to instantiate as they either constitute a family - -- application or are themselves due to a properly oriented - -- instantiation - bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv - = do { lookupTV2 <- lookupTcTyVar tv2 - ; case lookupTV2 of - IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv - DoneTv _ -> bMetaInst swapped tv1 ty cotv - } - - -- updatable meta variable meets non-variable type - -- => occurs check, monotype check, and kinds match check, then bind - bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv - = bMetaInst swapped tv non_tv_ty cotv - - bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta" - - -- We know `tv' can be instantiated; check that `ty' is alright for - -- instantiating `tv' with and then record a binding; we return the - -- original equality if it is cyclic through a synonym family - bMetaInst swapped tv ty cotv - = do { -- occurs + monotype check - ; mb_ty' <- checkTauTvUpdate tv ty - - ; case mb_ty' of - Nothing -> - -- there may be a family in non_tv_ty due to an unzonked, - -- but updated skolem for a local equality - -- (cf `wantedToLocal') - return $ Just eq - Just ty' -> - do { checkKinds swapped tv ty' - ; bindMetaTyVar tv ty' -- bind meta var - ; bindMetaTyVar cotv ty' -- bind co var - ; return Nothing - } - } -\end{code} - - -%************************************************************************ -%* * -\section{Errors} -%* * -%************************************************************************ - -The infamous couldn't match expected type soandso against inferred type -somethingdifferent message. - -\begin{code} -eqInstMisMatch :: Inst -> TcM a -eqInstMisMatch inst - = ASSERT( isEqInst inst ) - setInstCtxt (instLoc inst) $ failWithMisMatch ty_act ty_exp - where - (ty_act, ty_exp) = eqInstTys inst - ------------------------ -failWithMisMatch :: TcType -> TcType -> TcM a --- Generate the message when two types fail to match, --- going to some trouble to make it helpful. --- The argument order is: actual type, expected type -failWithMisMatch ty_act ty_exp - = do { env0 <- tcInitTidyEnv - ; ty_exp <- zonkTcType ty_exp - ; ty_act <- zonkTcType ty_act - ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp)) - } - -misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc) -misMatchMsg env0 (ty_act, ty_exp) - = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp - (env2, pp_act, extra_act) = ppr_ty env1 ty_act - msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp, - nest 7 $ - ptext (sLit "against inferred type") <+> pp_act], - nest 2 (extra_exp $$ extra_act $$ extra_tyfun) ] - -- See Note [Non-injective type functions] - in - (env2, msg) - - where - extra_tyfun - = case (tcSplitTyConApp_maybe ty_act, tcSplitTyConApp_maybe ty_exp) of - (Just (tc_act,_), Just (tc_exp,_)) | tc_act == tc_exp - -> if isOpenSynTyCon tc_act then pp_open_tc tc_act - else WARN( True, ppr tc_act) -- If there's a mis-match, then - empty -- it should be a family - _ -> empty - - - pp_open_tc tc = ptext (sLit "NB:") <+> quotes (ppr tc) - <+> ptext (sLit "is a type function") <> pp_inj - where - pp_inj | isInjectiveTyCon tc = empty - | otherwise = ptext (sLit (", and may not be injective")) - - ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc) - ppr_ty env ty - = let (env1, tidy_ty) = tidyOpenType env ty - (env2, extra) = ppr_extra env1 tidy_ty - in - (env2, quotes (ppr tidy_ty), extra) - - -- (ppr_extra env ty) shows extra info about 'ty' - ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc) - ppr_extra env (TyVarTy tv) - | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv) - = (env1, pprSkolTvBinding tv1) - where - (env1, tv1) = tidySkolemTyVar env tv - - ppr_extra env _ty = (env, empty) -- Normal case -\end{code} - -Note [Non-injective type functions] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -It's very confusing to get a message like - Couldn't match expected type `Depend s' - against inferred type `Depend s1' -so pp_open_tc adds: - NB: `Depend' is type function, and hence may not be injective - -Warn of loopy local equalities that were dropped. - -\begin{code} -warnDroppingLoopyEquality :: TcType -> TcType -> TcM () -warnDroppingLoopyEquality ty1 ty2 - = do { env0 <- tcInitTidyEnv - ; ty1 <- zonkTcType ty1 - ; ty2 <- zonkTcType ty2 - ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1 - (_env2, tidy_ty2) = tidyOpenType env1 ty2 - ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality")) - 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2)) - } -\end{code} diff --git a/compiler/vectorise/VectMonad.hs b/compiler/vectorise/VectMonad.hs deleted file mode 100644 index 65a3489..0000000 --- a/compiler/vectorise/VectMonad.hs +++ /dev/null @@ -1,651 +0,0 @@ -{-# LANGUAGE NamedFieldPuns #-} - --- | The Vectorisation monad. -module VectMonad ( - VM, - - noV, traceNoV, ensureV, traceEnsureV, tryV, maybeV, traceMaybeV, orElseV, - onlyIfV, fixV, localV, closedV, - initV, cantVectorise, maybeCantVectorise, maybeCantVectoriseM, - liftDs, - cloneName, cloneId, cloneVar, - newExportedVar, newLocalVar, newLocalVars, newDummyVar, newTyVar, - - Builtins(..), sumTyCon, prodTyCon, prodDataCon, - selTy, selReplicate, selPick, selTags, selElements, - combinePDVar, scalarZip, closureCtrFun, - builtin, builtins, - - setFamInstEnv, - readGEnv, setGEnv, updGEnv, - - readLEnv, setLEnv, updLEnv, - - getBindName, inBind, - - lookupVar, defGlobalVar, globalScalars, - lookupTyCon, defTyCon, - lookupDataCon, defDataCon, - lookupTyConPA, defTyConPA, defTyConPAs, - lookupTyConPR, - lookupBoxedTyCon, - lookupPrimMethod, lookupPrimPArray, - lookupTyVarPA, defLocalTyVar, defLocalTyVarWithPA, localTyVars, - - lookupInst, lookupFamInst -) where - -#include "HsVersions.h" - -import VectBuiltIn -import Vectorise.Env - -import HscTypes hiding ( MonadThings(..) ) -import Module ( PackageId ) -import CoreSyn -import Class -import TyCon -import DataCon -import Type -import Var -import VarSet -import VarEnv -import Id -import Name -import NameEnv - -import DsMonad - -import InstEnv -import FamInstEnv - -import Outputable -import FastString -import SrcLoc ( noSrcSpan ) - -import Control.Monad - --- | Indicates what scope something (a variable) is in. -data Scope a b = Global a | Local b - - --- | The global environment. -data GlobalEnv = GlobalEnv { - -- | Mapping from global variables to their vectorised versions. - -- - global_vars :: VarEnv Var - - -- | Purely scalar variables. Code which mentions only these - -- variables doesn't have to be lifted. - , global_scalars :: VarSet - - -- | Exported variables which have a vectorised version - -- - , global_exported_vars :: VarEnv (Var, Var) - - -- | Mapping from TyCons to their vectorised versions. - -- TyCons which do not have to be vectorised are mapped to - -- themselves. - -- - , global_tycons :: NameEnv TyCon - - -- | Mapping from DataCons to their vectorised versions - -- - , global_datacons :: NameEnv DataCon - - -- | Mapping from TyCons to their PA dfuns - -- - , global_pa_funs :: NameEnv Var - - -- | Mapping from TyCons to their PR dfuns - , global_pr_funs :: NameEnv Var - - -- | Mapping from unboxed TyCons to their boxed versions - , global_boxed_tycons :: NameEnv TyCon - - -- | External package inst-env & home-package inst-env for class - -- instances - -- - , global_inst_env :: (InstEnv, InstEnv) - - -- | External package inst-env & home-package inst-env for family - -- instances - -- - , global_fam_inst_env :: FamInstEnvs - - -- | Hoisted bindings - , global_bindings :: [(Var, CoreExpr)] - } - --- | The local environment. -data LocalEnv = LocalEnv { - -- Mapping from local variables to their vectorised and - -- lifted versions - -- - local_vars :: VarEnv (Var, Var) - - -- In-scope type variables - -- - , local_tyvars :: [TyVar] - - -- Mapping from tyvars to their PA dictionaries - , local_tyvar_pa :: VarEnv CoreExpr - - -- Local binding name - , local_bind_name :: FastString - } - - --- | Create an initial global environment -initGlobalEnv :: VectInfo -> (InstEnv, InstEnv) -> FamInstEnvs -> GlobalEnv -initGlobalEnv info instEnvs famInstEnvs - = GlobalEnv { - global_vars = mapVarEnv snd $ vectInfoVar info - , global_scalars = emptyVarSet - , global_exported_vars = emptyVarEnv - , global_tycons = mapNameEnv snd $ vectInfoTyCon info - , global_datacons = mapNameEnv snd $ vectInfoDataCon info - , global_pa_funs = mapNameEnv snd $ vectInfoPADFun info - , global_pr_funs = emptyNameEnv - , global_boxed_tycons = emptyNameEnv - , global_inst_env = instEnvs - , global_fam_inst_env = famInstEnvs - , global_bindings = [] - } - - --- Operators on Global Environments ------------------------------------------- -extendImportedVarsEnv :: [(Var, Var)] -> GlobalEnv -> GlobalEnv -extendImportedVarsEnv ps genv - = genv { global_vars = extendVarEnvList (global_vars genv) ps } - -extendScalars :: [Var] -> GlobalEnv -> GlobalEnv -extendScalars vs genv - = genv { global_scalars = extendVarSetList (global_scalars genv) vs } - -setFamInstEnv :: FamInstEnv -> GlobalEnv -> GlobalEnv -setFamInstEnv l_fam_inst genv - = genv { global_fam_inst_env = (g_fam_inst, l_fam_inst) } - where - (g_fam_inst, _) = global_fam_inst_env genv - -extendTyConsEnv :: [(Name, TyCon)] -> GlobalEnv -> GlobalEnv -extendTyConsEnv ps genv - = genv { global_tycons = extendNameEnvList (global_tycons genv) ps } - -extendDataConsEnv :: [(Name, DataCon)] -> GlobalEnv -> GlobalEnv -extendDataConsEnv ps genv - = genv { global_datacons = extendNameEnvList (global_datacons genv) ps } - -extendPAFunsEnv :: [(Name, Var)] -> GlobalEnv -> GlobalEnv -extendPAFunsEnv ps genv - = genv { global_pa_funs = extendNameEnvList (global_pa_funs genv) ps } - -setPRFunsEnv :: [(Name, Var)] -> GlobalEnv -> GlobalEnv -setPRFunsEnv ps genv - = genv { global_pr_funs = mkNameEnv ps } - -setBoxedTyConsEnv :: [(Name, TyCon)] -> GlobalEnv -> GlobalEnv -setBoxedTyConsEnv ps genv - = genv { global_boxed_tycons = mkNameEnv ps } - - --- | Create an empty local environment. -emptyLocalEnv :: LocalEnv -emptyLocalEnv = LocalEnv { - local_vars = emptyVarEnv - , local_tyvars = [] - , local_tyvar_pa = emptyVarEnv - , local_bind_name = fsLit "fn" - } - --- FIXME -updVectInfo :: GlobalEnv -> TypeEnv -> VectInfo -> VectInfo -updVectInfo env tyenv info - = info { - vectInfoVar = global_exported_vars env - , vectInfoTyCon = mk_env typeEnvTyCons global_tycons - , vectInfoDataCon = mk_env typeEnvDataCons global_datacons - , vectInfoPADFun = mk_env typeEnvTyCons global_pa_funs - } - where - mk_env :: NamedThing from => - (TypeEnv -> [from]) - -> (GlobalEnv -> NameEnv to) - -> NameEnv (from,to) - mk_env from_tyenv from_env = mkNameEnv [(name, (from,to)) - | from <- from_tyenv tyenv - , let name = getName from - , Just to <- [lookupNameEnv (from_env env) name]] - --- The Vectorisation Monad ---------------------------------------------------- - --- Vectorisation can either succeed with new envionment and a value, --- or return with failure. --- -data VResult a = Yes GlobalEnv LocalEnv a | No - -newtype VM a = VM { runVM :: Builtins -> GlobalEnv -> LocalEnv -> DsM (VResult a) } - -instance Monad VM where - return x = VM $ \_ genv lenv -> return (Yes genv lenv x) - VM p >>= f = VM $ \bi genv lenv -> do - r <- p bi genv lenv - case r of - Yes genv' lenv' x -> runVM (f x) bi genv' lenv' - No -> return No - - --- | Throw an error saying we can't vectorise something -cantVectorise :: String -> SDoc -> a -cantVectorise s d = pgmError - . showSDocDump - $ vcat [text "*** Vectorisation error ***", - nest 4 $ sep [text s, nest 4 d]] - -maybeCantVectorise :: String -> SDoc -> Maybe a -> a -maybeCantVectorise s d Nothing = cantVectorise s d -maybeCantVectorise _ _ (Just x) = x - -maybeCantVectoriseM :: Monad m => String -> SDoc -> m (Maybe a) -> m a -maybeCantVectoriseM s d p - = do - r <- p - case r of - Just x -> return x - Nothing -> cantVectorise s d - - --- Control -------------------------------------------------------------------- --- | Return some result saying we've failed. -noV :: VM a -noV = VM $ \_ _ _ -> return No - -traceNoV :: String -> SDoc -> VM a -traceNoV s d = pprTrace s d noV - - --- | If True then carry on, otherwise fail. -ensureV :: Bool -> VM () -ensureV False = noV -ensureV True = return () - - --- | If True then return the first argument, otherwise fail. -onlyIfV :: Bool -> VM a -> VM a -onlyIfV b p = ensureV b >> p - -traceEnsureV :: String -> SDoc -> Bool -> VM () -traceEnsureV s d False = traceNoV s d -traceEnsureV _ _ True = return () - - --- | Try some vectorisation computaton. --- If it succeeds then return Just the result, --- otherwise return Nothing. -tryV :: VM a -> VM (Maybe a) -tryV (VM p) = VM $ \bi genv lenv -> - do - r <- p bi genv lenv - case r of - Yes genv' lenv' x -> return (Yes genv' lenv' (Just x)) - No -> return (Yes genv lenv Nothing) - - -maybeV :: VM (Maybe a) -> VM a -maybeV p = maybe noV return =<< p - -traceMaybeV :: String -> SDoc -> VM (Maybe a) -> VM a -traceMaybeV s d p = maybe (traceNoV s d) return =<< p - -orElseV :: VM a -> VM a -> VM a -orElseV p q = maybe q return =<< tryV p - -fixV :: (a -> VM a) -> VM a -fixV f = VM (\bi genv lenv -> fixDs $ \r -> runVM (f (unYes r)) bi genv lenv ) - where - -- NOTE: It is essential that we are lazy in r above so do not replace - -- calls to this function by an explicit case. - unYes (Yes _ _ x) = x - unYes No = panic "VectMonad.fixV: no result" - - --- Local Environments --------------------------------------------------------- --- | Perform a computation in its own local environment. --- This does not alter the environment of the current state. -localV :: VM a -> VM a -localV p = do - env <- readLEnv id - x <- p - setLEnv env - return x - --- | Perform a computation in an empty local environment. -closedV :: VM a -> VM a -closedV p = do - env <- readLEnv id - setLEnv (emptyLocalEnv { local_bind_name = local_bind_name env }) - x <- p - setLEnv env - return x - --- Lifting -------------------------------------------------------------------- --- | Lift a desugaring computation into the vectorisation monad. -liftDs :: DsM a -> VM a -liftDs p = VM $ \_ genv lenv -> do { x <- p; return (Yes genv lenv x) } - - - --- Builtins ------------------------------------------------------------------- --- Operations on Builtins -liftBuiltinDs :: (Builtins -> DsM a) -> VM a -liftBuiltinDs p = VM $ \bi genv lenv -> do { x <- p bi; return (Yes genv lenv x)} - - --- | Project something from the set of builtins. -builtin :: (Builtins -> a) -> VM a -builtin f = VM $ \bi genv lenv -> return (Yes genv lenv (f bi)) - -builtins :: (a -> Builtins -> b) -> VM (a -> b) -builtins f = VM $ \bi genv lenv -> return (Yes genv lenv (`f` bi)) - - --- Environments --------------------------------------------------------------- --- | Project something from the global environment. -readGEnv :: (GlobalEnv -> a) -> VM a -readGEnv f = VM $ \_ genv lenv -> return (Yes genv lenv (f genv)) - -setGEnv :: GlobalEnv -> VM () -setGEnv genv = VM $ \_ _ lenv -> return (Yes genv lenv ()) - -updGEnv :: (GlobalEnv -> GlobalEnv) -> VM () -updGEnv f = VM $ \_ genv lenv -> return (Yes (f genv) lenv ()) - - --- | Project something from the local environment. -readLEnv :: (LocalEnv -> a) -> VM a -readLEnv f = VM $ \_ genv lenv -> return (Yes genv lenv (f lenv)) - --- | Set the local environment. -setLEnv :: LocalEnv -> VM () -setLEnv lenv = VM $ \_ genv _ -> return (Yes genv lenv ()) - --- | Update the enviroment using a provided function. -updLEnv :: (LocalEnv -> LocalEnv) -> VM () -updLEnv f = VM $ \_ genv lenv -> return (Yes genv (f lenv) ()) - - --- InstEnv -------------------------------------------------------------------- -getInstEnv :: VM (InstEnv, InstEnv) -getInstEnv = readGEnv global_inst_env - -getFamInstEnv :: VM FamInstEnvs -getFamInstEnv = readGEnv global_fam_inst_env - - --- Names ---------------------------------------------------------------------- --- | Get the name of the local binding currently being vectorised. -getBindName :: VM FastString -getBindName = readLEnv local_bind_name - -inBind :: Id -> VM a -> VM a -inBind id p - = do updLEnv $ \env -> env { local_bind_name = occNameFS (getOccName id) } - p - -cloneName :: (OccName -> OccName) -> Name -> VM Name -cloneName mk_occ name = liftM make (liftDs newUnique) - where - occ_name = mk_occ (nameOccName name) - - make u | isExternalName name = mkExternalName u (nameModule name) - occ_name - (nameSrcSpan name) - | otherwise = mkSystemName u occ_name - -cloneId :: (OccName -> OccName) -> Id -> Type -> VM Id -cloneId mk_occ id ty - = do - name <- cloneName mk_occ (getName id) - let id' | isExportedId id = Id.mkExportedLocalId name ty - | otherwise = Id.mkLocalId name ty - return id' - --- Make a fresh instance of this var, with a new unique. -cloneVar :: Var -> VM Var -cloneVar var = liftM (setIdUnique var) (liftDs newUnique) - -newExportedVar :: OccName -> Type -> VM Var -newExportedVar occ_name ty - = do - mod <- liftDs getModuleDs - u <- liftDs newUnique - - let name = mkExternalName u mod occ_name noSrcSpan - - return $ Id.mkExportedLocalId name ty - -newLocalVar :: FastString -> Type -> VM Var -newLocalVar fs ty - = do - u <- liftDs newUnique - return $ mkSysLocal fs u ty - -newLocalVars :: FastString -> [Type] -> VM [Var] -newLocalVars fs = mapM (newLocalVar fs) - -newDummyVar :: Type -> VM Var -newDummyVar = newLocalVar (fsLit "vv") - -newTyVar :: FastString -> Kind -> VM Var -newTyVar fs k - = do - u <- liftDs newUnique - return $ mkTyVar (mkSysTvName u fs) k - - --- | Add a mapping between a global var and its vectorised version to the state. -defGlobalVar :: Var -> Var -> VM () -defGlobalVar v v' = updGEnv $ \env -> - env { global_vars = extendVarEnv (global_vars env) v v' - , global_exported_vars = upd (global_exported_vars env) - } - where - upd env | isExportedId v = extendVarEnv env v (v, v') - | otherwise = env - --- Var ------------------------------------------------------------------------ --- | Lookup the vectorised and\/or lifted versions of this variable. --- If it's in the global environment we get the vectorised version. --- If it's in the local environment we get both the vectorised and lifted version. --- -lookupVar :: Var -> VM (Scope Var (Var, Var)) -lookupVar v - = do r <- readLEnv $ \env -> lookupVarEnv (local_vars env) v - case r of - Just e -> return (Local e) - Nothing -> liftM Global - . maybeCantVectoriseVarM v - . readGEnv $ \env -> lookupVarEnv (global_vars env) v - -maybeCantVectoriseVarM :: Monad m => Var -> m (Maybe Var) -> m Var -maybeCantVectoriseVarM v p - = do r <- p - case r of - Just x -> return x - Nothing -> dumpVar v - -dumpVar :: Var -> a -dumpVar var - | Just _ <- isClassOpId_maybe var - = cantVectorise "ClassOpId not vectorised:" (ppr var) - - | otherwise - = cantVectorise "Variable not vectorised:" (ppr var) - -------------------------------------------------------------------------------- -globalScalars :: VM VarSet -globalScalars = readGEnv global_scalars - -lookupTyCon :: TyCon -> VM (Maybe TyCon) -lookupTyCon tc - | isUnLiftedTyCon tc || isTupleTyCon tc = return (Just tc) - - | otherwise = readGEnv $ \env -> lookupNameEnv (global_tycons env) (tyConName tc) - -defTyCon :: TyCon -> TyCon -> VM () -defTyCon tc tc' = updGEnv $ \env -> - env { global_tycons = extendNameEnv (global_tycons env) (tyConName tc) tc' } - -lookupDataCon :: DataCon -> VM (Maybe DataCon) -lookupDataCon dc - | isTupleTyCon (dataConTyCon dc) = return (Just dc) - | otherwise = readGEnv $ \env -> lookupNameEnv (global_datacons env) (dataConName dc) - -defDataCon :: DataCon -> DataCon -> VM () -defDataCon dc dc' = updGEnv $ \env -> - env { global_datacons = extendNameEnv (global_datacons env) (dataConName dc) dc' } - -lookupPrimPArray :: TyCon -> VM (Maybe TyCon) -lookupPrimPArray = liftBuiltinDs . primPArray - -lookupPrimMethod :: TyCon -> String -> VM (Maybe Var) -lookupPrimMethod tycon = liftBuiltinDs . primMethod tycon - -lookupTyConPA :: TyCon -> VM (Maybe Var) -lookupTyConPA tc = readGEnv $ \env -> lookupNameEnv (global_pa_funs env) (tyConName tc) - -defTyConPA :: TyCon -> Var -> VM () -defTyConPA tc pa = updGEnv $ \env -> - env { global_pa_funs = extendNameEnv (global_pa_funs env) (tyConName tc) pa } - -defTyConPAs :: [(TyCon, Var)] -> VM () -defTyConPAs ps = updGEnv $ \env -> - env { global_pa_funs = extendNameEnvList (global_pa_funs env) - [(tyConName tc, pa) | (tc, pa) <- ps] } - -lookupTyVarPA :: Var -> VM (Maybe CoreExpr) -lookupTyVarPA tv = readLEnv $ \env -> lookupVarEnv (local_tyvar_pa env) tv - -lookupTyConPR :: TyCon -> VM (Maybe Var) -lookupTyConPR tc = readGEnv $ \env -> lookupNameEnv (global_pr_funs env) (tyConName tc) - -lookupBoxedTyCon :: TyCon -> VM (Maybe TyCon) -lookupBoxedTyCon tc = readGEnv $ \env -> lookupNameEnv (global_boxed_tycons env) - (tyConName tc) - -defLocalTyVar :: TyVar -> VM () -defLocalTyVar tv = updLEnv $ \env -> - env { local_tyvars = tv : local_tyvars env - , local_tyvar_pa = local_tyvar_pa env `delVarEnv` tv - } - -defLocalTyVarWithPA :: TyVar -> CoreExpr -> VM () -defLocalTyVarWithPA tv pa = updLEnv $ \env -> - env { local_tyvars = tv : local_tyvars env - , local_tyvar_pa = extendVarEnv (local_tyvar_pa env) tv pa - } - -localTyVars :: VM [TyVar] -localTyVars = readLEnv (reverse . local_tyvars) - --- Look up the dfun of a class instance. --- --- The match must be unique - ie, match exactly one instance - but the --- type arguments used for matching may be more specific than those of --- the class instance declaration. The found class instances must not have --- any type variables in the instance context that do not appear in the --- instances head (i.e., no flexi vars); for details for what this means, --- see the docs at InstEnv.lookupInstEnv. --- -lookupInst :: Class -> [Type] -> VM (DFunId, [Type]) -lookupInst cls tys - = do { instEnv <- getInstEnv - ; case lookupInstEnv instEnv cls tys of - ([(inst, inst_tys)], _) - | noFlexiVar -> return (instanceDFunId inst, inst_tys') - | otherwise -> pprPanic "VectMonad.lookupInst: flexi var: " - (ppr $ mkTyConApp (classTyCon cls) tys) - where - inst_tys' = [ty | Right ty <- inst_tys] - noFlexiVar = all isRight inst_tys - _other -> - pprPanic "VectMonad.lookupInst: not found " (ppr cls <+> ppr tys) - } - where - isRight (Left _) = False - isRight (Right _) = True - --- Look up the representation tycon of a family instance. --- --- The match must be unique - ie, match exactly one instance - but the --- type arguments used for matching may be more specific than those of --- the family instance declaration. --- --- Return the instance tycon and its type instance. For example, if we have --- --- lookupFamInst 'T' '[Int]' yields (':R42T', 'Int') --- --- then we have a coercion (ie, type instance of family instance coercion) --- --- :Co:R42T Int :: T [Int] ~ :R42T Int --- --- which implies that :R42T was declared as 'data instance T [a]'. --- -lookupFamInst :: TyCon -> [Type] -> VM (TyCon, [Type]) -lookupFamInst tycon tys - = ASSERT( isFamilyTyCon tycon ) - do { instEnv <- getFamInstEnv - ; case lookupFamInstEnv instEnv tycon tys of - [(fam_inst, rep_tys)] -> return (famInstTyCon fam_inst, rep_tys) - _other -> - pprPanic "VectMonad.lookupFamInst: not found: " - (ppr $ mkTyConApp tycon tys) - } - - --- | Run a vectorisation computation. -initV :: PackageId -> HscEnv -> ModGuts -> VectInfo -> VM a -> IO (Maybe (VectInfo, a)) -initV pkg hsc_env guts info p - = do - -- XXX: ignores error messages and warnings, check that this is - -- indeed ok (the use of "Just r" suggests so) - (_,Just r) <- initDs hsc_env (mg_module guts) - (mg_rdr_env guts) - (mg_types guts) - go - return r - where - - go = - do - builtins <- initBuiltins pkg - builtin_vars <- initBuiltinVars builtins - builtin_tycons <- initBuiltinTyCons builtins - let builtin_datacons = initBuiltinDataCons builtins - builtin_boxed <- initBuiltinBoxedTyCons builtins - builtin_scalars <- initBuiltinScalars builtins - - eps <- liftIO $ hscEPS hsc_env - let famInstEnvs = (eps_fam_inst_env eps, mg_fam_inst_env guts) - instEnvs = (eps_inst_env eps, mg_inst_env guts) - - builtin_prs <- initBuiltinPRs builtins instEnvs - builtin_pas <- initBuiltinPAs builtins instEnvs - - let genv = extendImportedVarsEnv builtin_vars - . extendScalars builtin_scalars - . extendTyConsEnv builtin_tycons - . extendDataConsEnv builtin_datacons - . extendPAFunsEnv builtin_pas - . setPRFunsEnv builtin_prs - . setBoxedTyConsEnv builtin_boxed - $ initGlobalEnv info instEnvs famInstEnvs - - r <- runVM p builtins genv emptyLocalEnv - case r of - Yes genv _ x -> return $ Just (new_info genv, x) - No -> return Nothing - - new_info genv = updVectInfo genv (mg_types guts) info -