Merge branch 'tc-untouchables' of http://darcs.haskell.org/ghc into tc-untouchables

8 files changed, 112 insertions, 109 deletions

diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs
index b6370b5c92..27588901e7 100644
--- a/compiler/typecheck/FamInst.lhs
+++ b/compiler/typecheck/FamInst.lhs
@@ -177,7 +177,9 @@ tcLookupFamInst tycon tys
   | otherwise
   = do { instEnv <- tcGetFamInstEnvs
        ; let mb_match = lookupFamInstEnv instEnv tycon tys 
-       ; traceTc "lookupFamInst" ((ppr tycon <+> ppr tys) $$ pprTvBndrs (varSetElems (tyVarsOfTypes tys)) $$ ppr mb_match $$ ppr instEnv)
+--       ; traceTc "lookupFamInst" ((ppr tycon <+> ppr tys) $$ 
+--                                  pprTvBndrs (varSetElems (tyVarsOfTypes tys)) $$ 
+--                                  ppr mb_match $$ ppr instEnv)
        ; case mb_match of
 	   [] -> return Nothing
 	   ((fam_inst, rep_tys):_) 
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 826375bd02..a966a39f4e 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -247,20 +247,15 @@ canClassNC d ev cls tys
     `andWhenContinue` emitSuperclasses
 
 canClass d ev cls tys
-  = do { -- sctx <- getTcSContext
-       ; (xis, cos) <- flattenMany d FMFullFlatten (ctEvFlavour ev) tys
+  = do { (xis, cos) <- flattenMany d FMFullFlatten (ctEvFlavour ev) tys
        ; let co = mkTcTyConAppCo (classTyCon cls) cos 
              xi = mkClassPred cls xis
-             
        ; mb <- rewriteCtFlavor ev xi co
-
        ; case mb of
-           Just new_ev -> 
-             let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_ev)
-             in continueWith $ 
-                CDictCan { cc_ev = new_ev, cc_loc = d
-                         , cc_tyargs = xis_for_dict, cc_class = cls }
-           Nothing -> return Stop }
+           Nothing -> return Stop
+           Just new_ev -> continueWith $ 
+                          CDictCan { cc_ev = new_ev, cc_loc = d
+                                   , cc_tyargs = xis, cc_class = cls } }
 
 emitSuperclasses :: Ct -> TcS StopOrContinue
 emitSuperclasses ct@(CDictCan { cc_loc = d, cc_ev = ev
@@ -567,24 +562,22 @@ flatten loc f ctxt (TyConApp tc tys)
                             			     , cc_tyargs = xi_args    
                             			     , cc_rhs    = rhs_ty
                             			     , cc_loc  = loc }
-                                ; updWorkListTcS $ extendWorkListEq ct
+                                ; updWorkListTcS $ extendWorkListFunEq ct
                                 ; return (co, rhs_ty) }
 
                          | otherwise -- Wanted or Derived: make new unification variable
                          -> do { traceTcS "flatten/flat-cache miss" $ empty 
                                ; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
-                               ; let pred = mkTcEqPred fam_ty rhs_xi_var
-                               ; mw <- newWantedEvVar pred
-                               ; case mw of
-                                   Fresh ctev -> 
-                                     do { let ct = CFunEqCan { cc_ev = ctev
-                                                             , cc_fun = tc
-                                                             , cc_tyargs = xi_args
-                                                             , cc_rhs    = rhs_xi_var 
-                                                             , cc_loc    = loc }
-                                        ; updWorkListTcS $ extendWorkListEq ct
-                                        ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
-                                   Cached {} -> panic "flatten TyConApp, var must be fresh!" } 
+                               ; ctev <- newWantedEvVarNC (mkTcEqPred fam_ty rhs_xi_var)
+                                   -- NC (no-cache) version because we've already
+                                   -- looked in the solved goals an inerts (lookupFlatEqn)
+                               ; let ct = CFunEqCan { cc_ev = ctev
+                                                    , cc_fun = tc
+                                                    , cc_tyargs = xi_args
+                                                    , cc_rhs    = rhs_xi_var 
+                                                    , cc_loc    = loc }
+                               ; updWorkListTcS $ extendWorkListFunEq ct
+                               ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
                     }
                   -- Emit the flat constraints
          ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
@@ -1071,19 +1064,15 @@ reOrient :: CtEvidence -> TypeClassifier -> TypeClassifier -> Bool
 -- We try to say False if possible, to minimise evidence generation
 --
 -- Postcondition: After re-orienting, first arg is not OTherCls
-reOrient _ev (OtherCls {}) (FunCls {})   = True
-reOrient _ev (OtherCls {}) (VarCls {})   = True
-reOrient _ev (OtherCls {}) (OtherCls {}) = panic "reOrient"  -- One must be Var/Fun
+reOrient _ev (OtherCls {}) cls2 = ASSERT( case cls2 of { OtherCls {} -> False; _ -> True } )
+                                  True  -- One must be Var/Fun
 
-reOrient _ev (FunCls {})   (VarCls _tv)  = False  
+reOrient _ev (FunCls {}) _      = False             -- Fun/Other on rhs
   -- But consider the following variation: isGiven ev && isMetaTyVar tv
-
   -- See Note [No touchables as FunEq RHS] in TcSMonad
-reOrient _ev (FunCls {}) _                = False             -- Fun/Other on rhs
-
-reOrient _ev (VarCls {}) (FunCls {})      = True 
-reOrient _ev (VarCls {})  (OtherCls {})   = False
 
+reOrient _ev (VarCls {})   (FunCls {})      = True 
+reOrient _ev (VarCls {})   (OtherCls {})   = False
 reOrient _ev (VarCls tv1)  (VarCls tv2)  
   | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True 
   | otherwise                                = False 
@@ -1153,7 +1142,7 @@ canEqLeafFunEq loc ev fn tys1 ty2  -- ev :: F tys1 ~ ty2
            Nothing -> return Stop ;
            Just new_ev 
              | isTcReflCo xco -> continueWith new_ct
-             | otherwise      -> do { updWorkListTcS (extendWorkListEq new_ct); return Stop }
+             | otherwise      -> do { updWorkListTcS (extendWorkListFunEq new_ct); return Stop }
              where
                new_ct = CFunEqCan { cc_ev = new_ev, cc_loc = loc
                                   , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } } } 
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 73a648f8ff..4d468721d8 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -296,11 +296,10 @@ spontaneousSolveStage workItem
            SPSolved new_tv
               -- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
               -- see Note [Spontaneously solved in TyBinds]
-              -> do { bumpStepCountTcS
-                   ; traceFireTcS workItem $
-                     ptext (sLit "Spontaneously solved:") <+> ppr workItem
-                   ; kickOutRewritable Given new_tv
-                   ; return Stop } }
+              -> do { traceFireTcS workItem $
+                      ptext (sLit "Spontaneously solved:") <+> ppr workItem
+                    ; kickOutRewritable Given new_tv
+                    ; return Stop } }
 \end{code}
 Note [Spontaneously solved in TyBinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -649,19 +648,16 @@ interactWithInertsStage wi
                               , ptext (sLit "WorkItem  =") <+> ppr wi ]
                ; case ir of 
                    IRWorkItemConsumed { ir_fire = rule } 
-                       -> do { bumpStepCountTcS
-                             ; traceFireTcS wi (mk_msg rule (text "WorkItemConsumed"))
+                       -> do { traceFireTcS wi (mk_msg rule (text "WorkItemConsumed"))
                              ; insertInertItemTcS atomic_inert
                              ; return Stop } 
                    IRReplace { ir_fire = rule }
-                       -> do { bumpStepCountTcS
-                             ; traceFireTcS atomic_inert 
+                       -> do { traceFireTcS atomic_inert 
                                             (mk_msg rule (text "InertReplace"))
                              ; insertInertItemTcS wi
                              ; return Stop } 
                    IRInertConsumed { ir_fire = rule }
-                       -> do { bumpStepCountTcS
-                             ; traceFireTcS atomic_inert 
+                       -> do { traceFireTcS atomic_inert 
                                             (mk_msg rule (text "InertItemConsumed"))
                              ; return (ContinueWith wi) }
                    IRKeepGoing {} -- Should we do a bumpStepCountTcS? No for now.
@@ -726,8 +722,9 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
                                   , cc_tyargs = args1, cc_rhs = xi1, cc_loc = d1 }) 
                     wi@(CFunEqCan { cc_ev = ev2, cc_fun = tc2
                                   , cc_tyargs = args2, cc_rhs = xi2, cc_loc = d2 })
-  | fl1 `canSolve` fl2 && lhss_match
-  = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
+  | fl1 `canSolve` fl2 
+  = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
+    do { traceTcS "interact with inerts: FunEq/FunEq" $ 
          vcat [ text "workItem =" <+> ppr wi
               , text "inertItem=" <+> ppr ii ]
 
@@ -744,8 +741,9 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
        ; emitWorkNC d2 ctevs 
        ; return (IRWorkItemConsumed "FunEq/FunEq") }
 
-  | fl2 `canSolve` fl1 && lhss_match
-  = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
+  | fl2 `canSolve` fl1
+  = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
+    do { traceTcS "interact with inerts: FunEq/FunEq" $ 
          vcat [ text "workItem =" <+> ppr wi
               , text "inertItem=" <+> ppr ii ]
 
@@ -1027,7 +1025,7 @@ So our problem is this
 
 We may add the given in the inert set, along with its superclasses
 [assuming we don't fail because there is a matching instance, see 
- tryTopReact, given case ]
+ topReactionsStage, given case ]
   Inert:
     d0 :_g Foo t 
   WorkList 
@@ -1339,20 +1337,14 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
 *********************************************************************************
 
 \begin{code}
-topReactionsStage :: SimplifierStage 
-topReactionsStage workItem 
- = tryTopReact workItem 
-   
-
-tryTopReact :: WorkItem -> TcS StopOrContinue
-tryTopReact wi 
+topReactionsStage :: WorkItem -> TcS StopOrContinue
+topReactionsStage wi 
  = do { inerts <- getTcSInerts
       ; tir <- doTopReact inerts wi
       ; case tir of 
           NoTopInt -> return (ContinueWith wi)
           SomeTopInt rule what_next 
-                   -> do { bumpStepCountTcS 
-                         ; traceFireTcS wi $
+                   -> do { traceFireTcS wi $
                            vcat [ ptext (sLit "Top react:") <+> text rule
                                 , text "WorkItem =" <+> ppr wi ]
                          ; return what_next } }
@@ -1440,18 +1432,18 @@ doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
                 -> CtLoc -> TcS TopInteractResult
 doTopReactFunEq ct fl fun_tc args xi loc
   = ASSERT (isSynFamilyTyCon fun_tc) -- No associated data families have 
-                                 -- reached that far 
-
-    -- First look in the cache of solved funeqs
+                                     -- reached this far 
+    -- Look in the cache of solved funeqs
     do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
        ; case lookupFamHead fun_eq_cache fam_ty of {
-            Just (CFunEqCan { cc_ev = ctev, cc_rhs = rhs_ty })
-                -> ASSERT( not (isDerived ctev) )
-                   succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
-            Just {}  -> pprPanic "doTopReactFunEq" (ppr ct) ;
-            Nothing -> 
-
-    -- No cached solved, so look up in top-level instances
+           Just (CFunEqCan { cc_ev = ctev, cc_rhs = rhs_ty })
+             | ctEvFlavour ctev `canRewrite` ctEvFlavour fl
+             -> ASSERT( not (isDerived ctev) )
+                succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
+           Just ct' -> pprPanic "doTopReactFunEq" (ppr ct') ;
+           Nothing -> 
+
+    -- Look up in top-level instances
     do { match_res <- matchFam fun_tc args   -- See Note [MATCHING-SYNONYMS]
        ; case match_res of {
            Nothing -> return NoTopInt ;
@@ -1462,7 +1454,7 @@ doTopReactFunEq ct fl fun_tc args xi loc
          unless (isDerived fl) (addSolvedFunEq ct fam_ty)
 
        ; let coe_ax = famInstAxiom famInst 
-       ; succeed_with "Fun/Top"(mkTcAxInstCo coe_ax rep_tys)
+       ; succeed_with "Fun/Top" (mkTcAxInstCo coe_ax rep_tys)
                       (mkAxInstRHS coe_ax rep_tys) } } } } }
   where
     fam_ty = mkTyConApp fun_tc args
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 877307831a..7a3db58e7c 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -155,17 +155,17 @@ newWantedEvVars theta = mapM newWantedEvVar theta
 
 newEvVar :: TcPredType -> TcM EvVar
 -- Creates new *rigid* variables for predicates
-newEvVar ty = do { name <- newName (predTypeOccName ty) 
+newEvVar ty = do { name <- newSysName (predTypeOccName ty) 
                  ; return (mkLocalId name ty) }
 
 newEq :: TcType -> TcType -> TcM EvVar
 newEq ty1 ty2
-  = do { name <- newName (mkVarOccFS (fsLit "cobox"))
+  = do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
        ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
 
 newDict :: Class -> [TcType] -> TcM DictId
 newDict cls tys 
-  = do { name <- newName (mkDictOcc (getOccName cls))
+  = do { name <- newSysName (mkDictOcc (getOccName cls))
        ; return (mkLocalId name (mkClassPred cls tys)) }
 
 predTypeOccName :: PredType -> OccName
@@ -679,7 +679,7 @@ zonkFlats binds_var untch cts
       , not (tv `elemVarSet` tyVarsOfType ty_lhs)
 --       , Just ty_lhs' <- occurCheck tv ty_lhs
       = ASSERT2( isWantedCt orig_ct, ppr orig_ct )
-        ASSERT2( case orig_ct of { CFunEqCan {} -> True; _ -> False }, ppr orig_ct )
+        ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
         do { writeMetaTyVar tv ty_lhs
            ; let evterm = EvCoercion (mkTcReflCo ty_lhs)
                  evvar  = ctev_evar (cc_ev zct)
diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs
index c40a9f725b..68301f7972 100644
--- a/compiler/typecheck/TcRnMonad.lhs
+++ b/compiler/typecheck/TcRnMonad.lhs
@@ -376,6 +376,11 @@ newName occ
        ; loc  <- getSrcSpanM
        ; return (mkInternalName uniq occ loc) }
 
+newSysName :: OccName -> TcM Name
+newSysName occ
+  = do { uniq <- newUnique
+       ; return (mkSystemName uniq occ) }
+
 newSysLocalIds :: FastString -> [TcType] -> TcRnIf gbl lcl [TcId]
 newSysLocalIds fs tys
   = do  { us <- newUniqueSupply
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 7324798257..f4c0c4af2e 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -13,7 +13,8 @@ module TcSMonad (
 
     WorkList(..), isEmptyWorkList, emptyWorkList,
     workListFromEq, workListFromNonEq, workListFromCt, 
-    extendWorkListEq, extendWorkListNonEq, extendWorkListCt, 
+    extendWorkListEq, extendWorkListFunEq, 
+    extendWorkListNonEq, extendWorkListCt, 
     extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
     withWorkList,
 
@@ -31,7 +32,7 @@ module TcSMonad (
     mkGivenLoc, 
 
     TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality 
-    traceFireTcS, bumpStepCountTcS, 
+    traceFireTcS, 
     tryTcS, nestTcS, nestImplicTcS, recoverTcS,
     wrapErrTcS, wrapWarnTcS,
 
@@ -46,7 +47,7 @@ module TcSMonad (
 
     xCtFlavor,        -- Transform a CtEvidence during a step 
     rewriteCtFlavor,  -- Specialized version of xCtFlavor for coercions
-    newWantedEvVar, instDFunConstraints,
+    newWantedEvVar, newWantedEvVarNC, instDFunConstraints,
     newDerived,
     
        -- Creation of evidence variables
@@ -167,8 +168,8 @@ mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
 %*									*
 %************************************************************************
 
-Note [WorkList]
-~~~~~~~~~~~~~~~
+Note [WorkList priorities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
 A WorkList contains canonical and non-canonical items (of all flavors). 
 Notice that each Ct now has a simplification depth. We may 
 consider using this depth for prioritization as well in the future. 
@@ -179,6 +180,7 @@ so that it's easier to deal with them first, but the separation
 is not strictly necessary. Notice that non-canonical constraints 
 are also parts of the worklist. 
 
+
 Note [NonCanonical Semantics]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Note that canonical constraints involve a CNonCanonical constructor. In the worklist
@@ -219,7 +221,7 @@ extractDeque (DQ [] bs)     = case reverse bs of
                                 (a:as) -> Just (DQ as [], a)
                                 [] -> panic "extractDeque"
 
--- See Note [WorkList]
+-- See Note [WorkList priorities]
 data WorkList = WorkList { wl_eqs    :: [Ct]
                          , wl_funeqs :: Deque Ct
                          , wl_rest   :: [Ct] 
@@ -237,10 +239,14 @@ extendWorkListEq :: Ct -> WorkList -> WorkList
 -- Extension by equality
 extendWorkListEq ct wl 
   | Just {} <- isCFunEqCan_Maybe ct
-  = wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
+  = extendWorkListFunEq ct wl
   | otherwise
   = wl { wl_eqs = ct : wl_eqs wl }
 
+extendWorkListFunEq :: Ct -> WorkList -> WorkList
+extendWorkListFunEq ct wl 
+  = wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
+
 extendWorkListEqs :: [Ct] -> WorkList -> WorkList
 -- Append a list of equalities
 extendWorkListEqs cts wl = foldr extendWorkListEq wl cts
@@ -954,17 +960,14 @@ traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
 
-bumpStepCountTcS :: TcS ()
-bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
-                                    ; n <- TcM.readTcRef ref
-                                    ; TcM.writeTcRef ref (n+1) }
-
 traceFireTcS :: Ct -> SDoc -> TcS ()
--- Dump a rule-firing trace
+-- Dump a rule-firing trace, and bumpt the counter
 traceFireTcS ct doc 
   = TcS $ \env -> 
     TcM.ifDOptM Opt_D_dump_cs_trace $ 
-    do { n <- TcM.readTcRef (tcs_count env)
+    do { let count_ref = tcs_count env
+       ; n <- TcM.readTcRef count_ref
+       ; TcM.writeTcRef count_ref (n+1)
        ; let msg = int n <> brackets (int (ctLocDepth (cc_loc ct))) <+> doc
        ; TcM.dumpTcRn msg }
 
@@ -1404,6 +1407,12 @@ newGivenEvVar pred rhs
        ; setEvBind new_ev rhs
        ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev }) }
 
+newWantedEvVarNC :: TcPredType -> TcS CtEvidence
+-- Don't look up in the solved/inerts; we know it's not there
+newWantedEvVarNC pty
+  = do { new_ev <- wrapTcS $ TcM.newEvVar pty
+       ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev })}
+
 newWantedEvVar :: TcPredType -> TcS MaybeNew
 newWantedEvVar pty
   = do { mb_ct <- lookupInInerts pty
@@ -1411,10 +1420,8 @@ newWantedEvVar pty
             Just ctev | not (isDerived ctev) 
                       -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
                             ; return (Cached (ctEvTerm ctev)) }
-            _ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
-                    ; traceTcS "newWantedEvVar/cache miss" $ ppr new_ev
-                    ; let ctev = CtWanted { ctev_pred = pty
-                                          , ctev_evar = new_ev }
+            _ -> do { ctev <- newWantedEvVarNC pty
+                    ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
                     ; return (Fresh ctev) } }
 
 newDerived :: TcPredType -> TcS (Maybe CtEvidence)
@@ -1471,7 +1478,7 @@ See Note [Coercion evidence terms] in TcEvidence.
 
 
 \begin{code}
-xCtFlavor :: CtEvidence              -- Original flavor   
+xCtFlavor :: CtEvidence            -- Original flavor   
           -> [TcPredType]          -- New predicate types
           -> XEvTerm               -- Instructions about how to manipulate evidence
           -> TcS [CtEvidence]
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 88dbd7f19a..781d4c8cd1 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -1013,18 +1013,21 @@ happy to have types of kind Constraint on either end of an arrow.
 matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
 -- Like unifyFunTy, but does not fail; instead just returns Nothing
 
-matchExpectedFunKind (TyVarTy kvar) = do
-    maybe_kind <- readMetaTyVar kvar
-    case maybe_kind of
-      Indirect fun_kind -> matchExpectedFunKind fun_kind
-      Flexi ->
-          do { arg_kind <- newMetaKindVar
-             ; res_kind <- newMetaKindVar
-             ; writeMetaTyVar kvar (mkArrowKind arg_kind res_kind)
-             ; return (Just (arg_kind,res_kind)) }
-
-matchExpectedFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
-matchExpectedFunKind _                         = return Nothing
+matchExpectedFunKind (FunTy arg_kind res_kind) 
+  = return (Just (arg_kind,res_kind))
+
+matchExpectedFunKind (TyVarTy kvar) 
+  | isTcTyVar kvar, isMetaTyVar kvar
+  = do { maybe_kind <- readMetaTyVar kvar
+       ; case maybe_kind of
+            Indirect fun_kind -> matchExpectedFunKind fun_kind
+            Flexi ->
+                do { arg_kind <- newMetaKindVar
+                   ; res_kind <- newMetaKindVar
+                   ; writeMetaTyVar kvar (mkArrowKind arg_kind res_kind)
+                   ; return (Just (arg_kind,res_kind)) } }
+
+matchExpectedFunKind _ = return Nothing
 
 -----------------  
 unifyKindX :: TcKind           -- k1 (actual)
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index fab8fa5de4..4599ddf04a 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -418,10 +418,11 @@ ppr_co p co@(ForAllCo {})      = ppr_forall_co p co
 ppr_co _ (CoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
 ppr_co p (AxiomInstCo con cos) = pprTypeNameApp p ppr_co (getName con) cos
 
-ppr_co p (TransCo co1 co2) = maybeParen p FunPrec $
-                             ppr_co FunPrec co1
-                             <+> ptext (sLit ";")
-                             <+> ppr_co FunPrec co2
+ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
+                           case trans_co_list co [] of
+                             [] -> panic "ppr_co"
+                             (co:cos) -> sep ( ppr_co FunPrec co
+                                             : [ char ';' <+> ppr_co FunPrec co | co <- cos])
 ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
                           pprParendCo co <> ptext (sLit "@") <> pprType ty
 
@@ -431,6 +432,10 @@ ppr_co p (SymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo c
 ppr_co p (NthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
 ppr_co p (LRCo sel co)      = pprPrefixApp p (ppr sel) [pprParendCo co]
 
+trans_co_list :: Coercion -> [Coercion] -> [Coercion]
+trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
+trans_co_list co                cos = co : cos
+
 instance Outputable LeftOrRight where
   ppr CLeft    = ptext (sLit "Left")
   ppr CRight   = ptext (sLit "Right")