summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorsimonpj@microsoft.com <unknown>2009-12-11 12:01:22 +0000
committersimonpj@microsoft.com <unknown>2009-12-11 12:01:22 +0000
commitdcba7784a1af5fd0c054031c49fe159d69af4f86 (patch)
tree602a9bbc98221971dafaa4511f13d8e1846d8cb8
parentab222dbdbf95e9a6a63dc4f8ed8cb7fc7784a991 (diff)
downloadhaskell-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.lhs47
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