From: Manuel M T Chakravarty Date: Wed, 3 Oct 2007 14:57:15 +0000 (+0000) Subject: TcTyFuns.eqInstToRewrite X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=7b3a6b7645b86f55a8e7109c139b0a3a5a7f43d2 TcTyFuns.eqInstToRewrite --- diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 126a029..bfe5207 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -99,27 +99,72 @@ tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType) tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst \end{code} -Normalise a type relative to the rewrite rule implied by one EqInst or an -already unpacked EqInst (ie, an equality rewrite rule). +An elementary rewrite is a properly oriented equality with associated coercion +that has one of the following two forms: + +(1) co :: F t1..tn ~ t +(2) co :: a ~ t , where t /= F t1..tn + +The following functions takes an equality instance and turns it into an +elementary rewrite if possible. \begin{code} --- Rewrite by EqInst -tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, Type) -tcEqInstNormaliseFamInst inst = - ASSERT( isEqInst inst ) - tcEqRuleNormaliseFamInst (pat, rhs, co) +data Rewrite = Rewrite TcType -- lhs of rewrite rule + TcType -- rhs of rewrite rule + TcType -- coercion witnessing the rewrite rule + +eqInstToRewrite :: Inst -> Maybe Rewrite +eqInstToRewrite inst + = ASSERT( isEqInst inst ) + go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst) where - pat = eqInstLeftTy inst - rhs = eqInstRightTy inst - co = eqInstType 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 + + -- rewrite type family applications + go ty1@(TyConApp con _) ty2 co + | isOpenSynTyCon con + = Just $ Rewrite ty1 ty2 co + + -- rewrite skolems + go ty1@(TyVarTy tv) ty2 co + | isSkolemTyVar tv + = Just $ Rewrite ty1 ty2 co + + -- rewrite type family applications from right-to-left, only after + -- having checked whether we can work left-to-right + go ty1 ty2@(TyConApp con _) co + | isOpenSynTyCon con + = Just $ Rewrite ty2 ty1 (mkSymCoercion co) + + -- rewrite skolems from right-to-left, only after having checked + -- whether we can work left-to-right + go ty1 ty2@(TyVarTy tv) co + | isSkolemTyVar tv + = Just $ Rewrite ty2 ty1 (mkSymCoercion co) + + go _ _ _ = Nothing +\end{code} + +Normalise a type relative to an elementary rewrite implied by an EqInst or an +explicitly given elementary rewrite. + +\begin{code} +-- Rewrite by EqInst +-- Precondition: the EqInst passes the occurs check +tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType) +tcEqInstNormaliseFamInst inst ty + = case eqInstToRewrite inst of + Just rewrite -> tcEqRuleNormaliseFamInst rewrite ty + Nothing -> return (IdCo, ty) -- Rewrite by equality rewrite rule -tcEqRuleNormaliseFamInst :: (TcType, -- rewrite rule lhs - TcType, -- rewrite rule rhs - TcType) -- coercion witnessing the rewrite rule - -> TcType -- type to rewrite - -> TcM (CoercionI, Type) -tcEqRuleNormaliseFamInst (pat, rhs, co) ty +tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite + -> TcType -- type to rewrite + -> TcM (CoercionI, -- witnessing coercion + TcType) -- rewritten type +tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty = tcGenericNormaliseFamInst matchEqRule ty where matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co) @@ -526,12 +571,13 @@ skolemOccurs insts -- this equality is not a rewrite rule => ignore isRewriteRule _ _ = return ([inst], return ()) - + ------------------ breakRecursion pat body swapped | null tysToLiftOut = return ([inst], return ()) | otherwise - = do { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut + = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut + ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut ; let skTvs_tysTLO = zip skTvs tysToLiftOut insertSkolems = return . replace skTvs_tysTLO ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body @@ -539,6 +585,7 @@ skolemOccurs insts else mkEqInst (EqPred pat body') co -- ensure to reconstruct the inst in the -- original orientation + ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst' ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst') skTvs_tysTLO ; return (inst':insts, sequence_ undoSk) @@ -564,6 +611,7 @@ skolemOccurs insts = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv)) (mkGivenCo $ mkSymCoercion (fromACo co)) + -- co /= IdCo due to construction of inst' ; return (inst, writeMetaTyVar skTv tyTLO) } \end{code} @@ -799,43 +847,14 @@ substRule insts = tryAllInsts insts [] -- substInst :: Inst -> [Inst] -> TcM ([Inst], Bool) substInst inst insts - = ASSERT( isEqInst inst ) - go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst) + = case eqInstToRewrite inst of + Just rewrite -> substEquality rewrite insts + Nothing -> return (insts, False) where - -- 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 - - -- rewrite type family applications - go ty1@(TyConApp con _) ty2 co - | isOpenSynTyCon con - = substEquality (ty1, ty2, co) insts - - -- rewrite skolems - go ty1@(TyVarTy tv) ty2 co - | isSkolemTyVar tv - = substEquality (ty1, ty2, co) insts - - -- rewrite type family applications from right-to-left, only after - -- having checked whether we can work left-to-right - go ty1 ty2@(TyConApp con _) co - | isOpenSynTyCon con - = substEquality (ty2, ty1, mkSymCoercion co) insts - - -- rewrite skolems from right-to-left, only after having checked - -- whether we can work left-to-right - go ty1 ty2@(TyVarTy tv) co - | isSkolemTyVar tv - = substEquality (ty2, ty1, mkSymCoercion co) insts - - go _ _ _ = return (insts, False) - - substEquality :: (TcType, -- rewrite rule lhs - TcType, -- rewrite rule rhs - TcType) -- coercion witnessing the rewrite rule - -> [Inst] -- insts to rewrite + substEquality :: Rewrite -- elementary rewrite + -> [Inst] -- insts to rewrite -> TcM ([Inst], Bool) - substEquality eqRule@(pat, rhs, _) insts + substEquality eqRule@(Rewrite pat rhs _) insts | pat `tcPartOfType` rhs -- occurs check! = occurCheckErr pat rhs | otherwise diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 35cf5a5..05f1601 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -531,9 +531,9 @@ mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI mkForAllTyCoI _ IdCo = IdCo mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co +fromACo :: CoercionI -> Coercion fromACo (ACo co) = co - mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI -- mkClassPPredCoI cls tys cois = coi -- coi : PredTy (cls tys) ~ predTy (cls (tys `cast` cois))