X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcTyFuns.lhs;h=d7da2f76e5ee3d5d3633e30454e26876b65b437e;hb=3f1b316d7035c55cd712cd39a9981339bcef2e8c;hp=64c983034614e573d3093779851fe1b7c8c3ff79;hpb=6d2b0ae3ae3296cb6cdd496cbf85b897c7ce150b;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 64c9830..d7da2f7 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -11,7 +11,7 @@ module TcTyFuns ( substEqInDictInsts, -- errors - eqInstMisMatch, misMatchMsg, + misMatchMsg, failWithMisMatch ) where @@ -99,27 +99,80 @@ 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 and a is a skolem tyvar + +NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a +reqrite rule. Instead, such equalities are solved by unification. This is +essential; cf Note [skolemOccurs loop]. + +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, Bool) + -- True iff rewrite swapped equality +eqInstToRewrite inst + = ASSERT( isEqInst inst ) + go ty1 ty2 (eqInstType inst) where - pat = eqInstLeftTy inst - rhs = eqInstRightTy inst - co = eqInstType inst + (ty1,ty2) = eqInstTys 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 _) ty2 co + | isOpenSynTyCon con + = Just (Rewrite ty1 ty2 co, False) -- not swapped + + -- left-to-right rule with type variable head + go ty1@(TyVarTy tv) ty2 co + | isSkolemTyVar tv + = Just (Rewrite ty1 ty2 co, False) -- not swapped + + -- right-to-left rule with type family head, 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), True) -- swapped + + -- right-to-left rule with type variable head, 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), True) -- swapped + + -- this equality is not a rewrite rule => ignore + 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) @@ -444,7 +497,7 @@ oriented properly, like F a ~ [G (F a)] or even - a ~ [G a] + a ~ [G a] , where a is a skolem tyvar The left-to-right orientiation is not suitable because it does not terminate. The right-to-left orientation is not suitable because it @@ -489,6 +542,45 @@ NB: We perform this transformation for multiple occurences of ty1 under one rule doesn't need to be applied multiple times at a single inst). As a result we can get two or more insts back. +Note [skolemOccurs loop] +~~~~~~~~~~~~~~~~~~~~~~~~ +You might think that under + + type family F a + type instance F [a] = [F a] + +a signature such as + + foo :: (F [a] ~ a) => a + +will get us into a loop. However, this is *not* the case. Here is why: + + F [a] ~ a + + -->(TOP) + + [F a] ~ a + + -->(SkolemOccurs) + + [b] ~ a + F [b] ~ b , with b := F a + + -->(TOP) + + [b] ~ a + [F b] ~ b , with b := F a + +At this point (SkolemOccurs) does *not* apply anymore, as + + [F b] ~ b + +is not used as a rewrite rule. The variable b is not a skolem (cf +eqInstToRewrite). + +(The regression test indexed-types/should_compile/Simple20 checks that the +described property of the system does not change.) + \begin{code} skolemOccurs :: PrecondRule skolemOccurs insts @@ -498,40 +590,24 @@ skolemOccurs insts where oneSkolemOccurs inst = ASSERT( isEqInst inst ) - isRewriteRule (eqInstLeftTy inst) (eqInstRightTy inst) + case eqInstToRewrite inst of + Just (rewrite, swapped) -> breakRecursion rewrite swapped + Nothing -> return ([inst], return ()) where + -- inst is an elementary rewrite rule, check whether we need to break + -- it up + breakRecursion (Rewrite pat body _) swapped - -- look through synonyms - isRewriteRule ty1 ty2 | Just ty1' <- tcView ty1 = isRewriteRule ty1' ty2 - isRewriteRule ty1 ty2 | Just ty2' <- tcView ty2 = isRewriteRule ty1 ty2' - - -- left-to-right rule with type family head - isRewriteRule ty1@(TyConApp con _) ty2 - | isOpenSynTyCon con - = breakRecursion ty1 ty2 False -- not swapped - - -- left-to-right rule with type variable head - isRewriteRule ty1@(TyVarTy _) ty2 - = breakRecursion ty1 ty2 False -- not swapped - - -- right-to-left rule with type family head - isRewriteRule ty1 ty2@(TyConApp con _) - | isOpenSynTyCon con - = breakRecursion ty2 ty1 True -- swapped - - -- right-to-left rule with type variable head - isRewriteRule ty1 ty2@(TyVarTy _) - = breakRecursion ty2 ty1 True -- swapped - - -- this equality is not a rewrite rule => ignore - isRewriteRule _ _ = return ([inst], return ()) - - - breakRecursion pat body swapped + -- skolemOccurs does not apply, leave as is | null tysToLiftOut - = return ([inst], return ()) + = do { traceTc $ text "oneSkolemOccurs: no tys to lift out" + ; return ([inst], return ()) + } + + -- recursive occurence of pat in body under a type family application | 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 +615,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 +641,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} @@ -594,8 +672,7 @@ trivialRule insts | otherwise = return $ Just inst where - ty1 = eqInstLeftTy inst - ty2 = eqInstRightTy inst + (ty1,ty2) = eqInstTys inst \end{code} @@ -626,8 +703,9 @@ decompRule insts where decomp inst = ASSERT( isEqInst inst ) - go (eqInstLeftTy inst) (eqInstRightTy inst) + go ty1 ty2 where + (ty1,ty2) = eqInstTys inst go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' @@ -746,8 +824,7 @@ topRule insts } } where - ty1 = eqInstLeftTy inst - ty2 = eqInstRightTy inst + (ty1,ty2) = eqInstTys inst \end{code} @@ -799,43 +876,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 @@ -874,8 +922,7 @@ substInst inst insts } } where - ty1 = eqInstLeftTy inst - ty2 = eqInstRightTy inst + (ty1,ty2) = eqInstTys inst \end{code} @@ -912,9 +959,10 @@ unifyMetaRule insts where unifyMeta inst = ASSERT( isEqInst inst ) - go (eqInstLeftTy inst) (eqInstRightTy inst) + go ty1 ty2 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst) where + (ty1,ty2) = eqInstTys inst go ty1 ty2 cotv | Just ty1' <- tcView ty1 = go ty1' ty2 cotv | Just ty2' <- tcView ty2 = go ty1 ty2' cotv @@ -953,10 +1001,14 @@ unifyMetaRule insts -- updatable meta variable meets non-variable type -- => occurs check, monotype check, and kinds match check, then update uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv - = do { ty' <- checkTauTvUpdate tv ty -- occurs + monotype check - ; checkUpdateMeta swapped tv ref ty' -- update meta var - ; writeMetaTyVar cotv ty' -- update the co var - ; return ([], True) + = do { mb_ty' <- checkTauTvUpdate tv ty -- occurs + monotype check + ; case mb_ty' of + Nothing -> return ([inst], False) -- tv occurs in faminst + Just ty' -> + do { checkUpdateMeta swapped tv ref ty' -- update meta var + ; writeMetaTyVar cotv ty' -- update co var + ; return ([], True) + } } uMeta _ _ _ _ _ = panic "uMeta" @@ -1150,45 +1202,49 @@ somethingdifferent message. eqInstMisMatch :: Inst -> TcM a eqInstMisMatch inst = ASSERT( isEqInst inst ) - do { (env, msg) <- misMatchMsg ty_act ty_exp - ; setErrCtxt ctxt $ - failWithTcM (env, msg) - } + setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp where - ty_act = eqInstLeftTy inst - ty_exp = eqInstRightTy inst - InstLoc _ _ ctxt = instLoc inst + (ty_act, ty_exp) = eqInstTys inst + InstLoc _ _ ctxt = instLoc inst ----------------------- -misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc) +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 -misMatchMsg ty_act ty_exp +failWithMisMatch ty_act ty_exp = do { env0 <- tcInitTidyEnv ; ty_exp <- zonkTcType ty_exp ; ty_act <- zonkTcType ty_act - ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp - ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act - ; return (env2, - sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp, - nest 7 $ + ; 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)]) } - -ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc) -ppr_ty env ty - = do { let (env1, tidy_ty) = tidyOpenType env ty - ; (env2, extra) <- ppr_extra env1 tidy_ty - ; return (env2, quotes (ppr tidy_ty), extra) } - --- (ppr_extra env ty) shows extra info about 'ty' -ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc) -ppr_extra env (TyVarTy tv) - | isSkolemTyVar tv || isSigTyVar tv - = return (env1, pprSkolTvBinding tv1) + nest 2 (extra_exp $$ extra_act)] + in + (env2, msg) + where - (env1, tv1) = tidySkolemTyVar env tv + 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 = return (env, empty) -- Normal case + ppr_extra env _ty = (env, empty) -- Normal case \end{code}