X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcTyFuns.lhs;h=0066d2fd03e03f4fe6f71dbc0b8128bb8f4c5479;hb=27759873a8bd45c487a6e636f7a12c37e87f616f;hp=9a369d91f9d412a5130b68d5188b79c86d75ea6d;hpb=9892daf7fac4087813c6f5fedfc3de5d19410689;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 9a369d9..0066d2f 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -69,21 +69,16 @@ tcUnfoldSynFamInst (TyConApp tycon tys) | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances = return Nothing | otherwise - = do { -- we only use the indexing arguments for matching, - -- not the additional ones - ; maybeFamInst <- tcLookupFamInst tycon idxTys + = 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 tys', - mkTyConApp coe_tc tys') + Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys, + mkTyConApp coe_tc rep_tys) where - tys' = rep_tys ++ restTys coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst" (tyConFamilyCoercion_maybe rep_tc) } - where - n = tyConArity tycon - (idxTys, restTys) = splitAt n tys tcUnfoldSynFamInst _other = return Nothing \end{code} @@ -231,9 +226,6 @@ tcReduceEqs locals wanteds We maintain normalised equalities together with the skolems introduced as intermediates during flattening of equalities as well as -!!!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. -- @@ -286,7 +278,7 @@ no further propoagation is possible. -- normaliseEqs :: [Inst] -> TcM EqConfig normaliseEqs eqs - = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs ) + = do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs ) ; traceTc $ ptext (sLit "Entering normaliseEqs") ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs @@ -352,7 +344,7 @@ finaliseEqsAndDicts (EqConfig { eqs = eqs -- Assert that all cotvs of wanted equalities are still unfilled, and -- zonk all final insts, to make any improvement visible - ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' ) + ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' ) ; zonked_locals <- zonkInsts locals' ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds') ; return (zonked_locals, zonked_wanteds, final_binds, improved) @@ -384,9 +376,6 @@ 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 arbitrary, but total order on type variables -!!!TODO: We may need to keep track of swapping for error messages (and to -re-orient on finilisation). - \begin{code} data RewriteInst = RewriteVar -- Form (2) above @@ -960,9 +949,6 @@ applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1}) -- rule matches => rewrite | fam1 == fam2 && tcEqTypes args1 args2 && (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1)) --- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms --- !!!Check whether anything breaks by making tcEqTypes look through synonyms. --- !!!Should be ok and we don't want three type equalities. = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs) ; eq2' <- deriveEqInst eq2 lhs rhs co2' ; liftM Just $ normEqInst eq2' @@ -1194,16 +1180,26 @@ Return all remaining wanted equalities. The Boolean result component is True if at least one instantiation of a flexible that is *not* a skolem from flattening was performed. +We need to instantiate all flexibles that arose as skolems during flattening +of wanteds before we instantiate any other flexibles. Consider F delta ~ +alpha, F alpha ~ delta, where alpha is a skolem and delta a free 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. + \begin{code} instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool) instantiateAndExtract eqs localsEmpty skolems = do { traceTc $ hang (ptext (sLit "instantiateAndExtract:")) 4 (ppr eqs $$ ppr skolems) - ; results <- mapM inst wanteds - ; let residuals = [eq | Left eq <- results] - only_skolems = and [tv `elemVarSet` skolems | Right tv <- results] + -- start by *only* instantiating skolem flexibles from flattening + ; unflat_wanteds <- liftM catMaybes $ + mapM (inst (`elemVarSet` skolems)) wanteds + -- only afterwards instantiate free flexibles + ; residuals <- liftM catMaybes $ mapM (inst (const True)) unflat_wanteds + ; let improvement = length residuals < length unflat_wanteds ; residuals' <- mapM rewriteInstToInst residuals - ; return (residuals', not only_skolems) + ; return (residuals', improvement) } where wanteds = filter (isWantedCo . rwi_co) eqs @@ -1211,9 +1207,9 @@ instantiateAndExtract eqs localsEmpty skolems -- no local equalities or dicts => checking mode -- co :: alpha ~ t or co :: a ~ alpha - inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co}) - = do { flexi_tv1 <- isFlexible tv1 - ; maybe_flexi_tv2 <- isFlexibleTy ty2 + inst mayInst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co}) + = do { flexi_tv1 <- isFlexible mayInst tv1 + ; maybe_flexi_tv2 <- isFlexibleTy mayInst ty2 ; case (flexi_tv1, maybe_flexi_tv2) of (True, _) -> -- co :: alpha ~ t @@ -1221,31 +1217,31 @@ instantiateAndExtract eqs localsEmpty skolems (False, Just tv2) -> -- co :: a ~ alpha doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq - _ -> return $ Left eq + _ -> return $ Just 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}) + inst mayInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, + rwi_right = ty2, rwi_co = co}) | Just tv2 <- tcGetTyVar_maybe ty2 , isMetaTyVar tv2 - , checkingMode || tv2 `elemVarSet` skolems - -- !!!TODO: this is too liberal, even if tv2 is in + , mayInst tv2 && (checkingMode || tv2 `elemVarSet` skolems) + -- !!!FIXME: this is too liberal, even if tv2 is in -- skolems we shouldn't instantiate if tvs occurs -- in other equalities that may propagate it into the -- environment = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq - inst eq = return $ Left eq + inst _mayInst eq = return $ Just eq -- tv is a meta var and not filled - isFlexible tv - | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv - | otherwise = return False + isFlexible mayInst tv + | isMetaTyVar tv && mayInst tv = liftM isFlexi $ readMetaTyVar tv + | otherwise = return False -- type is a tv that is a meta var and not filled - isFlexibleTy ty - | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv + isFlexibleTy mayInst ty + | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible mayInst tv ; if flexi then return $ Just tv else return Nothing } @@ -1265,7 +1261,7 @@ instantiateAndExtract eqs localsEmpty skolems ptext (sLit "flexible") <+> ppr tv <+> ptext (sLit "already filled with") <+> ppr fill_ty <+> ptext (sLit "meant to fill with") <+> ppr ty - ; return $ Left eq + ; return $ Just eq } -- type variable meets type variable @@ -1288,7 +1284,7 @@ instantiateAndExtract eqs localsEmpty skolems -- signature skolem meets non-variable type -- => cannot update (retain the equality)! uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv - = return $ Left eq + = return $ Just eq -- updatable meta variable meets non-variable type -- => occurs check, monotype check, and kinds match check, then update @@ -1298,12 +1294,13 @@ instantiateAndExtract eqs localsEmpty skolems ; case mb_ty' of Nothing -> - -- normalisation shouldn't leave families in non_tv_ty - panic "TcTyFuns.uMeta: unexpected synonym family" + -- there may be a family in non_tv_ty due to an unzonked, + -- but updated skolem for a local equality + return $ Just eq Just ty' -> do { checkUpdateMeta swapped tv ref ty' -- update meta var ; writeMetaTyVar cotv ty' -- update co var - ; return $ Right tv + ; return Nothing } } @@ -1315,38 +1312,36 @@ instantiateAndExtract eqs localsEmpty skolems uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2) ; writeMetaTyVar cotv (mkTyVarTy tv2) - ; return $ Right tv1 + ; return Nothing } -- 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 { tv <- 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 >> return tv1 + = 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 $ Right tv + ; return Nothing } where -- Kinds should be guaranteed ok at this point update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2) - >> return tv1 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1) - >> return tv2 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $ unifyKindMisMatch k1 k2