Fix the constraint simplifier (Trac #7967)

Richard's bug report showed up a couple of subtleties in the constraint solver

* We can strengthen the kind invariants on CTyEqCan and CFunEqCan
    See Note [Kind orientation for CTyEqCan]
    and Note [Kind orientation for CFunEqCan] in TcRnTypes
  There are some changes to reOrient and checkKind in TcCanonical
  to support these stronger invarants.

* In TcSimplify we must make sure that we re-simplify if defaultTyVar
  does anything.  See Note [Must simplify after defaulting] in TcSimplify.

The usual round of refactoring follows!

5 files changed, 194 insertions, 169 deletions

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index db1c5a0a55..c0c02fbcc0 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -27,7 +27,7 @@ import OccName( OccName )
 import Outputable
 import Control.Monad    ( when )
 import TysWiredIn ( eqTyCon )
-
+import DynFlags( DynFlags )
 import VarSet
 import TcSMonad
 import FastString
@@ -180,7 +180,7 @@ canonicalize (CTyEqCan { cc_loc  = d
                        , cc_tyvar  = tv
                        , cc_rhs    = xi })
   = {-# SCC "canEqLeafTyVarEq" #-}
-    canEqLeafTyVarEq d ev tv xi
+    canEqLeafTyVar d ev tv xi
 
 canonicalize (CFunEqCan { cc_loc = d
                         , cc_ev = ev
@@ -188,7 +188,7 @@ canonicalize (CFunEqCan { cc_loc = d
                         , cc_tyargs = xis1
                         , cc_rhs    = xi2 })
   = {-# SCC "canEqLeafFunEq" #-}
-    canEqLeafFunEq d ev fn xis1 xi2
+    canEqLeafFun d ev fn xis1 xi2
 
 canonicalize (CIrredEvCan { cc_ev = ev
                           , cc_loc = d })
@@ -544,20 +544,20 @@ flatten loc f ctxt (TyConApp tc tys)
                              -- cache as well when we interact an equality with the inert. 
                              -- The design choice is: do we keep the flat cache rewritten or not?
                              -- For now I say we don't keep it fully rewritten.
-                            do { traceTcS "flatten/flat-cache hit" $ ppr ctev
-                               ; (rhs_xi,co) <- flatten loc f flav rhs_ty
+                            do { (rhs_xi,co) <- flatten loc f flav rhs_ty
                                ; let final_co = evTermCoercion (ctEvTerm ctev)
                                                 `mkTcTransCo` mkTcSymCo co
+                               ; traceTcS "flatten/flat-cache hit" $ (ppr ctev $$ ppr rhs_xi $$ ppr final_co)
                                ; return (final_co, rhs_xi) }
                           
-                        _ -> do { traceTcS "flatten/flat-cache miss" $ ppr fam_ty
-                                ; (ctev, rhs_xi) <- newFlattenSkolem ctxt fam_ty
+                        _ -> do { (ctev, rhs_xi) <- newFlattenSkolem ctxt fam_ty
                                 ; let ct = CFunEqCan { cc_ev     = ctev
                                                      , cc_fun    = tc
                                                      , cc_tyargs = xi_args
                                                      , cc_rhs    = rhs_xi
                                                      , cc_loc    = loc }
                                 ; updWorkListTcS $ extendWorkListFunEq ct
+                                ; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr rhs_xi $$ ppr ctev)
                                 ; return (evTermCoercion (ctEvTerm ctev), rhs_xi) }
                     }
                   -- Emit the flat constraints
@@ -609,13 +609,15 @@ flattenTyVar loc f ctxt tv
   | otherwise
   = do { mb_ty <- isFilledMetaTyVar_maybe tv
        ; case mb_ty of {
-           Just ty -> flatten loc f ctxt ty ;
+           Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
+                         ; flatten loc f ctxt ty } ;
            Nothing -> 
 
     -- Try in ty_binds
     do { ty_binds <- getTcSTyBindsMap
        ; case lookupVarEnv ty_binds tv of {
-           Just (_tv,ty) -> flatten loc f ctxt ty ;
+           Just (_tv,ty) -> do { traceTcS "Following bound tyvar" (ppr tv <+> equals <+> ppr ty)
+                               ; flatten loc f ctxt ty } ;
                  -- NB: ty_binds coercions are all ReflCo,
                  -- so no need to transitively compose co' with another coercion,
                  -- unlike in 'flatten_from_inerts'
@@ -626,7 +628,8 @@ flattenTyVar loc f ctxt tv
        ; let mco = tv_eq_subst ieqs tv  -- co : v ~ ty
        ; case mco of { 
            Just (co,ty) -> 
-             do { (ty_final,co') <- flatten loc f ctxt ty
+             do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr ty)
+                ; (ty_final,co') <- flatten loc f ctxt ty
                 ; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } ;
        -- NB recursive call. 
        -- Why? Because inert subst. non-idempotent, Note [Detailed InertCans Invariants]
@@ -1015,9 +1018,14 @@ reOrient (FunCls {}) _      = False             -- Fun/Other on rhs
 reOrient (VarCls {})   (FunCls {})           = True 
 reOrient (VarCls {})   (OtherCls {})         = False
 reOrient (VarCls tv1)  (VarCls tv2)  
-  | isMetaTyVar     tv2 && not (isMetaTyVar tv1)      = True 
-  | isFlatSkolTyVar tv2 && not (isFlatSkolTyVar tv1)  = True  -- Note [Eliminate flat-skols]
-  | otherwise                                         = False 
+  | not (k2 `isSubKind` k1),   k1 `isSubKind` k2   = True  -- Note [Kind orientation for CTyEqCan]
+                                                           -- in TcRnTypes
+  | not (isMetaTyVar tv1),     isMetaTyVar     tv2 = True 
+  | not (isFlatSkolTyVar tv1), isFlatSkolTyVar tv2 = True  -- Note [Eliminate flat-skols]
+  | otherwise                                      = False 
+  where
+    k1 = tyVarKind tv1
+    k2 = tyVarKind tv2
   -- Just for efficiency, see CTyEqCan invariants 
 
 ------------------
@@ -1060,18 +1068,14 @@ canEqLeaf loc ev s1 s2
 canEqLeafOriented :: CtLoc -> CtEvidence
                   -> TypeClassifier -> TcType -> TcS StopOrContinue
 -- By now s1 will either be a variable or a type family application
--- Precondition: the LHS and RHS have `compatKind` kinds
---               so we can safely generate a CTyEqCan or CFunEqCan
-canEqLeafOriented loc ev (FunCls fn tys1) s2 = canEqLeafFunEq loc ev fn tys1 s2
-canEqLeafOriented loc ev (VarCls tv)      s2 = canEqLeafTyVarEq loc ev tv s2
+canEqLeafOriented loc ev (FunCls fn tys1) s2 = canEqLeafFun loc ev fn tys1 s2
+canEqLeafOriented loc ev (VarCls tv)      s2 = canEqLeafTyVar loc ev tv s2
 canEqLeafOriented _   ev (OtherCls {})    _  = pprPanic "canEqLeafOriented" (ppr (ctEvPred ev))
 
-canEqLeafFunEq :: CtLoc -> CtEvidence
-               -> TyCon -> [TcType] -> TcType -> TcS StopOrContinue
--- Precondition: LHS and RHS have compatible kinds 
---               (guaranteed by canEqLeaf0
-canEqLeafFunEq loc ev fn tys1 ty2  -- ev :: F tys1 ~ ty2
-  = do { traceTcS "canEqLeafFunEq" $ pprEq (mkTyConApp fn tys1) ty2
+canEqLeafFun :: CtLoc -> CtEvidence
+             -> TyCon -> [TcType] -> TcType -> TcS StopOrContinue
+canEqLeafFun loc ev fn tys1 ty2  -- ev :: F tys1 ~ ty2
+  = do { traceTcS "canEqLeafFun" $ pprEq (mkTyConApp fn tys1) ty2
        ; let flav = ctEvFlavour ev
 
             -- Flatten type function arguments
@@ -1085,95 +1089,102 @@ canEqLeafFunEq loc ev fn tys1 ty2  -- ev :: F tys1 ~ ty2
        ; let fam_head = mkTyConApp fn xis1
              xco = mkHdEqPred ty2 (mkTcTyConAppCo fn cos1) co2
              -- xco :: (F xis1 ~ xi2) ~ (F tys1 ~ ty2)
-             
-       ; checkKind loc ev fam_head xi2 xco $ \new_ev -> 
-         continueWith (CFunEqCan { cc_ev = new_ev, cc_loc = loc
-                                 , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 }) }
-
-canEqLeafTyVarEq :: CtLoc -> CtEvidence
-                   -> TcTyVar -> TcType -> TcS StopOrContinue
--- Precondition: LHS and RHS have compatible kinds 
---               (guaranteed by canEqLeaf0
-canEqLeafTyVarEq loc ev tv s2              -- ev :: tv ~ s2
-  = do { traceTcS "canEqLeafTyVarEq" $ pprEq (mkTyVarTy tv) s2
+
+       ; mb <- rewriteCtFlavor ev (mkTcEqPred fam_head xi2) xco
+       ; case mb of 
+            Nothing     -> return Stop 
+            Just new_ev | typeKind fam_head `isSubKind` typeKind xi2
+                        -- Establish CFunEqCan kind invariant
+                        -> continueWith (CFunEqCan { cc_ev = new_ev, cc_loc = loc
+                                                   , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 })
+                        | otherwise
+                        -> checkKind loc new_ev fam_head xi2 }
+
+canEqLeafTyVar :: CtLoc -> CtEvidence
+               -> TcTyVar -> TcType -> TcS StopOrContinue
+canEqLeafTyVar loc ev tv s2              -- ev :: tv ~ s2
+  = do { traceTcS "canEqLeafTyVar 1" $ pprEq (mkTyVarTy tv) s2
        ; let flav = ctEvFlavour ev
        ; (xi1,co1) <- flattenTyVar loc FMFullFlatten flav tv -- co1 :: xi1 ~ tv
        ; (xi2,co2) <- flatten      loc FMFullFlatten flav s2 -- co2 :: xi2 ~ s2 
        ; let co = mkHdEqPred s2 co1 co2
              -- co :: (xi1 ~ xi2) ~ (tv ~ s2)
        
-       ; traceTcS "canEqLeafTyVarEq2" $ vcat [ppr xi1, ppr xi1]
-       ; case (getTyVar_maybe xi1, getTyVar_maybe xi2) of {
+       ; traceTcS "canEqLeafTyVar 2" $ vcat [ppr xi1, ppr xi2]
+       ; case (getTyVar_maybe xi1, getTyVar_maybe xi2) of
            (Nothing,  _) -> -- Rewriting the LHS did not yield a type variable
                             -- so go around again to canEq
                             do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2) co
                                ; case mb of
                                    Nothing     -> return Stop
-                                   Just new_ev -> canEqNC loc new_ev xi1 xi2 } ;
+                                   Just new_ev -> canEqNC loc new_ev xi1 xi2 }
 
            (Just tv1, Just tv2) | tv1 == tv2
               -> do { when (isWanted ev) $
                       setEvBind (ctev_evar ev) (mkEvCast (EvCoercion (mkTcReflCo xi1)) co)
-                    ; return Stop } ;
-
-           (Just tv1, _) ->
-
-         -- LHS rewrote to a type variable, RHS to something else
-    do { dflags <- getDynFlags
-       ; case occurCheckExpand dflags tv1 xi2 of
-           OC_OK xi2' -> -- No occurs check, so we can continue; but make sure
-                         -- that the new goal has enough type synonyms expanded by 
-                         -- by the occurCheckExpand
-                         checkKind loc ev xi1 xi2' co $ \new_ev -> 
-                         continueWith (CTyEqCan { cc_ev = new_ev, cc_loc = loc
-                                                , cc_tyvar  = tv1, cc_rhs = xi2' })
-
-           _bad ->  -- Occurs check error
-                    do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2) co
-                       ; case mb of
-                              Nothing     -> return Stop
-                              Just new_ev -> canEqFailure loc new_ev xi1 xi2 }
-    } } }
+                    ; return Stop } 
+
+           (Just tv1, _) -> do { dflags <- getDynFlags
+                               ; canEqLeafTyVar2 dflags loc ev tv1 xi2 co } }
+
+canEqLeafTyVar2 :: DynFlags -> CtLoc -> CtEvidence
+                -> TyVar -> Type -> TcCoercion 
+                -> TcS StopOrContinue
+-- LHS rewrote to a type variable, 
+-- RHS to something else (possibly a tyvar, but not the *same* tyvar)
+canEqLeafTyVar2 dflags loc ev tv1 xi2 co
+  | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2  -- No occurs check
+  = do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2') co
+                -- Ensure that the new goal has enough type synonyms 
+                -- expanded by the occurCheckExpand; hence using xi2' here
+
+       ; case mb of 
+            Nothing     -> return Stop 
+            Just new_ev | typeKind xi2' `isSubKind` tyVarKind tv1
+                        -- Establish CTyEqCan kind invariant
+                        -- Reorientation has done its best, but the kinds might
+                        -- simply be incompatible
+                        -> continueWith (CTyEqCan { cc_ev = new_ev, cc_loc = loc
+                                                  , cc_tyvar  = tv1, cc_rhs = xi2' })
+                        | otherwise
+                        -> checkKind loc new_ev xi1 xi2' }
+
+  | otherwise  -- Occurs check error
+  = do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2) co
+       ; case mb of
+           Nothing     -> return Stop
+           Just new_ev -> canEqFailure loc new_ev xi1 xi2 }
+  where
+    xi1 = mkTyVarTy tv1
 
 checkKind :: CtLoc 
           -> CtEvidence          -- t1~t2
           -> TcType -> TcType    -- s1~s2, flattened and zonked
-          -> TcCoercion          -- (s1~s2) ~ (t2~t2)
-          -> (CtEvidence -> TcS StopOrContinue)  -- Do this if kinds are OK
           -> TcS StopOrContinue
--- Do the rewrite, test for incompatible kinds, and continue
--- 
--- See Note [Equalities with incompatible kinds]
--- If there are incompatible kinds, emit an "irreducible" constraint 
+-- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint 
 --       CIrredEvCan (NOT CTyEqCan or CFunEqCan)
 -- for the type equality; and continue with the kind equality constraint.
 -- When the latter is solved, it'll kick out the irreducible equality for 
 -- a second attempt at solving
+-- See Note [Equalities with incompatible kinds]
 
-checkKind loc ev s1 s2 co normal_kont
-  = do { mb <- rewriteCtFlavor ev (mkTcEqPred s1 s2) co
-       ; case mb of {
-            Nothing                          -> return Stop ;
-            Just new_ev | k1 `compatKind` k2 -> normal_kont new_ev
-                        | otherwise          ->
-
-    ASSERT( isKind k1 && isKind k2 )
+checkKind loc new_ev s1 s2
+  = ASSERT( isKind k1 && isKind k2 )
     do {  -- See Note [Equalities with incompatible kinds]
-         traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr s1 <+> dcolon <+> ppr k1,
-                                                         ppr s2 <+> dcolon <+> ppr k2])
+         traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
        ; updWorkListTcS $ extendWorkListNonEq $ 
          CIrredEvCan { cc_ev = new_ev, cc_loc = loc }
        ; mw <- newDerived (mkEqPred k1 k2) 
        ; case mw of
            Nothing  -> return Stop
-           Just kev -> canEqNC kind_co_loc kev k1 k2 } } }
-  where
-    k1 = typeKind s1
-    k2 = typeKind s2
+           Just kev -> canEqNC kind_co_loc kev k1 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.
+  where
+    k1 = typeKind s1
+    k2 = typeKind s2
     kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
 
 
@@ -1206,8 +1217,10 @@ the fsk.
 Note [Equalities with incompatible kinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
-invariant that LHS and RHS have `compatKind` kinds.  What if we try
-to unify two things with incompatible kinds?
+invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
+CFunEqCan.  What if we try to unify two things with incompatible
+kinds?
+
 eg    a ~ b  where a::*, b::*->*
 or    a ~ b  where a::*, b::k, k is a kind variable
 
@@ -1227,6 +1240,9 @@ NB: it is important that the types s1,s2 are flattened and zonked
     E.g. it is WRONG to make an irred (a:k1)~(b:k2)
          if we already have a substitution k1:=k2
 
+See also Note [Kind orientation for CTyEqCan] and
+         Note [Kind orientation for CFunEqCan] in TcRnTypes
+
 Note [Type synonyms and canonicalization]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We treat type synonym applications as xi types, that is, they do not
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index ce03a9e685..3828a4d9c9 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -243,9 +243,14 @@ spontaneousSolveStage workItem
   = do { mb_solved <- trySpontaneousSolve workItem
        ; case mb_solved of
            SPCantSolve
-              | CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
+              | CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = fl } <- workItem
               -- Unsolved equality
-              -> do { n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
+              -> do { untch <- getUntouchables
+                    ; traceTcS "Can't solve tyvar equality" 
+                          (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+                                , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
+                                , text "Untouchables =" <+> ppr untch ])
+                    ; n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
                     ; traceFireTcS workItem $
                       ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked <> colon 
                       <+> ppr workItem
@@ -404,7 +409,8 @@ trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
 trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
                                        , cc_tyvar = tv1, cc_rhs = xi, cc_loc = d })
   | isGiven gw
-  = return SPCantSolve
+  = do { traceTcS "No spontaneous solve for given" (ppr workItem)
+       ; return SPCantSolve }
   | Just tv2 <- tcGetTyVar_maybe xi
   = do { tch1 <- isTouchableMetaTyVarTcS tv1
        ; tch2 <- isTouchableMetaTyVarTcS tv2
@@ -412,21 +418,17 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
            (True,  True)  -> trySpontaneousEqTwoWay d gw tv1 tv2
            (True,  False) -> trySpontaneousEqOneWay d gw tv1 xi
            (False, True)  -> trySpontaneousEqOneWay d gw tv2 (mkTyVarTy tv1)
-	   _ -> return SPCantSolve }
+	   _              -> return SPCantSolve }
   | otherwise
   = do { tch1 <- isTouchableMetaTyVarTcS tv1
        ; if tch1 then trySpontaneousEqOneWay d gw tv1 xi
-                 else do { untch <- getUntouchables
-                         ; traceTcS "Untouchable LHS, can't spontaneously solve workitem" $
-                           vcat [text "Untouchables =" <+> ppr untch
-                                , text "Workitem =" <+> ppr workItem ]
-                         ; return SPCantSolve }
-       }
+                 else return SPCantSolve }
 
   -- No need for 
   --      trySpontaneousSolve (CFunEqCan ...) = ...
   -- See Note [No touchables as FunEq RHS] in TcSMonad
-trySpontaneousSolve _ = return SPCantSolve
+trySpontaneousSolve item = do { traceTcS "Spont: no tyvar on lhs" (ppr item)
+                              ; return SPCantSolve }
 
 ----------------
 trySpontaneousEqOneWay :: CtLoc -> CtEvidence 
@@ -457,57 +459,6 @@ trySpontaneousEqTwoWay d gw tv1 tv2
     nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
 \end{code}
 
-Note [Kind errors] 
-~~~~~~~~~~~~~~~~~~
-Consider the wanted problem: 
-      alpha ~ (# Int, Int #) 
-where alpha :: ArgKind and (# Int, Int #) :: (#). We can't spontaneously solve this constraint, 
-but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay' 
-simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and 
-get quantified over in inference mode. That's bad because we do know at this point that the 
-constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
-
-The same applies in canonicalization code in case of kind errors in the givens. 
-
-However, when we canonicalize givens we only check for compatibility (@compatKind@). 
-If there were a kind error in the givens, this means some form of inconsistency or dead code.
-
-You may think that when we spontaneously solve wanteds we may have to look through the 
-bindings to determine the right kind of the RHS type. E.g one may be worried that xi is 
-@alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
-But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
-so this situation can't happen. 
-
-Note [Spontaneous solving and kind compatibility] 
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Note that our canonical constraints insist that *all* equalities (tv ~
-xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
-the same kinds.  ("compatible" means one is a subKind of the other.)
-
-  - It can't be *equal* kinds, because
-     b) wanted constraints don't necessarily have identical kinds
-               eg   alpha::? ~ Int
-     b) a solved wanted constraint becomes a given
-
-  - SPJ thinks that *given* constraints (tv ~ tau) always have that
-    tau has a sub-kind of tv; and when solving wanted constraints
-    in trySpontaneousEqTwoWay we re-orient to achieve this.
-
-  - Note that the kind invariant is maintained by rewriting.
-    Eg wanted1 rewrites wanted2; if both were compatible kinds before,
-       wanted2 will be afterwards.  Similarly givens.
-
-Caveat:
-  - Givens from higher-rank, such as: 
-          type family T b :: * -> * -> * 
-          type instance T Bool = (->) 
-
-          f :: forall a. ((T a ~ (->)) => ...) -> a -> ... 
-          flop = f (...) True 
-     Whereas we would be able to apply the type instance, we would not be able to 
-     use the given (T Bool ~ (->)) in the body of 'flop' 
-
-
 Note [Avoid double unifications] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The spontaneous solver has to return a given which mentions the unified unification
@@ -527,8 +478,6 @@ double unifications is the main reason we disallow touchable
 unification variables as RHS of type family equations: F xis ~ alpha.
 
 \begin{code}
-----------------
-
 solveWithIdentity :: CtLoc -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
 -- Solve with the identity coercion 
 -- Precondition: kind(xi) is a sub-kind of kind(tv)
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index e2b9cf80cf..b53c40d358 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -885,7 +885,8 @@ data Ct
       cc_ev :: CtEvidence,   -- See Note [Ct/evidence invariant]
         -- The ctev_pred of the evidence is 
         -- of form   (tv xi1 xi2 ... xin)
-        --      or   (t1 ~ t2)   where not (kind(t1) `compatKind` kind(t2)
+        --      or   (tv1 ~ ty2)   where the CTyEqCan  kind invariant fails
+        --      or   (F tys ~ ty)  where the CFunEqCan kind invariant fails
         -- See Note [CIrredEvCan constraints]
       cc_loc :: CtLoc
     }
@@ -893,8 +894,8 @@ data Ct
   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
        -- Invariant:
        --   * tv not in tvs(xi)   (occurs check)
-       --   * typeKind xi `compatKind` typeKind tv
-       --       See Note [Spontaneous solving and kind compatibility]
+       --   * typeKind xi `subKind` typeKind tv
+       --       See Note [Kind orientation for CTyEqCan]
        --   * We prefer unification variables on the left *JUST* for efficiency
       cc_ev :: CtEvidence,    -- See Note [Ct/evidence invariant]
       cc_tyvar  :: TcTyVar,
@@ -904,7 +905,8 @@ data Ct
 
   | CFunEqCan {  -- F xis ~ xi
        -- Invariant: * isSynFamilyTyCon cc_fun
-       --            * typeKind (F xis) `compatKind` typeKind xi
+       --            * typeKind (F xis) `subKind` typeKind xi
+       --       See Note [Kind orientation for CFunEqCan]
       cc_ev     :: CtEvidence,  -- See Note [Ct/evidence invariant]
       cc_fun    :: TyCon,       -- A type function
       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
@@ -926,6 +928,49 @@ data Ct
     }
 \end{code}
 
+Note [Kind orientation for CTyEqCan]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given an equality  (t:* ~ s:Open), we absolutely want to re-orient it.
+We can't solve it by updating t:=s, ragardless of how touchable 't' is,
+because the kinds don't work.  Indeed we don't want to leave it with
+the orientation (t ~ s), becuase if that gets into the inert set we'll
+start replacing t's by s's, and that too is the wrong way round.
+
+Hence in a CTyEqCan, (t:k1 ~ xi:k2) we require that k2 is a subkind of k1.
+
+If the two have incompatible kinds, we just don't use a CTyEqCan at all.
+See Note [Equalities with incompatible kinds] in TcCanonical
+
+We can't require *equal* kinds, because
+     * wanted constraints don't necessarily have identical kinds
+               eg   alpha::? ~ Int
+     * a solved wanted constraint becomes a given
+
+Note [Kind orientation for CFunEqCan]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For (F xis ~ rhs) we require that kind(rhs) is a subkind of kind(lhs).
+This reallly only maters when rhs is an Open type variable (since only type
+variables have Open kinds):
+   F ty ~ (a:Open)
+which can happen, say, from
+      f :: F a b
+      f = undefined   -- The a:Open comes from instantiating 'undefined'
+
+Note that the kind invariant is maintained by rewriting.
+Eg wanted1 rewrites wanted2; if both were compatible kinds before,
+   wanted2 will be afterwards.  Similarly givens.
+
+Caveat:
+  - Givens from higher-rank, such as: 
+          type family T b :: * -> * -> * 
+          type instance T Bool = (->) 
+
+          f :: forall a. ((T a ~ (->)) => ...) -> a -> ... 
+          flop = f (...) True 
+     Whereas we would be able to apply the type instance, we would not be able to 
+     use the given (T Bool ~ (->)) in the body of 'flop' 
+
+
 Note [CIrredEvCan constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 CIrredEvCan constraints are used for constraints that are "stuck"
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index e03368de5c..dd5b56116b 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -81,7 +81,7 @@ module TcSMonad (
     newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
     cloneMetaTyVar,
 
-    compatKind, mkKindErrorCtxtTcS,
+    mkKindErrorCtxtTcS,
 
     Untouchables, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe,
     zonkTyVarsAndFV,
@@ -149,15 +149,11 @@ import Digraph
 
 
 \begin{code}
-compatKind :: Kind -> Kind -> Bool
-compatKind k1 k2 = k1 `tcIsSubKind` k2 || k2 `tcIsSubKind` k1 
-
 mkKindErrorCtxtTcS :: Type -> Kind 
                    -> Type -> Kind 
                    -> ErrCtxt
 mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
   = (False,TcM.mkKindErrorCtxt ty1 ty2 ki1 ki2)
-
 \end{code}
 
 %************************************************************************
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 4945a0ce95..1f92532dcc 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -77,34 +77,53 @@ simplifyTop wanteds
     simpl_top :: WantedConstraints -> TcS WantedConstraints
     simpl_top wanteds
       = do { wc_first_go <- nestTcS (solve_wanteds_and_drop wanteds)
-           ; free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc_first_go) 
-           ; let meta_tvs = filterVarSet isMetaTyVar free_tvs
+                            -- This is where the main work happens
+           ; try_tyvar_defaulting wc_first_go }
+
+    try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
+    try_tyvar_defaulting wc
+      | isEmptyWC wc 
+      = return wc
+      | otherwise
+      = do { free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc) 
+           ; let meta_tvs = varSetElems (filterVarSet isMetaTyVar free_tvs)
                    -- zonkTyVarsAndFV: the wc_first_go is not yet zonked
                    -- filter isMetaTyVar: we might have runtime-skolems in GHCi, 
                    -- and we definitely don't want to try to assign to those!
 
-           ; mapM_ defaultTyVar (varSetElems meta_tvs)   -- Has unification side effects
-           ; simpl_top_loop wc_first_go }
+           ; meta_tvs' <- mapM defaultTyVar meta_tvs   -- Has unification side effects
+           ; if meta_tvs' == meta_tvs   -- No defaulting took place;
+                                        -- (defaulting returns fresh vars)
+             then try_class_defaulting wc
+             else do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
+                            -- See Note [Must simplify after defaulting]
+                     ; try_class_defaulting wc_residual } }
     
-    simpl_top_loop wc
+    try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
+    try_class_defaulting wc
       | isEmptyWC wc || insolubleWC wc
-             -- Don't do type-class defaulting if there are insolubles
-             -- Doing so is not going to solve the insolubles
-      = return wc
+      = return wc  -- Don't do type-class defaulting if there are insolubles
+                   -- Doing so is not going to solve the insolubles
       | otherwise
-      = do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
-           ; let wc_flat_approximate = approximateWC wc_residual
-           ; something_happened <- applyDefaultingRules wc_flat_approximate
-                                        -- See Note [Top-level Defaulting Plan]
-           ; if something_happened then 
-               simpl_top_loop wc_residual 
-             else 
-               return wc_residual }
+      = do { something_happened <- applyDefaultingRules (approximateWC wc)
+                                   -- See Note [Top-level Defaulting Plan]
+           ; if something_happened 
+             then do { wc_residual <- nestTcS (solve_wanteds_and_drop wc)
+                     ; try_class_defaulting wc_residual }
+             else return wc }
 \end{code}
 
+Note [Must simplify after defaulting]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We may have a deeply buried constraint
+    (t:*) ~ (a:Open)
+which we couldn't solve because of the kind incompatibility, and 'a' is free.
+Then when we default 'a' we can solve the constraint.  And we want to do
+that before starting in on type classes.  We MUST do it before reporting
+errors, because it isn't an error!  Trac #7967 was due to this.
+
 Note [Top-level Defaulting Plan]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 We have considered two design choices for where/when to apply defaulting.   
    (i) Do it in SimplCheck mode only /whenever/ you try to solve some 
        flat constraints, maybe deep inside the context of implications.