Merge branch 'master' of darcs.haskell.org:/home/darcs/ghc

Conflicts:
	compiler/coreSyn/CoreLint.lhs

32 files changed, 787 insertions, 638 deletions

diff --git a/compiler/basicTypes/DataCon.lhs b/compiler/basicTypes/DataCon.lhs
index a504c5bbe7..6b918dbc08 100644
--- a/compiler/basicTypes/DataCon.lhs
+++ b/compiler/basicTypes/DataCon.lhs
@@ -45,8 +45,8 @@ module DataCon (
         deepSplitProductType_maybe,
 
         -- ** Promotion related functions
-        promoteType, isPromotableType, isPromotableTyCon,
-        buildPromotedTyCon, buildPromotedDataCon,
+        isPromotableTyCon, promoteTyCon, 
+        promoteDataCon, promoteDataCon_maybe
     ) where
 
 #include "HsVersions.h"
@@ -386,9 +386,11 @@ data DataCon
 	-- An entirely separate wrapper function is built in TcTyDecls
 	dcIds :: DataConIds,
 
-	dcInfix :: Bool		-- True <=> declared infix
+	dcInfix :: Bool,	-- True <=> declared infix
 				-- Used for Template Haskell and 'deriving' only
 				-- The actual fixity is stored elsewhere
+
+        dcPromoted :: Maybe TyCon    -- The promoted TyCon if this DataCon is promotable
   }
   deriving Data.Typeable.Typeable
 
@@ -519,10 +521,7 @@ mkDataCon name declared_infix
 -- so the error is detected properly... it's just that asaertions here
 -- are a little dodgy.
 
-  = -- ASSERT( not (any isEqPred theta) )
-	-- We don't currently allow any equality predicates on
-	-- a data constructor (apart from the GADT ones in eq_spec)
-    con
+  = con
   where
     is_vanilla = null ex_tvs && null eq_spec && null theta
     con = MkData {dcName = name, dcUnique = nameUnique name, 
@@ -537,7 +536,8 @@ mkDataCon name declared_infix
 		  dcStrictMarks = arg_stricts, 
 		  dcRepStrictness = rep_arg_stricts,
 		  dcFields = fields, dcTag = tag, dcRepType = ty,
-		  dcIds = ids }
+		  dcIds = ids,
+                  dcPromoted = mb_promoted }
 
 	-- Strictness marks for source-args
 	--	*after unboxing choices*, 
@@ -559,6 +559,16 @@ mkDataCon name declared_infix
 	  mkFunTys rep_arg_tys $
 	  mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
 
+    mb_promoted 
+      | is_vanilla   -- No existentials or context
+      , all (isLiftedTypeKind . tyVarKind) univ_tvs
+      , all isPromotableType orig_arg_tys
+      = Just (mkPromotedDataCon con name (getUnique name) prom_kind arity)
+      | otherwise 
+      = Nothing          
+    prom_kind = promoteType (dataConUserType con)
+    arity     = dataConSourceArity con
+
 eqSpecPreds :: [(TyVar,Type)] -> ThetaType
 eqSpecPreds spec = [ mkEqPred (mkTyVarTy tv) ty | (tv,ty) <- spec ]
 
@@ -978,24 +988,22 @@ computeRep stricts tys
 %*                                                                      *
 %************************************************************************
 
-These two 'buildPromoted..' functions are here because
+These two 'promoted..' functions are here because
  * They belong together
- * 'buildPromotedTyCon' is used by promoteType
- * 'buildPromotedTyCon' depends on DataCon stuff
+ * 'promoteTyCon'  is used by promoteType
+ * 'prmoteDataCon' depends on DataCon stuff
 
 \begin{code}
-buildPromotedTyCon :: TyCon -> TyCon
-buildPromotedTyCon tc
-  = mkPromotedTyCon tc (promoteKind (tyConKind tc))
+promoteDataCon :: DataCon -> TyCon
+promoteDataCon (MkData { dcPromoted = Just tc }) = tc
+promoteDataCon dc = pprPanic "promoteDataCon" (ppr dc)
+
+promoteDataCon_maybe :: DataCon -> Maybe TyCon
+promoteDataCon_maybe (MkData { dcPromoted = mb_tc }) = mb_tc
 
-buildPromotedDataCon :: DataCon -> TyCon
-buildPromotedDataCon dc 
-  = ASSERT ( isPromotableType ty )
-    mkPromotedDataCon dc (getName dc) (getUnique dc) kind arity
-  where 
-    ty    = dataConUserType dc
-    kind  = promoteType ty
-    arity = dataConSourceArity dc
+promoteTyCon :: TyCon -> TyCon
+promoteTyCon tc
+  = mkPromotedTyCon tc (promoteKind (tyConKind tc))
 \end{code}
 
 Note [Promoting a Type to a Kind]
@@ -1017,16 +1025,11 @@ The transformation from type to kind is done by promoteType
 
 \begin{code}
 isPromotableType :: Type -> Bool
-isPromotableType ty
-  = all (isLiftedTypeKind . tyVarKind) tvs
-    && go rho
-  where
-    (tvs, rho) = splitForAllTys ty
-    go (TyConApp tc tys) | Just n <- isPromotableTyCon tc
-                         = tys `lengthIs` n && all go tys
-    go (FunTy arg res)   = go arg && go res
-    go (TyVarTy tvar)    = tvar `elem` tvs
-    go _                 = False
+isPromotableType (TyConApp tc tys) 
+  | Just n <- isPromotableTyCon tc = tys `lengthIs` n && all isPromotableType tys
+isPromotableType (FunTy arg res)   = isPromotableType arg && isPromotableType res
+isPromotableType (TyVarTy {})      = True
+isPromotableType _                 = False
 
 -- If tc's kind is [ *^n -> * ] returns [ Just n ], else returns [ Nothing ]
 isPromotableTyCon :: TyCon -> Maybe Int
@@ -1048,7 +1051,7 @@ promoteType ty
     kvs = [ mkKindVar (tyVarName tv) superKind | tv <- tvs ]
     env = zipVarEnv tvs kvs
 
-    go (TyConApp tc tys) = mkTyConApp (buildPromotedTyCon tc) (map go tys)
+    go (TyConApp tc tys) = mkTyConApp (promoteTyCon tc) (map go tys)
     go (FunTy arg res)   = mkArrowKind (go arg) (go res)
     go (TyVarTy tv)      | Just kv <- lookupVarEnv env tv 
                          = TyVarTy kv
diff --git a/compiler/basicTypes/OccName.lhs b/compiler/basicTypes/OccName.lhs
index 6c70dc597a..afdde7c996 100644
--- a/compiler/basicTypes/OccName.lhs
+++ b/compiler/basicTypes/OccName.lhs
@@ -758,29 +758,54 @@ There's a wrinkle for operators.  Consider '>>='.  We can't use '>>=1'
 because that isn't a single lexeme.  So we encode it to 'lle' and *then*
 tack on the '1', if necessary.
 
+Note [TidyOccEnv]
+~~~~~~~~~~~~~~~~~
+type TidyOccEnv = UniqFM Int
+
+* Domain = The OccName's FastString. These FastStrings are "taken";
+           make sure that we don't re-use
+
+* Int, n = A plausible starting point for new guesses
+           There is no guarantee that "FSn" is available; 
+           you must look that up in the TidyOccEnv.  But
+           it's a good place to start looking.
+
+* When looking for a renaming for "foo2" we strip off the "2" and start
+  with "foo".  Otherwise if we tidy twice we get silly names like foo23.
+
 \begin{code}
-type TidyOccEnv = OccEnv Int	-- The in-scope OccNames
-	-- Range gives a plausible starting point for new guesses
+type TidyOccEnv = UniqFM Int	-- The in-scope OccNames
+  -- See Note [TidyOccEnv]
 
 emptyTidyOccEnv :: TidyOccEnv
-emptyTidyOccEnv = emptyOccEnv
+emptyTidyOccEnv = emptyUFM
 
 initTidyOccEnv :: [OccName] -> TidyOccEnv	-- Initialise with names to avoid!
-initTidyOccEnv = foldl (\env occ -> extendOccEnv env occ 1) emptyTidyOccEnv
+initTidyOccEnv = foldl add emptyUFM
+  where
+    add env (OccName _ fs) = addToUFM env fs 1
 
 tidyOccName :: TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
-
-tidyOccName in_scope occ@(OccName occ_sp fs)
-  = case lookupOccEnv in_scope occ of
-	Nothing -> 	-- Not already used: make it used
-		   (extendOccEnv in_scope occ 1, occ)
-
-	Just n  -> 	-- Already used: make a new guess, 
-			-- change the guess base, and try again
-		   tidyOccName  (extendOccEnv in_scope occ (n+1))
-                                (mkOccName occ_sp (base_occ ++ show n))
+tidyOccName env occ@(OccName occ_sp fs)
+  = case lookupUFM env fs of
+	Just n  -> find n
+	Nothing -> (addToUFM env fs 1, occ)
   where
-    base_occ = reverse (dropWhile isDigit (reverse (unpackFS fs)))
+    base :: String  -- Drop trailing digits (see Note [TidyOccEnv])
+    base = reverse (dropWhile isDigit (reverse (unpackFS fs)))
+ 
+    find n 
+      = case lookupUFM env new_fs of
+          Just n' -> find (n1 `max` n')
+                     -- The max ensures that n increases, avoiding loops
+          Nothing -> (addToUFM (addToUFM env fs n1) new_fs n1,
+                      OccName occ_sp new_fs)
+                     -- We update only the beginning and end of the
+                     -- chain that find explores; it's a little harder to
+                     -- update the middle and there's no real need.
+       where
+         n1 = n+1
+         new_fs = mkFastString (base ++ show n)
 \end{code}
 
 %************************************************************************
diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index 144e25b4c8..afd7e05913 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -886,7 +886,8 @@ lintCoercion co@(AxiomInstCo (CoAxiom { co_ax_tvs = ktvs
            ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
                   -- Using subst_l is ok, because subst_l and subst_r
                   -- must agree on kind equalities
-           ; unless (k `isSubKind` ktv_kind) (bad_ax (ptext (sLit "check_ki2") $$ ppr k $$ ppr ktv_kind $$ ppr ktv $$ ppr co))
+           ; unless (k `isSubKind` ktv_kind) 
+                    (bad_ax (ptext (sLit "check_ki2") <+> vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] ))
            ; return (Type.extendTvSubst subst_l ktv t1, 
                      Type.extendTvSubst subst_r ktv t2) } 
 \end{code}
diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs
index cad80128b9..33c7a9debb 100644
--- a/compiler/coreSyn/CoreUtils.lhs
+++ b/compiler/coreSyn/CoreUtils.lhs
@@ -675,7 +675,7 @@ exprIsWorkFree e = go 0 e
                                               [ go n rhs | (_,_,rhs) <- alts ]
          -- See Note [Case expressions are work-free]
     go _ (Let {})                     = False
-    go n (Var v)                      = n==0 || n < idArity v
+    go n (Var v)                      = isCheapApp v n
     go n (Tick t e) | tickishCounts t = False
                     | otherwise       = go n e
     go n (Lam x e)  | isRuntimeVar x = n==0 || go (n-1) e
@@ -740,7 +740,6 @@ exprIsCheap = exprIsCheap' isCheapApp
 exprIsExpandable :: CoreExpr -> Bool
 exprIsExpandable = exprIsCheap' isExpandableApp -- See Note [CONLIKE pragma] in BasicTypes
 
-type CheapAppFun = Id -> Int -> Bool
 exprIsCheap' :: CheapAppFun -> CoreExpr -> Bool
 exprIsCheap' _        (Lit _)      = True
 exprIsCheap' _        (Type _)    = True
@@ -779,16 +778,26 @@ exprIsCheap' good_app other_expr        -- Applications and variables
     go (App f a) val_args | isRuntimeArg a = go f (a:val_args)
                           | otherwise      = go f val_args
 
-    go (Var _) [] = True        -- Just a type application of a variable
-                                -- (f t1 t2 t3) counts as WHNF
+    go (Var _) [] = True        
+         -- Just a type application of a variable
+         -- (f t1 t2 t3) counts as WHNF
+         -- This case is probably handeld by the good_app case
+         -- below, which should have a case for n=0, but putting
+         -- it here too is belt and braces; and it's such a common
+         -- case that checking for null directly seems like a 
+         -- good plan
+
     go (Var f) args
+       | good_app f (length args) 
+       = go_pap args
+
+       | otherwise
         = case idDetails f of
-                RecSelId {}                  -> go_sel args
-                ClassOpId {}                 -> go_sel args
-                PrimOpId op                  -> go_primop op args
-                _ | good_app f (length args) -> go_pap args
-                  | isBottomingId f          -> True
-                  | otherwise                -> False
+                RecSelId {}         -> go_sel args
+                ClassOpId {}        -> go_sel args
+                PrimOpId op         -> go_primop op args
+                _ | isBottomingId f -> True
+                  | otherwise       -> False
                         -- Application of a function which
                         -- always gives bottom; we treat this as cheap
                         -- because it certainly doesn't need to be shared!
@@ -820,9 +829,17 @@ exprIsCheap' good_app other_expr        -- Applications and variables
                 -- BUT: Take care with (sel d x)!  The (sel d) might be cheap, but
                 --      there's no guarantee that (sel d x) will be too.  Hence (n_val_args == 1)
 
+-------------------------------------
+type CheapAppFun = Id -> Int -> Bool  
+  -- Is an application of this function to n *value* args 
+  -- always cheap, assuming the arguments are cheap?  
+  -- Mainly true of partial applications, data constructors,
+  -- and of course true if the number of args is zero
+
 isCheapApp :: CheapAppFun
 isCheapApp fn n_val_args
-  = isDataConWorkId fn
+  =  isDataConWorkId fn 
+  || n_val_args == 0 
   || n_val_args < idArity fn
 
 isExpandableApp :: CheapAppFun
@@ -833,6 +850,7 @@ isExpandableApp fn n_val_args
   where
   -- See if all the arguments are PredTys (implicit params or classes)
   -- If so we'll regard it as expandable; see Note [Expandable overloadings]
+  -- This incidentally picks up the (n_val_args = 0) case
      go 0 _ = True
      go n_val_args ty
        | Just (_, ty) <- splitForAllTy_maybe ty   = go n_val_args ty
diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index d9e851ae62..405b7687a5 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -265,9 +265,8 @@ repTyDefn tc bndrs opt_tys tv_names
        ; case new_or_data of
            NewType  -> do { con1 <- repC tv_names (head cons)
                           ; repNewtype cxt1 tc bndrs opt_tys con1 derivs1 }
-           DataType -> do { cons1 <- mapM (repC tv_names) cons
-                          ; cons2 <- coreList conQTyConName cons1
-                          ; repData cxt1 tc bndrs opt_tys cons2 derivs1 } }
+           DataType -> do { cons1 <- repList conQTyConName (repC tv_names) cons
+                          ; repData cxt1 tc bndrs opt_tys cons1 derivs1 } }
 
 repTyDefn tc bndrs opt_tys _ (TySynonym { td_synRhs = ty })
   = do { ty1 <- repLTy ty
@@ -305,16 +304,12 @@ mk_extra_tvs tc tvs defn
 -- represent fundeps
 --
 repLFunDeps :: [Located (FunDep Name)] -> DsM (Core [TH.FunDep])
-repLFunDeps fds = do fds' <- mapM repLFunDep fds
-                     fdList <- coreList funDepTyConName fds'
-                     return fdList
+repLFunDeps fds = repList funDepTyConName repLFunDep fds
 
 repLFunDep :: Located (FunDep Name) -> DsM (Core TH.FunDep)
-repLFunDep (L _ (xs, ys)) = do xs' <- mapM lookupBinder xs
-                               ys' <- mapM lookupBinder ys
-                               xs_list <- coreList nameTyConName xs'
-                               ys_list <- coreList nameTyConName ys'
-                               repFunDep xs_list ys_list
+repLFunDep (L _ (xs, ys)) = do xs' <- repList nameTyConName lookupBinder xs
+                               ys' <- repList nameTyConName lookupBinder ys
+                               repFunDep xs' ys'
 
 -- represent family declaration flavours
 --
@@ -364,9 +359,8 @@ repFamInstD (FamInstDecl { fid_tycon = tc_name
        ; let loc = getLoc tc_name
              hs_tvs = HsQTvs { hsq_kvs = kv_names, hsq_tvs = userHsTyVarBndrs loc tv_names }   -- Yuk
        ; addTyClTyVarBinds hs_tvs $ \ bndrs ->
-         do { tys1 <- repLTys tys
-            ; tys2 <- coreList typeQTyConName tys1
-            ; repTyDefn tc bndrs (Just tys2) tv_names defn } }
+         do { tys1 <- repList typeQTyConName repLTy tys
+            ; repTyDefn tc bndrs (Just tys1) tv_names defn } }
 
 repForD :: Located (ForeignDecl Name) -> DsM (SrcSpan, Core TH.DecQ)
 repForD (L loc (ForeignImport name typ _ (CImport cc s mch cis)))
@@ -415,20 +409,29 @@ repFixD (L loc (FixitySig name (Fixity prec dir)))
 
 repRuleD :: LRuleDecl Name -> DsM (SrcSpan, Core TH.DecQ)
 repRuleD (L loc (HsRule n act bndrs lhs _ rhs _))
-  = do { n'     <- coreStringLit $ unpackFS n
-       ; phases <- repPhases act
-       ; bndrs' <- mapM repRuleBndr bndrs >>= coreList ruleBndrQTyConName
-       ; lhs'   <- repLE lhs
-       ; rhs'   <- repLE rhs
-       ; pragma <- repPragRule n' bndrs' lhs' rhs' phases
-       ; return (loc, pragma) }
+  = do { let bndr_names = concatMap ruleBndrNames bndrs
+       ; ss <- mkGenSyms bndr_names
+       ; rule1 <- addBinds ss $
+                  do { bndrs' <- repList ruleBndrQTyConName repRuleBndr bndrs
+                     ; n'   <- coreStringLit $ unpackFS n
+                     ; act' <- repPhases act
+                     ; lhs' <- repLE lhs
+                     ; rhs' <- repLE rhs
+                     ; repPragRule n' bndrs' lhs' rhs' act' }
+       ; rule2 <- wrapGenSyms ss rule1
+       ; return (loc, rule2) }
+
+ruleBndrNames :: RuleBndr Name -> [Name]
+ruleBndrNames (RuleBndr n)      = [unLoc n]
+ruleBndrNames (RuleBndrSig n (HsWB { hswb_kvs = kvs, hswb_tvs = tvs })) 
+  = unLoc n : kvs ++ tvs
 
 repRuleBndr :: RuleBndr Name -> DsM (Core TH.RuleBndrQ)
 repRuleBndr (RuleBndr n)
-  = do { MkC n' <- lookupLOcc n
+  = do { MkC n' <- lookupLBinder n
        ; rep2 ruleVarName [n'] }
 repRuleBndr (RuleBndrSig n (HsWB { hswb_cts = ty }))
-  = do { MkC n'  <- lookupLOcc n
+  = do { MkC n'  <- lookupLBinder n
        ; MkC ty' <- repLTy ty
        ; rep2 typedRuleVarName [n', ty'] }
 
@@ -527,8 +530,7 @@ repBangTy ty= do
 repDerivs :: Maybe [LHsType Name] -> DsM (Core [TH.Name])
 repDerivs Nothing = coreList nameTyConName []
 repDerivs (Just ctxt)
-  = do { strs <- mapM rep_deriv ctxt ;
-	 coreList nameTyConName strs }
+  = repList nameTyConName rep_deriv ctxt
   where
     rep_deriv :: LHsType Name -> DsM (Core TH.Name)
 	-- Deriving clauses must have the simple H98 form
@@ -578,11 +580,10 @@ rep_ty_sig loc (L _ ty) nm
     rep_ty (HsForAllTy Explicit tvs ctxt ty)
       = do { let rep_in_scope_tv tv = do { name <- lookupBinder (hsLTyVarName tv)
                                          ; repTyVarBndrWithKind tv name }
-           ; bndrs1 <- mapM rep_in_scope_tv (hsQTvBndrs tvs)
-           ; bndrs2 <- coreList tyVarBndrTyConName bndrs1
+           ; bndrs1 <- repList tyVarBndrTyConName rep_in_scope_tv (hsQTvBndrs tvs)
            ; ctxt1  <- repLContext ctxt
            ; ty1    <- repLTy ty
-           ; repTForall bndrs2 ctxt1 ty1 }
+           ; repTForall bndrs1 ctxt1 ty1 }
 
     rep_ty ty = repTy ty
 
@@ -653,9 +654,8 @@ addTyVarBinds :: LHsTyVarBndrs Name	                       -- the binders to be
 addTyVarBinds tvs m
   = do { freshNames <- mkGenSyms (hsLKiTyVarNames tvs)
        ; term <- addBinds freshNames $ 
-	    	 do { kbs1 <- mapM mk_tv_bndr (hsQTvBndrs tvs `zip` freshNames)
-                    ; kbs2 <- coreList tyVarBndrTyConName kbs1
-	    	    ; m kbs2 }
+	    	 do { kbs <- repList tyVarBndrTyConName mk_tv_bndr (hsQTvBndrs tvs `zip` freshNames)
+	    	    ; m kbs }
        ; wrapGenSyms freshNames term }
   where
     mk_tv_bndr (tv, (_,v)) = repTyVarBndrWithKind tv (coreVar v)
@@ -677,13 +677,12 @@ addTyClTyVarBinds tvs m
             -- This makes things work for family declarations
 
        ; term <- addBinds freshNames $ 
-	    	 do { kbs1 <- mapM mk_tv_bndr (hsQTvBndrs tvs)
-                    ; kbs2 <- coreList tyVarBndrTyConName kbs1
-	    	    ; m kbs2 }
+	    	 do { kbs <- repList tyVarBndrTyConName mk_tv_bndr (hsQTvBndrs tvs)
+	    	    ; m kbs }
 
        ; wrapGenSyms freshNames term }
   where
-    mk_tv_bndr tv = do { v <- lookupOcc (hsLTyVarName tv)
+    mk_tv_bndr tv = do { v <- lookupBinder (hsLTyVarName tv)
                        ; repTyVarBndrWithKind tv v }
 
 -- Produce kinded binder constructors from the Haskell tyvar binders
@@ -701,10 +700,8 @@ repLContext :: LHsContext Name -> DsM (Core TH.CxtQ)
 repLContext (L _ ctxt) = repContext ctxt
 
 repContext :: HsContext Name -> DsM (Core TH.CxtQ)
-repContext ctxt = do
-	            preds    <- mapM repLPred ctxt
-		    predList <- coreList predQTyConName preds
-		    repCtxt predList
+repContext ctxt = do preds <- repList predQTyConName repLPred ctxt
+		     repCtxt preds
 
 -- represent a type predicate
 --
@@ -716,9 +713,8 @@ repPred ty
   | Just (cls, tys) <- splitHsClassTy_maybe ty
   = do
       cls1 <- lookupOcc cls
-      tys1 <- repLTys tys
-      tys2 <- coreList typeQTyConName tys1
-      repClassP cls1 tys2
+      tys1 <- repList typeQTyConName repLTy tys
+      repClassP cls1 tys1
 repPred (HsEqTy tyleft tyright)
   = do
       tyleft1  <- repLTy tyleft
@@ -860,8 +856,7 @@ repSplice (HsSplice n _)
 -----------------------------------------------------------------------------
 
 repLEs :: [LHsExpr Name] -> DsM (Core [TH.ExpQ])
-repLEs es = do { es'  <- mapM repLE es ;
-		 coreList expQTyConName es' }
+repLEs es = repList expQTyConName repLE es
 
 -- FIXME: some of these panics should be converted into proper error messages
 --	  unless we can make sure that constructs, which are plainly not
@@ -1024,10 +1019,11 @@ repLGRHS (L _ (GRHS ss rhs))
 
 repFields :: HsRecordBinds Name -> DsM (Core [TH.Q TH.FieldExp])
 repFields (HsRecFields { rec_flds = flds })
-  = do	{ fnames <- mapM lookupLOcc (map hsRecFieldId flds)
-	; es <- mapM repLE (map hsRecFieldArg flds)
-	; fs <- zipWithM repFieldExp fnames es
-	; coreList fieldExpQTyConName fs }
+  = repList fieldExpQTyConName rep_fld flds
+  where
+    rep_fld fld = do { fn <- lookupLOcc (hsRecFieldId fld)
+                     ; e  <- repLE (hsRecFieldArg fld)
+                     ; repFieldExp fn e }
 
 
 -----------------------------------------------------------------------------
@@ -1210,8 +1206,7 @@ repLambda (L _ m) = notHandled "Guarded labmdas" (pprMatch (LambdaExpr :: HsMatc
 
 -- Process a list of patterns
 repLPs :: [LPat Name] -> DsM (Core [TH.PatQ])
-repLPs ps = do { ps' <- mapM repLP ps ;
-		 coreList patQTyConName ps' }
+repLPs ps = repList patQTyConName repLP ps
 
 repLP :: LPat Name -> DsM (Core TH.PatQ)
 repLP (L _ p) = repP p
@@ -1232,16 +1227,17 @@ repP (ConPatIn dc details)
  = do { con_str <- lookupLOcc dc
       ; case details of
          PrefixCon ps -> do { qs <- repLPs ps; repPcon con_str qs }
-         RecCon rec   -> do { let flds = rec_flds rec
-			    ; vs <- sequence $ map lookupLOcc (map hsRecFieldId flds)
-                            ; ps <- sequence $ map repLP (map hsRecFieldArg flds)
-                            ; fps <- zipWithM (\x y -> rep2 fieldPatName [unC x,unC y]) vs ps
-                            ; fps' <- coreList fieldPatQTyConName fps
-                            ; repPrec con_str fps' }
+         RecCon rec   -> do { fps <- repList fieldPatQTyConName rep_fld (rec_flds rec)
+                            ; repPrec con_str fps }
          InfixCon p1 p2 -> do { p1' <- repLP p1;
                                 p2' <- repLP p2;
                                 repPinfix p1' con_str p2' }
    }
+ where
+   rep_fld fld = do { MkC v <- lookupLOcc (hsRecFieldId fld)
+                    ; MkC p <- repLP (hsRecFieldArg fld)
+                    ; rep2 fieldPatName [v,p] }
+ 
 repP (NPat l Nothing _)  = do { a <- repOverloadedLiteral l; repPlit a }
 repP (ViewPat e p _) = do { e' <- repLE e; p' <- repLP p; repPview e' p' }
 repP p@(NPat _ (Just _) _) = notHandled "Negative overloaded patterns" (ppr p)
@@ -1679,16 +1675,16 @@ repEqualP (MkC ty1) (MkC ty2) = rep2 equalPName [ty1, ty2]
 repConstr :: Core TH.Name -> HsConDeclDetails Name
           -> DsM (Core TH.ConQ)
 repConstr con (PrefixCon ps)
-    = do arg_tys  <- mapM repBangTy ps
-         arg_tys1 <- coreList strictTypeQTyConName arg_tys
-         rep2 normalCName [unC con, unC arg_tys1]
+    = do arg_tys  <- repList strictTypeQTyConName repBangTy ps
+         rep2 normalCName [unC con, unC arg_tys]
 repConstr con (RecCon ips)
-    = do arg_vs   <- mapM lookupLOcc (map cd_fld_name ips)
-         arg_tys  <- mapM repBangTy (map cd_fld_type ips)
-         arg_vtys <- zipWithM (\x y -> rep2 varStrictTypeName [unC x, unC y])
-                              arg_vs arg_tys
-         arg_vtys' <- coreList varStrictTypeQTyConName arg_vtys
-         rep2 recCName [unC con, unC arg_vtys']
+    = do { arg_vtys <- repList varStrictTypeQTyConName rep_ip ips
+         ; rep2 recCName [unC con, unC arg_vtys] }
+    where
+      rep_ip ip = do { MkC v  <- lookupLOcc (cd_fld_name ip)
+                     ; MkC ty <- repBangTy  (cd_fld_type ip)
+                     ; rep2 varStrictTypeName [v,ty] }
+
 repConstr con (InfixCon st1 st2)
     = do arg1 <- repBangTy st1
          arg2 <- repBangTy st2
@@ -1863,6 +1859,12 @@ repSequenceQ ty_a (MkC list)
 ------------ Lists and Tuples -------------------
 -- turn a list of patterns into a single pattern matching a list
 
+repList :: Name -> (a  -> DsM (Core b)) 
+                -> [a] -> DsM (Core [b])
+repList tc_name f args
+  = do { args1 <- mapM f args
+       ; coreList tc_name args1 }
+
 coreList :: Name	-- Of the TyCon of the element type
 	 -> [Core a] -> DsM (Core [a])
 coreList tc_name es
diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs
index f15ef5d3cc..24ed16f1c9 100644
--- a/compiler/hsSyn/HsBinds.lhs
+++ b/compiler/hsSyn/HsBinds.lhs
@@ -574,22 +574,6 @@ signatures. Since some of the signatures contain a list of names, testing for
 equality is not enough -- we have to check if they overlap.
 
 \begin{code}
-overlapHsSig :: Eq a => LSig a -> LSig a -> Bool
-overlapHsSig sig1 sig2 = case (unLoc sig1, unLoc sig2) of
-  (FixSig (FixitySig n1 _), FixSig (FixitySig n2 _)) -> unLoc n1 == unLoc n2
-  (IdSig n1,                IdSig n2)                -> n1 == n2
-  (TypeSig ns1 _,           TypeSig ns2 _)           -> ns1 `overlaps_with` ns2
-  (GenericSig ns1 _,        GenericSig ns2 _)        -> ns1 `overlaps_with` ns2
-  (InlineSig n1 _,          InlineSig n2 _)          -> unLoc n1 == unLoc n2
-  -- For specialisations, we don't have equality over HsType, so it's not
-  -- convenient to spot duplicate specialisations here.  Check for this later,
-  -- when we're in Type land
-  (_other1,                 _other2)                 -> False
-  where
-    ns1 `overlaps_with` ns2 = not (null (intersect (map unLoc ns1) (map unLoc ns2)))
-\end{code}
-
-\begin{code}
 instance (OutputableBndr name) => Outputable (Sig name) where
     ppr sig = ppr_sig sig
 
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 37965185cf..652eb0ad11 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -1364,7 +1364,7 @@ tcIfaceTyCon (IfaceTc name)
        ; case thing of    -- A "type constructor" can be a promoted data constructor
                           --           c.f. Trac #5881
            ATyCon   tc -> return tc
-           ADataCon dc -> return (buildPromotedDataCon dc)
+           ADataCon dc -> return (promoteDataCon dc)
            _ -> pprPanic "tcIfaceTyCon" (ppr name $$ ppr thing) }
 
 tcIfaceKindCon :: IfaceTyCon -> IfL TyCon
@@ -1374,7 +1374,7 @@ tcIfaceKindCon (IfaceTc name)
                           --           c.f. Trac #5881
            ATyCon tc 
              | isSuperKind (tyConKind tc) -> return tc   -- Mainly just '*' or 'AnyK'
-             | otherwise                  -> return (buildPromotedTyCon tc)
+             | otherwise                  -> return (promoteTyCon tc)
 
            _ -> pprPanic "tcIfaceKindCon" (ppr name $$ ppr thing) }
 
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 47756c5ea1..ac1fe9ac4f 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -495,7 +495,6 @@ data ExtensionFlag
    | Opt_MultiParamTypeClasses
    | Opt_FunctionalDependencies
    | Opt_UnicodeSyntax
-   | Opt_PolymorphicComponents
    | Opt_ExistentialQuantification
    | Opt_MagicHash
    | Opt_EmptyDataDecls
@@ -509,7 +508,6 @@ data ExtensionFlag
    | Opt_TupleSections
    | Opt_PatternGuards
    | Opt_LiberalTypeSynonyms
-   | Opt_Rank2Types
    | Opt_RankNTypes
    | Opt_ImpredicativeTypes
    | Opt_TypeOperators
@@ -2447,7 +2445,6 @@ xFlags = [
   ( "PatternGuards",                    Opt_PatternGuards, nop ),
   ( "UnicodeSyntax",                    Opt_UnicodeSyntax, nop ),
   ( "MagicHash",                        Opt_MagicHash, nop ),
-  ( "PolymorphicComponents",            Opt_PolymorphicComponents, nop ),
   ( "ExistentialQuantification",        Opt_ExistentialQuantification, nop ),
   ( "KindSignatures",                   Opt_KindSignatures, nop ),
   ( "EmptyDataDecls",                   Opt_EmptyDataDecls, nop ),
@@ -2460,7 +2457,10 @@ xFlags = [
   ( "CApiFFI",                          Opt_CApiFFI, nop ),
   ( "GHCForeignImportPrim",             Opt_GHCForeignImportPrim, nop ),
   ( "LiberalTypeSynonyms",              Opt_LiberalTypeSynonyms, nop ),
-  ( "Rank2Types",                       Opt_Rank2Types, nop ),
+  ( "PolymorphicComponents",            Opt_RankNTypes, 
+     deprecatedForExtension "RankNTypes" ),
+  ( "Rank2Types",                       Opt_RankNTypes, 
+     deprecatedForExtension "RankNTypes" ),
   ( "RankNTypes",                       Opt_RankNTypes, nop ),
   ( "ImpredicativeTypes",               Opt_ImpredicativeTypes, nop),
   ( "TypeOperators",                    Opt_TypeOperators, nop ),
@@ -2576,11 +2576,9 @@ default_PIC platform =
 impliedFlags :: [(ExtensionFlag, TurnOnFlag, ExtensionFlag)]
 impliedFlags
   = [ (Opt_RankNTypes,                turnOn, Opt_ExplicitForAll)
-    , (Opt_Rank2Types,                turnOn, Opt_ExplicitForAll)
     , (Opt_ScopedTypeVariables,       turnOn, Opt_ExplicitForAll)
     , (Opt_LiberalTypeSynonyms,       turnOn, Opt_ExplicitForAll)
     , (Opt_ExistentialQuantification, turnOn, Opt_ExplicitForAll)
-    , (Opt_PolymorphicComponents,     turnOn, Opt_ExplicitForAll)
     , (Opt_FlexibleInstances,         turnOn, Opt_TypeSynonymInstances)
     , (Opt_FunctionalDependencies,    turnOn, Opt_MultiParamTypeClasses)
 
@@ -2729,7 +2727,6 @@ glasgowExtsFlags = [
            , Opt_MultiParamTypeClasses
            , Opt_FunctionalDependencies
            , Opt_MagicHash
-           , Opt_PolymorphicComponents
            , Opt_ExistentialQuantification
            , Opt_UnicodeSyntax
            , Opt_PostfixOperators
diff --git a/compiler/prelude/PrelRules.lhs b/compiler/prelude/PrelRules.lhs
index 72cb8780a7..2ee14679b2 100644
--- a/compiler/prelude/PrelRules.lhs
+++ b/compiler/prelude/PrelRules.lhs
@@ -12,7 +12,7 @@ ToDo:
    (i1 + i2) only if it results in a valid Float.
 
 \begin{code}
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE RankNTypes #-}
 {-# OPTIONS -optc-DNON_POSIX_SOURCE #-}
 
 module PrelRules ( primOpRules, builtinRules ) where
diff --git a/compiler/prelude/TysWiredIn.lhs b/compiler/prelude/TysWiredIn.lhs
index 78e1f74b4d..5071b33e9a 100644
--- a/compiler/prelude/TysWiredIn.lhs
+++ b/compiler/prelude/TysWiredIn.lhs
@@ -322,10 +322,10 @@ tupleTyCon UnboxedTuple i = fst (unboxedTupleArr ! i)
 tupleTyCon ConstraintTuple    i = fst (factTupleArr    ! i)
 
 promotedTupleTyCon :: TupleSort -> Arity -> TyCon
-promotedTupleTyCon sort i = buildPromotedTyCon (tupleTyCon sort i)
+promotedTupleTyCon sort i = promoteTyCon (tupleTyCon sort i)
 
 promotedTupleDataCon :: TupleSort -> Arity -> TyCon
-promotedTupleDataCon sort i = buildPromotedDataCon (tupleCon sort i)
+promotedTupleDataCon sort i = promoteDataCon (tupleCon sort i)
 
 tupleCon :: TupleSort -> Arity -> DataCon
 tupleCon sort i | i > mAX_TUPLE_SIZE = snd (mk_tuple sort i)	-- Build one specially
@@ -605,7 +605,7 @@ mkPromotedListTy :: Type -> Type
 mkPromotedListTy ty = mkTyConApp promotedListTyCon [ty]
 
 promotedListTyCon :: TyCon
-promotedListTyCon = buildPromotedTyCon listTyCon
+promotedListTyCon = promoteTyCon listTyCon
 
 nilDataCon :: DataCon
 nilDataCon  = pcDataCon nilDataConName alpha_tyvar [] listTyCon
diff --git a/compiler/rename/RnBinds.lhs b/compiler/rename/RnBinds.lhs
index dfead07797..fbbaf65819 100644
--- a/compiler/rename/RnBinds.lhs
+++ b/compiler/rename/RnBinds.lhs
@@ -50,7 +50,7 @@ import Digraph		( SCC(..) )
 import Bag
 import Outputable
 import FastString
-import Data.List	( partition )
+import Data.List	( partition, sort )
 import Maybes		( orElse )
 import Control.Monad
 \end{code}
@@ -653,15 +653,7 @@ renameSigs :: HsSigCtxt
 	   -> RnM ([LSig Name], FreeVars)
 -- Renames the signatures and performs error checks
 renameSigs ctxt sigs 
-  = do	{ mapM_ dupSigDeclErr (findDupsEq overlapHsSig sigs)  -- Duplicate
-	  	-- Check for duplicates on RdrName version, 
-		-- because renamed version has unboundName for
-		-- not-in-scope binders, which gives bogus dup-sig errors
-		-- NB: in a class decl, a 'generic' sig is not considered 
-		--     equal to an ordinary sig, so we allow, say
-		--     	     class C a where
-		--	       op :: a -> a
- 		--             default op :: Eq a => a -> a
+  = do	{ mapM_ dupSigDeclErr (findDupSigs sigs)
 		
 	; (sigs', sig_fvs) <- mapFvRn (wrapLocFstM (renameSig ctxt)) sigs
 
@@ -748,6 +740,32 @@ okHsSig ctxt (L _ sig)
 
      (SpecInstSig {}, InstDeclCtxt {}) -> True
      (SpecInstSig {}, _)               -> False
+
+-------------------
+findDupSigs :: [LSig RdrName] -> [[(Located RdrName, Sig RdrName)]]
+-- Check for duplicates on RdrName version, 
+-- because renamed version has unboundName for
+-- not-in-scope binders, which gives bogus dup-sig errors
+-- NB: in a class decl, a 'generic' sig is not considered 
+--     equal to an ordinary sig, so we allow, say
+--     	     class C a where
+--	       op :: a -> a
+--             default op :: Eq a => a -> a
+findDupSigs sigs
+  = findDupsEq matching_sig (concatMap (expand_sig . unLoc) sigs)
+  where
+    expand_sig sig@(FixSig (FixitySig n _)) = [(n,sig)]
+    expand_sig sig@(InlineSig n _)          = [(n,sig)]
+    expand_sig sig@(TypeSig  ns _)   = [(n,sig) | n <- ns]
+    expand_sig sig@(GenericSig ns _) = [(n,sig) | n <- ns]
+    expand_sig _ = []
+
+    matching_sig (L _ n1,sig1) (L _ n2,sig2) = n1 == n2 && mtch sig1 sig2
+    mtch (FixSig {})     (FixSig {})     = True
+    mtch (InlineSig {})  (InlineSig {})  = True
+    mtch (TypeSig {})    (TypeSig {})    = True
+    mtch (GenericSig {}) (GenericSig {}) = True
+    mtch _ _ = False
 \end{code}
 
 
@@ -848,14 +866,15 @@ rnGRHS' ctxt rnBody (GRHS guards rhs)
 %************************************************************************
 
 \begin{code}
-dupSigDeclErr :: [LSig RdrName] -> RnM ()
-dupSigDeclErr sigs@(L loc sig : _)
+dupSigDeclErr :: [(Located RdrName, Sig RdrName)] -> RnM ()
+dupSigDeclErr pairs@((L loc name, sig) : _)
   = addErrAt loc $
-	vcat [ptext (sLit "Duplicate") <+> what_it_is <> colon,
-	      nest 2 (vcat (map ppr_sig sigs))]
+    vcat [ ptext (sLit "Duplicate") <+> what_it_is 
+           <> ptext (sLit "s for") <+> quotes (ppr name)
+         , ptext (sLit "at") <+> vcat (map ppr $ sort $ map (getLoc . fst) pairs) ]
   where
     what_it_is = hsSigDoc sig
-    ppr_sig (L loc sig) = ppr loc <> colon <+> ppr sig
+
 dupSigDeclErr [] = panic "dupSigDeclErr"
 
 misplacedSigErr :: LSig Name -> RnM ()
diff --git a/compiler/simplCore/OccurAnal.lhs b/compiler/simplCore/OccurAnal.lhs
index 4705f6b694..d75a224bb8 100644
--- a/compiler/simplCore/OccurAnal.lhs
+++ b/compiler/simplCore/OccurAnal.lhs
@@ -429,7 +429,7 @@ We are in an infinite loop.
 
 A more elaborate example (that I actually saw in practice when I went to
 mark GHC.List.filter as INLINABLE) is as follows. Say I have this module:
-  {-# LANGUAGE Rank2Types #-}
+  {-# LANGUAGE RankNTypes #-}
   module GHCList where
 
   import Prelude hiding (filter)
diff --git a/compiler/simplCore/Simplify.lhs b/compiler/simplCore/Simplify.lhs
index f794b88114..1c50c6b4c8 100644
--- a/compiler/simplCore/Simplify.lhs
+++ b/compiler/simplCore/Simplify.lhs
@@ -1796,7 +1796,7 @@ rebuildCase env scrut case_bndr [(_, bndrs, rhs)] cont
           --                            ppr scrut]) $
           tick (CaseElim case_bndr)
         ; env' <- simplNonRecX env case_bndr scrut
-          -- If case_bndr is deads, simplNonRecX will discard
+          -- If case_bndr is dead, simplNonRecX will discard
         ; simplExprF env' rhs cont }
   where
     elim_lifted   -- See Note [Case elimination: lifted case]
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index dac8fd1367..5b6364b196 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -212,19 +212,21 @@ instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
 -- Instantiates the TcTheta, puts all constraints thereby generated
 -- into the LIE, and returns a HsWrapper to enclose the call site.
 
-instCallConstraints _ [] = return idHsWrapper
-
-instCallConstraints origin (pred : preds)
-  | Just (ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut
-  = do  { traceTc "instCallConstraints" $ ppr (mkEqPred ty1 ty2)
-        ; co <- unifyType ty1 ty2
-	; co_fn <- instCallConstraints origin preds
-        ; return (co_fn <.> WpEvApp (EvCoercion co)) }
-
+instCallConstraints orig preds
+  | null preds 
+  = return idHsWrapper
   | otherwise
-  = do	{ ev_var <- emitWanted origin pred
-	; co_fn <- instCallConstraints origin preds
-	; return (co_fn <.> WpEvApp (EvId ev_var)) }
+  = do { evs <- mapM go preds
+       ; traceTc "instCallConstraints" (ppr evs)
+       ; return (mkWpEvApps evs) }
+  where
+    go pred 
+     | Just (ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut
+     = do  { co <- unifyType ty1 ty2
+           ; return (EvCoercion co) }
+     | otherwise
+     = do { ev_var <- emitWanted orig pred
+     	  ; return (EvId ev_var) }
 
 ----------------
 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
@@ -522,6 +524,10 @@ hasEqualities givens = any (has_eq . evVarPred) givens
     has_eq' (ClassPred cls _tys) = any has_eq (classSCTheta cls)
     has_eq' (TuplePred ts)       = any has_eq ts
     has_eq' (IrredPred _)        = True -- Might have equalities in it after reduction?
+       -- This is conservative.  e.g. if there's a constraint function FC with
+       --    type instance FC Int = Show
+       -- then we won't float from inside a given constraint (FC Int a), even though
+       -- it's really the innocuous (Show a).  Too bad!  Add a type signature
 
 ---------------- Getting free tyvars -------------------------
 tyVarsOfCt :: Ct -> TcTyVarSet
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 33c62dcc15..3309e12a33 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -7,7 +7,7 @@
 -- for details
 
 module TcCanonical(
-    canonicalize, occurCheckExpand, emitWorkNC,
+    canonicalize, emitWorkNC,
     StopOrContinue (..)
  ) where
 
@@ -25,8 +25,6 @@ import Var
 import VarEnv
 import Outputable
 import Control.Monad    ( when )
-import MonadUtils
-import Control.Applicative ( (<|>) )
 import TysWiredIn ( eqTyCon )
 
 import VarSet
@@ -1112,7 +1110,7 @@ canEqLeafFunEq loc ev fn tys1 ty2  -- ev :: F tys1 ~ ty2
       ; (xi2, co2)  <- flatten     loc FMFullFlatten flav ty2
            
           -- Fancy higher-dimensional coercion between equalities!
-         -- SPJ asks why?  Why not just co : F xis1 ~ F tys1?
+          -- SPJ asks why?  Why not just co : F xis1 ~ F tys1?
        ; let fam_head = mkTyConApp fn xis1
              xco = mkHdEqPred ty2 (mkTcTyConAppCo fn cos1) co2
              -- xco :: (F xis1 ~ xi2) ~ (F tys1 ~ ty2)
@@ -1181,78 +1179,6 @@ mkHdEqPred t2 co1 co2 = mkTcTyConAppCo eqTyCon [mkTcReflCo (defaultKind (typeKin
    -- Why defaultKind? Same reason as the comment on TcType/mkTcEqPred. I truly hate this (DV)
 \end{code}
 
-Note [Occurs check expansion]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-@occurCheckExpand tv xi@ expands synonyms in xi just enough to get rid
-of occurrences of tv outside type function arguments, if that is
-possible; otherwise, it returns Nothing.
-
-For example, suppose we have
-  type F a b = [a]
-Then
-  occurCheckExpand b (F Int b) = Just [Int]
-but
-  occurCheckExpand a (F a Int) = Nothing
-
-We don't promise to do the absolute minimum amount of expanding
-necessary, but we try not to do expansions we don't need to.  We
-prefer doing inner expansions first.  For example,
-  type F a b = (a, Int, a, [a])
-  type G b   = Char
-We have
-  occurCheckExpand b (F (G b)) = F Char
-even though we could also expand F to get rid of b.
-
-See also Note [Type synonyms and canonicalization].
-
-\begin{code}
-occurCheckExpand :: TcTyVar -> Type -> Maybe Type
--- Check whether the given variable occurs in the given type.  We may
--- have needed to do some type synonym unfolding in order to get rid
--- of the variable, so we also return the unfolded version of the
--- type, which is guaranteed to be syntactically free of the given
--- type variable.  If the type is already syntactically free of the
--- variable, then the same type is returned.
-
-occurCheckExpand tv ty
-  | not (tv `elemVarSet` tyVarsOfType ty) = Just ty
-  | otherwise                             = go ty
-  where
-    go t@(TyVarTy tv') | tv == tv' = Nothing
-                       | otherwise = Just t
-    go ty@(LitTy {}) = return ty
-    go (AppTy ty1 ty2) = do { ty1' <- go ty1
-           		    ; ty2' <- go ty2  
-           		    ; return (mkAppTy ty1' ty2') }
-    -- mkAppTy <$> go ty1 <*> go ty2
-    go (FunTy ty1 ty2) = do { ty1' <- go ty1 
-           		    ; ty2' <- go ty2 
-           		    ; return (mkFunTy ty1' ty2') } 
-    -- mkFunTy <$> go ty1 <*> go ty2
-    go ty@(ForAllTy {})
-       | tv `elemVarSet` tyVarsOfTypes tvs_knds = Nothing
-           -- Can't expand away the kinds unless we create 
-           -- fresh variables which we don't want to do at this point.
-       | otherwise = do { rho' <- go rho
-                        ; return (mkForAllTys tvs rho') }
-       where
-         (tvs,rho) = splitForAllTys ty
-         tvs_knds  = map tyVarKind tvs 
-
-    -- For a type constructor application, first try expanding away the
-    -- offending variable from the arguments.  If that doesn't work, next
-    -- see if the type constructor is a type synonym, and if so, expand
-    -- it and try again.
-    go ty@(TyConApp tc tys)
-      | isSynFamilyTyCon tc    -- It's ok for tv to occur under a type family application
-       = return ty             -- Eg.  (a ~ F a) is not an occur-check error
-                               -- NB This case can't occur during canonicalisation,
-                               --    because the arg is a Xi-type, but can occur in the
-                               --    call from TcErrors
-      | otherwise
-      = (mkTyConApp tc <$> mapM go tys) <|> (tcView ty >>= go)
-\end{code}
-
 Note [Type synonyms and canonicalization]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We treat type synonym applications as xi types, that is, they do not
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 74a687f409..6ac8793f6c 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -16,7 +16,6 @@ module TcErrors(
 
 #include "HsVersions.h"
 
-import TcCanonical( occurCheckExpand )
 import TcRnTypes
 import TcRnMonad
 import TcMType
@@ -576,7 +575,6 @@ mkEqErr1 ctxt ct
     mk_wanted_extra orig@(TypeEqOrigin {})
       = mkExpectedActualMsg ty1 ty2 orig
 
-
     mk_wanted_extra (KindEqOrigin cty1 cty2 sub_o)
       = (Nothing, msg1 $$ msg2)
       where
@@ -596,8 +594,10 @@ mkEqErr_help, reportEqErr
    -> TcType -> TcType -> TcM ErrMsg
 mkEqErr_help ctxt extra ct oriented ty1 ty2
   | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr ctxt extra ct oriented tv1 ty2
-  | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr ctxt extra ct oriented tv2 ty1
+  | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr ctxt extra ct swapped  tv2 ty1
   | otherwise                        = reportEqErr  ctxt extra ct oriented ty1 ty2
+  where
+    swapped = fmap flipSwap oriented
 
 reportEqErr ctxt extra1 ct oriented ty1 ty2
   = do { (ctxt', extra2) <- mkEqInfoMsg ctxt ct ty1 ty2
@@ -621,9 +621,10 @@ mkTyVarEqErr ctxt extra ct oriented tv1 ty2
   = 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)
+  = do { let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:")
+                              2 (sep [ppr ty1, char '~', ppr ty2])
+       ; (ctxt', extra2) <- mkEqInfoMsg ctxt ct ty1 ty2
+       ; mkErrorMsg ctxt' ct (occCheckMsg $$ extra2 $$ extra) }
 
   -- Check for skolem escape
   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
@@ -701,7 +702,7 @@ isUserSkolem ctxt tv
     is_user_skol_info _ = True
 
 misMatchOrCND :: ReportErrCtxt -> Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
--- If oriented then ty1 is expected, ty2 is actual
+-- If oriented then ty1 is actual, ty2 is expected
 misMatchOrCND ctxt ct oriented ty1 ty2
   | null givens || 
     (isRigid ty1 && isRigid ty2) || 
@@ -713,7 +714,7 @@ misMatchOrCND ctxt ct oriented ty1 ty2
   = couldNotDeduce givens ([mkEqPred ty1 ty2], orig)
   where
     givens = getUserGivens ctxt
-    orig   = TypeEqOrigin ty1 ty2
+    orig   = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
 
 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
 couldNotDeduce givens (wanteds, orig)
@@ -767,13 +768,13 @@ kindErrorMsg ty1 ty2
 
 --------------------
 misMatchMsg :: Maybe SwapFlag -> TcType -> TcType -> SDoc	   -- Types are already tidy
--- If oriented then ty1 is expected, ty2 is actual
+-- If oriented then ty1 is actual, ty2 is expected
 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) ]
+  = sep [ ptext (sLit "Couldn't match expected") <+> what <+> quotes (ppr ty2)
+        , nest 12 $   ptext (sLit "with actual") <+> what <+> quotes (ppr ty1) ]
   | otherwise
   = sep [ ptext (sLit "Couldn't match") <+> what <+> quotes (ppr ty1)
         , nest 14 $ ptext (sLit "with") <+> quotes (ppr ty2) ]
@@ -782,9 +783,10 @@ misMatchMsg oriented ty1 ty2
          | otherwise  = ptext (sLit "type")
 
 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> (Maybe SwapFlag, SDoc)
+-- NotSwapped means (actual, expected), IsSwapped is the reverse
 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)
+  | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (Just NotSwapped,  empty)
+  | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (Just IsSwapped, empty)
   | otherwise                                    = (Nothing, msg)
   where
     msg = vcat [ text "Expected type:" <+> ppr exp
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index e21eb4e4da..9075033ff2 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -823,8 +823,7 @@ tcExpr (PArrSeq _ _) _
 #ifdef GHCI	/* Only if bootstrapped */
 	-- Rename excludes these cases otherwise
 tcExpr (HsSpliceE splice) res_ty = tcSpliceExpr splice res_ty
-tcExpr (HsBracket brack)  res_ty = do	{ e <- tcBracket brack res_ty
-					; return (unLoc e) }
+tcExpr (HsBracket brack)  res_ty = tcBracket brack res_ty
 tcExpr e@(HsQuasiQuoteE _) _ =
     pprPanic "Should never see HsQuasiQuoteE in type checker" (ppr e)
 #endif /* GHCI */
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index 122e510c6b..70559f7e7c 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -74,6 +74,7 @@ import Outputable
 import FastString
 import Util
 
+import Data.Maybe
 import Control.Monad ( unless, when, zipWithM )
 import PrelNames( ipClassName, funTyConKey )
 \end{code}
@@ -278,7 +279,7 @@ tcHsLiftedType ty = addTypeCtxt ty $ tc_lhs_type ty ekLifted
 tcCheckLHsType :: LHsType Name -> Kind -> TcM Type
 tcCheckLHsType hs_ty exp_kind
   = addTypeCtxt hs_ty $ 
-    tc_lhs_type hs_ty (EK exp_kind (ptext (sLit "Expected")))
+    tc_lhs_type hs_ty (EK exp_kind expectedKindMsg)
 
 tcLHsType :: LHsType Name -> TcM (TcType, TcKind)
 -- Called from outside: set the context
@@ -290,7 +291,7 @@ tcCheckHsTypeAndGen :: HsType Name -> Kind -> TcM Type
 -- Typecheck a type signature, and kind-generalise it
 -- The result is not necessarily zonked, and has not been checked for validity
 tcCheckHsTypeAndGen hs_ty kind
-  = do { ty  <- tc_hs_type hs_ty (EK kind (ptext (sLit "Expected")))
+  = do { ty  <- tc_hs_type hs_ty (EK kind expectedKindMsg)
        ; kvs <- kindGeneralize (tyVarsOfType ty) []
        ; return (mkForAllTys kvs ty) }
 \end{code}
@@ -304,7 +305,7 @@ the expected kind.
 tc_infer_lhs_type :: LHsType Name -> TcM (TcType, TcKind)
 tc_infer_lhs_type ty =
   do { kv <- newMetaKindVar
-     ; r <- tc_lhs_type ty (EK kv (ptext (sLit "Expected")))
+     ; r <- tc_lhs_type ty (EK kv expectedKindMsg)
      ; return (r, kv) }
 
 tc_lhs_type :: LHsType Name -> ExpKind -> TcM TcType
@@ -426,8 +427,8 @@ tc_hs_type hs_ty@(HsExplicitListTy _k tys) exp_kind
        ; checkExpectedKind hs_ty (mkPromotedListTy kind) exp_kind
        ; return (foldr (mk_cons kind) (mk_nil kind) taus) }
   where
-    mk_cons k a b = mkTyConApp (buildPromotedDataCon consDataCon) [k, a, b]
-    mk_nil  k     = mkTyConApp (buildPromotedDataCon nilDataCon) [k]
+    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
+    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
 
 tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind
   = do { tks <- mapM tc_infer_lhs_type tys
@@ -441,8 +442,7 @@ tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind
 
 --------- Constraint types
 tc_hs_type ipTy@(HsIParamTy n ty) exp_kind
-  = do { ty' <- tc_lhs_type ty 
-            (EK liftedTypeKind (ptext (sLit "The type argument of the implicit parameter had")))
+  = do { ty' <- tc_lhs_type ty ekLifted
        ; checkExpectedKind ipTy constraintKind exp_kind
        ; ipClass <- tcLookupClass ipClassName
        ; let n' = mkStrLitTy $ hsIPNameFS n
@@ -453,16 +453,21 @@ tc_hs_type ty@(HsEqTy ty1 ty2) exp_kind
   = do { (ty1', kind1) <- tc_infer_lhs_type ty1
        ; (ty2', kind2) <- tc_infer_lhs_type ty2
        ; checkExpectedKind ty2 kind2
-              (EK kind1 (ptext (sLit "The left argument of the equality predicate had")))
+              (EK kind1 msg_fn)
        ; checkExpectedKind ty constraintKind exp_kind
        ; return (mkNakedTyConApp eqTyCon [kind1, ty1', ty2']) }
+  where
+    msg_fn pkind = ptext (sLit "The left argument of the equality had kind")
+                   <+> quotes (pprKind pkind)
 
 --------- Misc
 tc_hs_type (HsKindSig ty sig_k) exp_kind 
   = do { sig_k' <- tcLHsKind sig_k
        ; checkExpectedKind ty sig_k' exp_kind
-       ; tc_lhs_type ty
-             (EK sig_k' (ptext (sLit "An enclosing kind signature specified"))) }
+       ; tc_lhs_type ty (EK sig_k' msg_fn) }
+  where
+    msg_fn pkind = ptext (sLit "The signature specified kind") 
+                   <+> quotes (pprKind pkind)
 
 tc_hs_type (HsCoreTy ty) exp_kind
   = do { checkExpectedKind ty (typeKind ty) exp_kind
@@ -602,12 +607,10 @@ tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
            AGlobal (ATyCon tc) -> inst_tycon (mkTyConApp tc) (tyConKind tc)
 
            AGlobal (ADataCon dc)
-             | isPromotableType ty -> inst_tycon (mkTyConApp tc) (tyConKind tc)
+             | Just tc <- promoteDataCon_maybe dc
+             -> inst_tycon (mkTyConApp tc) (tyConKind tc)
              | otherwise -> failWithTc (quotes (ppr dc) <+> ptext (sLit "of type")
-                            <+> quotes (ppr ty) <+> ptext (sLit "is not promotable"))
-             where
-               ty = dataConUserType dc
-               tc = buildPromotedDataCon dc
+                            <+> quotes (ppr (dataConUserType dc)) <+> ptext (sLit "is not promotable"))
 
            APromotionErr err -> promotionErr name err
 
@@ -822,11 +825,13 @@ kcScopedKindVars kv_ns thing_inside
                      -- NB: use mutable signature variables
        ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) thing_inside } 
 
-kcHsTyVarBndrs :: Bool    -- Default UserTyVar to *
+kcHsTyVarBndrs :: Bool    -- True <=> full kind signature provided
+                          -- Default UserTyVar to *
                           -- and use KindVars not meta kind vars
                -> LHsTyVarBndrs Name 
 	       -> ([TcKind] -> TcM r)
 	       -> TcM r
+-- Used in getInitialKind
 kcHsTyVarBndrs full_kind_sig (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
   = do { kvs <- if full_kind_sig 
                 then return (map mkKindSigVar kv_ns)
@@ -845,6 +850,14 @@ kcHsTyVarBndrs full_kind_sig (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thin
            ; return (n, kind) }
     kc_hs_tv (KindedTyVar n k) 
       = do { kind <- tcLHsKind k
+               -- In an associated type decl, the type variable may already 
+               -- be in scope; in that case we want to make sure its kind
+               -- matches the one declared here
+           ; mb_thing <- tcLookupLcl_maybe n
+           ; case mb_thing of
+               Nothing          -> return ()
+               Just (AThing ks) -> checkKind kind ks
+               Just thing       -> pprPanic "check_in_scope" (ppr thing)
            ; return (n, kind) }
 
 tcScopedKindVars :: [Name] -> TcM a -> TcM a
@@ -967,38 +980,29 @@ kcLookupKind nm
            AGlobal (ATyCon tc) -> return (tyConKind tc)
            _                   -> pprPanic "kcLookupKind" (ppr tc_ty_thing) }
 
-kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> (TcKind -> TcM a) -> TcM a
+kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> TcM a -> TcM a
 -- Used for the type variables of a type or class decl,
 -- when doing the initial kind-check.  
 kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
   = kcScopedKindVars kvs $
     do 	{ tc_kind <- kcLookupKind name
-	; let (arg_ks, res_k) = splitKindFunTysN (length hs_tvs) tc_kind
+	; let (arg_ks, _res_k) = splitKindFunTysN (length hs_tvs) tc_kind
                      -- There should be enough arrows, because
                      -- getInitialKinds used the tcdTyVars
         ; name_ks <- zipWithM kc_tv hs_tvs arg_ks
-        ; tcExtendKindEnv name_ks (thing_inside res_k) }
+        ; tcExtendKindEnv name_ks thing_inside }
   where
+    -- getInitialKind has already gotten the kinds of these type
+    -- variables, but tiresomely we need to check them *again* 
+    -- to match the kind variables they mention against the ones 
+    -- we've freshly brought into scope
     kc_tv :: LHsTyVarBndr Name -> Kind -> TcM (Name, Kind)
     kc_tv (L _ (UserTyVar n)) exp_k 
-      = do { check_in_scope n exp_k
-           ; return (n, exp_k) }
+      = return (n, exp_k)
     kc_tv (L _ (KindedTyVar n hs_k)) exp_k
       = do { k <- tcLHsKind hs_k
            ; checkKind k exp_k
-           ; check_in_scope n exp_k
-           ; return (n, k) }
-
-    check_in_scope :: Name -> Kind -> TcM ()
-    -- In an associated type decl, the type variable may already 
-    -- be in scope; in that case we want to make sure it matches
-    -- any signature etc here
-    check_in_scope n exp_k
-      = do { mb_thing <- tcLookupLcl_maybe n
-           ; case mb_thing of
-               Nothing         -> return ()
-               Just (AThing k) -> checkKind k exp_k
-               Just thing      -> pprPanic "check_in_scope" (ppr thing) }
+           ; return (n, exp_k) }
 
 -----------------------
 tcTyClTyVars :: Name -> LHsTyVarBndrs Name	-- LHS of the type or class decl
@@ -1268,21 +1272,36 @@ We would like to get a decent error message from
 -- The ExpKind datatype means "expected kind" and contains 
 -- some info about just why that kind is expected, to improve
 -- the error message on a mis-match
-data ExpKind = EK TcKind SDoc
+data ExpKind = EK TcKind (TcKind -> SDoc)
+   -- The second arg is function that takes a *tidied* version 
+   -- of the first arg, and produces something like
+   --    "Expected kind k"
+   --    "Expected a constraint"
+   --    "The argument of Maybe should have kind k"
 
 instance Outputable ExpKind where
-  ppr (EK k _) = ptext (sLit "Expected kind:") <+> ppr k
+  ppr (EK k f) = f k
 
 ekLifted, ekOpen, ekConstraint :: ExpKind
-ekLifted     = EK liftedTypeKind (ptext (sLit "Expected"))
-ekOpen       = EK openTypeKind   (ptext (sLit "Expected"))
-ekConstraint = EK constraintKind (ptext (sLit "Expected"))
+ekLifted     = EK liftedTypeKind expectedKindMsg
+ekOpen       = EK openTypeKind   expectedKindMsg
+ekConstraint = EK constraintKind expectedKindMsg
+
+expectedKindMsg :: TcKind -> SDoc
+expectedKindMsg pkind
+  | isConstraintKind pkind = ptext (sLit "Expected a constraint")
+  | isOpenTypeKind   pkind = ptext (sLit "Expected a type")
+  | otherwise = ptext (sLit "Expected kind") <+> quotes (pprKind pkind)
 
 -- Build an ExpKind for arguments
 expArgKind :: SDoc -> TcKind -> Int -> ExpKind
-expArgKind exp kind arg_no = EK kind (ptext (sLit "The") <+> speakNth arg_no 
-                                  <+> ptext (sLit "argument of") <+> exp
-                                  <+> ptext (sLit "should have"))
+expArgKind exp kind arg_no = EK kind msg_fn
+  where
+    msg_fn pkind 
+      = sep [ ptext (sLit "The") <+> speakNth arg_no 
+              <+> ptext (sLit "argument of") <+> exp
+            , nest 2 $ ptext (sLit "should have kind") 
+              <+> quotes (pprKind pkind) ]
 
 unifyKinds :: SDoc -> [(TcType, TcKind)] -> TcM TcKind
 unifyKinds fun act_kinds
@@ -1306,9 +1325,8 @@ 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)
-      ; mb_subk <- unifyKindX act_kind exp_kind
+checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
+ = do { mb_subk <- unifyKindX act_kind exp_kind
 
          -- Kind unification only generates definite errors
       ; case mb_subk of {
@@ -1320,6 +1338,7 @@ checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt)
          -- Now to find out what sort
         exp_kind <- zonkTcKind exp_kind
       ; act_kind <- zonkTcKind act_kind
+      ; traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr exp_kind)
       ; env0 <- tcInitTidyEnv
       ; let (exp_as, _) = splitKindFunTys exp_kind
             (act_as, _) = splitKindFunTys act_kind
@@ -1330,21 +1349,15 @@ checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt)
             (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)
+            occurs_check 
+               | Just act_tv <- tcGetTyVar_maybe act_kind
+               = isNothing (occurCheckExpand act_tv exp_kind)
+               | Just exp_tv <- tcGetTyVar_maybe exp_kind
+               = isNothing (occurCheckExpand exp_tv act_kind)
+               | otherwise 
+               = False
 
-                  -- 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
+            err | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
                 = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
                     <+> ptext (sLit "is unlifted")
 
@@ -1352,14 +1365,26 @@ checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt)
                 = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
                     <+> ptext (sLit "is lifted")
 
+                | occurs_check   -- Must precede the "more args expected" check
+                = ptext (sLit "Kind occurs check") $$ more_info
+
+                | n_exp_as < n_act_as     -- E.g. [Maybe]
+                = vcat [ 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)
+                       , more_info ]
+
+                  -- Now n_exp_as >= n_act_as. In the next two cases,
+                  -- n_exp_as == 0, and hence so is n_act_as
                 | otherwise               -- E.g. Monad [Int]
-                = ptext (sLit "Kind mis-match") $$ more_info
+                = 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)]
+            more_info = sep [ ek_ctxt tidy_exp_kind <> comma
+                            , nest 2 $ ptext (sLit "but") <+> quotes (ppr ty)
+                              <+> ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
 
+      ; traceTc "checkExpectedKind 1" (ppr ty $$ ppr tidy_act_kind $$ ppr tidy_exp_kind $$ ppr env1 $$ ppr env2)
       ; failWithTcM (env2, err) } } }
 \end{code}
 
@@ -1439,7 +1464,7 @@ tc_kind_var_app name arg_kis
   	           ; unless data_kinds $ addErr (dataKindsErr name)
   	     	   ; case isPromotableTyCon tc of
   	     	       Just n | n == length arg_kis ->
-  	     	         return (mkTyConApp (buildPromotedTyCon tc) arg_kis)
+  	     	         return (mkTyConApp (promoteTyCon tc) arg_kis)
   	     	       Just _  -> tycon_err tc "is not fully applied"
   	     	       Nothing -> tycon_err tc "is not promotable" }
 
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index db7f36297f..a75890f70a 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -182,6 +182,7 @@ runSolverPipeline pipeline workItem
            ContinueWith ct -> do { traceFireTcS ct (ptext (sLit "Kept as inert:") <+> ppr ct)
                                  ; traceTcS "End solver pipeline (not discharged) }" $
                                        vcat [ ptext (sLit "final_item = ") <+> ppr ct
+                                            , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
                                             , ptext (sLit "inerts     = ") <+> ppr final_is]
                                  ; insertInertItemTcS ct }
        }
@@ -235,26 +236,6 @@ thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
 *                                                                               *
 *********************************************************************************
 
-Note [Efficient Orientation] 
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-There are two cases where we have to be careful about 
-orienting equalities to get better efficiency. 
-
-Case 1: In Rewriting Equalities (function rewriteEqLHS) 
-
-    When rewriting two equalities with the same LHS:
-          (a)  (tv ~ xi1) 
-          (b)  (tv ~ xi2) 
-    We have a choice of producing work (xi1 ~ xi2) (up-to the
-    canonicalization invariants) However, to prevent the inert items
-    from getting kicked out of the inerts first, we prefer to
-    canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
-    ~ xi1) if (a) comes from the inert set.
-    
-Case 2: Functional Dependencies 
-    Again, we should prefer, if possible, the inert variables on the RHS
-
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 
 spontaneousSolveStage workItem
@@ -707,7 +688,8 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
                                   , cc_tyargs = args1, cc_rhs = xi1, cc_loc = d1 }) 
                     wi@(CFunEqCan { cc_ev = ev2, cc_fun = tc2
                                   , cc_tyargs = args2, cc_rhs = xi2, cc_loc = d2 })
-  | fl1 `canSolve` fl2 
+  | i_solves_w && (not (w_solves_i && isMetaTyVarTy xi1))
+               -- See Note [Carefully solve the right CFunEqCan]
   = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
     do { traceTcS "interact with inerts: FunEq/FunEq" $ 
          vcat [ text "workItem =" <+> ppr wi
@@ -721,8 +703,8 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
              xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]
 
        ; ctevs <- xCtFlavor ev2 [mkTcEqPred xi2 xi1] xev
-                         -- No caching!  See Note [Cache-caused loops]
-                         -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
+             -- No caching!  See Note [Cache-caused loops]
+             -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
        ; emitWorkNC d2 ctevs 
        ; return (IRWorkItemConsumed "FunEq/FunEq") }
 
@@ -740,7 +722,7 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
              xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
 
        ; ctevs <- xCtFlavor ev1 [mkTcEqPred xi2 xi1] xev 
-                  -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
+             -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
 
        ; emitWorkNC d1 ctevs 
        ; return (IRInertConsumed "FunEq/FunEq") }
@@ -751,11 +733,59 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
     mk_sym_co x = mkTcSymCo (evTermCoercion x)
     fl1 = ctEvFlavour ev1
     fl2 = ctEvFlavour ev2
+
+    i_solves_w = fl1 `canSolve` fl2 
+    w_solves_i = fl2 `canSolve` fl1 
     
-doInteractWithInert _ _ = return (IRKeepGoing "NOP")
 
+doInteractWithInert _ _ = return (IRKeepGoing "NOP")
 \end{code}
 
+Note [Efficient Orientation] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are interacting two FunEqCans with the same LHS:
+          (inert)  ci :: (F ty ~ xi_i) 
+          (work)   cw :: (F ty ~ xi_w) 
+We prefer to keep the inert (else we pass the work item on down
+the pipeline, which is a bit silly).  If we keep the inert, we
+will (a) discharge 'cw' 
+     (b) produce a new equality work-item (xi_w ~ xi_i)
+Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
+    new_work :: xi_w ~ xi_i
+    cw := ci ; sym new_work
+Why?  Consider the simplest case when xi1 is a type variable.  If
+we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
+If we generate xi2~xi1, there is less chance of that happening.
+Of course it can and should still happen if xi1=a, xi1=Int, say.
+But we want to avoid it happening needlessly.
+
+Similarly, if we *can't* keep the inert item (because inert is Wanted,
+and work is Given, say), we prefer to orient the new equality (xi_i ~
+xi_w).
+
+Note [Carefully solve the right CFunEqCan]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the constraints
+  c1 :: F Int ~ a      -- Arising from an application line 5
+  c2 :: F Int ~ Bool   -- Arising from an application line 10
+Suppose that 'a' is a unification variable, arising only from 
+flattening.  So there is no error on line 5; it's just a flattening
+variable.  But there is (or might be) an error on line 10.
+
+Two ways to combine them, leaving either (Plan A)
+  c1 :: F Int ~ a      -- Arising from an application line 5
+  c3 :: a ~ Bool       -- Arising from an application line 10
+or (Plan B)
+  c2 :: F Int ~ Bool   -- Arising from an application line 10
+  c4 :: a ~ Bool       -- Arising from an application line 5
+
+Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
+on the *totally innocent* line 5.  An example is test SimpleFail16
+where the expected/actual message comes out backwards if we use
+the wrong plan.
+
+The second is the right thing to do.  Hence the isMetaTyVarTy
+test when solving pairwise CFunEqCan.
 
 Note [Shadowing of Implicit Parameters]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 7a3db58e7c..afc575caf7 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -993,21 +993,16 @@ checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Not used for instance decls; checkValidInstance instead
 checkValidType ctxt ty 
   = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
-       ; rank2_flag      <- xoptM Opt_Rank2Types
-       ; rankn_flag      <- xoptM Opt_RankNTypes
-       ; polycomp        <- xoptM Opt_PolymorphicComponents
+       ; rankn_flag  <- xoptM Opt_RankNTypes
        ; let gen_rank :: Rank -> Rank
              gen_rank r | rankn_flag = ArbitraryRank
-	                | rank2_flag = r2
 	                | otherwise  = r
 
-             rank2 = gen_rank r2
              rank1 = gen_rank r1
              rank0 = gen_rank r0
 
              r0 = rankZeroMonoType
              r1 = LimitedRank True r0
-             r2 = LimitedRank True r1
 
              rank
 	       = case ctxt of
@@ -1021,10 +1016,8 @@ checkValidType ctxt ty
 	     	 ExprSigCtxt 	-> rank1
 	     	 FunSigCtxt _   -> rank1
 	     	 InfSigCtxt _   -> ArbitraryRank	-- Inferred type
-	     	 ConArgCtxt _   | polycomp -> rank2
-                                     -- We are given the type of the entire
-                                     -- constructor, hence rank 1
- 	     			| otherwise -> rank1
+	     	 ConArgCtxt _   -> rank1 -- We are given the type of the entire
+                                         -- constructor, hence rank 1
 
 	     	 ForSigCtxt _	-> rank1
 	     	 SpecInstCtxt   -> rank1
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index 6aab6af632..66791b5170 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -1701,15 +1701,9 @@ tcRnGetInfo :: HscEnv
 --  *and* as a type or class constructor;
 -- hence the call to dataTcOccs, and we return up to two results
 tcRnGetInfo hsc_env name
-  = initTcPrintErrors hsc_env iNTERACTIVE $
-    tcRnGetInfo' hsc_env name
-
-tcRnGetInfo' :: HscEnv
-             -> Name
-             -> TcRn (TyThing, Fixity, [ClsInst])
-tcRnGetInfo' hsc_env name
   = let ictxt = hsc_IC hsc_env in
-    setInteractiveContext hsc_env ictxt $ do
+    initTcPrintErrors hsc_env iNTERACTIVE $
+    setInteractiveContext hsc_env ictxt  $ do
 
         -- Load the interface for all unqualified types and classes
         -- That way we will find all the instance declarations
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 42e9d556ff..9c5249a615 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -909,10 +909,14 @@ data Ct
 Note [Ct/evidence invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If  ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field
-of (cc_ev ct).   Eg for CDictCan, 
+of (cc_ev ct), and is fully rewritten wrt the substitution.   Eg for CDictCan, 
    ctev_pred (cc_ev ct) = (cc_class ct) (cc_tyargs ct)
 This holds by construction; look at the unique place where CDictCan is
-built (in TcCanonical)
+built (in TcCanonical).
+
+In contrast, the type of the evidence *term* (ccev_evtm or ctev_evar) in
+the evidence may *not* be fully zonked; we are careful not to look at it
+during constraint solving.  Seee Note [Evidence field of CtEvidence]
 
 \begin{code}
 mkNonCanonical :: CtLoc -> CtEvidence -> Ct
@@ -1228,13 +1232,13 @@ may be un-zonked.
 
 \begin{code}
 data CtEvidence 
-  = CtGiven { ctev_pred :: TcPredType
-            , ctev_evtm :: EvTerm }          -- See Note [Evidence field of CtEvidence]
+  = CtGiven { ctev_pred :: TcPredType      -- See Note [Ct/evidence invariant]
+            , ctev_evtm :: EvTerm }        -- See Note [Evidence field of CtEvidence]
     -- Truly given, not depending on subgoals
     -- NB: Spontaneous unifications belong here
     
-  | CtWanted { ctev_pred :: TcPredType
-             , ctev_evar :: EvVar }          -- See Note [Evidence field of CtEvidence]
+  | CtWanted { ctev_pred :: TcPredType     -- See Note [Ct/evidence invariant]
+             , ctev_evar :: EvVar }        -- See Note [Evidence field of CtEvidence]
     -- Wanted goal 
     
   | CtDerived { ctev_pred :: TcPredType }
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 576df104a9..78fb0bf7e3 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -876,8 +876,8 @@ lookupFlatEqn fam_ty
             , inert_flat_cache = flat_cache
             , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
        ; return (lookupFamHead solved_funeqs fam_ty `firstJust` 
-                 lookupFamHead flat_cache fam_ty    `firstJust`
-                 lookup_in_inerts inert_funeqs) }
+                 lookup_in_inerts inert_funeqs    `firstJust`
+                 lookupFamHead flat_cache fam_ty) }
   where
     lookup_in_inerts inert_funeqs 
         = case lookupFamHead inert_funeqs fam_ty of
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 09a5b11c22..406fd3a812 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -75,7 +75,13 @@ simplifyTop wanteds
     simpl_top :: WantedConstraints -> TcS WantedConstraints
     simpl_top wanteds
       = do { wc_first_go <- nestTcS (solve_wanteds_and_drop wanteds)
-           ; applyTyVarDefaulting wc_first_go 
+           ; let meta_tvs = filter isMetaTyVar (varSetElems (tyVarsOfWC wc_first_go))
+                   -- tyVarsOfWC: post-simplification the WC should reflect
+                   --             all unifications that have happened
+                   -- filter isMetaTyVar: we might have runtime-skolems in GHCi, 
+                   -- and we definitely don't want to try to assign to those!
+
+           ; mapM_ defaultTyVar meta_tvs   -- Has unification side effects
            ; simpl_top_loop wc_first_go }
     
     simpl_top_loop wc
@@ -341,13 +347,8 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
        ; return (qtvs, [], False, emptyTcEvBinds) }
 
   | otherwise
-  = do { zonked_tau_tvs <- zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
-
-       ; ev_binds_var <- newTcEvBinds
-       ; traceTc "simplifyInfer {"  $ vcat
-             [ ptext (sLit "names =") <+> ppr (map fst name_taus)
-             , ptext (sLit "taus =") <+> ppr (map snd name_taus)
-             , ptext (sLit "tau_tvs (zonked) =") <+> ppr zonked_tau_tvs
+  = do { traceTc "simplifyInfer {"  $ vcat
+             [ ptext (sLit "binds =") <+> ppr name_taus
              , ptext (sLit "closed =") <+> ppr _top_lvl
              , ptext (sLit "apply_mr =") <+> ppr apply_mr
              , ptext (sLit "(unzonked) wanted =") <+> ppr wanteds
@@ -367,6 +368,8 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
               -- calling solveWanteds will side-effect their evidence
               -- bindings, so we can't just revert to the input
               -- constraint.
+
+       ; ev_binds_var <- newTcEvBinds
        ; wanted_transformed <- solveWantedsTcMWithEvBinds ev_binds_var wanteds $
                                solve_wanteds_and_drop
                                -- Post: wanted_transformed are zonked
@@ -381,29 +384,29 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
               -- We discard bindings, insolubles etc, because all we are
               -- care aout it
 
-       ; (quant_pred_candidates, _extra_binds)   
-             <- if insolubleWC wanted_transformed 
-                then return ([], emptyBag)   -- See Note [Quantification with errors]
-                else runTcS $ 
-                do { let quant_candidates = approximateWC wanted_transformed
-                   ; traceTcS "simplifyWithApprox" $
-                     text "quant_candidates = " <+> ppr quant_candidates
-                   ; promoteTyVars quant_candidates
-                   ; _implics <- solveInteract quant_candidates
-                   ; (flats, _insols) <- getInertUnsolved
+       ; tc_lcl_env <- TcRnMonad.getLclEnv
+       ; let untch = tcl_untch tc_lcl_env
+       ; quant_pred_candidates   
+           <- if insolubleWC wanted_transformed 
+              then return []   -- See Note [Quantification with errors]
+              else do { gbl_tvs <- tcGetGlobalTyVars
+                      ; let quant_cand = approximateWC wanted_transformed
+                            meta_tvs   = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand)) 
+                      ; ((flats, _insols), _extra_binds) <- runTcS $ 
+                        do { mapM_ (promoteAndDefaultTyVar untch gbl_tvs) meta_tvs
+                           ; _implics <- solveInteract quant_cand
+                           ; getInertUnsolved }
+                      ; return (map ctPred $ filter isWantedCt (bagToList flats)) }
                    -- NB: Dimitrios is slightly worried that we will get
                    -- family equalities (F Int ~ alpha) in the quantification
                    -- candidates, as we have performed no further unflattening
                    -- at this point. Nothing bad, but inferred contexts might
                    -- look complicated.
-                   ; return (map ctPred $ filter isWantedCt (bagToList flats)) }
 
-             -- NB: quant_pred_candidates is already the fixpoint of any 
-             --     unifications that may have happened
-                  
-       ; gbl_tvs        <- tcGetGlobalTyVars -- TODO: can we just use untch instead of gbl_tvs?
-       ; zonked_tau_tvs <- zonkTyVarsAndFV zonked_tau_tvs
-       
+       -- NB: quant_pred_candidates is already the fixpoint of any 
+       --     unifications that may have happened
+       ; gbl_tvs        <- tcGetGlobalTyVars
+       ; zonked_tau_tvs <- zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
        ; let init_tvs  = zonked_tau_tvs `minusVarSet` gbl_tvs
              poly_qtvs = growThetaTyVars quant_pred_candidates init_tvs 
                          `minusVarSet` gbl_tvs
@@ -448,8 +451,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
 
             -- Step 7) Emit an implication
        ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
-       ; lcl_env <- TcRnMonad.getLclEnv
-       ; let implic = Implic { ic_untch    = pushUntouchables (tcl_untch lcl_env)
+       ; let implic = Implic { ic_untch    = pushUntouchables untch
                              , ic_skols    = qtvs_to_return
                              , ic_fsks     = []  -- wanted_tansformed arose only from solveWanteds
                                                  -- hence no flatten-skolems (which come from givens)
@@ -458,7 +460,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
                              , ic_insol    = False
                              , ic_binds    = ev_binds_var
                              , ic_info     = skol_info
-                             , ic_env      = lcl_env }
+                             , ic_env      = tc_lcl_env }
        ; emitImplication implic
          
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
@@ -845,7 +847,8 @@ floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
   | otherwise 
   = do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
-       ; promoteTyVars float_eqs
+       ; untch <- TcSMonad.getUntouchables
+       ; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs))
        ; ty_binds <- getTcSTyBindsMap
        ; traceTcS "floatEqualities" (vcat [ text "Floated eqs =" <+> ppr float_eqs
                                           , text "Ty binds =" <+> ppr ty_binds])
@@ -859,22 +862,6 @@ floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
        where
          pred = ctPred ct
 
-promoteTyVars :: Cts -> TcS ()
--- When we float a constraint out of an implication we
--- must restore (MetaTvInv) in Note [Untouchable type variables]
--- in TcType
-promoteTyVars cts
-  = do { untch <- TcSMonad.getUntouchables
-       ; mapM_ (promote_tv untch) (varSetElems (tyVarsOfCts cts)) }
-  where
-    promote_tv untch tv 
-      | isFloatedTouchableMetaTyVar untch tv
-      = do { cloned_tv <- TcSMonad.cloneMetaTyVar tv
-           ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
-           ; setWantedTyBind tv (mkTyVarTy rhs_tv) }
-      | otherwise
-      = return ()
-
 growSkols :: WantedConstraints -> VarSet -> VarSet
 -- Find all the type variables that might possibly be unified
 -- with a type that mentions a skolem.  This test is very conservative.
@@ -885,17 +872,59 @@ growSkols (WC { wc_flat = flats }) skols
   where
     theta = foldrBag ((:) . ctPred) [] flats
 
+promoteTyVar :: Untouchables -> TcTyVar  -> TcS ()
+-- When we float a constraint out of an implication we must restore
+-- invariant (MetaTvInv) in Note [Untouchable type variables] in TcType
+promoteTyVar untch tv 
+  | isFloatedTouchableMetaTyVar untch tv
+  = do { cloned_tv <- TcSMonad.cloneMetaTyVar tv
+       ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
+       ; setWantedTyBind tv (mkTyVarTy rhs_tv) }
+  | otherwise
+  = return ()
+
+promoteAndDefaultTyVar :: Untouchables -> TcTyVarSet -> TyVar -> TcS ()
+-- See Note [Promote _and_ default when inferring]
+promoteAndDefaultTyVar untch gbl_tvs tv
+  = do { tv1 <- if tv `elemVarSet` gbl_tvs 
+                then return tv
+                else defaultTyVar tv
+       ; promoteTyVar untch tv1 }
+
+defaultTyVar :: TcTyVar -> TcS TcTyVar
+-- Precondition: MetaTyVars only
+-- See Note [DefaultTyVar]
+defaultTyVar the_tv
+  | not (k `eqKind` default_k)
+  = do { tv' <- TcSMonad.cloneMetaTyVar the_tv
+       ; let new_tv = setTyVarKind tv' default_k
+       ; traceTcS "defaultTyVar" (ppr the_tv <+> ppr new_tv)
+       ; setWantedTyBind the_tv (mkTyVarTy new_tv)
+       ; return new_tv }
+             -- Why not directly derived_pred = mkTcEqPred k default_k?
+             -- See Note [DefaultTyVar]
+             -- We keep the same Untouchables on tv'
+
+  | otherwise = return the_tv	 -- The common case
+  where
+    k = tyVarKind the_tv
+    default_k = defaultKind k
+
 approximateWC :: WantedConstraints -> Cts
 -- Postcondition: Wanted or Derived Cts 
-approximateWC wc = float_wc emptyVarSet wc
+approximateWC wc 
+  = float_wc emptyVarSet wc
   where 
     float_wc :: TcTyVarSet -> WantedConstraints -> Cts
-    float_wc skols (WC { wc_flat = flat, wc_impl = implic }) = floats1 `unionBags` floats2
-      where floats1 = do_bag (float_flat skols) flat
-            floats2 = do_bag (float_implic skols) implic
+    float_wc skols (WC { wc_flat = flats, wc_impl = implics }) 
+      = do_bag (float_flat skols)   flats  `unionBags` 
+        do_bag (float_implic skols) implics
                                  
     float_implic :: TcTyVarSet -> Implication -> Cts
     float_implic skols imp
+      | hasEqualities (ic_given imp)  -- Don't float out of equalities
+      = emptyCts                      -- cf floatEqualities
+      | otherwise                     -- See Note [approximateWC]
       = float_wc skols' (ic_wanted imp)
       where
         skols' = skols `extendVarSetList` ic_skols imp `extendVarSetList` ic_fsks imp
@@ -910,6 +939,76 @@ approximateWC wc = float_wc emptyVarSet wc
     do_bag f = foldrBag (unionBags.f) emptyBag
 \end{code}
 
+Note [ApproximateWC]
+~~~~~~~~~~~~~~~~~~~~
+approximateWC takes a constraint, typically arising from the RHS of a
+let-binding whose type we are *inferring*, and extracts from it some
+*flat* constraints that we might plausibly abstract over.  Of course
+the top-level flat constraints are plausible, but we also float constraints
+out from inside, if the are not captured by skolems.
+
+However we do *not* float anything out if the implication binds equality
+constriants, because that defeats the OutsideIn story.  Consider
+   data T a where
+     TInt :: T Int
+     MkT :: T a
+
+   f TInt = 3::Int
+
+We get the implication (a ~ Int => res ~ Int), where so far we've decided 
+  f :: T a -> res
+We don't want to float (res~Int) out because then we'll infer  
+  f :: T a -> Int
+which is only on of the possible types. (GHC 7.6 accidentally *did*
+float out of such implications, which meant it would happily infer
+non-principal types.)
+
+Note [DefaultTyVar]
+~~~~~~~~~~~~~~~~~~~
+defaultTyVar is used on any un-instantiated meta type variables to
+default the kind of OpenKind and ArgKind etc to *.  This is important 
+to ensure that instance declarations match.  For example consider
+
+     instance Show (a->b)
+     foo x = show (\_ -> True)
+
+Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
+and that won't match the typeKind (*) in the instance decl.  See tests
+tc217 and tc175.
+
+We look only at touchable type variables. No further constraints
+are going to affect these type variables, so it's time to do it by
+hand.  However we aren't ready to default them fully to () or
+whatever, because the type-class defaulting rules have yet to run.
+
+An important point is that if the type variable tv has kind k and the
+default is default_k we do not simply generate [D] (k ~ default_k) because:
+
+   (1) k may be ArgKind and default_k may be * so we will fail
+
+   (2) We need to rewrite all occurrences of the tv to be a type
+       variable with the right kind and we choose to do this by rewriting 
+       the type variable /itself/ by a new variable which does have the 
+       right kind.
+
+Note [Promote _and_ default when inferring]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we are inferring a type, we simplify the constraint, and then use
+approximateWC to produce a list of candidate constraints.  Then we MUST
+
+  a) Promote any meta-tyvars that have been floated out by 
+     approximateWC, to restore invariant (MetaTvInv) described in 
+     Note [Untouchable type variables] in TcType.
+
+  b) Default the kind of any meta-tyyvars that are not mentioned in
+     in the environment.
+
+To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
+have an instance (C ((x:*) -> Int)).  The instance doesn't match -- but it
+should!  If we don't solve the constraint, we'll stupidly quantify over 
+(C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
+(b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
+
 Note [Float Equalities out of Implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
 For ordinary pattern matches (including existentials) we float 
@@ -1028,6 +1127,7 @@ in TcMType.
 *                          Defaulting and disamgiguation                        *
 *                                                                               *
 *********************************************************************************
+
 \begin{code}
 applyDefaultingRules :: Cts -> TcS Bool
   -- True <=> I did some defaulting, reflected in ty_binds
@@ -1052,85 +1152,7 @@ applyDefaultingRules wanteds
        ; return (or something_happeneds) }
 \end{code}
 
-Note [tryTcS in defaulting]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-defaultTyVar and disambigGroup create new evidence variables for
-default equations, and hence update the EvVar cache. However, after
-applyDefaultingRules we will try to solve these default equations
-using solveInteractCts, which will consult the cache and solve those
-EvVars from themselves! That's wrong.
-
-To avoid this problem we guard defaulting under a @tryTcS@ which leaves
-the original cache unmodified.
-
-There is a second reason for @tryTcS@ in defaulting: disambGroup does
-some constraint solving to determine if a default equation is
-``useful'' in solving some wanted constraints, but we want to
-discharge all evidence and unifications that may have happened during
-this constraint solving.
-
-Finally, @tryTcS@ importantly does not inherit the original cache from
-the higher level but makes up a new cache, the reason is that disambigGroup
-will call solveInteractCts so the new derived and the wanteds must not be 
-in the cache!
-
-
-\begin{code}
-applyTyVarDefaulting :: WantedConstraints -> TcS ()
-applyTyVarDefaulting wc 
-  = do { let tvs = filter isMetaTyVar (varSetElems (tyVarsOfWC wc))
-                   -- tyVarsOfWC: post-simplification the WC should reflect
-                   --             all unifications that have happened
-                   -- filter isMetaTyVar: we might have runtime-skolems in GHCi, 
-                   -- and we definitely don't want to try to assign to those!
-
-       ; traceTcS "applyTyVarDefaulting {" (ppr tvs)
-       ; mapM_ defaultTyVar tvs
-       ; traceTcS "applyTyVarDefaulting end }" empty }
-
-defaultTyVar :: TcTyVar -> TcS ()
-defaultTyVar the_tv
-  | not (k `eqKind` default_k)
-  = do { tv' <- TcSMonad.cloneMetaTyVar the_tv
-       ; let rhs_ty = mkTyVarTy (setTyVarKind tv' default_k)
-       ; setWantedTyBind the_tv rhs_ty }
-             -- Why not directly derived_pred = mkTcEqPred k default_k?
-             -- See Note [DefaultTyVar]
-             -- We keep the same Untouchables on tv'
-
-  | otherwise = return ()	 -- The common case
-  where
-    k = tyVarKind the_tv
-    default_k = defaultKind k
-\end{code}
-
-Note [DefaultTyVar]
-~~~~~~~~~~~~~~~~~~~
-defaultTyVar is used on any un-instantiated meta type variables to
-default the kind of OpenKind and ArgKind etc to *.  This is important 
-to ensure that instance declarations match.  For example consider
-
-     instance Show (a->b)
-     foo x = show (\_ -> True)
-
-Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
-and that won't match the typeKind (*) in the instance decl.  See tests
-tc217 and tc175.
-
-We look only at touchable type variables. No further constraints
-are going to affect these type variables, so it's time to do it by
-hand.  However we aren't ready to default them fully to () or
-whatever, because the type-class defaulting rules have yet to run.
-
-An important point is that if the type variable tv has kind k and the
-default is default_k we do not simply generate [D] (k ~ default_k) because:
 
-   (1) k may be ArgKind and default_k may be * so we will fail
-
-   (2) We need to rewrite all occurrences of the tv to be a type
-       variable with the right kind and we choose to do this by rewriting 
-       the type variable /itself/ by a new variable which does have the 
-       right kind.
 
 \begin{code}
 findDefaultableGroups 
@@ -1192,29 +1214,26 @@ disambigGroup :: [Type]                  -- The default types
 disambigGroup []  _grp
   = return False
 disambigGroup (default_ty:default_tys) group
-  = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
-       ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
+  = do { traceTcS "disambigGroup {" (ppr group $$ ppr default_ty)
+       ; success <- tryTcS $ -- Why tryTcS? If this attempt fails, we want to 
+                             -- discard all side effects from the attempt
                     do { setWantedTyBind the_tv default_ty
-                       ; traceTcS "disambigGroup (solving) {" $
-                         text "trying to solve constraints along with default equations ..."
                        ; implics_from_defaulting <- solveInteract wanteds
                        ; MASSERT (isEmptyBag implics_from_defaulting)
                            -- I am not certain if any implications can be generated
                            -- but I am letting this fail aggressively if this ever happens.
                                      
-                       ; all_solved <- checkAllSolved
-                       ; traceTcS "disambigGroup (solving) }" $
-                         text "disambigGroup solved =" <+> ppr all_solved
-                       ; return all_solved }
+                       ; checkAllSolved }
+
        ; if success then
              -- Success: record the type variable binding, and return
              do { setWantedTyBind the_tv default_ty
                 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
-                ; traceTcS "disambigGroup succeeded" (ppr default_ty)
+                ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
                 ; return True }
          else
              -- Failure: try with the next type
-             do { traceTcS "disambigGroup failed, will try other default types"
+             do { traceTcS "disambigGroup failed, will try other default types }"
                            (ppr default_ty)
                 ; disambigGroup default_tys group } }
   where
diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs
index c5e09a3afa..d5acf6ca28 100644
--- a/compiler/typecheck/TcSplice.lhs
+++ b/compiler/typecheck/TcSplice.lhs
@@ -284,7 +284,7 @@ The predicate we use is TcEnv.thTopLevelId.
 %************************************************************************
 
 \begin{code}
-tcBracket     :: HsBracket Name -> TcRhoType -> TcM (LHsExpr TcId)
+tcBracket     :: HsBracket Name -> TcRhoType -> TcM (HsExpr TcId)
 tcSpliceDecls :: LHsExpr Name -> TcM [LHsDecl RdrName]
 tcSpliceExpr  :: HsSplice Name -> TcRhoType -> TcM (HsExpr TcId)
 tcSpliceType  :: HsSplice Name -> FreeVars -> TcM (TcType, TcKind)
@@ -350,22 +350,22 @@ tcBracket brack res_ty
           -- We build a single implication constraint with a BracketSkol;
           -- that in turn tells simplifyTop to report only definite
           -- errors
-       ; (_,lie) <- captureConstraints $
-                    newImplication BracketSkol [] [] $
-                    setStage brack_stage $
-                    do { meta_ty <- tc_bracket cur_stage brack
-                       ; unifyType meta_ty res_ty }
+       ; ((_binds1, meta_ty), lie) <- captureConstraints $
+                          newImplication BracketSkol [] [] $
+                          setStage brack_stage $
+                          tc_bracket cur_stage brack
 
           -- It's best to simplify the constraint now, even though in
           -- principle some later unification might be useful for it,
           -- because we don't want these essentially-junk TH implication
           -- contraints floating around nested inside other constraints
           -- See for example Trac #4949
-       ; _ <- simplifyTop lie
+       ; _binds2 <- simplifyTop lie
 
         -- Return the original expression, not the type-decorated one
        ; pendings <- readMutVar pending_splices
-       ; return (noLoc (HsBracketOut brack pendings)) }
+       ; co <- unifyType meta_ty res_ty
+       ; return (mkHsWrapCo co (HsBracketOut brack pendings)) }
 
 tc_bracket :: ThStage -> HsBracket Name -> TcM TcType
 tc_bracket outer_stage br@(VarBr _ name)     -- Note [Quoting names]
diff --git a/compiler/typecheck/TcSplice.lhs-boot b/compiler/typecheck/TcSplice.lhs-boot
index de14aa3b95..4f185fb208 100644
--- a/compiler/typecheck/TcSplice.lhs-boot
+++ b/compiler/typecheck/TcSplice.lhs-boot
@@ -18,7 +18,7 @@ tcSpliceType :: HsSplice Name -> FreeVars -> TcM (TcType, TcKind)
 
 tcBracket :: HsBracket Name 
           -> TcRhoType
-          -> TcM (LHsExpr TcId)
+          -> TcM (HsExpr TcId)
 
 tcSpliceDecls :: LHsExpr Name -> TcM [LHsDecl RdrName]
 
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index bbd0c93e6b..469635ef29 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -128,7 +128,7 @@ tcTyClGroup boot_details tyclds
 
                  -- Populate environment with knot-tied ATyCon for TyCons
                  -- NB: if the decls mention any ill-staged data cons
-                 -- (see Note [ARecDataCon: Recusion and promoting data constructors]
+                 -- (see Note [Recusion and promoting data constructors]
                  -- we will have failed already in kcTyClGroup, so no worries here
            ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
 
@@ -324,8 +324,12 @@ getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)]
 --      Example: data T a b = ...
 --      return (T, kv1 -> kv2 -> kv3)
 --
--- ALSO for each datacon, return (dc, ARecDataCon)
--- Note [ARecDataCon: Recusion and promoting data constructors]
+-- This pass deals with (ie incorporates into the kind it produces)
+--   * The kind signatures on type-variable binders
+--   * The result kinds signature on a TyClDecl
+--
+-- ALSO for each datacon, return (dc, APromotionErr RecDataConPE)
+-- Note [ARecDataCon: Recursion and promoting data constructors]
 -- 
 -- No family instances are passed to getInitialKinds
 
@@ -361,14 +365,15 @@ getInitialKind top_lvl decl@(TyDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcd
              kvs       = varSetElems (tyVarsOfType body_kind)
              main_pr   = (name, AThing (mkForAllTys kvs body_kind))
              inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ]
-             -- See Note [ARecDataCon: Recusion and promoting data constructors]
+             -- See Note [Recusion and promoting data constructors]
        ; return (main_pr : inner_prs) }
  
   | TyData { td_cons = cons } <- defn
   = kcHsTyVarBndrs False ktvs $ \ arg_kinds -> 
     do { let main_pr   = (name, AThing (mkArrowKinds arg_kinds liftedTypeKind))
-             inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ]
-             -- See Note [ARecDataCon: Recusion and promoting data constructors]
+             inner_prs = [ (unLoc (con_name con), APromotionErr RecDataConPE) 
+                         | L _ con <- cons ]
+             -- See Note [Recusion and promoting data constructors]
        ; return (main_pr : inner_prs) }
 
   | otherwise = pprPanic "getInitialKind" (ppr decl)
@@ -413,13 +418,18 @@ kcLTyClDecl (L loc decl)
 
 kcTyClDecl :: TyClDecl Name -> TcM ()
 -- This function is used solely for its side effect on kind variables
+-- NB kind signatures on the type variables and 
+--    result kind signature have aready been dealt with
+--    by getInitialKind, so we can ignore them here.
 
 kcTyClDecl decl@(TyDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdTyDefn = defn })
   | TyData { td_cons = cons, td_kindSig = Just _ } <- defn
-  = mapM_ (wrapLocM kcConDecl) cons  -- Ignore the td_ctxt; heavily deprecated and inconvenient
+  = mapM_ (wrapLocM kcConDecl) cons  
+    -- hs_tvs and td_kindSig already dealt with in getInitialKind
+    -- Ignore the td_ctxt; heavily deprecated and inconvenient
 
   | TyData { td_ctxt = ctxt, td_cons = cons } <- defn
-  = kcTyClTyVars name hs_tvs $ \ _res_k -> 
+  = kcTyClTyVars name hs_tvs $ 
     do	{ _ <- tcHsContext ctxt
         ; mapM_ (wrapLocM kcConDecl) cons }
 
@@ -427,7 +437,7 @@ kcTyClDecl decl@(TyDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdTyDefn = d
 
 kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
                        , tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats})
-  = kcTyClTyVars name hs_tvs $ \ _res_k -> 
+  = kcTyClTyVars name hs_tvs $ 
     do	{ _ <- tcHsContext ctxt
 	; mapM_ (wrapLocM kcTyClDecl) ats
 	; mapM_ (wrapLocM kc_sig)     sigs }
@@ -436,8 +446,8 @@ kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
     kc_sig (GenericSig _ op_ty) = discardResult (tcHsLiftedType op_ty)
     kc_sig _                    = return ()
 
-kcTyClDecl (ForeignType {}) = return ()
 kcTyClDecl (TyFamily {})    = return ()
+kcTyClDecl (ForeignType {}) = return ()
 
 -------------------
 kcConDecl :: ConDecl Name -> TcM ()
@@ -451,8 +461,8 @@ kcConDecl (ConDecl { con_name = name, con_qvars = ex_tvs
        ; return () }
 \end{code}
 
-Note [ARecDataCon: Recusion and promoting data constructors]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Recursion and promoting data constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We don't want to allow promotion in a strongly connected component
 when kind checking.
 
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index b8594afcec..aa69d75e56 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -64,7 +64,7 @@ module TcType (
   -- Predicates. 
   -- Again, newtypes are opaque
   eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
-  pickyEqType, eqKind, 
+  pickyEqType, eqKind,
   isSigmaTy, isOverloadedTy,
   isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
@@ -74,7 +74,7 @@ module TcType (
   
   ---------------------------------
   -- Misc type manipulators
-  deNoteType,
+  deNoteType, occurCheckExpand,
   orphNamesOfType, orphNamesOfDFunHead, orphNamesOfCo,
   getDFunTyKey,
   evVarPred_maybe, evVarPred,
@@ -554,25 +554,9 @@ tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
 -- ^ Add the free 'TyVar's to the env in tidy form,
 -- so that we can tidy the type they are free in
 tidyFreeTyVars (full_occ_env, var_env) tyvars 
-  = fst (tidyOpenTyVars (trimmed_occ_env, var_env) tv_list)
+  = fst (tidyOpenTyVars (full_occ_env, var_env) (varSetElems tyvars))
 
-  where
-    tv_list = varSetElems tyvars
-    
-    trimmed_occ_env = foldr mk_occ_env emptyOccEnv tv_list
-      -- The idea here is that we restrict the new TidyEnv to the 
-      -- _free_ vars of the type, so that we don't gratuitously rename
-      -- the _bound_ variables of the type
-
-    mk_occ_env :: TyVar -> TidyOccEnv -> TidyOccEnv
-    mk_occ_env tv env 
-       = case lookupOccEnv full_occ_env occ of
-            Just n  -> extendOccEnv env occ n
-            Nothing -> env
-       where
-         occ = getOccName tv
-
----------------
+        ---------------
 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
 
@@ -614,9 +598,13 @@ tidyType env (ForAllTy tv ty)	  = ForAllTy tvp $! (tidyType envp ty)
 -- and then uses 'tidyType' to work over the type itself
 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
 tidyOpenType env ty
-  = (env', tidyType env' ty)
+  = (env', tidyType (trimmed_occ_env, var_env) ty)
   where
-    env' = tidyFreeTyVars env (tyVarsOfType ty)
+    (env'@(_, var_env), tvs') = tidyOpenTyVars env (varSetElems (tyVarsOfType ty))
+    trimmed_occ_env = initTidyOccEnv (map getOccName tvs')
+      -- The idea here was that we restrict the new TidyEnv to the 
+      -- _free_ vars of the type, so that we don't gratuitously rename
+      -- the _bound_ variables of the type.
 
 ---------------
 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
@@ -1174,6 +1162,84 @@ pickyEqType ty1 ty2
     gos _ _ _ = False
 \end{code}
 
+Note [Occurs check expansion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+@occurCheckExpand tv xi@ expands synonyms in xi just enough to get rid
+of occurrences of tv outside type function arguments, if that is
+possible; otherwise, it returns Nothing.
+
+For example, suppose we have
+  type F a b = [a]
+Then
+  occurCheckExpand b (F Int b) = Just [Int]
+but
+  occurCheckExpand a (F a Int) = Nothing
+
+We don't promise to do the absolute minimum amount of expanding
+necessary, but we try not to do expansions we don't need to.  We
+prefer doing inner expansions first.  For example,
+  type F a b = (a, Int, a, [a])
+  type G b   = Char
+We have
+  occurCheckExpand b (F (G b)) = F Char
+even though we could also expand F to get rid of b.
+
+See also Note [Type synonyms and canonicalization] in TcCanonical
+
+\begin{code}
+occurCheckExpand :: TcTyVar -> Type -> Maybe Type
+-- See Note [Occurs check expansion]
+-- Check whether the given variable occurs in the given type.  We may
+-- have needed to do some type synonym unfolding in order to get rid
+-- of the variable, so we also return the unfolded version of the
+-- type, which is guaranteed to be syntactically free of the given
+-- type variable.  If the type is already syntactically free of the
+-- variable, then the same type is returned.
+
+occurCheckExpand tv ty
+  | not (tv `elemVarSet` tyVarsOfType ty) = Just ty
+  | otherwise                             = go ty
+  where
+    go t@(TyVarTy tv') | tv == tv' = Nothing
+                       | otherwise = Just t
+    go ty@(LitTy {}) = return ty
+    go (AppTy ty1 ty2) = do { ty1' <- go ty1
+           		    ; ty2' <- go ty2  
+           		    ; return (mkAppTy ty1' ty2') }
+    -- mkAppTy <$> go ty1 <*> go ty2
+    go (FunTy ty1 ty2) = do { ty1' <- go ty1 
+           		    ; ty2' <- go ty2 
+           		    ; return (mkFunTy ty1' ty2') } 
+    -- mkFunTy <$> go ty1 <*> go ty2
+    go ty@(ForAllTy {})
+       | tv `elemVarSet` tyVarsOfTypes tvs_knds = Nothing
+           -- Can't expand away the kinds unless we create 
+           -- fresh variables which we don't want to do at this point.
+       | otherwise = do { rho' <- go rho
+                        ; return (mkForAllTys tvs rho') }
+       where
+         (tvs,rho) = splitForAllTys ty
+         tvs_knds  = map tyVarKind tvs 
+
+    -- For a type constructor application, first try expanding away the
+    -- offending variable from the arguments.  If that doesn't work, next
+    -- see if the type constructor is a type synonym, and if so, expand
+    -- it and try again.
+    go ty@(TyConApp tc tys)
+{-
+      | isSynFamilyTyCon tc    -- It's ok for tv to occur under a type family application
+       = return ty             -- Eg.  (a ~ F a) is not an occur-check error
+                               -- NB This case can't occur during canonicalisation,
+                               --    because the arg is a Xi-type, but can occur in the
+                               --    call from TcErrors
+      | otherwise
+-}
+      = do { tys <- mapM go tys; return (mkTyConApp tc tys) }
+        `firstJust` -- First try to eliminate the tyvar from the args
+        do { ty <- tcView ty; go ty }
+                    -- Failing that, try to expand a synonym
+\end{code}
+
 %************************************************************************
 %*									*
 \subsection{Predicate types}
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 4b92023a57..999575be85 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -55,12 +55,11 @@ import Kind
 import TyCon
 import TysWiredIn
 import Var
-import VarSet
 import VarEnv
 import ErrUtils
 import DynFlags
 import BasicTypes
-import Maybes ( allMaybes, isJust )
+import Maybes ( isJust )
 import Util
 import Outputable
 import FastString
@@ -767,22 +766,19 @@ uUnfilledVar origin swapped tv1 details1 non_var_ty2  -- ty2 is not a type varia
       MetaTv { mtv_info = TauTv, mtv_ref = ref1 }
         -> do { mb_ty2' <- checkTauTvUpdate tv1 non_var_ty2
               ; case mb_ty2' of
-                  Nothing   -> do { traceTc "Occ/kind defer" (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
-                                                              $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
-                                  ; defer }
                   Just ty2' -> updateMeta tv1 ref1 ty2'
+                  Nothing   -> do { traceTc "Occ/kind defer" 
+                                        (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
+                                         $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
+                                  ; defer }
               }
 
       _other -> do { traceTc "Skolem defer" (ppr tv1); defer }	-- Skolems of all sorts
   where
-    defer | Just ty2' <- tcView non_var_ty2	-- Note [Avoid deferring]
-    	    	         	   		-- non_var_ty2 isn't expanded yet
-          = uUnfilledVar origin swapped tv1 details1 ty2'
-          | otherwise
-          = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
-          -- Occurs check or an untouchable: just defer
-	  -- NB: occurs check isn't necessarily fatal: 
-	  --     eg tv1 occured in type family parameter
+    defer = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
+               -- Occurs check or an untouchable: just defer
+	       -- NB: occurs check isn't necessarily fatal: 
+	       --     eg tv1 occured in type family parameter
 
 ----------------
 uUnfilledVars :: CtOrigin
@@ -839,7 +835,6 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 -- We are about to update the TauTv tv with ty.
 -- Check (a) that tv doesn't occur in ty (occurs check)
 --       (b) that kind(ty) is a sub-kind of kind(tv)
---       (c) that ty does not contain any type families, see Note [Type family sharing]
 -- 
 -- We have two possible outcomes:
 -- (1) Return the type to update the type variable with, 
@@ -856,53 +851,66 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 -- we return Nothing, leaving it to the later constraint simplifier to
 -- sort matters out.
 
--- Used in debug meesages only
-_ppr_sub :: Maybe Ordering -> SDoc
-_ppr_sub (Just LT) = text "LT"
-_ppr_sub (Just EQ) = text "EQ"
-_ppr_sub (Just GT) = text "GT"
-_ppr_sub Nothing   = text "Nothing"
-
 checkTauTvUpdate tv ty
-  = do { ty'   <- zonkTcType ty
-       ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty')
---       ; traceTc "checktttv" (ppr tv $$ ppr ty' $$ ppr (tyVarKind tv) $$ ppr (typeKind ty') $$ _ppr_sub sub_k)
+  = do { ty1   <- zonkTcType ty
+       ; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty1)
        ; case sub_k of
-           Nothing -> return Nothing
-           Just LT -> return Nothing
-           _       -> return (ok ty') }
+           Nothing           -> return Nothing
+           Just LT           -> return Nothing
+           _  | defer_me ty1   -- Quick test
+              -> -- Failed quick test so try harder
+                 case occurCheckExpand tv ty1 of 
+                   Nothing -> return Nothing
+                   Just ty2 | defer_me ty2 -> return Nothing
+                            | otherwise    -> return (Just ty2)
+              | otherwise   -> return (Just ty1) }
   where 
-    ok :: TcType -> Maybe TcType 
-    -- Checks that tv does not occur in the arg type
-    -- expanding type synonyms where necessary to make this so
-    -- eg type Phantom a = Bool
-    --     ok (tv -> Int)         = Nothing
-    --     ok (x -> Int)          = Just (x -> Int)
-    --     ok (Phantom tv -> Int) = Just (Bool -> Int)
-    ok (TyVarTy tv') | not (tv == tv') = Just (TyVarTy tv') 
-    ok this_ty@(TyConApp tc tys) 
-      | not (isSynFamilyTyCon tc), Just tys' <- allMaybes (map ok tys) 
-      = Just (TyConApp tc tys') 
-      | isSynTyCon tc, Just ty_expanded <- tcView this_ty
-      = ok ty_expanded -- See Note [Type synonyms and the occur check] 
-    ok ty@(LitTy {}) = Just ty
-    ok (FunTy arg res) | Just arg' <- ok arg, Just res' <- ok res
-                       = Just (FunTy arg' res') 
-    ok (AppTy fun arg) | Just fun' <- ok fun, Just arg' <- ok arg 
-                       = Just (AppTy fun' arg') 
-    ok (ForAllTy tv1 ty1) | Just ty1' <- ok ty1 = Just (ForAllTy tv1 ty1') 
-    -- Fall-through 
-    ok _ty = Nothing 
+    defer_me :: TcType -> Bool
+    -- Checks for (a) occurrence of tv
+    --            (b) type family applicatios
+    -- See Note [Conservative unification check]
+    defer_me (LitTy {})        = False
+    defer_me (TyVarTy tv')     = tv == tv'
+    defer_me (TyConApp tc tys) = isSynFamilyTyCon tc || any defer_me tys
+    defer_me (FunTy arg res)   = defer_me arg || defer_me res
+    defer_me (AppTy fun arg)   = defer_me fun || defer_me arg
+    defer_me (ForAllTy _ ty)   = defer_me ty
 \end{code}
 
-Note [Avoid deferring]
-~~~~~~~~~~~~~~~~~~~~~~
-We try to avoid creating deferred constraints only for efficiency.
-Example (Trac #4917)
+Note [Conservative unification check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When unifying (tv ~ rhs), w try to avoid creating deferred constraints
+only for efficiency.  However, we do not unify (the defer_me check) if
+  a) There's an occurs check (tv is in fvs(rhs))
+  b) There's a type-function call in 'rhs'
+
+If we fail defer_me we use occurCheckExpand to try to make it pass,
+(see Note [Type synonyms and the occur check]) and then use defer_me
+again to check.  Example: Trac #4917)
        a ~ Const a b
 where type Const a b = a.  We can solve this immediately, even when
 'a' is a skolem, just by expanding the synonym.
 
+We always defer type-function calls, even if it's be perfectly safe to
+unify, eg (a ~ F [b]).  Reason: this ensures that the constraint
+solver gets to see, and hence simplify the type-function call, which
+in turn might simplify the type of an inferred function.  Test ghci046
+is a case in point.
+
+More mysteriously, test T7010 gave a horrible error 
+  T7010.hs:29:21:
+    Couldn't match type `Serial (ValueTuple Float)' with `IO Float'
+    Expected type: (ValueTuple Vector, ValueTuple Vector)
+      Actual type: (ValueTuple Vector, ValueTuple Vector)
+because an insoluble type function constraint got mixed up with
+a soluble one when flattening.  I never fully understood this, but
+deferring type-function applications made it go away :-(.
+T5853 also got a less-good error message with more aggressive
+unification of type functions.
+
+Moreover the Note [Type family sharing] gives another reason, but
+again I'm not sure if it's really valid.
+
 Note [Type synonyms and the occur check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Generally speaking we try to update a variable with type synonyms not
@@ -928,8 +936,7 @@ the underlying definition of the type synonym.
 The same applies later on in the constraint interaction code; see TcInteract, 
 function @occ_check_ok@. 
 
-
-Note [Type family sharing]
+Note [Type family sharing]  
 ~~~~~~~~~~~~~~~~~~~~~~~~~~ 
 We must avoid eagerly unifying type variables to types that contain function symbols, 
 because this may lead to loss of sharing, and in turn, in very poor performance of the
@@ -942,7 +949,7 @@ constraint simplifier. Assume that we have a wanted constraint:
   D m2, 
   D m3 
 } 
-where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m2], 
+where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m4], 
 then, after zonking, our constraint simplifier will be faced with the following wanted 
 constraint: 
 { 
@@ -950,12 +957,19 @@ constraint:
   D [F [F m4]], 
   D [F m4] 
 } 
-which has to be flattened by the constraint solver. However, because the sharing is lost, 
-an polynomially larger number of flatten skolems will be created and the constraint sets 
-we are working with will be polynomially larger. 
+which has to be flattened by the constraint solver. In the absence of
+a flat-cache, this may generate a polynomially larger number of
+flatten skolems and the constraint sets we are working with will be
+polynomially larger.
+
+Instead, if we defer the unifications m1 := [F m2], etc. we will only
+be generating three flatten skolems, which is the maximum possible
+sharing arising from the original constraint.  That's why we used to
+use a local "ok" function, a variant of TcType.occurCheckExpand.
 
-Instead, if we defer the unifications m1 := [F m2], etc. we will only be generating three 
-flatten skolems, which is the maximum possible sharing arising from the original constraint. 
+HOWEVER, we *do* now have a flat-cache, which effectively recovers the
+sharing, so there's no great harm in losing it -- and it's generally
+more efficient to do the unification up-front.
 
 \begin{code}
 data LookupTyVarResult	-- The result of a lookupTcTyVar call
@@ -1125,14 +1139,16 @@ uUnboundKVar kv1 k2@(TyVarTy kv2)
   = do { writeMetaTyVar kv1 k2; return (Just EQ) }
 
 uUnboundKVar kv1 non_var_k2
-  = do  { k2' <- zonkTcKind non_var_k2
-        ; let k2'' = defaultKind k2'
+  | isSigTyVar kv1
+  = return Nothing
+  | otherwise
+  = do { k2a <- zonkTcKind non_var_k2
+       ; let k2b = defaultKind k2a
                 -- MetaKindVars must be bound only to simple kinds
 
-        ; if not (elemVarSet kv1 (tyVarsOfType k2''))
-          && not (isSigTyVar kv1)
-          then do { writeMetaTyVar kv1 k2''; return (Just EQ) }
-          else return Nothing }
+       ; case occurCheckExpand kv1 k2b of
+           Just k2c -> do { writeMetaTyVar kv1 k2c; return (Just EQ) }
+           _        -> return Nothing }
 
 mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc)
 mkKindErrorCtxt ty1 ty2 k1 k2 env0
diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs
index 7318891d87..50d382f5fa 100644
--- a/compiler/types/Kind.lhs
+++ b/compiler/types/Kind.lhs
@@ -167,7 +167,7 @@ okArrowResultKind _                = False
 --              Subkinding
 -- The tc variants are used during type-checking, where we don't want the
 -- Constraint kind to be a subkind of anything
--- After type-checking (in core), Constraint is a subkind of argTypeKind
+-- After type-checking (in core), Constraint is a subkind of openTypeKind
 isSubOpenTypeKind :: Kind -> Bool
 -- ^ True of any sub-kind of OpenTypeKind
 isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 5919779703..88fbb3a7e9 100644
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -607,7 +607,7 @@ via the PromotedTyCon alternative in TyCon.
   kind signature on the forall'd variable; so the tc_kind field of
   PromotedTyCon is not identical to the dataConUserType of the
   DataCon.  But it's the same modulo changing the variable kinds,
-  done by Kind.promoteType.
+  done by DataCon.promoteType.
 
 * Small note: We promote the *user* type of the DataCon.  Eg
      data T = MkT {-# UNPACK #-} !(Bool, Bool)
diff --git a/mk/validate-settings.mk b/mk/validate-settings.mk
index 03f4e71060..bd582ff828 100644
--- a/mk/validate-settings.mk
+++ b/mk/validate-settings.mk
@@ -84,6 +84,16 @@ libraries/containers_dist-install_EXTRA_HC_OPTS += -fno-warn-deprecations
 
 # Temporarily turn off unused-do-bind warnings for the time package
 libraries/time_dist-install_EXTRA_HC_OPTS += -fno-warn-unused-do-bind 
+
+
+# Rank2Types is deprecated, so switch off deprecation warnings
+libraries/time_dist-install_EXTRA_HC_OPTS += -fno-warn-deprecations
+libraries/containers_dist-install_EXTRA_HC_OPTS += -fno-warn-deprecations
+libraries/dph/dph-lifted-copy_dist-install_EXTRA_HC_OPTS += -fno-warn-deprecations
+# vector already has -Wwarn
+# Cabal already has -Wwarn
+
+
 # Temporary: mkTyCon is deprecated
 libraries/time_dist-install_EXTRA_HC_OPTS += -fno-warn-deprecations
 # On Windows, there are also some unused import warnings