diff options
author | simonpj@microsoft.com <unknown> | 2009-12-11 12:01:22 +0000 |
---|---|---|
committer | simonpj@microsoft.com <unknown> | 2009-12-11 12:01:22 +0000 |
commit | dcba7784a1af5fd0c054031c49fe159d69af4f86 (patch) | |
tree | 602a9bbc98221971dafaa4511f13d8e1846d8cb8 | |
parent | ab222dbdbf95e9a6a63dc4f8ed8cb7fc7784a991 (diff) | |
download | haskell-dcba7784a1af5fd0c054031c49fe159d69af4f86.tar.gz |
Fix two related bugs in u_tys
When we normalise a type family application we must recursively call
uTys, *not* 'go', because the latter loop is only there to look
through type synonyms. This bug made the type checker generate
ill-typed coercions, which were rejected by Core Lint.
A related bug only affects the size of coercions. If faced with
(m a) ~ (F b c)
where F has arity 1, we want to decompose to
m ~ F Int, a ~ c
rather than deferring. The application decomposition was being
tried last, so we were missing this opportunity.
Thanks to Roman for an example that showed all this up.
-rw-r--r-- | compiler/typecheck/TcUnify.lhs | 47 |
1 files changed, 24 insertions, 23 deletions
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 064f19956a..b067d99ebe 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -1213,29 +1213,6 @@ 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 @@ -1261,6 +1238,30 @@ 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 } + -- If we can reduce a family app => proceed with reduct + -- NB1: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must + -- defer oversaturated applications! + -- + -- NB2: Do this *after* trying decomposing applications, so that decompose + -- (m a) ~ (F Int b) + -- where F has arity 1 + go _ _ ty1@(TyConApp con1 _) _ ty2 + | isOpenSynTyCon con1 + = do { (coi1, ty1') <- tcNormaliseFamInst ty1 + ; case coi1 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (coi1 `mkTransCoI`) $ uTys nb1 ty1' nb2 ty2 + } + + go _ _ ty1 _ ty2@(TyConApp con2 _) + | isOpenSynTyCon con2 + = do { (coi2, ty2') <- tcNormaliseFamInst ty2 + ; case coi2 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (`mkTransCoI` mkSymCoI coi2) $ + uTys nb1 ty1 nb2 ty2' + } + -- Anything else fails go outer _ _ _ _ = bale_out outer |