Type families: fix decomposition problem

* Fixes the problem reported in 
  <http://www.haskell.org/pipermail/haskell-cafe/2008-July/044911.html>

3 files changed, 52 insertions, 45 deletions

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index 113ea43bd5..bed053d2d6 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 1a3fad7360..fe5ea39692 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 94af19c6ee..9f5daeb0bc 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)