From 654d07dd0fb679d014ac363e13c004b0086d0d6e Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Thu, 25 Sep 2008 08:41:39 +0000 Subject: [PATCH] Type families: fix decomposition problem * Fixes the problem reported in --- compiler/typecheck/TcTyFuns.lhs | 35 ++++++++++++++---------- compiler/typecheck/TcType.lhs | 5 ++-- compiler/typecheck/TcUnify.lhs | 57 +++++++++++++++++++-------------------- 3 files changed, 52 insertions(+), 45 deletions(-) diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 113ea43..bed053d 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -470,22 +470,29 @@ normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet) -- Normalise one equality. normEqInst inst = ASSERT( isEqInst inst ) - go ty1 ty2 (eqInstCoercion inst) + do { traceTc $ ptext (sLit "normEqInst of ") <+> + pprEqInstCo co <+> text "::" <+> + ppr ty1 <+> text "~" <+> ppr ty2 + ; res <- go ty1 ty2 co + ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res + ; return res + } where (ty1, ty2) = eqInstTys inst + co = eqInstCoercion 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 (TyConApp con args) ty2 co - | isOpenSynTyCon con + go ty1@(TyConApp con args) ty2 co + | isOpenSynTyConApp ty1 -- only if not oversaturated = mkRewriteFam False con args ty2 co -- right-to-left rule with type family head go ty1 ty2@(TyConApp con args) co - | isOpenSynTyCon con + | isOpenSynTyConApp ty2 -- only if not oversaturated = do { co' <- mkSymEqInstCo co (ty2, ty1) ; mkRewriteFam True con args ty1 co' } @@ -573,13 +580,7 @@ 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 - = 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 - } + = go ty1 ty2 where -- look through synonyms go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 @@ -669,10 +670,10 @@ flattenType inst ty go ty@(TyVarTy _) = return (ty, ty, [] , emptyVarSet) - -- type family application + -- type family application & family arity matches number of args -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh) go ty@(TyConApp con args) - | isOpenSynTyCon con + | isOpenSynTyConApp ty -- only if not oversaturated = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args ; alpha <- newFlexiTyVar (typeKind ty) ; let alphaTy = mkTyVarTy alpha @@ -695,6 +696,7 @@ flattenType inst ty -- data constructor application => flatten subtypes -- NB: Special cased for efficiency - could be handled as type application go ty@(TyConApp con args) + | not (isOpenSynTyCon con) -- don't match oversaturated family apps = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args ; if null args_eqss then -- unchanged, keep the old type with folded synonyms @@ -722,7 +724,10 @@ flattenType inst ty } -- type application => flatten subtypes - go ty@(AppTy ty_l ty_r) + go ty + | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty + -- need to use the smart split as ty may be an + -- oversaturated family application = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r ; if null eqs_l && null eqs_r @@ -749,6 +754,8 @@ flattenType inst ty go (PredTy _) = panic "TcTyFuns.flattenType: unexpected PredType" + go _ = panic "TcTyFuns: suppress bogus warning" + adjustCoercions :: EqInstCo -- coercion of original equality -> Coercion -- coercion witnessing the left rewrite -> Coercion -- coercion witnessing the right rewrite diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index 1a3fad7..fe5ea39 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -1007,8 +1007,9 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of -- hence no 'coreView'. This could, however, be changed without breaking -- any code. isOpenSynTyConApp :: TcTauType -> Bool -isOpenSynTyConApp (TyConApp tc _) = isOpenSynTyCon tc -isOpenSynTyConApp _other = False +isOpenSynTyConApp (TyConApp tc tys) = isOpenSynTyCon tc && + length tys == tyConArity tc +isOpenSynTyConApp _other = False \end{code} diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 94af19c..9f5daeb 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -1192,13 +1192,13 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 go outer _ (PredTy p1) _ (PredTy p2) = uPred outer nb1 p1 nb2 p2 - -- Type constructors must match + -- Non-synonym type constructors must match go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2) | con1 == con2 && not (isOpenSynTyCon con1) = do { cois <- uTys_s nb1 tys1 nb2 tys2 ; return $ mkTyConAppCoI con1 tys1 cois } - -- See Note [TyCon app] + -- Family synonyms See Note [TyCon app] | con1 == con2 && identicalOpenSynTyConApp = do { cois <- uTys_s nb1 tys1' nb2 tys2' ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois) @@ -1210,6 +1210,29 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2 -- See Note [OpenSynTyCon app] + -- If we can reduce a family app => proceed with reduct + -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must + -- defer oversaturated applications! + go outer sty1 ty1@(TyConApp con1 _) sty2 ty2 + | isOpenSynTyCon con1 + = do { (coi1, ty1') <- tcNormaliseFamInst ty1 + ; case coi1 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2 + } + + -- If we can reduce a family app => proceed with reduct + -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must + -- defer oversaturated applications! + go outer sty1 ty1 sty2 ty2@(TyConApp con2 _) + | isOpenSynTyCon con2 + = do { (coi2, ty2') <- tcNormaliseFamInst ty2 + ; case coi2 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (`mkTransCoI` mkSymCoI coi2) $ + go outer sty1 ty1 sty2 ty2' + } + -- Functions; just check the two parts go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2) = do { coi_l <- uTys nb1 fun1 nb2 fun2 @@ -1235,36 +1258,12 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 ; coi_t <- uTys nb1 t1 nb2 t2 ; return $ mkAppTyCoI s1 coi_s t1 coi_t } - -- One or both outermost constructors are type family applications. - -- If we can normalise them away, proceed as usual; otherwise, we - -- need to defer unification by generating a wanted equality constraint. - go outer sty1 ty1 sty2 ty2 - | ty1_is_fun || ty2_is_fun - = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1 - else return (IdCo, ty1) - ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2 - else return (IdCo, ty2) - ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2' - then do { -- One type family app can't be reduced yet - -- => defer - ; ty1'' <- zonkTcType ty1' - ; ty2'' <- zonkTcType ty2' - ; if tcEqType ty1'' ty2'' - then return IdCo - else -- see [Deferred Unification] - defer_unification outer False orig_ty1 orig_ty2 - } - else -- unification can proceed - go outer sty1 ty1' sty2 ty2' - ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2) - } - where - ty1_is_fun = isOpenSynTyConApp ty1 - ty2_is_fun = isOpenSynTyConApp ty2 - -- Anything else fails go outer _ _ _ _ = bale_out outer + defer = defer_unification outer False orig_ty1 orig_ty2 + + ---------- uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2) -- 1.7.10.4