FIX: Make boxy splitters aware of type families
authorManuel M T Chakravarty <chak@cse.unsw.edu.au>
Fri, 28 Sep 2007 22:55:41 +0000 (22:55 +0000)
committerManuel M T Chakravarty <chak@cse.unsw.edu.au>
Fri, 28 Sep 2007 22:55:41 +0000 (22:55 +0000)
MERGE TO STABLE

compiler/hsSyn/HsPat.lhs
compiler/hsSyn/HsUtils.lhs
compiler/typecheck/TcArrows.lhs
compiler/typecheck/TcExpr.lhs
compiler/typecheck/TcMatches.lhs
compiler/typecheck/TcPat.lhs
compiler/typecheck/TcUnify.lhs

index d4b0e1b..ddd6ec2 100644 (file)
@@ -19,7 +19,7 @@ module HsPat (
        HsConPatDetails, hsConPatArgs, 
        HsRecFields(..), HsRecField(..), hsRecFields,
 
-       mkPrefixConPat, mkCharLitPat, mkNilPat, mkCoPat,
+       mkPrefixConPat, mkCharLitPat, mkNilPat, mkCoPat, mkCoPatCoI,
 
        isBangHsBind,   
        patsAreAllCons, isConPat, isSigPat, isWildPat,
@@ -37,6 +37,7 @@ import HsLit
 import HsTypes
 import BasicTypes
 -- others:
+import Coercion
 import PprCore         ( {- instance OutputableBndr TyVar -} )
 import TysWiredIn
 import Var
@@ -292,10 +293,14 @@ mkNilPat ty = mkPrefixConPat nilDataCon [] ty
 mkCharLitPat :: Char -> OutPat id
 mkCharLitPat c = mkPrefixConPat charDataCon [noLoc $ LitPat (HsCharPrim c)] charTy
 
-mkCoPat :: HsWrapper -> OutPat id -> Type -> OutPat id
-mkCoPat co lpat@(L loc pat) ty
-  | isIdHsWrapper co = lpat
-  | otherwise = L loc (CoPat co pat ty)
+mkCoPat :: HsWrapper -> Pat id -> Type -> Pat id
+mkCoPat co pat ty
+  | isIdHsWrapper co = pat
+  | otherwise        = CoPat co pat ty
+
+mkCoPatCoI :: CoercionI -> Pat id -> Type -> Pat id
+mkCoPatCoI IdCo     pat ty = pat
+mkCoPatCoI (ACo co) pat ty = mkCoPat (WpCo co) pat ty
 \end{code}
 
 
index 3b9271a..0f75769 100644 (file)
@@ -32,6 +32,7 @@ import HsLit
 
 import RdrName
 import Var
+import Coercion
 import Type
 import DataCon
 import Name
@@ -89,6 +90,10 @@ mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
 mkHsWrap co_fn e | isIdHsWrapper co_fn = e
                 | otherwise          = HsWrap co_fn e
 
+mkHsWrapCoI :: CoercionI -> HsExpr id -> HsExpr id
+mkHsWrapCoI IdCo     e = e
+mkHsWrapCoI (ACo co) e = mkHsWrap (WpCo co) e
+
 mkHsLam :: [LPat id] -> LHsExpr id -> LHsExpr id
 mkHsLam pats body = mkHsPar (L (getLoc body) (HsLam matches))
        where
index c575808..8276bc8 100644 (file)
@@ -31,6 +31,7 @@ import TcGadt
 import TcPat
 import TcUnify
 import TcRnMonad
+import Coercion
 import Inst
 import Name
 import TysWiredIn
@@ -52,16 +53,18 @@ import Util
 \begin{code}
 tcProc :: InPat Name -> LHsCmdTop Name         -- proc pat -> expr
        -> BoxyRhoType                          -- Expected type of whole proc expression
-       -> TcM (OutPat TcId, LHsCmdTop TcId)
+       -> TcM (OutPat TcId, LHsCmdTop TcId, CoercionI)
 
 tcProc pat cmd exp_ty
   = newArrowScope $
-    do { (exp_ty1, res_ty) <- boxySplitAppTy exp_ty 
-       ; (arr_ty, arg_ty)  <- boxySplitAppTy exp_ty1
+    do { ((exp_ty1, res_ty), coi) <- boxySplitAppTy exp_ty 
+       ; ((arr_ty, arg_ty), coi1) <- boxySplitAppTy exp_ty1
        ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
        ; (pat', cmd') <- tcLamPat pat arg_ty (emptyRefinement, res_ty) $
                          tcCmdTop cmd_env cmd []
-       ; return (pat', cmd') }
+        ; let res_coi = mkTransCoI coi (mkAppTyCoI exp_ty1 coi1 res_ty IdCo)
+       ; return (pat', cmd', res_coi) 
+        }
 \end{code}
 
 
index e03f65d..2c17568 100644 (file)
@@ -133,7 +133,7 @@ tcExpr (HsVar name)     res_ty = tcId (OccurrenceOf name) name res_ty
 
 tcExpr (HsLit lit)     res_ty = do { let lit_ty = hsLitType lit
                                    ; coi <- boxyUnify lit_ty res_ty
-                                   ; return $ wrapExprCoI (HsLit lit) coi
+                                   ; return $ mkHsWrapCoI coi (HsLit lit)
                                    }
 
 tcExpr (HsPar expr)     res_ty = do { expr' <- tcMonoExpr expr res_ty
@@ -289,33 +289,21 @@ tcExpr (HsDo do_or_lc stmts body _) res_ty
   = tcDoStmts do_or_lc stmts body res_ty
 
 tcExpr in_expr@(ExplicitList _ exprs) res_ty   -- Non-empty list
-  = do         { elt_ty <- boxySplitListTy res_ty
+  = do         { (elt_ty, coi) <- boxySplitListTy res_ty
        ; exprs' <- mappM (tc_elt elt_ty) exprs
-       ; return (ExplicitList elt_ty exprs') }
+       ; return $ mkHsWrapCoI coi (ExplicitList elt_ty exprs') }
   where
     tc_elt elt_ty expr = tcPolyExpr expr elt_ty
-{- TODO: Version from Tom's original patch.  Unfortunately, we cannot do it this
-   way, but need to teach boxy splitters about match deferral and coercions.
-  = do         { elt_tv <- newBoxyTyVar argTypeKind
-       ; let elt_ty = TyVarTy elt_tv
-       ; coi    <- boxyUnify (mkTyConApp listTyCon [elt_ty]) res_ty
-       -- ; elt_ty <- boxySplitListTy res_ty
-       ; exprs' <- mappM (tc_elt elt_ty) exprs
-       ; return $ wrapExprCoI (ExplicitList elt_ty exprs') coi  }
-       -- ; return (ExplicitList elt_ty exprs') }
-  where
-    tc_elt elt_ty expr = tcPolyExpr expr elt_ty
- -}
 
 tcExpr in_expr@(ExplicitPArr _ exprs) res_ty   -- maybe empty
-  = do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty
+  = do { (elt_ty, coi) <- boxySplitPArrTy res_ty
        ; exprs' <- mappM (tc_elt elt_ty) exprs 
        ; ifM (null exprs) (zapToMonotype elt_ty)
                -- If there are no expressions in the comprehension
                -- we must still fill in the box
                -- (Not needed for [] and () becuase they happen
                --  to parse as data constructors.)
-       ; return (ExplicitPArr elt_ty exprs') }
+       ; return $ mkHsWrapCoI coi (ExplicitPArr elt_ty exprs') }
   where
     tc_elt elt_ty expr = tcPolyExpr expr elt_ty
 
@@ -335,8 +323,8 @@ tcExpr (ExplicitTuple exprs boxity) res_ty
        ; return (mkHsWrap co_fn (ExplicitTuple exprs' boxity)) }
 
 tcExpr (HsProc pat cmd) res_ty
-  = do { (pat', cmd') <- tcProc pat cmd res_ty
-       ; return (HsProc pat' cmd') }
+  = do { (pat', cmd', coi) <- tcProc pat cmd res_ty
+       ; return $ mkHsWrapCoI coi (HsProc pat' cmd') }
 
 tcExpr e@(HsArrApp _ _ _ _ _) _
   = failWithTc (vcat [ptext SLIT("The arrow command"), nest 2 (ppr e), 
@@ -527,54 +515,58 @@ tcExpr expr@(RecordUpd record_expr rbinds _ _ _) res_ty
 
 \begin{code}
 tcExpr (ArithSeq _ seq@(From expr)) res_ty
-  = do { elt_ty <- boxySplitListTy res_ty
+  = do { (elt_ty, coi) <- boxySplitListTy res_ty
        ; expr' <- tcPolyExpr expr elt_ty
        ; enum_from <- newMethodFromName (ArithSeqOrigin seq) 
                              elt_ty enumFromName
-       ; return (ArithSeq (HsVar enum_from) (From expr')) }
+       ; return $ mkHsWrapCoI coi (ArithSeq (HsVar enum_from) (From expr')) }
 
 tcExpr in_expr@(ArithSeq _ seq@(FromThen expr1 expr2)) res_ty
-  = do { elt_ty <- boxySplitListTy res_ty
+  = do { (elt_ty, coi) <- boxySplitListTy res_ty
        ; expr1' <- tcPolyExpr expr1 elt_ty
        ; expr2' <- tcPolyExpr expr2 elt_ty
        ; enum_from_then <- newMethodFromName (ArithSeqOrigin seq) 
                              elt_ty enumFromThenName
-       ; return (ArithSeq (HsVar enum_from_then) (FromThen expr1' expr2')) }
-
+       ; return $ mkHsWrapCoI coi 
+                    (ArithSeq (HsVar enum_from_then) (FromThen expr1' expr2')) }
 
 tcExpr in_expr@(ArithSeq _ seq@(FromTo expr1 expr2)) res_ty
-  = do { elt_ty <- boxySplitListTy res_ty
+  = do { (elt_ty, coi) <- boxySplitListTy res_ty
        ; expr1' <- tcPolyExpr expr1 elt_ty
        ; expr2' <- tcPolyExpr expr2 elt_ty
        ; enum_from_to <- newMethodFromName (ArithSeqOrigin seq) 
                              elt_ty enumFromToName
-       ; return (ArithSeq (HsVar enum_from_to) (FromTo expr1' expr2')) }
+       ; return $ mkHsWrapCoI coi 
+                     (ArithSeq (HsVar enum_from_to) (FromTo expr1' expr2')) }
 
 tcExpr in_expr@(ArithSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty
-  = do { elt_ty <- boxySplitListTy res_ty
+  = do { (elt_ty, coi) <- boxySplitListTy res_ty
        ; expr1' <- tcPolyExpr expr1 elt_ty
        ; expr2' <- tcPolyExpr expr2 elt_ty
        ; expr3' <- tcPolyExpr expr3 elt_ty
        ; eft <- newMethodFromName (ArithSeqOrigin seq) 
                      elt_ty enumFromThenToName
-       ; return (ArithSeq (HsVar eft) (FromThenTo expr1' expr2' expr3')) }
+       ; return $ mkHsWrapCoI coi 
+                     (ArithSeq (HsVar eft) (FromThenTo expr1' expr2' expr3')) }
 
 tcExpr in_expr@(PArrSeq _ seq@(FromTo expr1 expr2)) res_ty
-  = do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty
+  = do { (elt_ty, coi) <- boxySplitPArrTy res_ty
        ; expr1' <- tcPolyExpr expr1 elt_ty
        ; expr2' <- tcPolyExpr expr2 elt_ty
        ; enum_from_to <- newMethodFromName (PArrSeqOrigin seq) 
                                      elt_ty enumFromToPName
-       ; return (PArrSeq (HsVar enum_from_to) (FromTo expr1' expr2')) }
+       ; return $ mkHsWrapCoI coi 
+                     (PArrSeq (HsVar enum_from_to) (FromTo expr1' expr2')) }
 
 tcExpr in_expr@(PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty
-  = do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty
+  = do { (elt_ty, coi) <- boxySplitPArrTy res_ty
        ; expr1' <- tcPolyExpr expr1 elt_ty
        ; expr2' <- tcPolyExpr expr2 elt_ty
        ; expr3' <- tcPolyExpr expr3 elt_ty
        ; eft <- newMethodFromName (PArrSeqOrigin seq)
                      elt_ty enumFromThenToPName
-       ; return (PArrSeq (HsVar eft) (FromThenTo expr1' expr2' expr3')) }
+       ; return $ mkHsWrapCoI coi 
+                     (PArrSeq (HsVar eft) (FromThenTo expr1' expr2' expr3')) }
 
 tcExpr (PArrSeq _ _) _ 
   = panic "TcExpr.tcMonoExpr: Infinite parallel array!"
@@ -1214,9 +1206,3 @@ polySpliceErr id
   = ptext SLIT("Can't splice the polymorphic local variable") <+> quotes (ppr id)
 #endif
 \end{code}
-
-\begin{code}
-wrapExprCoI :: HsExpr a -> CoercionI -> HsExpr a
-wrapExprCoI expr IdCo     = expr
-wrapExprCoI expr (ACo co) = mkHsWrap (WpCo co) expr
-\end{code}
index 54f8756..3569038 100644 (file)
@@ -222,29 +222,31 @@ tcDoStmts :: HsStmtContext Name
          -> BoxyRhoType
          -> TcM (HsExpr TcId)          -- Returns a HsDo
 tcDoStmts ListComp stmts body res_ty
-  = do { elt_ty <- boxySplitListTy res_ty
+  = do { (elt_ty, coi) <- boxySplitListTy res_ty
        ; (stmts', body') <- tcStmts ListComp (tcLcStmt listTyCon) stmts 
                                     (emptyRefinement,elt_ty) $
                             tcBody body
-       ; return (HsDo ListComp stmts' body' (mkListTy elt_ty)) }
+       ; return $ mkHsWrapCoI coi 
+                     (HsDo ListComp stmts' body' (mkListTy elt_ty)) }
 
 tcDoStmts PArrComp stmts body res_ty
-  = do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty
+  = do { (elt_ty, coi) <- boxySplitPArrTy res_ty
        ; (stmts', body') <- tcStmts PArrComp (tcLcStmt parrTyCon) stmts 
                                     (emptyRefinement, elt_ty) $
                             tcBody body
-       ; return (HsDo PArrComp stmts' body' (mkPArrTy elt_ty)) }
+       ; return $ mkHsWrapCoI coi 
+                     (HsDo PArrComp stmts' body' (mkPArrTy elt_ty)) }
 
 tcDoStmts DoExpr stmts body res_ty
-  = do { (m_ty, elt_ty) <- boxySplitAppTy res_ty
+  = do { ((m_ty, elt_ty), coi) <- boxySplitAppTy res_ty
        ; let res_ty' = mkAppTy m_ty elt_ty     -- The boxySplit consumes res_ty
        ; (stmts', body') <- tcStmts DoExpr (tcDoStmt m_ty) stmts 
                                     (emptyRefinement, res_ty') $
                             tcBody body
-       ; return (HsDo DoExpr stmts' body' res_ty') }
+       ; return $ mkHsWrapCoI coi (HsDo DoExpr stmts' body' res_ty') }
 
 tcDoStmts ctxt@(MDoExpr _) stmts body res_ty
-  = do { (m_ty, elt_ty) <- boxySplitAppTy res_ty
+  = do { ((m_ty, elt_ty), coi) <- boxySplitAppTy res_ty
        ; let res_ty' = mkAppTy m_ty elt_ty     -- The boxySplit consumes res_ty
              tc_rhs rhs = withBox liftedTypeKind $ \ pat_ty ->
                           tcMonoExpr rhs (mkAppTy m_ty pat_ty)
@@ -255,7 +257,9 @@ tcDoStmts ctxt@(MDoExpr _) stmts body res_ty
 
        ; let names = [mfixName, bindMName, thenMName, returnMName, failMName]
        ; insts <- mapM (newMethodFromName DoOrigin m_ty) names
-       ; return (HsDo (MDoExpr (names `zip` insts)) stmts' body' res_ty') }
+       ; return $ 
+            mkHsWrapCoI coi 
+              (HsDo (MDoExpr (names `zip` insts)) stmts' body' res_ty') }
 
 tcDoStmts ctxt stmts body res_ty = pprPanic "tcDoStmts" (pprStmtContext ctxt)
 
index 0640675..f009db5 100644 (file)
@@ -408,20 +408,21 @@ tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
 ------------------------
 -- Lists, tuples, arrays
 tc_pat pstate (ListPat pats _) pat_ty thing_inside
-  = do { elt_ty <- boxySplitListTy pat_ty
+  = do { (elt_ty, coi) <- boxySplitListTy pat_ty
        ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                                pats pstate thing_inside
-       ; return (ListPat pats' elt_ty, pats_tvs, res) }
+       ; return (mkCoPatCoI coi (ListPat pats' elt_ty) pat_ty, pats_tvs, res) }
 
 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
-  = do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
+  = do { (elt_ty, coi) <- boxySplitPArrTy pat_ty
        ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                                pats pstate thing_inside 
-       ; ifM (null pats) (zapToMonotype pat_ty)        -- c.f. ExplicitPArr in TcExpr
-       ; return (PArrPat pats' elt_ty, pats_tvs, res) }
+       ; ifM (null pats) (zapToMonotype pat_ty)  -- c.f. ExplicitPArr in TcExpr
+       ; return (mkCoPatCoI coi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res) }
 
 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
-  = do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
+  = do { let tc = tupleTyCon boxity (length pats)
+        ; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty
        ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
                                               pstate thing_inside
 
@@ -429,13 +430,17 @@ tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
        -- so that we can experiment with lazy tuple-matching.
        -- This is a pretty odd place to make the switch, but
        -- it was easy to do.
-       ; let unmangled_result = TuplePat pats' boxity pat_ty
+       ; let pat_ty'          = mkTyConApp tc arg_tys
+                                     -- pat_ty /= pat_ty iff coi /= IdCo
+              unmangled_result = TuplePat pats' boxity pat_ty'
              possibly_mangled_result
-               | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
-               | otherwise                               = unmangled_result
+               | opt_IrrefutableTuples && 
+                  isBoxed boxity            = LazyPat (noLoc unmangled_result)
+               | otherwise                 = unmangled_result
 
-       ; ASSERT( length arg_tys == length pats )       -- Syntactically enforced
-         return (possibly_mangled_result, pats_tvs, res) }
+       ; ASSERT( length arg_tys == length pats )      -- Syntactically enforced
+         return (mkCoPatCoI coi possibly_mangled_result pat_ty, pats_tvs, res) 
+        }
 
 ------------------------
 -- Data constructors
@@ -455,7 +460,8 @@ tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
                        -- pattern coercions have to
                        -- be of kind: pat_ty ~ lit_ty
                        -- hence, sym coi
-       ; returnM (wrapPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, [], res) }
+       ; returnM (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, 
+                   [], res) }
 
 ------------------------
 -- Overloaded patterns: n, and n+k
@@ -571,7 +577,7 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
              origin    = SigOrigin skol_info
 
          -- Instantiate the constructor type variables [a->ty]
-       ; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty
+       ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty
        ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs  -- Get location from monad,
                                                        -- not from ex_tvs
        ; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
@@ -593,13 +599,16 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 
        ; addDataConStupidTheta data_con ctxt_res_tys
 
-       ; return
-           (unwrapFamInstScrutinee tycon ctxt_res_tys $
-              ConPatOut { pat_con = L con_span data_con, 
-                          pat_tvs = ex_tvs' ++ co_vars,
-                          pat_dicts = map instToVar dicts, 
-                          pat_binds = dict_binds,
-                          pat_args = arg_pats', pat_ty = pat_ty },
+        ; let pat_ty' = mkTyConApp tycon ctxt_res_tys
+                                     -- pat_ty /= pat_ty iff coi /= IdCo
+              res_pat = ConPatOut { pat_con = L con_span data_con, 
+                                   pat_tvs = ex_tvs' ++ co_vars,
+                                   pat_dicts = map instToVar dicts, 
+                                   pat_binds = dict_binds,
+                                   pat_args = arg_pats', pat_ty = pat_ty' }
+       ; return 
+           (mkCoPatCoI coi
+               (unwrapFamInstScrutinee tycon ctxt_res_tys res_pat) pat_ty,
             ex_tvs' ++ inner_tvs, res)
        }
   where
@@ -610,10 +619,10 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
       case tyConFamInst_maybe tycon of
         Nothing                   -> boxySplitTyConApp tycon pat_ty
        Just (fam_tycon, instTys) -> 
-         do { scrutinee_arg_tys <- boxySplitTyConApp fam_tycon pat_ty
+         do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty
             ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
             ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
-            ; return freshTvs
+            ; return (freshTvs, coi)
             }
       where
         traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
@@ -992,9 +1001,3 @@ nonRigidResult res_ty
 inaccessibleAlt msg
   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
 \end{code}
-
-\begin{code}
-wrapPatCoI :: CoercionI -> Pat a -> TcType -> Pat a
-wrapPatCoI IdCo     pat ty = pat
-wrapPatCoI (ACo co) pat ty = CoPat (WpCo co) pat ty
-\end{code}
index 233e87d..67cdf20 100644 (file)
@@ -28,7 +28,7 @@ module TcUnify (
   -- Holes
   tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, 
   boxyUnify, boxyUnifyList, zapToMonotype,
-  boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
+  boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy,
   wrapFunResCoercion
   ) where
 
@@ -191,8 +191,9 @@ subFunTys error_herald n_pats res_ty thing_inside
 ----------------------
 boxySplitTyConApp :: TyCon                     -- T :: k1 -> ... -> kn -> *
                  -> BoxyRhoType                -- Expected type (T a b c)
-                 -> TcM [BoxySigmaType]        -- Element types, a b c
-  -- It's used for wired-in tycons, so we call checkWiredInTyCOn
+                 -> TcM ([BoxySigmaType],      -- Element types, a b c
+                          CoercionI)
+  -- It's used for wired-in tycons, so we call checkWiredInTyCon
   -- Precondition: never called with FunTyCon
   -- Precondition: input type :: *
 
@@ -203,14 +204,26 @@ boxySplitTyConApp tc orig_ty
     loop n_req args_so_far ty 
       | Just ty' <- tcView ty = loop n_req args_so_far ty'
 
-    loop n_req args_so_far (TyConApp tycon args)
+    loop n_req args_so_far ty@(TyConApp tycon args)
       | tc == tycon
       = ASSERT( n_req == length args)  -- ty::*
-       return (args ++ args_so_far)
+       return (args ++ args_so_far, IdCo)
+
+      | isOpenSynTyCon tycon        -- try to normalise type family application
+      = do { (coi1, ty') <- tcNormaliseFamInst ty
+           ; case coi1 of
+              IdCo   -> defer    -- no progress, but maybe solvable => defer
+               ACo _  ->          -- progress: so lets try again
+                do { (args, coi2) <- loop n_req args_so_far ty'
+                   ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
+                   }
+           }
 
     loop n_req args_so_far (AppTy fun arg)
       | n_req > 0
-      = loop (n_req - 1) (arg:args_so_far) fun
+      = do { (args, coi) <- loop (n_req - 1) (arg:args_so_far) fun
+           ; return (args, mkAppTyCoI fun coi arg IdCo)
+           }
 
     loop n_req args_so_far (TyVarTy tv)
       | isTyConableTyVar tv
@@ -219,23 +232,42 @@ boxySplitTyConApp tc orig_ty
           ; case cts of
               Indirect ty -> loop n_req args_so_far ty
               Flexi       -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
-                                ; return (arg_tys ++ args_so_far) }
-       }
+                                ; return (arg_tys ++ args_so_far, IdCo) }
+          }
+      | otherwise             -- defer as tyvar may be refined by equalities
+      = defer
       where
-       mk_res_ty arg_tys' = mkTyConApp tc arg_tys'
        (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc)
 
-    loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty
+    loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc)))
+                                  orig_ty
+
+    -- defer splitting by generating an equality constraint
+    defer = boxySplitDefer arg_kinds mk_res_ty orig_ty
+      where
+        (arg_kinds, _) = splitKindFunTys (tyConKind tc)
+
+    -- apply splitted tycon to arguments
+    mk_res_ty = mkTyConApp tc
 
 ----------------------
-boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType    -- Special case for lists
-boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty
-                           ; return elt_ty }
+boxySplitListTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
+-- Special case for lists
+boxySplitListTy exp_ty 
+ = do { ([elt_ty], coi) <- boxySplitTyConApp listTyCon exp_ty
+      ; return (elt_ty, coi) }
 
+----------------------
+boxySplitPArrTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
+-- Special case for parrs
+boxySplitPArrTy exp_ty 
+  = do { ([elt_ty], coi) <- boxySplitTyConApp parrTyCon exp_ty
+       ; return (elt_ty, coi) }
 
 ----------------------
 boxySplitAppTy :: BoxyRhoType                          -- Type to split: m a
-              -> TcM (BoxySigmaType, BoxySigmaType)    -- Returns m, a
+              -> TcM ((BoxySigmaType, BoxySigmaType),  -- Returns m, a
+                       CoercionI)
 -- If the incoming type is a mutable type variable of kind k, then 
 -- boxySplitAppTy returns a new type variable (m: * -> k); note the *.
 -- If the incoming type is boxy, then so are the result types; and vice versa
@@ -248,18 +280,29 @@ boxySplitAppTy orig_ty
 
     loop ty 
       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
-      = return (fun_ty, arg_ty)
+      = return ((fun_ty, arg_ty), IdCo)
+
+    loop ty@(TyConApp tycon args)
+      | isOpenSynTyCon tycon        -- try to normalise type family application
+      = do { (coi1, ty') <- tcNormaliseFamInst ty
+           ; case coi1 of
+              IdCo   -> defer    -- no progress, but maybe solvable => defer
+               ACo co ->          -- progress: so lets try again
+                do { (args, coi2) <- loop ty'
+                   ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
+                   }
+           }
 
     loop (TyVarTy tv)
       | isTyConableTyVar tv
       = do { cts <- readMetaTyVar tv
           ; case cts of
               Indirect ty -> loop ty
-              Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty
-                                ; return (fun_ty, arg_ty) } }
+              Flexi -> do { [fun_ty, arg_ty] <- withMetaTvs tv kinds mk_res_ty
+                          ; return ((fun_ty, arg_ty), IdCo) } }
+      | otherwise             -- defer as tyvar may be refined by equalities
+      = defer
       where
-        mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
-       mk_res_ty other = panic "TcUnify.mk_res_ty2"
        tv_kind = tyVarKind tv
        kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind),
                                                -- m :: * -> k
@@ -271,11 +314,36 @@ boxySplitAppTy orig_ty
        
     loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty
 
+    -- defer splitting by generating an equality constraint
+    defer = do { ([ty1, ty2], coi) <- boxySplitDefer arg_kinds mk_res_ty orig_ty
+               ; return ((ty1, ty2), coi)
+               }
+      where
+       orig_kind = typeKind orig_ty
+       arg_kinds = [mkArrowKind liftedTypeKind (defaultKind orig_kind),
+                                               -- m :: * -> k
+                    liftedTypeKind]            -- arg type :: *
+    -- build type application
+    mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
+    mk_res_ty _other             = panic "TcUnify.mk_res_ty2"
+
 ------------------
 boxySplitFailure actual_ty expected_ty
   = unifyMisMatch False False actual_ty expected_ty
        -- "outer" is False, so we don't pop the context
        -- which is what we want since we have not pushed one!
+
+------------------
+boxySplitDefer :: [Kind]                   -- kinds of required arguments
+               -> ([TcType] -> TcTauType)  -- construct lhs from argument tyvars
+               -> BoxyRhoType              -- type to split
+               -> TcM ([TcType], CoercionI)
+boxySplitDefer kinds mkTy orig_ty
+  = do { tau_tys <- mapM newFlexiTyVarTy kinds
+       ; coi <- defer_unification False False (mkTy tau_tys) orig_ty
+       ; return (tau_tys, coi)
+       }
 \end{code}