From 37df27c6f21452c60c45b5cf6defc9003a41da15 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Mon, 10 Sep 2007 08:34:57 +0000 Subject: [PATCH] Cleaned up version of Tom's unflattened skolemOccurs --- compiler/typecheck/TcMType.lhs | 12 --- compiler/typecheck/TcTyFuns.lhs | 184 +++++++++++++++++++++++++++------------ compiler/types/Coercion.lhs | 5 +- compiler/types/Type.lhs | 48 +++++++++- 4 files changed, 181 insertions(+), 68 deletions(-) diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 1ae1b2b..e85d3b8 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -1442,16 +1442,4 @@ sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' sizePred (IParam _ ty) = sizeType ty sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 - --- Type family instances occuring in a type after expanding synonyms -tyFamInsts :: Type -> [(TyCon, [Type])] -tyFamInsts ty - | Just exp_ty <- tcView ty = tyFamInsts exp_ty -tyFamInsts (TyVarTy _) = [] -tyFamInsts (TyConApp tc tys) - | isOpenSynTyCon tc = [(tc, tys)] - | otherwise = concat (map tyFamInsts tys) -tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 -tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 -tyFamInsts (ForAllTy _ ty) = tyFamInsts ty \end{code} diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index e5a562c..c89fcae 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -84,13 +84,28 @@ possible (ie, we treat family instances as a TRS). Also zonk meta variables. then co : ty ~ ty' \begin{code} -tcNormalizeFamInst :: Type -> TcM (CoercionI, Type) +tcNormalizeFamInst :: TcType -> TcM (CoercionI, TcType) tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType) tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst \end{code} +Normalise a type relative to the rewrite rule implied by one EqInst. + +\begin{code} +tcEqInstNormalizeFamInst :: Inst -> TcType -> TcM (CoercionI, Type) +tcEqInstNormalizeFamInst inst = ASSERT( isEqInst inst ) + tcGenericNormalizeFamInst matchInst + where + pat = eqInstLeftTy inst + rhs = eqInstRightTy inst + co = eitherEqInst inst TyVarTy id + -- + matchInst ty | pat `tcEqType` ty = return $ Just (rhs, co) + | otherwise = return $ Nothing +\end{code} + Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and apply the normalisation function gives as the first argument to every TyConApp and every TyVarTy subterm. @@ -107,10 +122,10 @@ 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} -tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion))) +tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType, Coercion))) -- what to do with type functions and tyvars -> TcType -- old type - -> TcM (CoercionI, Type) -- (coercion, new type) + -> TcM (CoercionI, TcType) -- (coercion, new type) tcGenericNormalizeFamInst fun ty | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty' tcGenericNormalizeFamInst fun (TyConApp tyCon tys) @@ -273,48 +288,99 @@ normaliseGivens givens ; traceTc (text "normaliseGivens ->" <+> ppr result) ; return (result, deSkolem) } +\end{code} + --- An explanation of what this does would be helpful! -=chak +This is an (attempt at, yet unproven, an) *unflattened* version of +the SubstL-Ev completion rule. + +The above rule is essential to catch non-terminating +rules that cannot be oriented properly, like + + F a ~ [G (F a)] + or even + a ~ [G a] + +The left-to-right orientiation is not suitable because it does not +terminate. +The right-to-left orientation is not suitable because it +does not have a type-function on the left. This is undesirable because +it would hide information. E.g. assume + instance C [x] +then rewriting C [G (F a)] to C (F a) is bad because we cannot now +see that the C [x] instance applies. + +The rule also caters for badly-oriented rules of the form: + F a ~ G (F a) +for which other solutions are possible, but this one will do too. + +It's behavior is: + co : ty1 ~ ty2{F ty1} + >--> + co : ty1 ~ ty2{b} + sym (F co) : F ty2{b} ~ b + where b is a fresh skolem variable + +We also return an action (b := ty1) which is used to eliminate b +after the dust of normalisation with the completed rewrite system +has settled. + +A subtle point of this transformation is that both coercions in the results +are strictly speaking incorrect. However, they are correct again after the +action {B := ty1} has removed the skolem again. This happens immediately +after constraint entailment has been checked; ie, code outside of the +simplification and entailment checking framework will never see these +temporarily incorrect coercions. + +NB: We perform this transformation for multiple occurences of ty1 under one + or multiple family applications on the left-hand side at once (ie, the + rule doesn't need to be applied multiple times at a single inst). As a + result we can get two or more insts back. + +\begin{code} skolemOccurs :: PrecondRule -skolemOccurs [] = return ([], return ()) -skolemOccurs (inst@(EqInst {}):insts) - = do { (insts',actions) <- skolemOccurs insts - -- check whether the current inst co :: ty1 ~ ty2 suffers - -- from the occurs check issue: F ty1 \in ty2 - ; let occurs = go False ty2 - ; if occurs - then - -- if it does generate two new coercions: - do { skolem_var <- newMetaTyVar TauTv (typeKind ty1) - ; let skolem_ty = TyVarTy skolem_var - -- ty1 :: ty1 ~ b - ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1) - -- sym co :: ty2 ~ b - ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co) - -- to replace the old one - -- the corresponding action is - -- b := ty1 - ; let action = writeMetaTyVar skolem_var ty1 - ; return (inst1:inst2:insts', action >> actions) - } - else - return (inst:insts', actions) - } - where - ty1 = eqInstLeftTy inst - ty2 = eqInstRightTy inst - co = eqInstCoercion inst - check :: Bool -> TcType -> Bool - check flag ty - = if flag && ty1 `tcEqType` ty - then True - else go flag ty - - go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys - go flag (FunTy arg res) = or $ map (check flag) [arg,res] - go flag (AppTy fun arg) = or $ map (check flag) [fun,arg] - go _ _ = False -skolemOccurs _ = panic "TcTyFuns.skolemOccurs: not EqInst" +skolemOccurs insts + = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts + ; return (concat instss, sequence_ undoSkolems) + } + where + oneSkolemOccurs inst + | null tysToLiftOut + = return ([inst], return ()) + | otherwise + = do { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut + ; let skTvs_tysTLO = zip skTvs tysToLiftOut + insertSkolems = return . replace skTvs_tysTLO + ; (_, ty2') <- tcGenericNormalizeFamInst insertSkolems ty2 + ; inst' <- mkEqInst (EqPred ty1 ty2') co + ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst') skTvs_tysTLO + ; return (inst':insts, sequence_ undoSk) + } + where + ty1 = eqInstLeftTy inst + ty2 = eqInstRightTy inst + co = eqInstCoercion inst + + -- all subtypes that are (1) type family instances and (2) contain the + -- lhs type as part of the type arguments of the type family constructor + tysToLiftOut = ASSERT( isEqInst inst ) + [mkTyConApp tc tys | (tc, tys) <- tyFamInsts ty2 + , any (ty1 `tcPartOfType`) tys] + + replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion) + replace [] _ = Nothing + replace ((skTv, tyTLO):rest) ty + | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined) + | otherwise = replace rest ty + + -- create the EqInst for the equality determining the skolem and a + -- TcM action undoing the skolem introduction + mkSkolemInst inst' (skTv, tyTLO) + = do { (co, tyLiftedOut) <- tcEqInstNormalizeFamInst inst' tyTLO + ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv)) + (mkGivenCo $ mkSymCoercion (fromACo co)) + ; return (inst, writeMetaTyVar skTv tyTLO) + } \end{code} @@ -476,12 +542,18 @@ swapInsts insts } -- (Swap) - -- g1 : c ~ Fd + -- g1 : c ~ F d -- >--> - -- g2 : Fd ~ c + -- g2 : F d ~ c -- g1 := sym g2 + -- where c isn't a function call + -- and -- - -- This is not all, is it? Td ~ c is also rewritten to c ~ Td! + -- g1 : c ~ a + -- >--> + -- g2 : a ~ c + -- g1 := sym g2 + -- where c isn't a function call or other variable swapInst :: Inst -> TcM (Inst, Bool) swapInst i@(EqInst {}) = go ty1 ty2 @@ -639,6 +711,12 @@ substInstsWorker (i:is) acc then return ((i:is'),True) else substInstsWorker is (i:acc) } + | (TyVarTy _) <- tci_left i + = do { (is',change) <- substInst i (acc ++ is) + ; if change + then return ((i:is'),True) + else substInstsWorker is (i:acc) + } | otherwise = substInstsWorker is (i:acc) @@ -649,12 +727,11 @@ substInstsWorker (i:is) acc -- g2 : s1{t} ~ s2{t} -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g} substInst :: Inst -> [Inst] -> TcM ([Inst], Bool) -substInst _inst [] - = return ([],False) -substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is) +substInst _inst [] = return ([],False) +substInst inst (i@(EqInst {tci_left = ty1, tci_right = ty2}):is) = do { (is',changed) <- substInst inst is - ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1 - ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2 + ; (coi1,ty1') <- normalise ty1 + ; (coi2,ty2') <- normalise ty2 ; case (coi1,coi2) of (IdCo,IdCo) -> return (i:is',changed) @@ -674,9 +751,8 @@ substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci ; return (new_inst:is',True) } } - where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing - - coercion = eitherEqInst inst TyVarTy id + where + normalise = tcEqInstNormalizeFamInst inst substInst _ _ = panic "TcTyFuns.substInst: not EqInst" -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index fa4a6b7..770988d 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -371,7 +371,10 @@ transCoercionTyCon = where composeCoercionKindsOf (co1:co2:rest) = ASSERT( null rest ) - WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug") + WARN( not (r1 `coreEqType` a2), + text "Strange! Type mismatch in trans coercion, probably a bug" + $$ + ppr r1 <+> text "=/=" <+> ppr a2) (a1, r2) where (a1, r1) = coercionKind co1 diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index aa3cd07..b6b246b 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -74,6 +74,9 @@ module Type ( tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta, typeKind, addFreeTyVars, + -- Type families + tyFamInsts, + -- Tidying up for printing tidyType, tidyTypes, tidyOpenType, tidyOpenTypes, @@ -84,7 +87,7 @@ module Type ( -- Comparison coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, - tcEqPred, tcCmpPred, tcEqTypeX, + tcEqPred, tcCmpPred, tcEqTypeX, tcPartOfType, tcPartOfPred, -- Seq seqType, seqTypes, @@ -709,6 +712,28 @@ addFreeTyVars ty = NoteTy (FTVNote (tyVarsOfType ty)) ty %************************************************************************ %* * +\subsection{Type families} +%* * +%************************************************************************ + +Type family instances occuring in a type after expanding synonyms. + +\begin{code} +tyFamInsts :: Type -> [(TyCon, [Type])] +tyFamInsts ty + | Just exp_ty <- tcView ty = tyFamInsts exp_ty +tyFamInsts (TyVarTy _) = [] +tyFamInsts (TyConApp tc tys) + | isOpenSynTyCon tc = [(tc, tys)] + | otherwise = concat (map tyFamInsts tys) +tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 +tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 +tyFamInsts (ForAllTy _ ty) = tyFamInsts ty +\end{code} + + +%************************************************************************ +%* * \subsection{TidyType} %* * %************************************************************************ @@ -974,6 +999,27 @@ tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2 \end{code} +Checks whether the second argument is a subterm of the first. (We don't care +about binders, as we are only interested in syntactic subterms.) + +\begin{code} +tcPartOfType :: Type -> Type -> Bool +tcPartOfType t1 t2 = tcEqType t1 t2 +tcPartOfType t1 t2 + | Just t2' <- tcView t2 = tcPartOfType t1 t2' +tcPartOfType t1 (ForAllTy _ t2) = tcPartOfType t1 t2 +tcPartOfType t1 (AppTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2 +tcPartOfType t1 (FunTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2 +tcPartOfType t1 (PredTy p2) = tcPartOfPred t1 p2 +tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts +tcPartOfType t1 (NoteTy _ t2) = tcPartOfType t1 t2 + +tcPartOfPred :: Type -> PredType -> Bool +tcPartOfPred t1 (IParam _ t2) = tcPartOfType t1 t2 +tcPartOfPred t1 (ClassP _ ts) = any (tcPartOfType t1) ts +tcPartOfPred t1 (EqPred s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2 +\end{code} + Now here comes the real worker \begin{code} -- 1.7.10.4