Refactor the handling of kind errors

* Treat kind-equality constraints as *derived* equalities,
  with no evidence.  That is really what they are at the moment.

* Get rid of EvKindCast and friends.

* Postpone kind errors properly to the constraint solver
  (lots of small knock-on effects)

I moved SwapFlag to BasicTypes as well

10 files changed, 185 insertions, 293 deletions

diff --git a/compiler/basicTypes/BasicTypes.lhs b/compiler/basicTypes/BasicTypes.lhs
index 2760156e1c..616316c7ff 100644
--- a/compiler/basicTypes/BasicTypes.lhs
+++ b/compiler/basicTypes/BasicTypes.lhs
@@ -66,6 +66,7 @@ module BasicTypes(
         StrictnessMark(..), isMarkedStrict,
 
 	DefMethSpec(..),
+        SwapFlag(..), flipSwap, unSwap,
 
         CompilerPhase(..), PhaseNum,
         Activation(..), isActive, isActiveIn,
@@ -125,6 +126,31 @@ type Alignment = Int -- align to next N-byte boundary (N must be a power of 2).
 
 %************************************************************************
 %*									*
+           Swap flag
+%*									*
+%************************************************************************
+
+\begin{code}
+data SwapFlag 
+  = NotSwapped	-- Args are: actual,   expected
+  | IsSwapped   -- Args are: expected, actual
+
+instance Outputable SwapFlag where
+  ppr IsSwapped  = ptext (sLit "Is-swapped")
+  ppr NotSwapped = ptext (sLit "Not-swapped")
+
+flipSwap :: SwapFlag -> SwapFlag
+flipSwap IsSwapped  = NotSwapped
+flipSwap NotSwapped = IsSwapped
+
+unSwap :: SwapFlag -> (a->a->b) -> a -> a -> b
+unSwap NotSwapped f a b = f a b
+unSwap IsSwapped  f a b = f b a
+\end{code}
+
+
+%************************************************************************
+%*									*
 \subsection[FunctionOrData]{FunctionOrData}
 %*									*
 %************************************************************************
diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index b418c8d592..95d36f3879 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -741,10 +741,6 @@ dsEvTerm (EvCast tm co)
                         -- 'v' is always a lifted evidence variable so it is
                         -- unnecessary to call varToCoreExpr v here.
 
-dsEvTerm (EvKindCast v co)
-  = do { v' <- dsEvTerm v
-       ; dsTcCoercion co $ (\_ -> v') }
-
 dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms
                                      ; return (Var df `mkTyApps` tys `mkApps` tms') }
 dsEvTerm (EvCoercion co)         = dsTcCoercion co mkEqBox
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index d20a7019d0..826375bd02 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -622,13 +622,17 @@ because now the 'b' has escaped its scope.  We'd have to flatten to
 and we have not begun to think about how to make that work!
 
 \begin{code}
-flattenTyVar :: CtLoc -> FlattenMode 
-             -> CtFlavour -> TcTyVar -> TcS (Xi, TcCoercion)
+flattenTyVar, flattenFinalTyVar
+        :: CtLoc -> FlattenMode 
+        -> CtFlavour -> TcTyVar -> TcS (Xi, TcCoercion)
 -- "Flattening" a type variable means to apply the substitution to it
 -- The substitution is actually the union of the substitution in the TyBinds
 -- for the unification variables that have been unified already with the inert
 -- equalities, see Note [Spontaneously solved in TyBinds] in TcInteract.
 flattenTyVar loc f ctxt tv
+  | not (isTcTyVar tv)	              -- Happens when flatten under a (forall a. ty)
+  = flattenFinalTyVar loc f ctxt tv   -- So ty contains referneces to the non-TcTyVar a
+  | otherwise
   = do { mb_ty <- isFilledMetaTyVar_maybe tv
        ; case mb_ty of {
            Just ty -> flatten loc f ctxt ty ;
@@ -655,13 +659,7 @@ flattenTyVar loc f ctxt tv
        -- In fact, because of flavors, it couldn't possibly be idempotent,
        -- this is explained in Note [Non-idempotent inert substitution]
 
-           Nothing -> 
-
-    -- Done, but make sure the kind is zonked
-    do { let knd = tyVarKind tv
-       ; (new_knd,_kind_co) <- flatten loc f ctxt knd
-       ; let ty = mkTyVarTy (setVarType tv new_knd)
-       ; return (ty, mkTcReflCo ty) }
+           Nothing -> flattenFinalTyVar loc f ctxt tv
     } } } } } } 
   where
     tv_eq_subst subst tv
@@ -672,6 +670,13 @@ flattenTyVar loc f ctxt tv
               -- NB: even if ct is Derived we are not going to 
               -- touch the actual coercion so we are fine. 
        | otherwise = Nothing
+
+flattenFinalTyVar loc f ctxt tv
+  = -- Done, but make sure the kind is zonked
+    do { let knd = tyVarKind tv
+       ; (new_knd,_kind_co) <- flatten loc f ctxt knd
+       ; let ty = mkTyVarTy (setVarType tv new_knd)
+       ; return (ty, mkTcReflCo ty) }
 \end{code}
 
 Note [Non-idempotent inert substitution]
@@ -795,11 +800,11 @@ canEq loc ev ty1 ty2
            Nothing     -> return Stop
            Just new_ev -> last_chance new_ev s1 s2 }
   where
-    last_chance new_ev ty1 ty2
+    last_chance ev ty1 ty2
       | Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
       , Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
       , isDecomposableTyCon tc1 && isDecomposableTyCon tc2
-      = canDecomposableTyConApp loc new_ev tc1 tys1 tc2 tys2
+      = canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2
     
       | Just (s1,t1) <- tcSplitAppTy_maybe ty1
       , Just (s2,t2) <- tcSplitAppTy_maybe ty2
@@ -811,7 +816,7 @@ canEq loc ev ty1 ty2
        	   ; canEvVarsCreated loc ctevs }
 
       | otherwise
-      = do { emitInsoluble (CNonCanonical { cc_ev = new_ev, cc_loc = loc })
+      = do { emitInsoluble (CNonCanonical { cc_ev = ev, cc_loc = loc })
            ; return Stop }
 
 ------------------------
@@ -860,47 +865,25 @@ emitKindConstraint ct   -- By now ct is canonical
 
       _   -> continueWith ct
   where
-    emit_kind_constraint loc ev ty1 ty2 
+    emit_kind_constraint loc _ev ty1 ty2 
        | compatKind k1 k2    -- True when ty1,ty2 are themselves kinds,
        = continueWith ct     -- because then k1, k2 are BOX
        
        | otherwise
        = ASSERT( isKind k1 && isKind k2 )
-         do { mw <- newWantedEvVar (mkEqPred k1 k2) 
-            ; kev_tm <- case mw of
-                         Cached ev_tm -> return ev_tm
-                         Fresh kev   -> do { emitWorkNC kind_co_loc [kev]
-                                           ; return (ctEvTerm kev) } 
-
-            ; let xcomp [x] = mkEvKindCast x (evTermCoercion kev_tm)
-                  xcomp _   = panic "emit_kind_constraint:can't happen"
-                  xdecomp x = [mkEvKindCast x (evTermCoercion kev_tm)]
-                  xev = XEvTerm xcomp xdecomp
-
-            ; ctevs <- xCtFlavor ev [mkTcEqPred ty1 ty2] xev 
-                     -- Important: Do not cache original as Solved since we are supposed to 
-                     -- solve /exactly/ the same constraint later!  Example:
-                     -- (alpha :: kappa0) 
-                     -- (T :: *)
-                     -- Equality is: (alpha ~ T), so we will emitConstraint (kappa0 ~ *) but
-                     -- we don't want to say that (alpha ~ T) is now Solved!
-                     --
-                     -- We do need to do this xCtFlavor so that in the case of
-                     -- -fdefer-type-errors we still make a demand on kev_tm
-
-            ; case ctevs of
-                []         -> return Stop
-                [new_ctev] -> continueWith (ct { cc_ev = new_ctev }) 
-                _          -> panic "emitKindConstraint" }
+         do { mw <- newDerived (mkEqPred k1 k2) 
+            ; case mw of
+                Nothing  -> return ()
+                Just kev -> emitWorkNC kind_co_loc [kev]
+            ; continueWith ct }
        where
          k1 = typeKind ty1
          k2 = typeKind ty2
-         ctxt = mkKindErrorCtxtTcS ty1 k1 ty2 k2
 
          -- Always create a Wanted kind equality even if 
          -- you are decomposing a given constraint.
          -- NB: DV finds this reasonable for now. Maybe we have to revisit.
-         kind_co_loc = pushErrCtxtSameOrigin ctxt loc
+         kind_co_loc = setCtLocOrigin loc (KindEqOrigin ty1 ty2 (ctLocOrigin loc))
 \end{code}
 
 Note [Make sure that insolubles are fully rewritten]
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index a7159681f1..4f95abc933 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -126,14 +126,11 @@ report_unsolved mb_binds_var defer wanted
        ; let tidy_env = tidyFreeTyVars env0 free_tvs
              free_tvs = tyVarsOfWC wanted
              err_ctxt = CEC { cec_encl  = []
-                            , cec_insol = False
-                                          --errs_so_far || insolubleWC wanted
-                                          -- Don't report ambiguity errors if
-                                          -- there are any other solid errors 
-                                          -- to report
                             , cec_tidy  = tidy_env
                             , cec_defer    = defer
-                            , cec_suppress = False
+                            , cec_suppress = insolubleWC wanted
+                                  -- Suppress all but insolubles if there are
+                                  -- any insoulubles, or earlier errors
                             , cec_binds    = mb_binds_var }
 
        ; traceTc "reportUnsolved (after unflattening):" $ 
@@ -151,9 +148,6 @@ data ReportErrCtxt
                 	       	       --   (innermost first)
                                        -- ic_skols and givens are tidied, rest are not
           , cec_tidy  :: TidyEnv
-          , cec_insol :: Bool       -- True <=> do not report errors involving 
-                                    --          ambiguous errors
-
           , cec_binds :: Maybe EvBindsVar 
                          -- Nothinng <=> Report all errors, including holes; no bindings
                          -- Just ev  <=> make some errors (depending on cec_defer)
@@ -185,23 +179,20 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
     implic' = implic { ic_skols = tvs'
                      , ic_given = map (tidyEvVar env2) given
                      , ic_info  = info' }
-    insoluble' = case info of
-                   InferSkol {} -> ic_insoluble
-                   _            -> cec_insol ctxt    
     ctxt' = ctxt { cec_tidy  = env2
                  , cec_encl  = implic' : cec_encl ctxt
-                 , cec_insol = insoluble'
                  , cec_binds = case cec_binds ctxt of
                                  Nothing -> Nothing
                                  Just {} -> Just evb }
 
 reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM ()
 reportWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics })
-  = do { reportFlats ctxt tidy_cts
+  = do { reportFlats (ctxt { cec_suppress = False }) (mapBag (tidyCt env) insols)
+       ; reportFlats ctxt                            (mapBag (tidyCt env) flats)
        ; mapBagM_ (reportImplic ctxt) implics }
   where
     env = cec_tidy ctxt
-    tidy_cts = mapBag (tidyCt env) (insols `unionBags` flats)
+--    tidy_cts = mapBag (tidyCt env) (insols `unionBags` flats)
                   -- All the Derived ones have been filtered out alrady
                   -- by the constraint solver. This is ok; we don't want
                   -- to report unsolved Derived goals as error
@@ -263,14 +254,6 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
                       _ -> Nothing
 
 -----------------
-{-
-reportAmbigErrs :: Reporter
-reportAmbigErrs ctxt cts
-  | cec_insol ctxt = return ()
-  | otherwise      = reportFlatErrs ctxt cts
-          -- Only report ambiguity if no other errors (at all) happened
-          -- See Note [Avoiding spurious errors] in TcSimplify
--}
 reportFlatErrs :: Reporter
 -- Called once for non-ambigs, once for ambigs
 -- Report equality errors, and others only if we've done all 
@@ -279,12 +262,10 @@ reportFlatErrs :: Reporter
 reportFlatErrs
   = tryReporters
       [ ("Equalities", is_equality, mkGroupReporter mkEqErr) ]
-      (\ctxt cts -> do { let ctxt' | cec_insol ctxt = ctxt { cec_suppress = True }
-                                   | otherwise      = ctxt
-                       ; let (dicts, ips, irreds) = go cts [] [] []
-                       ; mkGroupReporter mkIPErr    ctxt' ips   
-                       ; mkGroupReporter mkIrredErr ctxt' irreds
-                       ; mkGroupReporter mkDictErr  ctxt' dicts })
+      (\ctxt cts -> do { let (dicts, ips, irreds) = go cts [] [] []
+                       ; mkGroupReporter mkIPErr    ctxt ips   
+                       ; mkGroupReporter mkIrredErr ctxt irreds
+                       ; mkGroupReporter mkDictErr  ctxt dicts })
   where
     is_equality _ (EqPred {}) = True
     is_equality _ _           = False
@@ -558,10 +539,11 @@ mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
 mkEqErr1 ctxt ct
   = do { (ctxt, binds_msg) <- relevantBindings ctxt ct
        ; (ctxt, orig) <- zonkTidyOrigin ctxt orig
+       ; let (is_oriented, wanted_msg) = mk_wanted_extra orig
        ; if isGiven ev then 
-           mkEqErr_help ctxt (inaccessible_msg orig $$ binds_msg) ct False ty1 ty2
+           mkEqErr_help ctxt (inaccessible_msg orig $$ binds_msg) ct Nothing ty1 ty2
          else
-           mk_err binds_msg orig }
+           mkEqErr_help ctxt (wanted_msg $$ binds_msg) ct is_oriented ty1 ty2 }
   where
     ev         = cc_ev ct
     orig       = ctLocOrigin (cc_loc ct)
@@ -572,24 +554,26 @@ mkEqErr1 ctxt ct
 
        -- If the types in the error message are the same as the types
        -- we are unifying, don't add the extra expected/actual message
-    mk_err extra (TypeEqOrigin (UnifyOrigin { uo_actual = act, uo_expected = exp })) 
-      | act `pickyEqType` ty1
-      , exp `pickyEqType` ty2 = mkEqErr_help ctxt extra  ct True  ty2 ty1
-      | exp `pickyEqType` ty1
-      , act `pickyEqType` ty2 = mkEqErr_help ctxt extra  ct True  ty1 ty2
-      | otherwise             = mkEqErr_help ctxt extra1 ct False ty1 ty2
+    mk_wanted_extra orig@(TypeEqOrigin {})
+      = mkExpectedActualMsg ty1 ty2 orig
+
+
+    mk_wanted_extra (KindEqOrigin cty1 cty2 sub_o)
+      = (Nothing, msg1 $$ msg2)
       where
-        extra1 = msg $$ extra
-        msg    = mkExpectedActualMsg exp act
-    mk_err extra _ = mkEqErr_help ctxt extra ct False ty1 ty2
+        msg1 = hang (ptext (sLit "When matching types"))
+                  2 (vcat [ ppr cty1 <+> dcolon <+> ppr (typeKind cty1)
+                          , ppr cty2 <+> dcolon <+> ppr (typeKind cty2) ])
+        msg2 = case sub_o of
+                 TypeEqOrigin {} -> snd (mkExpectedActualMsg cty1 cty2 sub_o)
+                 _ -> empty
+
+    mk_wanted_extra _ = (Nothing, empty)
 
 mkEqErr_help, reportEqErr 
    :: ReportErrCtxt -> SDoc
    -> Ct
-   -> Bool     -- True  <=> Types are correct way round;
-               --           report "expected ty1, actual ty2"
-               -- False <=> Just report a mismatch without orientation
-               --           The ReportErrCtxt has expected/actual 
+   -> Maybe SwapFlag   -- Nothing <=> not sure
    -> TcType -> TcType -> TcM ErrMsg
 mkEqErr_help ctxt extra ct oriented ty1 ty2
   | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr ctxt extra ct oriented tv1 ty2
@@ -601,7 +585,7 @@ reportEqErr ctxt extra1 ct oriented ty1 ty2
        ; mkErrorMsg ctxt' ct (vcat [ misMatchOrCND ctxt' ct oriented ty1 ty2
                                    , extra2, extra1]) }
 
-mkTyVarEqErr :: ReportErrCtxt -> SDoc -> Ct -> Bool -> TcTyVar -> TcType -> TcM ErrMsg
+mkTyVarEqErr :: ReportErrCtxt -> SDoc -> Ct -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
 -- tv1 and ty2 are already tidied
 mkTyVarEqErr ctxt extra ct oriented tv1 ty2
   -- Occurs check
@@ -697,7 +681,7 @@ isUserSkolem ctxt tv
     is_user_skol_info (InferSkol {}) = False
     is_user_skol_info _ = True
 
-misMatchOrCND :: ReportErrCtxt -> Ct -> Bool -> TcType -> TcType -> SDoc
+misMatchOrCND :: ReportErrCtxt -> Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
 -- If oriented then ty1 is expected, ty2 is actual
 misMatchOrCND ctxt ct oriented ty1 ty2
   | null givens || 
@@ -710,7 +694,7 @@ misMatchOrCND ctxt ct oriented ty1 ty2
   = couldNotDeduce givens ([mkEqPred ty1 ty2], orig)
   where
     givens = getUserGivens ctxt
-    orig   = TypeEqOrigin (UnifyOrigin ty1 ty2)
+    orig   = TypeEqOrigin ty1 ty2
 
 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
 couldNotDeduce givens (wanteds, orig)
@@ -763,10 +747,12 @@ kindErrorMsg ty1 ty2
     k2 = typeKind ty2
 
 --------------------
-misMatchMsg :: Bool -> TcType -> TcType -> SDoc	   -- Types are already tidy
+misMatchMsg :: Maybe SwapFlag -> TcType -> TcType -> SDoc	   -- Types are already tidy
 -- If oriented then ty1 is expected, ty2 is actual
-misMatchMsg oriented ty1 ty2 
-  | oriented
+misMatchMsg oriented ty1 ty2  
+  | Just IsSwapped <- oriented
+  = misMatchMsg (Just NotSwapped) ty2 ty1
+  | Just NotSwapped <- oriented
   = sep [ ptext (sLit "Couldn't match expected") <+> what <+> quotes (ppr ty1)
         , nest 12 $   ptext (sLit "with actual") <+> what <+> quotes (ppr ty2) ]
   | otherwise
@@ -776,10 +762,16 @@ misMatchMsg oriented ty1 ty2
     what | isKind ty1 = ptext (sLit "kind")
          | otherwise  = ptext (sLit "type")
 
-mkExpectedActualMsg :: Type -> Type -> SDoc
-mkExpectedActualMsg exp_ty act_ty
-  = vcat [ text "Expected type:" <+> ppr exp_ty
-         , text "  Actual type:" <+> ppr act_ty ]
+mkExpectedActualMsg :: Type -> Type -> CtOrigin -> (Maybe SwapFlag, SDoc)
+mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act, uo_expected = exp })
+  | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (Just IsSwapped,  empty)
+  | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (Just NotSwapped, empty)
+  | otherwise                                    = (Nothing, msg)
+  where
+    msg = vcat [ text "Expected type:" <+> ppr exp
+               , text "  Actual type:" <+> ppr act ]
+
+mkExpectedActualMsg _ _ _ = panic "mkExprectedAcutalMsg"
 \end{code}
 
 Note [Reporting occurs-check errors]
@@ -874,7 +866,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
     cannot_resolve_msg has_ambig_tvs binds_msg ambig_msg
       = vcat [ addArising orig (no_inst_herald <+> pprParendType pred)
              , vcat (pp_givens givens)
-             , if (has_ambig_tvs && all_tyvars)
+             , if (has_ambig_tvs && not (null unifiers && null givens))
                then vcat [ ambig_msg, binds_msg, potential_msg ]
                else empty
              , show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes) ]
@@ -1232,10 +1224,15 @@ zonkTidyOrigin ctxt (GivenOrigin skol_info)
   = do { skol_info1 <- zonkSkolemInfo skol_info
        ; let (env1, skol_info2) = tidySkolemInfo (cec_tidy ctxt) skol_info1
        ; return (ctxt { cec_tidy = env1 }, GivenOrigin skol_info2) }
-zonkTidyOrigin ctxt (TypeEqOrigin (UnifyOrigin { uo_actual = act, uo_expected = exp }))
+zonkTidyOrigin ctxt (TypeEqOrigin { uo_actual = act, uo_expected = exp })
   = do { (env1, act') <- zonkTidyTcType (cec_tidy ctxt) act
        ; (env2, exp') <- zonkTidyTcType env1            exp
        ; return ( ctxt { cec_tidy = env2 }
-                , TypeEqOrigin (UnifyOrigin { uo_actual = act', uo_expected = exp' })) }
+                , TypeEqOrigin { uo_actual = act', uo_expected = exp' }) }
+zonkTidyOrigin ctxt (KindEqOrigin ty1 ty2 orig)
+  = do { (env1, ty1') <- zonkTidyTcType (cec_tidy ctxt) ty1
+       ; (env2, ty2') <- zonkTidyTcType env1            ty2
+       ; (ctxt2, orig') <- zonkTidyOrigin (ctxt { cec_tidy = env2 }) orig
+       ; return (ctxt2, KindEqOrigin ty1' ty2' orig') }
 zonkTidyOrigin ctxt orig = return (ctxt, orig)
 \end{code}
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index c88b350616..0c31bc0c3d 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -16,7 +16,7 @@ module TcEvidence (
 
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, 
 
-  EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,
+  EvTerm(..), mkEvCast, evVarsOfTerm, 
   EvLit(..), evTermCoercion,
 
   -- TcCoercion
@@ -483,8 +483,6 @@ data EvTerm
                                  -- dictionaries, even though the former have no
                                  -- selector Id.  We count up from _0_
 
-  | EvKindCast EvTerm TcCoercion  -- See Note [EvKindCast]
-
   | EvLit EvLit                  -- Dictionary for class "SingI" for type lits.
                                  -- Note [EvLit]
 
@@ -521,19 +519,6 @@ and the constraint
     [G] g1 :: a~Bool
 See Trac [7238]
 
-Note [EvKindCast] 
-~~~~~~~~~~~~~~~~~ 
-EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2) 
-but the kinds of s1 and s2 (k1 and k2 respectively) don't match but 
-are rather equal by a coercion. You may think that this coercion will
-always turn out to be ReflCo, so why is this needed? Because sometimes
-we will want to defer kind errors until the runtime and in these cases
-that coercion will be an 'error' term, which we want to evaluate rather
-than silently forget about!
-
-The relevant (and only) place where such a coercion is produced in 
-the simplifier is in TcCanonical.emitKindConstraint.
-
 Note [EvBinds/EvTerm]
 ~~~~~~~~~~~~~~~~~~~~~
 How evidence is created and updated. Bindings for dictionaries,
@@ -595,11 +580,6 @@ mkEvCast ev lco
   | isTcReflCo lco = ev
   | otherwise      = EvCast ev lco
 
-mkEvKindCast :: EvTerm -> TcCoercion -> EvTerm
-mkEvKindCast ev lco
-  | isTcReflCo lco = ev
-  | otherwise      = EvKindCast ev lco
-
 emptyTcEvBinds :: TcEvBinds
 emptyTcEvBinds = EvBinds emptyBag
 
@@ -625,7 +605,6 @@ evVarsOfTerm (EvSuperClass v _)   = evVarsOfTerm v
 evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
 evVarsOfTerm (EvTupleMk evs)      = evVarsOfTerms evs
 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
-evVarsOfTerm (EvKindCast v co)    = coVarsOfTcCo co `unionVarSet` evVarsOfTerm v
 evVarsOfTerm (EvLit _)            = emptyVarSet
 
 evVarsOfTerms :: [EvTerm] -> VarSet
@@ -683,7 +662,6 @@ instance Outputable EvBind where
 instance Outputable EvTerm where
   ppr (EvId v)           = ppr v
   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
-  ppr (EvKindCast v co)  = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co
   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co
   ppr (EvTupleSel v n)   = ptext (sLit "tupsel") <> parens (ppr (v,n))
   ppr (EvTupleMk vs)     = ptext (sLit "tupmk") <+> ppr vs
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 9da6ea5434..86cff0f474 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -1117,11 +1117,6 @@ zonkEvTerm env (EvCoercion co)    = do { co' <- zonkTcLCoToLCo env co
 zonkEvTerm env (EvCast tm co)     = do { tm' <- zonkEvTerm env tm
                                        ; co' <- zonkTcLCoToLCo env co
                                        ; return (mkEvCast tm' co') }
-
-zonkEvTerm env (EvKindCast v co)  = do { v'  <- zonkEvTerm env v
-                                       ; co' <- zonkTcLCoToLCo env co
-                                       ; return (mkEvKindCast v' co') }
-
 zonkEvTerm env (EvTupleSel tm n)  = do { tm' <- zonkEvTerm env tm
                                        ; return (EvTupleSel tm' n) }
 zonkEvTerm env (EvTupleMk tms)    = do { tms' <- mapM (zonkEvTerm env) tms
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index 55388b024e..2f397a06fc 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -29,8 +29,7 @@ module TcHsType (
 	tcLHsType, tcCheckLHsType, 
         tcHsContext, tcInferApps, tcHsArgTys,
 
-        ExpKind(..), ekConstraint, expArgKind, 
-        kindGeneralize,
+        kindGeneralize, checkKind,
 
 		-- Sort-checking kinds
 	tcLHsKind, 
@@ -967,7 +966,7 @@ kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
            ; return (n, exp_k) }
     kc_tv (L _ (KindedTyVar n hs_k)) exp_k
       = do { k <- tcLHsKind hs_k
-           ; _ <- unifyKind k exp_k
+           ; checkKind k exp_k
            ; check_in_scope n exp_k
            ; return (n, k) }
 
@@ -979,7 +978,7 @@ kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
       = do { mb_thing <- tcLookupLcl_maybe n
            ; case mb_thing of
                Nothing         -> return ()
-               Just (AThing k) -> discardResult (unifyKind k exp_k)
+               Just (AThing k) -> checkKind k exp_k
                Just thing      -> pprPanic "check_in_scope" (ppr thing) }
 
 -----------------------
@@ -1014,7 +1013,7 @@ tcTyClTyVars tycon (HsQTvs { hsq_kvs = hs_kvs, hsq_tvs = hs_tvs }) thing_inside
   where
     tc_hs_tv (L _ (UserTyVar n))        kind = return (mkTyVar n kind)
     tc_hs_tv (L _ (KindedTyVar n hs_k)) kind = do { tc_kind <- tcLHsKind hs_k
-                                                  ; _ <- unifyKind kind tc_kind
+                                                  ; checkKind kind tc_kind
                                                   ; return (mkTyVar n kind) }
 
 -----------------------------------
@@ -1274,8 +1273,15 @@ unifyKinds fun act_kinds
        ; mapM_ check (zip [1..] act_kinds)
        ; return kind }
 
+checkKind :: TcKind -> TcKind -> TcM ()
+checkKind act_kind exp_kind
+  = do { mb_subk <- unifyKindX act_kind exp_kind
+       ; case mb_subk of
+           Just EQ -> return ()
+           _       -> unifyKindMisMatch act_kind exp_kind }
+
 checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
--- A fancy wrapper for 'unifyKind', which tries
+-- A fancy wrapper for 'unifyKindX', which tries
 -- to give decent error messages.
 --      (checkExpectedKind ty act_kind exp_kind)
 -- checks that the actual kind act_kind is compatible
@@ -1283,12 +1289,13 @@ checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
 -- The first argument, ty, is used only in the error message generation
 checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt)
  = do { traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr ek)
-      ; (_, lie) <- captureConstraints (unifyKind act_kind exp_kind)
+      ; mb_subk <- unifyKindX act_kind exp_kind
 
          -- Kind unification only generates definite errors
-      ; if isEmptyWC lie 
-        then return () -- Unification succeeded
-        else do
+      ; case mb_subk of {
+          Just LT -> return () ;    -- act_kind is a sub-kind of exp_kind
+          Just EQ -> return () ;    -- The two are equal
+          _other  -> do
 
       {  -- So there's an error
          -- Now to find out what sort
@@ -1334,7 +1341,7 @@ checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt)
                               ptext (sLit "but") <+> quotes (ppr ty) <+>
                                   ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
 
-      ; failWithTcM (env2, err) } }
+      ; failWithTcM (env2, err) } } }
 \end{code}
 
 %************************************************************************
@@ -1489,5 +1496,15 @@ badPatSigTvs sig_ty bad_tvs
 	  	 ptext (sLit "but are actually discarded by a type synonym") ]
          , ptext (sLit "To fix this, expand the type synonym") 
          , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
+
+unifyKindMisMatch :: TcKind -> TcKind -> TcM a
+unifyKindMisMatch ki1 ki2 = do
+    ki1' <- zonkTcKind ki1
+    ki2' <- zonkTcKind ki2
+    let msg = hang (ptext (sLit "Couldn't match kind"))
+              2 (sep [quotes (ppr ki1'),
+                      ptext (sLit "against"),
+                      quotes (ppr ki2')])
+    failWithTc msg
 \end{code}
 
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index a409b11fe7..aa5dec9bd2 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -65,7 +65,7 @@ module TcRnTypes(
         CtLoc(..), ctLocSpan, ctLocEnv, ctLocOrigin, 
         ctLocDepth, bumpCtLocDepth,
         setCtLocOrigin,
-	CtOrigin(..), EqOrigin(..), 
+	CtOrigin(..), 
         pushErrCtxt, pushErrCtxtSameOrigin,
 
 	SkolemInfo(..),
@@ -1480,7 +1480,11 @@ data CtOrigin
 
   | SpecPragOrigin Name		-- Specialisation pragma for identifier
 
-  | TypeEqOrigin EqOrigin
+  | TypeEqOrigin { uo_actual   :: TcType
+                 , uo_expected :: TcType }
+  | KindEqOrigin 
+      TcType TcType             -- A kind equality arising from unifying these two types
+      CtOrigin                  -- originally arising from this
 
   | IPOccOrigin  HsIPName 	-- Occurrence of an implicit parameter
 
@@ -1510,14 +1514,6 @@ data CtOrigin
   | FunDepOrigin
   | HoleOrigin
 
-data EqOrigin 
-  = UnifyOrigin 
-       { uo_actual   :: TcType
-       , uo_expected :: TcType }
-
-instance Outputable CtOrigin where
-  ppr orig = pprO orig
-
 pprO :: CtOrigin -> SDoc
 pprO (GivenOrigin sk)      = ppr sk
 pprO (OccurrenceOf name)   = hsep [ptext (sLit "a use of"), quotes (ppr name)]
@@ -1544,12 +1540,13 @@ pprO DefaultOrigin	   = ptext (sLit "a 'default' declaration")
 pprO DoOrigin	           = ptext (sLit "a do statement")
 pprO MCompOrigin           = ptext (sLit "a statement in a monad comprehension")
 pprO ProcOrigin	           = ptext (sLit "a proc expression")
-pprO (TypeEqOrigin eq)     = ptext (sLit "an equality") <+> ppr eq
+pprO (TypeEqOrigin t1 t2)  = ptext (sLit "a type equality") <+> sep [ppr t1, char '~', ppr t2]
+pprO (KindEqOrigin t1 t2 _) = ptext (sLit "a kind equality arising from") <+> sep [ppr t1, char '~', ppr t2]
 pprO AnnOrigin             = ptext (sLit "an annotation")
 pprO FunDepOrigin          = ptext (sLit "a functional dependency")
 pprO HoleOrigin            = ptext (sLit "a use of the hole") <+> quotes (ptext $ sLit "_")
 
-instance Outputable EqOrigin where
-  ppr (UnifyOrigin t1 t2) = ppr t1 <+> char '~' <+> ppr t2
+instance Outputable CtOrigin where
+  ppr = pprO
 \end{code}
 
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index c62b188e83..4d5e7d5937 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -28,7 +28,6 @@ module TcTyClsDecls (
 import HsSyn
 import HscTypes
 import BuildTyCl
-import TcUnify
 import TcRnMonad
 import TcEnv
 import TcHsSyn
@@ -659,7 +658,7 @@ tcTyDefn calc_isrec tc_name tvs kind
            Nothing   -> return ()
            Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
                            ; tc_kind <- tcLHsKind hs_k
-                           ; _ <- unifyKind kind tc_kind
+                           ; checkKind kind tc_kind
                            ; return () }
 
        ; dataDeclChecks tc_name new_or_data stupid_theta cons
@@ -771,12 +770,12 @@ kcTyDefn (TySynonym { td_synRhs = rhs_ty }) res_k
 ------------------
 kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM ()
 kcResultKind Nothing res_k
-  = discardResult (unifyKind res_k liftedTypeKind)
+  = checkKind res_k liftedTypeKind
       --             type family F a 
       -- defaults to type family F a :: *
-kcResultKind (Just k ) res_k
+kcResultKind (Just k) res_k
   = do { k' <- tcLHsKind k
-       ; discardResult (unifyKind k' res_k) }
+       ; checkKind  k' res_k }
 
 -------------------------
 -- Kind check type patterns and kind annotate the embedded type variables.
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index a93f808c4f..65e787103f 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -19,7 +19,8 @@ module TcUnify (
   checkConstraints, newImplication, 
 
   -- Various unifications
-  unifyType, unifyTypeList, unifyTheta, unifyKind, 
+  unifyType, unifyTypeList, unifyTheta, 
+  unifyKindX, 
 
   --------------------------------
   -- Holes
@@ -466,7 +467,9 @@ non-exported generic functions.
 unifyType :: TcTauType -> TcTauType -> TcM TcCoercion
 -- Actual and expected types
 -- Returns a coercion : ty1 ~ ty2
-unifyType ty1 ty2 = uType [] ty1 ty2
+unifyType ty1 ty2 = uType origin ty1 ty2
+  where
+    origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
 
 ---------------
 unifyPred :: PredType -> PredType -> TcM TcCoercion
@@ -508,25 +511,9 @@ second, except that if the first is a synonym then the second may be a
 de-synonym'd version.  This way we get better error messages.
 
 \begin{code}
-data SwapFlag 
-  = NotSwapped	-- Args are: actual,   expected
-  | IsSwapped   -- Args are: expected, actual
-
-instance Outputable SwapFlag where
-  ppr IsSwapped  = ptext (sLit "Is-swapped")
-  ppr NotSwapped = ptext (sLit "Not-swapped")
-
-flipSwap :: SwapFlag -> SwapFlag
-flipSwap IsSwapped  = NotSwapped
-flipSwap NotSwapped = IsSwapped
-
-unSwap :: SwapFlag -> (a->a->b) -> a -> a -> b
-unSwap NotSwapped f a b = f a b
-unSwap IsSwapped  f a b = f b a
-
 ------------
-uType, uType_np, uType_defer
-  :: [EqOrigin]
+uType, uType_defer
+  :: CtOrigin
   -> TcType    -- ty1 is the *actual* type
   -> TcType    -- ty2 is the *expected* type
   -> TcM TcCoercion
@@ -534,10 +521,9 @@ uType, uType_np, uType_defer
 --------------
 -- It is always safe to defer unification to the main constraint solver
 -- See Note [Deferred unification]
-uType_defer items ty1 ty2
-  = ASSERT( not (null items) )
-    do { eqv <- newEq ty1 ty2
-       ; loc <- getCtLoc (TypeEqOrigin (last items))
+uType_defer origin ty1 ty2
+  = do { eqv <- newEq ty1 ty2
+       ; loc <- getCtLoc origin
        ; let ctev = CtWanted { ctev_evar = eqv
                              , ctev_pred = mkTcEqPred ty1 ty2 }
        ; emitFlat $ mkNonCanonical loc ctev 
@@ -549,18 +535,13 @@ uType_defer items ty1 ty2
             { ctxt <- getErrCtxt
             ; doc <- mkErrInfo emptyTidyEnv ctxt
             ; traceTc "utype_defer" (vcat [ppr eqv, ppr ty1,
-                                           ppr ty2, ppr items, doc])
+                                           ppr ty2, ppr origin, doc])
             }
        ; return (mkTcCoVarCo eqv) }
 
 --------------
--- Push a new item on the origin stack (the most common case)
-uType origin ty1 ty2  -- Push a new item on the origin stack
-  = uType_np (pushOrigin ty1 ty2 origin) ty1 ty2
-
---------------
 -- unify_np (short for "no push" on the origin stack) does the work
-uType_np origin orig_ty1 orig_ty2
+uType origin orig_ty1 orig_ty2
   = do { untch <- getUntouchables
        ; traceTc "u_tys " $ vcat 
               [ text "untch" <+> ppr untch
@@ -651,11 +632,11 @@ uType_np origin orig_ty1 orig_ty2
 
     ------------------
     go_app s1 t1 s2 t2
-      = do { co_s <- uType_np origin s1 s2  -- See Note [Unifying AppTy]
+      = do { co_s <- uType origin s1 s2  -- See Note [Unifying AppTy]
            ; co_t <- uType origin t1 t2        
            ; return $ mkTcAppCo co_s co_t }
 
-unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM TcCoercion
+unifySigmaTy :: CtOrigin -> TcType -> TcType -> TcM TcCoercion
 unifySigmaTy origin ty1 ty2
   = do { let (tvs1, body1) = tcSplitForAllTys ty1
              (tvs2, body2) = tcSplitForAllTys ty2
@@ -762,7 +743,7 @@ of the substitution; rather, notice that @uVar@ (defined below) nips
 back into @uTys@ if it turns out that the variable is already bound.
 
 \begin{code}
-uUnfilledVar :: [EqOrigin]
+uUnfilledVar :: CtOrigin
              -> SwapFlag
              -> TcTyVar -> TcTyVarDetails       -- Tyvar 1
              -> TcTauType  			-- Type 2
@@ -802,7 +783,7 @@ uUnfilledVar origin swapped tv1 details1 non_var_ty2  -- ty2 is not a type varia
 	  --     eg tv1 occured in type family parameter
 
 ----------------
-uUnfilledVars :: [EqOrigin]
+uUnfilledVars :: CtOrigin
               -> SwapFlag
               -> TcTyVar -> TcTyVarDetails      -- Tyvar 1
               -> TcTyVar -> TcTyVarDetails      -- Tyvar 2
@@ -813,8 +794,7 @@ uUnfilledVars :: [EqOrigin]
 uUnfilledVars origin swapped tv1 details1 tv2 details2
   = do { traceTc "uUnfilledVars" (    text "trying to unify" <+> ppr k1
                                   <+> text "with"            <+> ppr k2)
-       ; let ctxt = mkKindErrorCtxt ty1 ty2 k1 k2
-       ; mb_sub_kind <- addErrCtxtM ctxt $ unifyKind k1 k2
+       ; mb_sub_kind <- unifyKindX k1 k2
        ; case mb_sub_kind of {
            Nothing -> unSwap swapped (uType_defer origin) (mkTyVarTy tv1) ty2 ;
            Just sub_kind -> 
@@ -838,10 +818,10 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
 	   -- This happens for skolems of all sorts
            (_, _, _) -> unSwap swapped (uType_defer origin) ty1 ty2 } }
   where
-    k1       = tyVarKind tv1
-    k2       = tyVarKind tv2
-    ty1      = mkTyVarTy tv1
-    ty2      = mkTyVarTy tv2
+    k1  = tyVarKind tv1
+    k2  = tyVarKind tv2
+    ty1 = mkTyVarTy tv1
+    ty2 = mkTyVarTy tv2
 
     nicer_to_update_tv1 _     SigTv = True
     nicer_to_update_tv1 SigTv _     = False
@@ -875,13 +855,8 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 -- sort matters out.
 
 checkTauTvUpdate tv ty
-  = do { ty' <- zonkTcType ty
-       ; let k2 = typeKind ty'
-       ; k1 <- zonkTcKind (tyVarKind tv)
-       ; let ctxt = mkKindErrorCtxt (mkTyVarTy tv) ty' k1 k2
-       ; sub_k <- addErrCtxtM ctxt $
-                  unifyKind (tyVarKind tv) (typeKind ty')
-
+  = do { ty'   <- zonkTcType ty
+       ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty')
        ; case sub_k of
            Nothing -> return Nothing
            Just LT -> return Nothing
@@ -1010,50 +985,6 @@ we return a made-up TcTyVarDetails, but I think it works smoothly.
 
 %************************************************************************
 %*                                                                      *
-        Errors and contexts
-%*                                                                      *
-%************************************************************************
-
-\begin{code}
-pushOrigin :: TcType -> TcType -> [EqOrigin] -> [EqOrigin]
-pushOrigin ty_act ty_exp origin
-  = UnifyOrigin { uo_actual = ty_act, uo_expected = ty_exp } : origin
-\end{code}
-
-
------------------------------------------
-	UNUSED FOR NOW
------------------------------------------
-
-----------------
-----------------
--- If an error happens we try to figure out whether the function
--- function has been given too many or too few arguments, and say so.
-addSubCtxt :: InstOrigin -> TcType -> TcType -> TcM a -> TcM a
-addSubCtxt orig actual_res_ty expected_res_ty thing_inside
-  = addErrCtxtM mk_err thing_inside
-  where
-    mk_err tidy_env
-      = do { exp_ty' <- zonkTcType expected_res_ty
-           ; act_ty' <- zonkTcType actual_res_ty
-           ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
-                 (env2, act_ty'') = tidyOpenType env1     act_ty'
-                 (exp_args, _)    = tcSplitFunTys exp_ty''
-                 (act_args, _)    = tcSplitFunTys act_ty''
-
-                 len_act_args     = length act_args
-                 len_exp_args     = length exp_args
-
-                 message = case orig of
-                             OccurrenceOf fun
-                                  | len_exp_args < len_act_args -> wrongArgsCtxt "too few"  fun
-                                  | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
-                             _ -> mkExpectedActualMsg act_ty'' exp_ty''
-           ; return (env2, message) }
-
-
-%************************************************************************
-%*                                                                      *
                 Kind unification
 %*                                                                      *
 %************************************************************************
@@ -1086,31 +1017,31 @@ matchExpectedFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind
 matchExpectedFunKind _                         = return Nothing
 
 -----------------  
-unifyKind :: TcKind           -- k1 (actual)
-          -> TcKind           -- k2 (expected)
-          -> TcM (Maybe Ordering)     
+unifyKindX :: TcKind           -- k1 (actual)
+           -> TcKind           -- k2 (expected)
+           -> TcM (Maybe Ordering)     
                               -- Returns the relation between the kinds
                               -- Just LT <=> k1 is a sub-kind of k2
                               -- Nothing <=> incomparable
 
--- unifyKind deals with the top-level sub-kinding story
+-- unifyKindX deals with the top-level sub-kinding story
 -- but recurses into the simpler unifyKindEq for any sub-terms
 -- The sub-kinding stuff only applies at top level
 
-unifyKind (TyVarTy kv1) k2 = uKVar NotSwapped unifyKind kv1 k2
-unifyKind k1 (TyVarTy kv2) = uKVar IsSwapped  unifyKind kv2 k1
+unifyKindX (TyVarTy kv1) k2 = uKVar NotSwapped unifyKindX kv1 k2
+unifyKindX k1 (TyVarTy kv2) = uKVar IsSwapped  unifyKindX kv2 k1
 
-unifyKind k1 k2       -- See Note [Expanding synonyms during unification]
-  | Just k1' <- tcView k1 = unifyKind k1' k2
-  | Just k2' <- tcView k2 = unifyKind k1  k2'
+unifyKindX k1 k2       -- See Note [Expanding synonyms during unification]
+  | Just k1' <- tcView k1 = unifyKindX k1' k2
+  | Just k2' <- tcView k2 = unifyKindX k1  k2'
 
-unifyKind k1@(TyConApp kc1 []) k2@(TyConApp kc2 [])
+unifyKindX (TyConApp kc1 []) (TyConApp kc2 [])
   | kc1 == kc2               = return (Just EQ)
   | kc1 `tcIsSubKindCon` kc2 = return (Just LT)
   | kc2 `tcIsSubKindCon` kc1 = return (Just GT)
-  | otherwise                = unifyKindMisMatch k1 k2
+  | otherwise                = return Nothing
 
-unifyKind k1 k2 = unifyKindEq k1 k2
+unifyKindX k1 k2 = unifyKindEq k1 k2
   -- In all other cases, let unifyKindEq do the work
 
 uKVar :: SwapFlag -> (TcKind -> TcKind -> TcM (Maybe Ordering))
@@ -1128,7 +1059,7 @@ uKVar swapped unify_kind kv1 k2
   = uKVar (flipSwap swapped) unify_kind kv2 (TyVarTy kv1)
 
   | otherwise 
-  = unSwap swapped unifyKindMisMatch (TyVarTy kv1) k2
+  = return Nothing
 
 {- Note [Unifying kind variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1166,7 +1097,7 @@ unifyKindEq (TyConApp kc1 k1s) (TyConApp kc2 k2s)
                  then Just EQ 
                  else Nothing) }
 
-unifyKindEq k1 k2 = unifyKindMisMatch k1 k2
+unifyKindEq _ _ = return Nothing
 
 ----------------
 uUnboundKVar :: MetaKindVar -> TcKind -> TcM (Maybe Ordering)
@@ -1201,34 +1132,7 @@ mkKindErrorCtxt ty1 ty2 k1 k2 env0
           k1  <- zonkTcKind k1'
           k2  <- zonkTcKind k2'
           return (env4, 
-                  vcat [ ptext (sLit "Kind incompatibility when matching types:")
+                  vcat [ ptext (sLit "Kind incompatibility when matching types xx:")
                        , nest 2 (vcat [ ppr ty1 <+> dcolon <+> ppr k1
                                       , ppr ty2 <+> dcolon <+> ppr k2 ]) ])
-
-unifyKindMisMatch :: TcKind -> TcKind -> TcM (Maybe Ordering)
-unifyKindMisMatch ki1 ki2 
-  = do { _ <- uType_defer (pushOrigin ki1 ki2 []) ki1 ki2
-       ; return Nothing }
-{-
-do
-    ki1' <- zonkTcKind ki1
-    ki2' <- zonkTcKind ki2
-    let msg = hang (ptext (sLit "Couldn't match kind"))
-              2 (sep [quotes (ppr ki1'),
-                      ptext (sLit "against"),
-                      quotes (ppr ki2')])
-    failWithTc msg
-
-
-----------------
-kindOccurCheckErr :: Var -> Type -> SDoc
-kindOccurCheckErr tyvar ty
-  = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
-       2 (sep [ppr tyvar, char '=', ppr ty])
-
-kindSigVarErr :: Var -> Type -> SDoc
-kindSigVarErr tv ty
-  = hang (ptext (sLit "Cannot unify the kind variable") <+> quotes (ppr tv))
-       2 (ptext (sLit "with the kind") <+> quotes (ppr ty))
--}
 \end{code}