X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcTyFuns.lhs;h=ba73891fa4945365d6940ad8929a491d28fb3e47;hb=c7ae8f20f93b4e36837fc3ecafccd3f49c95cb6b;hp=e1270cd6d81d13da163397034f38deacb6d95026;hpb=7ef52f1d8104b990b2f0b2da240f45ecf2de7bf0;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index e1270cd..ba73891 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -269,6 +269,10 @@ emptyEqConfig = EqConfig , binds = emptyBag , skolems = emptyVarSet } + +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 @@ -284,7 +288,7 @@ no further propoagation is possible. normaliseEqs :: [Inst] -> TcM EqConfig normaliseEqs eqs = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs ) - ; traceTc $ ptext (sLit "normaliseEqs") + ; traceTc $ ptext (sLit "Entering normaliseEqs") ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs ; return $ emptyEqConfig { eqs = concat eqss @@ -300,7 +304,7 @@ normaliseEqs eqs -- normaliseDicts :: Bool -> [Inst] -> TcM EqConfig normaliseDicts isWanted insts - = do { traceTc $ ptext (sLit "normaliseDicts") <+> + = do { traceTc $ ptext (sLit "Entering normaliseDicts") <+> ptext (if isWanted then sLit "[Wanted]" else sLit "[Local]") ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted) insts @@ -316,7 +320,9 @@ normaliseDicts isWanted insts -- propagateEqs :: EqConfig -> TcM EqConfig propagateEqs eqCfg@(EqConfig {eqs = todoEqs}) - = do { traceTc $ ptext (sLit "propagateEqs") + = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:")) + 4 (ppr eqCfg) + ; propagate todoEqs (eqCfg {eqs = []}) } @@ -341,7 +347,7 @@ finaliseEqsAndDicts (EqConfig { eqs = eqs }) = do { traceTc $ ptext (sLit "finaliseEqsAndDicts") ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds - ; (eqs'', improved) <- instantiateAndExtract eqs' + ; (eqs'', improved) <- instantiateAndExtract eqs' (null locals) ; final_binds <- filterM nonTrivialDictBind $ bagToList (subst_binds `unionBags` binds) @@ -433,6 +439,24 @@ deriveEqInst rewrite ty1 ty2 co 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 @@ -481,9 +505,9 @@ normEqInst inst = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2 ; let ty12_eqs = ty1_eqs ++ ty2_eqs - rewriteCo = co1 `mkTransCoercion` mkSymCoercion co2 + sym_co2 = mkSymCoercion co2 eqTys = (ty1', ty2') - ; (co', ty12_eqs') <- adjustCoercions co rewriteCo eqTys ty12_eqs + ; (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) @@ -503,11 +527,11 @@ normEqInst inst = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M (flattenType inst) args ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2 - ; let rewriteCo = mkTyConApp con cargs `mkTransCoercion` - mkSymCoercion co2 + ; 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 rewriteCo eqTys all_eqs + ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs ; let thisRewriteFam = RewriteFam { rwi_fam = con , rwi_args = args' @@ -559,7 +583,13 @@ checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst] -- 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 + = do { traceTc $ ptext (sLit "checkOrientation of ") <+> + pprEqInstCo co <+> text "::" <+> + ppr ty1 <+> text "~" <+> ppr ty2 + ; eqs <- go ty1 ty2 + ; traceTc $ ptext (sLit "checkOrientation returns") <+> ppr eqs + ; return eqs + } where -- look through synonyms go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 @@ -636,7 +666,14 @@ flattenType inst ty = go ty where -- look through synonyms - go ty | Just ty' <- tcView ty = go ty' + go ty | Just ty' <- tcView ty + = do { (ty_flat, co, eqs, skolems) <- go ty' + ; if null eqs + then -- unchanged, keep the old type with folded synonyms + return (ty, ty, [], emptyVarSet) + else + return (ty_flat, co, eqs, skolems) + } -- type variable => nothing to do go ty@(TyVarTy _) @@ -667,34 +704,45 @@ flattenType inst ty -- data constructor application => flatten subtypes -- NB: Special cased for efficiency - could be handled as type application - go (TyConApp con args) + go ty@(TyConApp con args) = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args - ; return (mkTyConApp con args', - mkTyConApp con cargs, - concat args_eqss, - unionVarSets args_skolemss) + ; if null args_eqss + then -- unchanged, keep the old type with folded synonyms + return (ty, ty, [], emptyVarSet) + else + return (mkTyConApp con args', + mkTyConApp con cargs, + concat args_eqss, + unionVarSets args_skolemss) } -- function type => flatten subtypes -- NB: Special cased for efficiency - could be handled as type application - go (FunTy ty_l ty_r) + go ty@(FunTy ty_l ty_r) = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r - ; return (mkFunTy ty_l' ty_r', - mkFunTy co_l co_r, - eqs_l ++ eqs_r, - skolems_l `unionVarSet` skolems_r) + ; if null eqs_l && null eqs_r + then -- unchanged, keep the old type with folded synonyms + return (ty, ty, [], emptyVarSet) + else + return (mkFunTy ty_l' ty_r', + mkFunTy co_l co_r, + eqs_l ++ eqs_r, + skolems_l `unionVarSet` skolems_r) } -- type application => flatten subtypes - go (AppTy ty_l ty_r) --- | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty + go ty@(AppTy ty_l ty_r) = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r - ; return (mkAppTy ty_l' ty_r', - mkAppTy co_l co_r, - eqs_l ++ eqs_r, - skolems_l `unionVarSet` skolems_r) + ; if null eqs_l && null eqs_r + then -- unchanged, keep the old type with folded synonyms + return (ty, ty, [], emptyVarSet) + else + return (mkAppTy ty_l' ty_r', + mkAppTy co_l co_r, + eqs_l ++ eqs_r, + skolems_l `unionVarSet` skolems_r) } -- forall type => panic if the body contains a type family @@ -712,7 +760,8 @@ flattenType inst ty = panic "TcTyFuns.flattenType: unexpected PredType" adjustCoercions :: EqInstCo -- coercion of original equality - -> Coercion -- coercion witnessing the rewrite + -> 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 @@ -720,17 +769,17 @@ adjustCoercions :: EqInstCo -- coercion of original equality -- 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 co rewriteCo eqTys all_eqs - +adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs -- wanted => generate a fresh coercion variable for the flattened equality - | isWantedCo co - = do { co' <- mkRightTransEqInstCo co rewriteCo eqTys - ; return (co', all_eqs) + = do { cotv' <- newMetaCoVar ty_l ty_r + ; writeMetaTyVar 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 - | otherwise = do { all_eqs' <- mapM wantedToLocal all_eqs ; return (co, all_eqs') } @@ -1011,8 +1060,7 @@ substitute eqs locals wanteds = subst eqs [] emptyBag 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 { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr tv <+> - ptext (sLit "->") <+> ppr ty + = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co] tySubst = zipOpenTvSubst [tv] [ty] ; eqs' <- mapM (substEq eq coSubst tySubst) eqs @@ -1059,8 +1107,7 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds coSubst tySubst isWanted dict | isClassDict dict , tv `elemVarSet` tyVarsOfPred (tci_pred dict) - = do { let co1Subst = mkSymCoercion $ - PredTy (substPred coSubst (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') @@ -1078,16 +1125,19 @@ 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] -> TcM ([Inst], Bool) -instantiateAndExtract eqs - = do { let wanteds = filter (isWantedCo . rwi_co) eqs - ; wanteds' <- mapM inst wanteds +instantiateAndExtract :: [RewriteInst] -> Bool -> TcM ([Inst], Bool) +instantiateAndExtract eqs localsEmpty + = do { wanteds' <- mapM inst wanteds ; let residuals = catMaybes wanteds' improved = length wanteds /= length residuals ; residuals' <- mapM rewriteInstToInst residuals ; return (residuals', improved) } where + wanteds = filter (isWantedCo . rwi_co) eqs + checkingMode = length eqs > length wanteds || not localsEmpty + -- no local equalities or dicts => checking mode + inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co}) -- co :: alpha ~ t @@ -1099,6 +1149,14 @@ instantiateAndExtract eqs , isMetaTyVar tv2 = doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq + -- co :: F args ~ alpha, and we are in checking mode (ie, no locals) + inst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty2, + rwi_co = co}) + | checkingMode + , Just tv2 <- tcGetTyVar_maybe ty2 + , isMetaTyVar tv2 + = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq + inst eq = return $ Just eq doInst _swapped _tv _ty (Right ty) _eq