Fiddling with kind errors

8 files changed, 254 insertions, 176 deletions

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 527552a50c..d20a7019d0 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -764,24 +764,7 @@ canEq loc ev ty1 ty2
   | Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
   , Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
   , isDecomposableTyCon tc1 && isDecomposableTyCon tc2
-  = -- Generate equalities for each of the corresponding arguments
-    if (tc1 /= tc2 || length tys1 /= length tys2)
-    -- Fail straight away for better error messages
-    then canEqFailure loc ev ty1 ty2
-    else
-    do { let xcomp xs  = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
-             xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
-             xev = XEvTerm xcomp xdecomp
-       ; ctevs <- xCtFlavor ev (zipWith mkTcEqPred tys1 tys2) xev
-       ; canEvVarsCreated loc ctevs }
-
--- See Note [Equality between type applications]
---     Note [Care with type applications] in TcUnify
-canEq loc ev ty1 ty2    -- e.g.  F a b ~ Maybe c
-                          -- where F has arity 1
-  | Just (s1,t1) <- tcSplitAppTy_maybe ty1
-  , Just (s2,t2) <- tcSplitAppTy_maybe ty2
-  = canEqAppTy loc ev s1 t1 s2 t2
+  = canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2 
 
 canEq loc ev s1@(ForAllTy {}) s2@(ForAllTy {})
  | tcIsForAllTy s1, tcIsForAllTy s2
@@ -798,20 +781,53 @@ canEq loc ev s1@(ForAllTy {}) s2@(ForAllTy {})
  = do { traceTcS "Ommitting decomposition of given polytype equality" $ 
         pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
       ; return Stop }
-canEq loc ev ty1 ty2  = canEqFailure loc ev ty1 ty2
+
+-- The last remaining source of success is an application
+-- e.g.  F a b ~ Maybe c   where F has arity 1
+-- See Note [Equality between type applications]
+--     Note [Care with type applications] in TcUnify
+canEq loc ev ty1 ty2 
+ =  do { let flav = ctEvFlavour ev
+       ; (s1, co1) <- flatten loc FMSubstOnly flav ty1
+       ; (s2, co2) <- flatten loc FMSubstOnly flav ty2
+       ; mb_ct <- rewriteCtFlavor ev (mkTcEqPred s1 s2) (mkHdEqPred s2 co1 co2)
+       ; case mb_ct of
+           Nothing     -> return Stop
+           Just new_ev -> last_chance new_ev s1 s2 }
+  where
+    last_chance new_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
+    
+      | Just (s1,t1) <- tcSplitAppTy_maybe ty1
+      , Just (s2,t2) <- tcSplitAppTy_maybe ty2
+      = do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
+             	 xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
+             	 xevdecomp x = let xco = evTermCoercion x 
+       	                       in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)]
+       	   ; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
+       	   ; canEvVarsCreated loc ctevs }
+
+      | otherwise
+      = do { emitInsoluble (CNonCanonical { cc_ev = new_ev, cc_loc = loc })
+           ; return Stop }
 
 ------------------------
--- Type application
-canEqAppTy :: CtLoc -> CtEvidence 
-           -> Type -> Type -> Type -> Type
-           -> TcS StopOrContinue
-canEqAppTy loc ev s1 t1 s2 t2
-  = ASSERT( not (isKind t1) && not (isKind t2) )
-    do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
-             xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
-             xevdecomp x = let xco = evTermCoercion x 
-                           in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)]
-       ; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
+canDecomposableTyConApp :: CtLoc -> CtEvidence 
+                        -> TyCon -> [TcType] 
+                        -> TyCon -> [TcType] 
+                        -> TcS StopOrContinue
+canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2
+  | tc1 /= tc2 || length tys1 /= length tys2
+    -- Fail straight away for better error messages
+  = canEqFailure loc ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
+  | otherwise
+  = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
+             xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
+             xev = XEvTerm xcomp xdecomp
+       ; ctevs <- xCtFlavor ev (zipWith mkTcEqPred tys1 tys2) xev
        ; canEvVarsCreated loc ctevs }
 
 canEqFailure :: CtLoc -> CtEvidence -> TcType -> TcType -> TcS StopOrContinue
@@ -1100,7 +1116,8 @@ canEqLeaf :: CtLoc -> CtEvidence
 -- saturated type function application).  
 
 -- Preconditions: 
---    * one of the two arguments is variable or family applications
+--    * one of the two arguments is variable 
+--      or an exactly-saturated family application
 --    * the two types are not equal (looking through synonyms)
 canEqLeaf loc ev s1 s2 
   | cls1 `re_orient` cls2
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 010c499829..a7159681f1 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -104,8 +104,7 @@ reportUnsolved wanted
 reportAllUnsolved :: WantedConstraints -> TcM ()
 -- Report all unsolved goals, even if -fdefer-type-errors is on
 -- See Note [Deferring coercion errors to runtime]
-reportAllUnsolved wanted 
-  = report_unsolved Nothing (panic "reportAllUnsolved") wanted
+reportAllUnsolved wanted = report_unsolved Nothing False wanted
 
 report_unsolved :: Maybe EvBindsVar  -- cec_binds
                 -> Bool              -- cec_defer
@@ -123,11 +122,12 @@ report_unsolved mb_binds_var defer wanted
                  
             -- If we are deferring we are going to need /all/ evidence around,
             -- including the evidence produced by unflattening (zonkWC)
-       ; errs_so_far <- ifErrsM (return True) (return False)
+--       ; errs_so_far <- ifErrsM (return True) (return False)
        ; let tidy_env = tidyFreeTyVars env0 free_tvs
              free_tvs = tyVarsOfWC wanted
              err_ctxt = CEC { cec_encl  = []
-                            , cec_insol = errs_so_far || insolubleWC wanted
+                            , cec_insol = False
+                                          --errs_so_far || insolubleWC wanted
                                           -- Don't report ambiguity errors if
                                           -- there are any other solid errors 
                                           -- to report
@@ -170,12 +170,12 @@ data ReportErrCtxt
 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
                                  , ic_wanted = wanted, ic_binds = evb
-                                 , ic_insol = insoluble, ic_info = info })
+                                 , ic_insol = ic_insoluble, ic_info = info })
   | BracketSkol <- info
-  , not insoluble -- For Template Haskell brackets report only
-  = return ()     -- definite errors. The whole thing will be re-checked
-                  -- later when we plug it in, and meanwhile there may
-                  -- certainly be un-satisfied constraints
+  , not ic_insoluble -- For Template Haskell brackets report only
+  = return ()        -- definite errors. The whole thing will be re-checked
+                     -- later when we plug it in, and meanwhile there may
+                     -- certainly be un-satisfied constraints
 
   | otherwise
   = reportWanteds ctxt' wanted
@@ -185,8 +185,12 @@ 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 }
@@ -205,7 +209,8 @@ reportWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics }
 
 reportFlats :: ReportErrCtxt -> Cts -> TcM ()
 reportFlats ctxt flats    -- Here 'flats' includes insolble goals
-  = tryReporters 
+  = traceTc "reportFlats" (ppr flats) >>
+    tryReporters 
       [ -- First deal with things that are utterly wrong
         -- Like Int ~ Bool (incl nullary TyCons)
         -- or  Int ~ t a   (AppTy on one side)
@@ -215,13 +220,12 @@ reportFlats ctxt flats    -- Here 'flats' includes insolble goals
         -- Report equalities of form (a~ty).  They are usually
         -- skolem-equalities, and they cause confusing knock-on 
         -- effects in other errors; see test T4093b.
-      , ("Skolem equalities",    skolem_eq,   mkUniReporter mkEqErr1)
-      , ("Unambiguous",          unambiguous, reportFlatErrs) ]
-      reportAmbigErrs
+      , ("Skolem equalities",    skolem_eq,   mkUniReporter mkEqErr1) ]
+--      , ("Unambiguous",          unambiguous, reportFlatErrs) ]
+      reportFlatErrs
       ctxt (bagToList flats)
   where
-    utterly_wrong, skolem_eq, unambiguous :: Ct -> PredTree -> Bool
-
+    utterly_wrong, skolem_eq :: Ct -> PredTree -> Bool
     utterly_wrong _ (EqPred ty1 ty2) = isRigid ty1 && isRigid ty2 
     utterly_wrong _ _ = False
 
@@ -230,6 +234,8 @@ reportFlats ctxt flats    -- Here 'flats' includes insolble goals
     skolem_eq _ (EqPred ty1 ty2) = isRigidOrSkol ty1 && isRigidOrSkol ty2 
     skolem_eq _ _ = False
 
+{-
+    unambiguous :: Ct -> PredTree -> Bool
     unambiguous ct pred 
       | not (any isAmbiguousTyVar (varSetElems (tyVarsOfCt ct)))
       = True
@@ -237,6 +243,7 @@ reportFlats ctxt flats    -- Here 'flats' includes insolble goals
       = case pred of
           EqPred ty1 ty2 -> isNothing (isTyFun_maybe ty1) && isNothing (isTyFun_maybe ty2)
           _              -> False
+-}
 
 ---------------
 isRigid, isRigidOrSkol :: Type -> Bool
@@ -256,13 +263,14 @@ 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 
@@ -271,10 +279,12 @@ reportFlatErrs :: Reporter
 reportFlatErrs
   = tryReporters
       [ ("Equalities", is_equality, mkGroupReporter mkEqErr) ]
-      (\ctxt cts -> do { let (dicts, ips, irreds) = go cts [] [] []
-                       ; mkGroupReporter mkIPErr    ctxt ips   
-                       ; mkGroupReporter mkIrredErr ctxt irreds
-                       ; mkGroupReporter mkDictErr  ctxt dicts })
+      (\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 })
   where
     is_equality _ (EqPred {}) = True
     is_equality _ _           = False
@@ -282,7 +292,8 @@ reportFlatErrs
     go [] dicts ips irreds
       = (dicts, ips, irreds)
     go (ct:cts) dicts ips irreds
-      | isIPPred (ctPred ct) = go cts dicts (ct:ips) irreds
+      | isIPPred (ctPred ct) 
+      = go cts dicts (ct:ips) irreds
       | otherwise
       = case classifyPredType (ctPred ct) of
           ClassPred {}  -> go cts (ct:dicts) ips irreds
@@ -376,6 +387,7 @@ tryReporters reporters deflt ctxt cts
                          -- Carry on with the rest, because we must make
                          -- deferred bindings for them if we have 
                          -- -fdefer-type-errors
+                         -- But suppress their error messages
       where
        (yeses, nos) = partition keep_me cts
        keep_me ct = pred ct (classifyPredType (ctPred ct))
@@ -593,13 +605,8 @@ mkTyVarEqErr :: ReportErrCtxt -> SDoc -> Ct -> Bool -> TcTyVar -> TcType -> TcM
 -- tv1 and ty2 are already tidied
 mkTyVarEqErr ctxt extra ct oriented tv1 ty2
   -- Occurs check
-  | isNothing (occurCheckExpand tv1 ty2)
-  = let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2
-                           (sep [ppr ty1, char '~', ppr ty2])
-    in mkErrorMsg ctxt ct (occCheckMsg $$ extra)
-
-  |  isSkolemTyVar tv1 	  -- ty2 won't be a meta-tyvar, or else the thing would
-     		   	  -- be oriented the other way round; see TcCanonical.reOrient
+  |  isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
+     		   	     -- be oriented the other way round; see TcCanonical.reOrient
   || isSigTyVar tv1 && not (isTyVarTy ty2)
   = mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
                              , extraTyVarInfo ctxt ty1 ty2
@@ -610,6 +617,11 @@ mkTyVarEqErr ctxt extra ct oriented tv1 ty2
   | not (k2 `tcIsSubKind` k1)   	 -- Kind error
   = mkErrorMsg ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra)
 
+  | isNothing (occurCheckExpand tv1 ty2)
+  = let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2
+                           (sep [ppr ty1, char '~', ppr ty2])
+    in mkErrorMsg ctxt ct (occCheckMsg $$ extra)
+
   -- Check for skolem escape
   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
   , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
@@ -674,6 +686,17 @@ mkEqInfoMsg ctxt ct ty1 ty2
                 <+> ptext (sLit "is a type function, and may not be injective")
               | otherwise = empty
 
+isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
+-- See Note [Reporting occurs-check errors]
+isUserSkolem ctxt tv
+  = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
+  where
+    is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
+      = tv `elem` sks && is_user_skol_info skol_info
+
+    is_user_skol_info (InferSkol {}) = False
+    is_user_skol_info _ = True
+
 misMatchOrCND :: ReportErrCtxt -> Ct -> Bool -> TcType -> TcType -> SDoc
 -- If oriented then ty1 is expected, ty2 is actual
 misMatchOrCND ctxt ct oriented ty1 ty2
@@ -759,6 +782,24 @@ mkExpectedActualMsg exp_ty act_ty
          , text "  Actual type:" <+> ppr act_ty ]
 \end{code}
 
+Note [Reporting occurs-check errors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
+type signature, then the best thing is to report that we can't unify
+a with [a], because a is a skolem variable.  That avoids the confusing
+"occur-check" error message.
+
+But nowadays when inferring the type of a function with no type signature,
+even if there are errors inside, we still generalise its signature and
+carry on. For example
+   f x = x:x
+Here we will infer somethiing like
+   f :: forall a. a -> [a]
+with a suspended error of (a ~ [a]).  So 'a' is now a skolem, but not
+one bound by the programmer!  Here we really should report an occurs check.
+
+So isUserSkolem distinguishes the two.
+
 Note [Non-injective type functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's very confusing to get a message like
@@ -814,6 +855,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
   | null matches  -- No matches but perhaps several unifiers
   = do { (ctxt, is_ambig, ambig_msg) <- mkAmbigMsg ctxt [ct]
        ; (ctxt, binds_msg) <- relevantBindings ctxt ct
+       ; traceTc "mk_dict_err" (ppr ct $$ ppr is_ambig $$ ambig_msg)
        ; return (ctxt, cannot_resolve_msg is_ambig binds_msg ambig_msg) }
 
   | not safe_haskell   -- Some matches => overlap errors
@@ -832,8 +874,8 @@ 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 && (not (null unifiers) || not (null givens))
-               then ambig_msg $$ binds_msg $$ potential_msg
+             , if (has_ambig_tvs && all_tyvars)
+               then vcat [ ambig_msg, binds_msg, potential_msg ]
                else empty
              , show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes) ]
 
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index c1221efd4d..55388b024e 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -29,7 +29,7 @@ module TcHsType (
 	tcLHsType, tcCheckLHsType, 
         tcHsContext, tcInferApps, tcHsArgTys,
 
-        ExpKind(..), ekConstraint, expArgKind, checkExpectedKind,
+        ExpKind(..), ekConstraint, expArgKind, 
         kindGeneralize,
 
 		-- Sort-checking kinds
@@ -1281,59 +1281,60 @@ checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
 -- checks that the actual kind act_kind is compatible
 --      with the expected kind exp_kind
 -- 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)
-    (_errs, mb_r) <- tryTc (unifyKind act_kind exp_kind)
-    case mb_r of
-        Just _  -> return ()  -- Unification succeeded
-        Nothing -> do
-
-        -- So there's definitely an error
-        -- Now to find out what sort
-           exp_kind <- zonkTcKind exp_kind
-           act_kind <- zonkTcKind act_kind
-
-           env0 <- tcInitTidyEnv
-           let (exp_as, _) = splitKindFunTys exp_kind
-               (act_as, _) = splitKindFunTys act_kind
-               n_exp_as  = length exp_as
-               n_act_as  = length act_as
-               n_diff_as = n_act_as - n_exp_as
-
-               (env1, tidy_exp_kind) = tidyOpenKind env0 exp_kind
-               (env2, tidy_act_kind) = tidyOpenKind env1 act_kind
-
-               err | n_exp_as < n_act_as     -- E.g. [Maybe]
-                   = ptext (sLit "Expecting") <+>
-                     speakN n_diff_as <+> ptext (sLit "more argument") <>
-                     (if n_diff_as > 1 then char 's' else empty) <+>
-                     ptext (sLit "to") <+> quotes (ppr ty)
-
-                     -- Now n_exp_as >= n_act_as. In the next two cases,
-                     -- n_exp_as == 0, and hence so is n_act_as
-                   | isConstraintKind tidy_act_kind
-                   = text "Predicate" <+> quotes (ppr ty) <+> text "used as a type"
-                   
-                   | isConstraintKind tidy_exp_kind
-                   = text "Type of kind" <+> ppr tidy_act_kind <+> text "used as a constraint"
-                   
-                   | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
-                   = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
-                       <+> ptext (sLit "is unlifted")
-
-                   | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
-                   = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
-                       <+> ptext (sLit "is lifted")
-
-                   | otherwise               -- E.g. Monad [Int]
-                   = ptext (sLit "Kind mis-match") $$ more_info
-
-               more_info = sep [ ek_ctxt <+> ptext (sLit "kind") 
-                                    <+> quotes (pprKind tidy_exp_kind) <> comma,
-                                 ptext (sLit "but") <+> quotes (ppr ty) <+>
-                                     ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
-
-           failWithTcM (env2, err)
+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)
+
+         -- Kind unification only generates definite errors
+      ; if isEmptyWC lie 
+        then return () -- Unification succeeded
+        else do
+
+      {  -- So there's an error
+         -- Now to find out what sort
+        exp_kind <- zonkTcKind exp_kind
+      ; act_kind <- zonkTcKind act_kind
+      ; env0 <- tcInitTidyEnv
+      ; let (exp_as, _) = splitKindFunTys exp_kind
+            (act_as, _) = splitKindFunTys act_kind
+            n_exp_as  = length exp_as
+            n_act_as  = length act_as
+            n_diff_as = n_act_as - n_exp_as
+
+            (env1, tidy_exp_kind) = tidyOpenKind env0 exp_kind
+            (env2, tidy_act_kind) = tidyOpenKind env1 act_kind
+
+            err | n_exp_as < n_act_as     -- E.g. [Maybe]
+                = ptext (sLit "Expecting") <+>
+                  speakN n_diff_as <+> ptext (sLit "more argument") <>
+                  (if n_diff_as > 1 then char 's' else empty) <+>
+                  ptext (sLit "to") <+> quotes (ppr ty)
+
+                  -- Now n_exp_as >= n_act_as. In the next two cases,
+                  -- n_exp_as == 0, and hence so is n_act_as
+                | isConstraintKind tidy_act_kind
+                = text "Predicate" <+> quotes (ppr ty) <+> text "used as a type"
+                
+                | isConstraintKind tidy_exp_kind
+                = text "Type of kind" <+> ppr tidy_act_kind <+> text "used as a constraint"
+                
+                | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
+                = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
+                    <+> ptext (sLit "is unlifted")
+
+                | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
+                = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
+                    <+> ptext (sLit "is lifted")
+
+                | otherwise               -- E.g. Monad [Int]
+                = ptext (sLit "Kind mis-match") $$ more_info
+
+            more_info = sep [ ek_ctxt <+> ptext (sLit "kind") 
+                                 <+> quotes (pprKind tidy_exp_kind) <> comma,
+                              ptext (sLit "but") <+> quotes (ppr ty) <+>
+                                  ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
+
+      ; failWithTcM (env2, err) } }
 \end{code}
 
 %************************************************************************
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index 9d83aed709..2e62cd78a8 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -573,7 +573,9 @@ tcFamInstDecl1 :: TyCon -> FamInstDecl Name -> TcM FamInst
 tcFamInstDecl1 fam_tc decl@(FamInstDecl { fid_tycon = fam_tc_name
                                         , fid_defn = TySynonym {} })
   = do { -- (0) Check it's an open type family
-         checkTc (isOpenSynFamilyTyCon fam_tc)
+         checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
+       ; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
+       ; checkTc (isOpenSynFamilyTyCon fam_tc)
                  (notOpenFamily fam_tc)
 
          -- (1) do the work of verifying the synonym
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 8c7582eedc..0a1dff2feb 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -457,6 +457,7 @@ trySpontaneousEqOneWay :: CtLoc -> CtEvidence
 -- tv is a MetaTyVar, not untouchable
 trySpontaneousEqOneWay d gw tv xi
   | not (isSigTyVar tv) || isTyVarTy xi
+  , typeKind xi `tcIsSubKind` tyVarKind tv
   = solveWithIdentity d gw tv xi
   | otherwise -- Still can't solve, sig tyvar and non-variable rhs
   = return SPCantSolve
@@ -467,10 +468,12 @@ trySpontaneousEqTwoWay :: CtLoc -> CtEvidence
 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
 
 trySpontaneousEqTwoWay d gw tv1 tv2
-  = do { let k1_sub_k2 = k1 `tcIsSubKind` k2
-       ; if k1_sub_k2 && nicer_to_update_tv2
-         then solveWithIdentity d gw tv2 (mkTyVarTy tv1)
-         else solveWithIdentity d gw tv1 (mkTyVarTy tv2) }
+  | k1 `tcIsSubKind` k2 && nicer_to_update_tv2
+  = solveWithIdentity d gw tv2 (mkTyVarTy tv1)
+  | k2 `tcIsSubKind` k1
+  = solveWithIdentity d gw tv1 (mkTyVarTy tv2)
+  | otherwise
+  = return SPCantSolve
   where
     k1 = tyVarKind tv1
     k2 = tyVarKind tv2
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 1e93ec4eec..a409b11fe7 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -1129,12 +1129,12 @@ instance Outputable Implication where
               , ic_wanted = wanted
               , ic_binds = binds, ic_info = info })
    = ptext (sLit "Implic") <+> braces 
-     (sep [ ptext (sLit "Untouchables = ") <+> ppr untch
-          , ptext (sLit "Skolems = ") <+> ppr skols
-          , ptext (sLit "Flatten-skolems = ") <+> ppr fsks
-          , ptext (sLit "Given = ") <+> pprEvVars given
-          , ptext (sLit "Wanted = ") <+> ppr wanted
-          , ptext (sLit "Binds = ") <+> ppr binds
+     (sep [ ptext (sLit "Untouchables =") <+> ppr untch
+          , ptext (sLit "Skolems =") <+> ppr skols
+          , ptext (sLit "Flatten-skolems =") <+> ppr fsks
+          , ptext (sLit "Given =") <+> pprEvVars given
+          , ptext (sLit "Wanted =") <+> ppr wanted
+          , ptext (sLit "Binds =") <+> ppr binds
           , pprSkolInfo info ])
 \end{code}
 
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index e34c220598..a93f808c4f 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -19,7 +19,7 @@ module TcUnify (
   checkConstraints, newImplication, 
 
   -- Various unifications
-  unifyType, unifyTypeList, unifyTheta, unifyKind, unifyKindEq,
+  unifyType, unifyTypeList, unifyTheta, unifyKind, 
 
   --------------------------------
   -- Holes
@@ -59,7 +59,7 @@ import VarEnv
 import ErrUtils
 import DynFlags
 import BasicTypes
-import Maybes ( allMaybes )
+import Maybes ( allMaybes, isJust )
 import Util
 import Outputable
 import FastString
@@ -516,6 +516,10 @@ 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
@@ -810,9 +814,12 @@ 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
-       ; sub_kind <- addErrCtxtM ctxt $ unifyKind k1 k2
+       ; mb_sub_kind <- addErrCtxtM ctxt $ unifyKind k1 k2
+       ; case mb_sub_kind of {
+           Nothing -> unSwap swapped (uType_defer origin) (mkTyVarTy tv1) ty2 ;
+           Just sub_kind -> 
 
-       ; case (sub_kind, details1, details2) of
+         case (sub_kind, details1, details2) of
            -- k1 < k2, so update tv2
            (LT, _, MetaTv { mtv_ref = ref2 }) -> updateMeta tv2 ref2 ty1
 
@@ -829,7 +836,7 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
 
 	   -- Can't do it in-place, so defer
 	   -- This happens for skolems of all sorts
-           (_, _, _) -> unSwap swapped (uType_defer origin) ty1 ty2 } 
+           (_, _, _) -> unSwap swapped (uType_defer origin) ty1 ty2 } }
   where
     k1       = tyVarKind tv1
     k2       = tyVarKind tv2
@@ -876,8 +883,9 @@ checkTauTvUpdate tv ty
                   unifyKind (tyVarKind tv) (typeKind ty')
 
        ; case sub_k of
-           LT -> return Nothing
-           _  -> return (ok ty') }
+           Nothing -> return Nothing
+           Just LT -> return Nothing
+           _       -> return (ok ty') }
   where 
     ok :: TcType -> Maybe TcType 
     -- Checks that tv does not occur in the arg type
@@ -1080,47 +1088,47 @@ matchExpectedFunKind _                         = return Nothing
 -----------------  
 unifyKind :: TcKind           -- k1 (actual)
           -> TcKind           -- k2 (expected)
-          -> TcM Ordering     -- Returns the relation between the kinds
-                              -- LT <=> k1 is a sub-kind of k2
+          -> 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
 -- but recurses into the simpler unifyKindEq for any sub-terms
 -- The sub-kinding stuff only applies at top level
 
-unifyKind (TyVarTy kv1) k2 = uKVar False unifyKind EQ kv1 k2
-unifyKind k1 (TyVarTy kv2) = uKVar True  unifyKind EQ kv2 k1
+unifyKind (TyVarTy kv1) k2 = uKVar NotSwapped unifyKind kv1 k2
+unifyKind k1 (TyVarTy kv2) = uKVar IsSwapped  unifyKind 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'
 
 unifyKind k1@(TyConApp kc1 []) k2@(TyConApp kc2 [])
-  | kc1 == kc2               = return EQ
-  | kc1 `tcIsSubKindCon` kc2 = return LT
-  | kc2 `tcIsSubKindCon` kc1 = return GT
+  | kc1 == kc2               = return (Just EQ)
+  | kc1 `tcIsSubKindCon` kc2 = return (Just LT)
+  | kc2 `tcIsSubKindCon` kc1 = return (Just GT)
   | otherwise                = unifyKindMisMatch k1 k2
 
-unifyKind k1 k2 = do { unifyKindEq k1 k2; return EQ }
+unifyKind k1 k2 = unifyKindEq k1 k2
   -- In all other cases, let unifyKindEq do the work
 
-uKVar :: Bool -> (TcKind -> TcKind -> TcM a) -> a
-      -> MetaKindVar -> TcKind -> TcM a
-uKVar isFlipped unify_kind eq_res kv1 k2
+uKVar :: SwapFlag -> (TcKind -> TcKind -> TcM (Maybe Ordering))
+      -> MetaKindVar -> TcKind -> TcM (Maybe Ordering)
+uKVar swapped unify_kind kv1 k2
   | isTcTyVar kv1, isMetaTyVar kv1       -- See Note [Unifying kind variables]
   = do  { mb_k1 <- readMetaTyVar kv1
         ; case mb_k1 of
-            Flexi -> do { uUnboundKVar kv1 k2; return eq_res }
-            Indirect k1 -> if isFlipped then unify_kind k2 k1
-                                        else unify_kind k1 k2 }
+            Flexi -> uUnboundKVar kv1 k2
+            Indirect k1 -> unSwap swapped unify_kind k1 k2 }
   | TyVarTy kv2 <- k2, kv1 == kv2 
-  = return eq_res
+  = return (Just EQ)
 
   | TyVarTy kv2 <- k2, isTcTyVar kv2, isMetaTyVar kv2
-  = uKVar (not isFlipped) unify_kind eq_res kv2 (TyVarTy kv1)
+  = uKVar (flipSwap swapped) unify_kind kv2 (TyVarTy kv1)
 
-  | otherwise = if isFlipped 
-                then unifyKindMisMatch k2 (TyVarTy kv1)
-                else unifyKindMisMatch (TyVarTy kv1) k2
+  | otherwise 
+  = unSwap swapped unifyKindMisMatch (TyVarTy kv1) k2
 
 {- Note [Unifying kind variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1138,49 +1146,49 @@ Hence the isTcTyVar tests before using isMetaTyVar.
 -}
 
 ---------------------------
-unifyKindEq :: TcKind -> TcKind -> TcM ()
-unifyKindEq (TyVarTy kv1) k2 = uKVar False unifyKindEq () kv1 k2
-unifyKindEq k1 (TyVarTy kv2) = uKVar True  unifyKindEq () kv2 k1
+unifyKindEq :: TcKind -> TcKind -> TcM (Maybe Ordering)
+-- Unify two kinds looking for equality not sub-kinding
+-- So it returns Nothing or (Just EQ) only
+unifyKindEq (TyVarTy kv1) k2 = uKVar NotSwapped unifyKindEq kv1 k2
+unifyKindEq k1 (TyVarTy kv2) = uKVar IsSwapped  unifyKindEq kv2 k1
 
 unifyKindEq (FunTy a1 r1) (FunTy a2 r2)
-  = do { unifyKindEq a1 a2; unifyKindEq r1 r2 }
+  = do { mb1 <- unifyKindEq a1 a2; mb2 <- unifyKindEq r1 r2
+       ; return (if isJust mb1 && isJust mb2 then Just EQ else Nothing) }
   
 unifyKindEq (TyConApp kc1 k1s) (TyConApp kc2 k2s)
   | kc1 == kc2
   = ASSERT (length k1s == length k2s)
        -- Should succeed since the kind constructors are the same, 
        -- and the kinds are sort-checked, thus fully applied
-    zipWithM_ unifyKindEq k1s k2s
+    do { mb_eqs <- zipWithM unifyKindEq k1s k2s
+       ; return (if all isJust mb_eqs 
+                 then Just EQ 
+                 else Nothing) }
 
 unifyKindEq k1 k2 = unifyKindMisMatch k1 k2
 
 ----------------
-uUnboundKVar :: MetaKindVar -> TcKind -> TcM ()
+uUnboundKVar :: MetaKindVar -> TcKind -> TcM (Maybe Ordering)
 uUnboundKVar kv1 k2@(TyVarTy kv2)
-  | kv1 == kv2 = return ()
+  | kv1 == kv2 = return (Just EQ)
   | isTcTyVar kv2, isMetaTyVar kv2   -- Distinct kind variables
   = do  { mb_k2 <- readMetaTyVar kv2
         ; case mb_k2 of
             Indirect k2 -> uUnboundKVar kv1 k2
-            Flexi -> writeMetaTyVar kv1 k2 }
-  | otherwise = writeMetaTyVar kv1 k2
+            Flexi       -> do { writeMetaTyVar kv1 k2; return (Just EQ) } }
+  | otherwise 
+  = do { writeMetaTyVar kv1 k2; return (Just EQ) }
 
 uUnboundKVar kv1 non_var_k2
   = do  { k2' <- zonkTcKind non_var_k2
         ; let k2'' = defaultKind k2'
                 -- MetaKindVars must be bound only to simple kinds
-        ; kindUnifCheck kv1 k2''
-        ; writeMetaTyVar kv1 k2'' }
 
-----------------
-kindUnifCheck :: TyVar -> Type -> TcM ()
-kindUnifCheck kv1 k2   -- k2 is zonked
-  | elemVarSet kv1 (tyVarsOfType k2)
-  = failWithTc (kindOccurCheckErr kv1 k2)
-  | isSigTyVar kv1
-  = failWithTc (kindSigVarErr kv1 k2)
-  | otherwise
-  = return ()
+        ; if not (elemVarSet kv1 (tyVarsOfType k2''))
+          && not (isSigTyVar kv1)
+          then do { writeMetaTyVar kv1 k2''; return (Just EQ) }
+          else return Nothing }
 
 mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc)
 mkKindErrorCtxt ty1 ty2 k1 k2 env0
@@ -1197,8 +1205,12 @@ mkKindErrorCtxt ty1 ty2 k1 k2 env0
                        , nest 2 (vcat [ ppr ty1 <+> dcolon <+> ppr k1
                                       , ppr ty2 <+> dcolon <+> ppr k2 ]) ])
 
-unifyKindMisMatch :: TcKind -> TcKind -> TcM a
-unifyKindMisMatch ki1 ki2 = do
+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"))
@@ -1207,6 +1219,7 @@ unifyKindMisMatch ki1 ki2 = do
                       quotes (ppr ki2')])
     failWithTc msg
 
+
 ----------------
 kindOccurCheckErr :: Var -> Type -> SDoc
 kindOccurCheckErr tyvar ty
@@ -1217,4 +1230,5 @@ 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}
diff --git a/compiler/typecheck/TcUnify.lhs-boot b/compiler/typecheck/TcUnify.lhs-boot
index 4d07229963..aa93536705 100644
--- a/compiler/typecheck/TcUnify.lhs-boot
+++ b/compiler/typecheck/TcUnify.lhs-boot
@@ -1,6 +1,6 @@
 \begin{code}
 module TcUnify where
-import TcType     ( TcTauType, TcKind, Type, Kind )
+import TcType     ( TcTauType, Type, Kind )
 import VarEnv     ( TidyEnv )
 import TcRnTypes  ( TcM )
 import TcEvidence ( TcCoercion )
@@ -10,6 +10,5 @@ import Outputable ( SDoc )
 --              TcUnify and Inst
 
 unifyType :: TcTauType -> TcTauType -> TcM TcCoercion
-unifyKindEq :: TcKind -> TcKind -> TcM ()
 mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc)
 \end{code}