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

Conflicts:
	compiler/types/Coercion.lhs

43 files changed, 859 insertions, 900 deletions

diff --git a/compiler/cmm/PprC.hs b/compiler/cmm/PprC.hs
index bcfb5dc2ce..45f46b83ba 100644
--- a/compiler/cmm/PprC.hs
+++ b/compiler/cmm/PprC.hs
@@ -358,10 +358,13 @@ pprExpr e = case e of
     CmmRegOff reg 0 -> pprCastReg reg
 
     CmmRegOff reg i
-        | i >  0    -> pprRegOff (char '+') i
-        | otherwise -> pprRegOff (char '-') (-i)
+        | i < 0 && negate_ok -> pprRegOff (char '-') (-i)
+        | otherwise          -> pprRegOff (char '+') i
       where
         pprRegOff op i' = pprCastReg reg <> op <> int i'
+        negate_ok = negate (fromIntegral i :: Integer) <
+                    fromIntegral (maxBound::Int)
+                     -- overflow is undefined; see #7620
 
     CmmMachOp mop args -> pprMachOpApp mop args
 
diff --git a/compiler/coreSyn/CoreSyn.lhs b/compiler/coreSyn/CoreSyn.lhs
index 9f34e4ac2e..2d90323be5 100644
--- a/compiler/coreSyn/CoreSyn.lhs
+++ b/compiler/coreSyn/CoreSyn.lhs
@@ -1329,8 +1329,9 @@ isRuntimeVar = isId
 isRuntimeArg :: CoreExpr -> Bool
 isRuntimeArg = isValArg
 
--- | Returns @False@ iff the expression is a 'Type' or 'Coercion'
--- expression at its top level
+-- | Returns @True@ for value arguments, false for type args
+-- NB: coercions are value arguments (zero width, to be sure,
+-- like State#, but still value args).
 isValArg :: Expr b -> Bool
 isValArg e = not (isTypeArg e)
 
diff --git a/compiler/coreSyn/CoreTidy.lhs b/compiler/coreSyn/CoreTidy.lhs
index a46dc65ccf..77a85c241e 100644
--- a/compiler/coreSyn/CoreTidy.lhs
+++ b/compiler/coreSyn/CoreTidy.lhs
@@ -24,7 +24,8 @@ import CoreSyn
 import CoreArity
 import Id
 import IdInfo
-import TcType( tidyType, tidyCo, tidyTyVarBndr )
+import Type( tidyType, tidyTyVarBndr )
+import Coercion( tidyCo )
 import Var
 import VarEnv
 import UniqFM
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index f40f07ba13..e5d9fd9c43 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -291,7 +291,6 @@ Library
         Packages
         PprTyThing
         StaticFlags
-        StaticFlagParser
         SysTools
         TidyPgm
         Ctype
diff --git a/compiler/ghci/Debugger.hs b/compiler/ghci/Debugger.hs
index 44cf6f3865..0ceffcdcf1 100644
--- a/compiler/ghci/Debugger.hs
+++ b/compiler/ghci/Debugger.hs
@@ -22,7 +22,8 @@ import Name
 import Var hiding ( varName )
 import VarSet
 import UniqSupply
-import TcType
+import Type
+import Kind
 import GHC
 import Outputable
 import PprTyThing
@@ -207,7 +208,7 @@ pprTypeAndContents id = do
   dflags  <- GHC.getSessionDynFlags
   let pefas     = gopt Opt_PrintExplicitForalls dflags
       pcontents = gopt Opt_PrintBindContents dflags
-      pprdId    = (pprTyThing pefas . AnId) id
+      pprdId    = (PprTyThing.pprTyThing pefas . AnId) id
   if pcontents 
     then do
       let depthBound = 100
diff --git a/compiler/hsSyn/HsTypes.lhs b/compiler/hsSyn/HsTypes.lhs
index 93d91b19b1..74aa4773b6 100644
--- a/compiler/hsSyn/HsTypes.lhs
+++ b/compiler/hsSyn/HsTypes.lhs
@@ -652,9 +652,12 @@ ppr_mono_ty ctxt_prec (HsAppTy fun_ty arg_ty)
   = maybeParen ctxt_prec pREC_CON $
     hsep [ppr_mono_lty pREC_FUN fun_ty, ppr_mono_lty pREC_CON arg_ty]
 
-ppr_mono_ty ctxt_prec (HsOpTy ty1 (wrapper, op) ty2)
+ppr_mono_ty ctxt_prec (HsOpTy ty1 (_wrapper, L _ op) ty2)
   = maybeParen ctxt_prec pREC_OP $
-    ppr_mono_lty pREC_OP ty1 <+> ppr_mono_ty pREC_CON (HsWrapTy wrapper (HsTyVar (unLoc op))) <+> ppr_mono_lty pREC_OP ty2
+    sep [ ppr_mono_lty pREC_OP ty1
+        , sep [pprInfixOcc op, ppr_mono_lty pREC_OP ty2 ] ]
+    -- Don't print the wrapper (= kind applications)
+    -- c.f. HsWrapTy
 
 ppr_mono_ty _         (HsParTy ty)
   = parens (ppr_mono_lty pREC_TOP ty)
diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs
index ac244fab79..7f9b24e6e4 100644
--- a/compiler/iface/BinIface.hs
+++ b/compiler/iface/BinIface.hs
@@ -1426,13 +1426,6 @@ instance Binary IfaceAT where
         defs <- get bh
         return (IfaceAT dec defs)
 
-instance Binary IfaceATDefault where
-    put_ bh (IfaceATD tvs pat_tys ty) = do
-        put_ bh tvs
-        put_ bh pat_tys
-        put_ bh ty
-    get bh = liftM3 IfaceATD (get bh) (get bh) (get bh)
-
 instance Binary IfaceClassOp where
     put_ bh (IfaceClassOp n def ty) = do 
         put_ bh (occNameFS n)
diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index 8ba5e86eb9..d8b3b95d33 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -14,7 +14,7 @@
 module IfaceSyn (
         module IfaceType,
 
-        IfaceDecl(..), IfaceClassOp(..), IfaceAT(..), IfaceATDefault(..),
+        IfaceDecl(..), IfaceClassOp(..), IfaceAT(..), 
         IfaceConDecl(..), IfaceConDecls(..),
         IfaceExpr(..), IfaceAlt, IfaceLetBndr(..),
         IfaceBinding(..), IfaceConAlt(..),
@@ -118,15 +118,13 @@ data IfaceClassOp = IfaceClassOp OccName DefMethSpec IfaceType
         -- Just False => ordinary polymorphic default method
         -- Just True  => generic default method
 
-data IfaceAT = IfaceAT IfaceDecl [IfaceATDefault]
+data IfaceAT = IfaceAT IfaceDecl [IfaceAxBranch]
         -- Nothing => no default associated type instance
         -- Just ds => default associated type instance from these templates
 
-data IfaceATDefault = IfaceATD [IfaceTvBndr] [IfaceType] IfaceType
-        -- Each associated type default template is a triple of:
-        --   1. TyVars of the RHS and family arguments (including the class TVs)
-        --   3. The instantiated family arguments
-        --   2. The RHS of the synonym
+instance Outputable IfaceAxBranch where
+   ppr (IfaceAxBranch { ifaxbTyVars = tvs, ifaxbLHS = pat_tys, ifaxbRHS = ty }) 
+      = ppr tvs <+> hsep (map ppr pat_tys) <+> char '=' <+> ppr ty
 
 -- this is just like CoAxBranch
 data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr]
@@ -538,11 +536,10 @@ pprIfaceDecl (IfaceClass {ifCtxt = context, ifName = clas, ifTyVars = tyvars,
 
 pprIfaceDecl (IfaceAxiom {ifName = name, ifTyCon = tycon, ifAxBranches = branches })
   = hang (ptext (sLit "axiom") <+> ppr name <> colon)
-       2 (vcat $ map (pprIfaceAxBranch tycon) branches)
-
-pprIfaceAxBranch :: IfaceTyCon -> IfaceAxBranch -> SDoc
-pprIfaceAxBranch tc (IfaceAxBranch { ifaxbTyVars = tyvars, ifaxbLHS = lhs, ifaxbRHS = rhs })
-  = pprIfaceTvBndrs tyvars <> dot <+> ppr (IfaceTyConApp tc lhs) <+> text "~#" <+> ppr rhs
+       2 (vcat $ map ppr_branch branches)
+  where
+     ppr_branch (IfaceAxBranch { ifaxbTyVars = tyvars, ifaxbLHS = lhs, ifaxbRHS = rhs })
+        = pprIfaceTvBndrs tyvars <> dot <+> ppr (IfaceTyConApp tycon lhs) <+> text "~#" <+> ppr rhs
 
 pprCType :: Maybe CType -> SDoc
 pprCType Nothing = ptext (sLit "No C type associated")
@@ -561,9 +558,6 @@ instance Outputable IfaceClassOp where
 instance Outputable IfaceAT where
    ppr (IfaceAT d defs) = hang (ppr d) 2 (vcat (map ppr defs))
 
-instance Outputable IfaceATDefault where
-   ppr (IfaceATD tvs pat_tys ty) = ppr tvs <+> hsep (map ppr pat_tys) <+> char '=' <+> ppr ty
-
 pprIfaceDeclHead :: IfaceContext -> OccName -> [IfaceTvBndr] -> SDoc
 pprIfaceDeclHead context thing tyvars
   = hsep [pprIfaceContext context, parenSymOcc thing (ppr thing),
@@ -837,12 +831,7 @@ freeNamesIfContext = fnList freeNamesIfType
 freeNamesIfAT :: IfaceAT -> NameSet
 freeNamesIfAT (IfaceAT decl defs)
   = freeNamesIfDecl decl &&&
-    fnList fn_at_def defs
-  where
-    fn_at_def (IfaceATD tvs pat_tys ty)
-      = freeNamesIfTvBndrs tvs &&&
-        fnList freeNamesIfType pat_tys &&&
-        freeNamesIfType ty
+    fnList freeNamesIfAxBranch defs
 
 freeNamesIfClsSig :: IfaceClassOp -> NameSet
 freeNamesIfClsSig (IfaceClassOp _n _dm ty) = freeNamesIfType ty
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
index f145ec1a3a..b7ebe917bf 100644
--- a/compiler/iface/MkIface.lhs
+++ b/compiler/iface/MkIface.lhs
@@ -63,6 +63,7 @@ import FlagChecker
 import Id
 import IdInfo
 import Demand
+import Coercion( tidyCo )
 import Annotations
 import CoreSyn
 import CoreFVs
@@ -1444,18 +1445,18 @@ coAxiomToIfaceDecl :: CoAxiom br -> IfaceDecl
 coAxiomToIfaceDecl ax@(CoAxiom { co_ax_tc = tycon, co_ax_branches = branches })
  = IfaceAxiom { ifName       = name
               , ifTyCon      = toIfaceTyCon tycon
-              , ifAxBranches = brListMap coAxBranchToIfaceBranch branches }
+              , ifAxBranches = brListMap (coAxBranchToIfaceBranch emptyTidyEnv) branches }
  where
    name = getOccName ax
 
 
-coAxBranchToIfaceBranch :: CoAxBranch -> IfaceAxBranch
-coAxBranchToIfaceBranch (CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs })
+coAxBranchToIfaceBranch :: TidyEnv -> CoAxBranch -> IfaceAxBranch
+coAxBranchToIfaceBranch env0 (CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs })
   = IfaceAxBranch { ifaxbTyVars = toIfaceTvBndrs tv_bndrs
-                  , ifaxbLHS    = map (tidyToIfaceType env) lhs
-                  , ifaxbRHS    = tidyToIfaceType env rhs }
+                  , ifaxbLHS    = map (tidyToIfaceType env1) lhs
+                  , ifaxbRHS    = tidyToIfaceType env1 rhs }
   where
-    (env, tv_bndrs) = tidyTyVarBndrs emptyTidyEnv tvs
+    (env1, tv_bndrs) = tidyTyVarBndrs env0 tvs
 
 -----------------
 tyConToIfaceDecl :: TidyEnv -> TyCon -> IfaceDecl
@@ -1549,14 +1550,7 @@ classToIfaceDecl env clas
     
     toIfaceAT :: ClassATItem -> IfaceAT
     toIfaceAT (tc, defs)
-      = IfaceAT (tyConToIfaceDecl env1 tc) (map to_if_at_def defs)
-      where
-        to_if_at_def (ATD tvs pat_tys ty _loc)
-          = IfaceATD (toIfaceTvBndrs tvs') 
-                     (map (tidyToIfaceType env2) pat_tys) 
-                     (tidyToIfaceType env2 ty)
-          where
-            (env2, tvs') = tidyTyClTyVarBndrs env1 tvs
+      = IfaceAT (tyConToIfaceDecl env1 tc) (map (coAxBranchToIfaceBranch env1) defs)
 
     toIfaceClassOp (sel_id, def_meth)
         = ASSERT(sel_tyvars == clas_tyvars)
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 3ef0ddcf18..947e4f1787 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -525,14 +525,9 @@ tc_iface_decl _parent ignore_prags
 
    tc_at cls (IfaceAT tc_decl defs_decls)
      = do ATyCon tc <- tc_iface_decl (AssocFamilyTyCon cls) ignore_prags tc_decl
-          defs <- mapM tc_iface_at_def defs_decls
+          defs <- mapM tc_ax_branch defs_decls
           return (tc, defs)
 
-   tc_iface_at_def (IfaceATD tvs pat_tys ty) =
-       bindIfaceTyVars_AT tvs $
-         \tvs' -> liftM2 (\pats tys -> ATD tvs' pats tys noSrcSpan)
-                           (mapM tcIfaceType pat_tys) (tcIfaceType ty)
-
    mk_op_doc op_name op_ty = ptext (sLit "Class op") <+> sep [ppr op_name, ppr op_ty]
 
    tc_fd (tvs1, tvs2) = do { tvs1' <- mapM tcIfaceTyVar tvs1
@@ -547,23 +542,23 @@ tc_iface_decl _ _ (IfaceForeign {ifName = rdr_name, ifExtName = ext_name})
 tc_iface_decl _ _ (IfaceAxiom {ifName = ax_occ, ifTyCon = tc, ifAxBranches = branches})
   = do { tc_name     <- lookupIfaceTop ax_occ
        ; tc_tycon    <- tcIfaceTyCon tc
-       ; tc_branches <- mapM tc_branch branches
+       ; tc_branches <- mapM tc_ax_branch branches
        ; let axiom = CoAxiom { co_ax_unique   = nameUnique tc_name
                              , co_ax_name     = tc_name
                              , co_ax_tc       = tc_tycon
                              , co_ax_branches = toBranchList tc_branches
                              , co_ax_implicit = False }
        ; return (ACoAxiom axiom) }
-  where tc_branch :: IfaceAxBranch -> IfL CoAxBranch
-        tc_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs, ifaxbLHS = lhs, ifaxbRHS = rhs })
-          = bindIfaceTyVars tv_bndrs $ \ tvs -> do
-            { tc_lhs <- mapM tcIfaceType lhs
-            ; tc_rhs <- tcIfaceType rhs
-            ; let branch = CoAxBranch { cab_loc = noSrcSpan
-                                      , cab_tvs = tvs
-                                      , cab_lhs = tc_lhs
-                                      , cab_rhs = tc_rhs }
-            ; return branch }
+
+tc_ax_branch :: IfaceAxBranch -> IfL CoAxBranch
+tc_ax_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs, ifaxbLHS = lhs, ifaxbRHS = rhs })
+  = bindIfaceTyVars tv_bndrs $ \ tvs -> do  -- Variables will all be fresh
+    { tc_lhs <- mapM tcIfaceType lhs
+    ; tc_rhs <- tcIfaceType rhs
+    ; return (CoAxBranch { cab_loc = noSrcSpan
+                         , cab_tvs = tvs
+                         , cab_lhs = tc_lhs
+                         , cab_rhs = tc_rhs } ) }
 
 tcIfaceDataCons :: Name -> TyCon -> [TyVar] -> IfaceConDecls -> IfL AlgTyConRhs
 tcIfaceDataCons tycon_name tycon _ if_cons
diff --git a/compiler/main/DriverPipeline.hs b/compiler/main/DriverPipeline.hs
index c24bb51833..81d0bc0165 100644
--- a/compiler/main/DriverPipeline.hs
+++ b/compiler/main/DriverPipeline.hs
@@ -1454,14 +1454,17 @@ runPhase LlvmLlc input_fn dflags
                                       else if (elem VFPv3D16 ext)
                                            then ["-mattr=+v7,+vfp3,+d16"]
                                            else []
+                   ArchARM ARMv6 ext _ -> if (elem VFPv2 ext)
+                                          then ["-mattr=+v6,+vfp2"]
+                                          else ["-mattr=+v6"]
                    _                 -> []
         -- On Ubuntu/Debian with ARM hard float ABI, LLVM's llc still
         -- compiles into soft-float ABI. We need to explicitly set abi
         -- to hard
         abiOpts = case platformArch (targetPlatform dflags) of
-                    ArchARM ARMv7 _ HARD -> ["-float-abi=hard"]
-                    ArchARM ARMv7 _ _    -> []
-                    _                    -> []
+                    ArchARM _ _ HARD -> ["-float-abi=hard"]
+                    ArchARM _ _ _    -> []
+                    _                -> []
 
         sseOpts | isSse4_2Enabled dflags = ["-mattr=+sse42"]
                 | isSse2Enabled dflags   = ["-mattr=+sse2"]
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index feadd3d6a8..5160f5a5d8 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -119,6 +119,8 @@ module DynFlags (
         mAX_PTR_TAG,
         tARGET_MIN_INT, tARGET_MAX_INT, tARGET_MAX_WORD,
 
+        unsafeGlobalDynFlags, setUnsafeGlobalDynFlags,
+
         -- * SSE
         isSse2Enabled,
         isSse4_2Enabled,
@@ -136,7 +138,6 @@ import Config
 import CmdLineParser
 import Constants
 import Panic
-import StaticFlags
 import Util
 import Maybes           ( orElse )
 import MonadUtils
@@ -149,9 +150,7 @@ import Foreign.C        ( CInt(..) )
 #endif
 import {-# SOURCE #-} ErrUtils ( Severity(..), MsgDoc, mkLocMessage )
 
-#ifdef GHCI
 import System.IO.Unsafe ( unsafePerformIO )
-#endif
 import Data.IORef
 import Control.Monad
 
@@ -3407,6 +3406,23 @@ makeDynFlagsConsistent dflags
           arch = platformArch platform
           os   = platformOS   platform
 
+--------------------------------------------------------------------------
+-- Do not use unsafeGlobalDynFlags!
+--
+-- unsafeGlobalDynFlags is a hack, necessary because we need to be able
+-- to show SDocs when tracing, but we don't always have DynFlags
+-- available.
+--
+-- Do not use it if you can help it. You may get the wrong value!
+
+GLOBAL_VAR(v_unsafeGlobalDynFlags, panic "v_unsafeGlobalDynFlags: not initialised", DynFlags)
+
+unsafeGlobalDynFlags :: DynFlags
+unsafeGlobalDynFlags = unsafePerformIO $ readIORef v_unsafeGlobalDynFlags
+
+setUnsafeGlobalDynFlags :: DynFlags -> IO ()
+setUnsafeGlobalDynFlags = writeIORef v_unsafeGlobalDynFlags
+
 -- -----------------------------------------------------------------------------
 -- SSE
 
diff --git a/compiler/main/DynFlags.hs-boot b/compiler/main/DynFlags.hs-boot
index 9f22439661..da54e49e66 100644
--- a/compiler/main/DynFlags.hs-boot
+++ b/compiler/main/DynFlags.hs-boot
@@ -5,7 +5,7 @@ import Platform
 
 data DynFlags
 
-targetPlatform :: DynFlags -> Platform
-pprUserLength :: DynFlags -> Int
-pprCols :: DynFlags -> Int
-
+targetPlatform       :: DynFlags -> Platform
+pprUserLength        :: DynFlags -> Int
+pprCols              :: DynFlags -> Int
+unsafeGlobalDynFlags :: DynFlags
diff --git a/compiler/main/GHC.hs b/compiler/main/GHC.hs
index 40e913ee80..35db120849 100644
--- a/compiler/main/GHC.hs
+++ b/compiler/main/GHC.hs
@@ -289,8 +289,7 @@ import DriverPhases     ( Phase(..), isHaskellSrcFilename )
 import Finder
 import HscTypes
 import DynFlags
-import StaticFlagParser
-import qualified StaticFlags
+import StaticFlags
 import SysTools
 import Annotations
 import Module
@@ -446,7 +445,7 @@ initGhcMonad mb_top_dir = do
   -- catch ^C
   liftIO $ installSignalHandlers
 
-  liftIO $ StaticFlags.initStaticOpts
+  liftIO $ initStaticOpts
 
   mySettings <- liftIO $ initSysTools mb_top_dir
   dflags <- liftIO $ initDynFlags (defaultDynFlags mySettings)
diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs
index 8d64900c71..4b23ad010a 100644
--- a/compiler/main/InteractiveEval.hs
+++ b/compiler/main/InteractiveEval.hs
@@ -71,6 +71,7 @@ import Outputable
 import FastString
 import MonadUtils
 
+import System.Mem.Weak
 import System.Directory
 import Data.Dynamic
 import Data.Either
@@ -415,9 +416,19 @@ sandboxIO dflags statusMVar thing =
 --  * clients of the GHC API can terminate a runStmt in progress
 --    without knowing the ThreadId of the sandbox thread (#1381)
 --
+-- NB. use a weak pointer to the thread, so that the thread can still
+-- be considered deadlocked by the RTS and sent a BlockedIndefinitely
+-- exception.  A symptom of getting this wrong is that conc033(ghci)
+-- will hang.
+--
 redirectInterrupts :: ThreadId -> IO a -> IO a
 redirectInterrupts target wait
-  = wait `catch` \e -> do throwTo target (e :: SomeException); wait
+  = do wtid <- mkWeakThreadId target
+       wait `catch` \e -> do
+          m <- deRefWeak wtid
+          case m of
+            Nothing -> wait
+            Just target -> do throwTo target (e :: SomeException); wait
 
 -- We want to turn ^C into a break when -fbreak-on-exception is on,
 -- but it's an async exception and we only break for sync exceptions.
diff --git a/compiler/main/Packages.lhs b/compiler/main/Packages.lhs
index 1c04c2ce8e..52361ce6af 100644
--- a/compiler/main/Packages.lhs
+++ b/compiler/main/Packages.lhs
@@ -230,14 +230,14 @@ readPackageConfig dflags conf_file = do
        else do
             isfile <- doesFileExist conf_file
             when (not isfile) $
-              throwGhcException $ InstallationError $
+              throwGhcExceptionIO $ InstallationError $
                 "can't find a package database at " ++ conf_file
             debugTraceMsg dflags 2 (text "Using package config file:" <+> text conf_file)
             str <- readFile conf_file
             case reads str of
                 [(configs, rest)]
                     | all isSpace rest -> return (map installedPackageInfoToPackageConfig configs)
-                _ -> throwGhcException $ InstallationError $
+                _ -> throwGhcExceptionIO $ InstallationError $
                         "invalid package database file " ++ conf_file
 
   let
@@ -410,12 +410,13 @@ packageFlagErr :: DynFlags
 -- for missing DPH package we emit a more helpful error message, because
 -- this may be the result of using -fdph-par or -fdph-seq.
 packageFlagErr dflags (ExposePackage pkg) [] | is_dph_package pkg
-  = throwGhcException (CmdLineError (showSDoc dflags $ dph_err))
+  = throwGhcExceptionIO (CmdLineError (showSDoc dflags $ dph_err))
   where dph_err = text "the " <> text pkg <> text " package is not installed."
                   $$ text "To install it: \"cabal install dph\"."
         is_dph_package pkg = "dph" `isPrefixOf` pkg
 
-packageFlagErr dflags flag reasons = throwGhcException (CmdLineError (showSDoc dflags $ err))
+packageFlagErr dflags flag reasons
+  = throwGhcExceptionIO (CmdLineError (showSDoc dflags $ err))
   where err = text "cannot satisfy " <> ppr_flag <>
                 (if null reasons then empty else text ": ") $$
               nest 4 (ppr_reasons $$
@@ -983,7 +984,7 @@ closeDeps dflags pkg_map ipid_map ps
 throwErr :: DynFlags -> MaybeErr MsgDoc a -> IO a
 throwErr dflags m
               = case m of
-                Failed e    -> throwGhcException (CmdLineError (showSDoc dflags e))
+                Failed e    -> throwGhcExceptionIO (CmdLineError (showSDoc dflags e))
                 Succeeded r -> return r
 
 closeDepsErr :: PackageConfigMap
@@ -1017,7 +1018,7 @@ add_package pkg_db ipid_map ps (p, mb_parent)
 
 missingPackageErr :: DynFlags -> String -> IO a
 missingPackageErr dflags p
-    = throwGhcException (CmdLineError (showSDoc dflags (missingPackageMsg p)))
+    = throwGhcExceptionIO (CmdLineError (showSDoc dflags (missingPackageMsg p)))
 
 missingPackageMsg :: String -> SDoc
 missingPackageMsg p = ptext (sLit "unknown package:") <+> text p
diff --git a/compiler/main/PprTyThing.hs b/compiler/main/PprTyThing.hs
index a60644155f..c14b853145 100644
--- a/compiler/main/PprTyThing.hs
+++ b/compiler/main/PprTyThing.hs
@@ -31,6 +31,7 @@ import Id
 import TyCon
 import Coercion( pprCoAxiom )
 import HscTypes( tyThingParent_maybe )
+import Type( tidyTopType, tidyOpenType )
 import TcType
 import Name
 import VarEnv( emptyTidyEnv )
diff --git a/compiler/main/StaticFlagParser.hs b/compiler/main/StaticFlagParser.hs
deleted file mode 100644
index 76454bdfa5..0000000000
--- a/compiler/main/StaticFlagParser.hs
+++ /dev/null
@@ -1,151 +0,0 @@
------------------------------------------------------------------------------
---
--- Static flags
---
--- Static flags can only be set once, on the command-line.  Inside GHC,
--- each static flag corresponds to a top-level value, usually of type Bool.
---
--- (c) The University of Glasgow 2005
---
------------------------------------------------------------------------------
-
-module StaticFlagParser (
-        parseStaticFlags,
-        parseStaticFlagsFull,
-        flagsStatic
-    ) where
-
-#include "HsVersions.h"
-
-import qualified StaticFlags as SF
-import StaticFlags ( v_opt_C_ready )
-import CmdLineParser
-import SrcLoc
-import Util
-import Panic
-
-import Control.Monad
-import Data.Char
-import Data.IORef
-import Data.List
-
------------------------------------------------------------------------------
--- Static flags
-
--- | Parses GHC's static flags from a list of command line arguments.
---
--- These flags are static in the sense that they can be set only once and they
--- are global, meaning that they affect every instance of GHC running;
--- multiple GHC threads will use the same flags.
---
--- This function must be called before any session is started, i.e., before
--- the first call to 'GHC.withGhc'.
---
--- Static flags are more of a hack and are static for more or less historical
--- reasons.  In the long run, most static flags should eventually become
--- dynamic flags.
---
--- XXX: can we add an auto-generated list of static flags here?
---
-parseStaticFlags :: [Located String] -> IO ([Located String], [Located String])
-parseStaticFlags = parseStaticFlagsFull flagsStatic
-
--- | Parse GHC's static flags as @parseStaticFlags@ does. However it also
--- takes a list of available static flags, such that certain flags can be
--- enabled or disabled through this argument.
-parseStaticFlagsFull :: [Flag IO] -> [Located String]
-                     -> IO ([Located String], [Located String])
-parseStaticFlagsFull flagsAvailable args = do
-  ready <- readIORef v_opt_C_ready
-  when ready $ throwGhcException (ProgramError "Too late for parseStaticFlags: call it before newSession")
-
-  (leftover, errs, warns) <- processArgs flagsAvailable args
-  when (not (null errs)) $ throwGhcException $ errorsToGhcException errs
-
-    -- see sanity code in staticOpts
-  writeIORef v_opt_C_ready True
-
-  return (leftover, warns)
-
-flagsStatic :: [Flag IO]
--- All the static flags should appear in this list.  It describes how each
--- static flag should be processed.  Two main purposes:
--- (a) if a command-line flag doesn't appear in the list, GHC can complain
--- (b) a command-line flag may remove, or add, other flags; e.g. the "-fno-X" things
---
--- The common (PassFlag addOpt) action puts the static flag into the bunch of
--- things that are searched up by the top-level definitions like
---      opt_foo = lookUp (fsLit "-dfoo")
-
--- Note that ordering is important in the following list: any flag which
--- is a prefix flag (i.e. HasArg, Prefix, OptPrefix, AnySuffix) will override
--- flags further down the list with the same prefix.
-
-flagsStatic = [
-        ------ Debugging ----------------------------------------------------
-    Flag "dppr-debug"                  (PassFlag addOpt)
-  , Flag "dno-debug-output"            (PassFlag addOpt)
-      -- rest of the debugging flags are dynamic
-
-        ----- RTS opts ------------------------------------------------------
-  , Flag "H"              (HasArg (\s -> liftEwM (setHeapSize (fromIntegral (decodeSize s)))))
-
-  , Flag "Rghc-timing"    (NoArg (liftEwM enableTimingStats))
-
-        ------ Compiler flags -----------------------------------------------
-
-        -- All other "-fno-<blah>" options cancel out "-f<blah>" on the hsc cmdline
-  , Flag "fno-"
-         (PrefixPred (\s -> isStaticFlag ("f"++s)) (\s -> removeOpt ("-f"++s)))
-
-
-        -- Pass all remaining "-f<blah>" options to hsc
-  , Flag "f" (AnySuffixPred isStaticFlag addOpt)
-  ]
-
-isStaticFlag :: String -> Bool
-isStaticFlag f =
-  f `elem` [
-    "fdicts-strict",
-    "fspec-inline-join-points",
-    "fno-hi-version-check",
-    "dno-black-holing",
-    "fno-state-hack",
-    "fruntime-types",
-    "fno-opt-coercion",
-    "fno-flat-cache",
-    "fhardwire-lib-paths",
-    "fcpr-off"
-    ]
-  || any (`isPrefixOf` f) [
-     ]
-
------------------------------------------------------------------------------
--- convert sizes like "3.5M" into integers
-
-decodeSize :: String -> Integer
-decodeSize str
-  | c == ""      = truncate n
-  | c == "K" || c == "k" = truncate (n * 1000)
-  | c == "M" || c == "m" = truncate (n * 1000 * 1000)
-  | c == "G" || c == "g" = truncate (n * 1000 * 1000 * 1000)
-  | otherwise            = throwGhcException (CmdLineError ("can't decode size: " ++ str))
-  where (m, c) = span pred str
-        n      = readRational m
-        pred c = isDigit c || c == '.'
-
-
-type StaticP = EwM IO
-
-addOpt :: String -> StaticP ()
-addOpt = liftEwM . SF.addOpt
-
-removeOpt :: String -> StaticP ()
-removeOpt = liftEwM . SF.removeOpt
-
------------------------------------------------------------------------------
--- RTS Hooks
-
-foreign import ccall unsafe "setHeapSize"       setHeapSize       :: Int -> IO ()
-foreign import ccall unsafe "enableTimingStats" enableTimingStats :: IO ()
-
diff --git a/compiler/main/StaticFlags.hs b/compiler/main/StaticFlags.hs
index 8c514a5af3..76845644e0 100644
--- a/compiler/main/StaticFlags.hs
+++ b/compiler/main/StaticFlags.hs
@@ -20,7 +20,8 @@
 -----------------------------------------------------------------------------
 
 module StaticFlags (
-        unsafeGlobalDynFlags, setUnsafeGlobalDynFlags,
+        -- entry point
+        parseStaticFlags,
 
 	staticFlags,
         initStaticOpts,
@@ -38,46 +39,129 @@ module StaticFlags (
 	opt_NoOptCoercion,
         opt_NoFlatCache,
 
-    -- For the parser
-    addOpt, removeOpt, v_opt_C_ready,
+        -- For the parser
+        addOpt, removeOpt, v_opt_C_ready,
 
-    -- Saving/restoring globals
-    saveStaticFlagGlobals, restoreStaticFlagGlobals
+        -- Saving/restoring globals
+        saveStaticFlagGlobals, restoreStaticFlagGlobals
   ) where
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} DynFlags (DynFlags)
-
+import CmdLineParser
 import FastString
+import SrcLoc
 import Util
 -- import Maybes		( firstJusts )
 import Panic
 
 import Control.Monad
+import Data.Char
 import Data.IORef
 import System.IO.Unsafe	( unsafePerformIO )
--- import Data.List
 
---------------------------------------------------------------------------
--- Do not use unsafeGlobalDynFlags!
+
+-----------------------------------------------------------------------------
+-- Static flags
+
+-- | Parses GHC's static flags from a list of command line arguments.
+--
+-- These flags are static in the sense that they can be set only once and they
+-- are global, meaning that they affect every instance of GHC running;
+-- multiple GHC threads will use the same flags.
 --
--- unsafeGlobalDynFlags is a hack, necessary because we need to be able
--- to show SDocs when tracing, but we don't always have DynFlags
--- available.
+-- This function must be called before any session is started, i.e., before
+-- the first call to 'GHC.withGhc'.
 --
--- Do not use it if you can help it. You may get the wrong value!
+-- Static flags are more of a hack and are static for more or less historical
+-- reasons.  In the long run, most static flags should eventually become
+-- dynamic flags.
+--
+-- XXX: can we add an auto-generated list of static flags here?
+--
+parseStaticFlags :: [Located String] -> IO ([Located String], [Located String])
+parseStaticFlags = parseStaticFlagsFull flagsStatic
+
+-- | Parse GHC's static flags as @parseStaticFlags@ does. However it also
+-- takes a list of available static flags, such that certain flags can be
+-- enabled or disabled through this argument.
+parseStaticFlagsFull :: [Flag IO] -> [Located String]
+                     -> IO ([Located String], [Located String])
+parseStaticFlagsFull flagsAvailable args = do
+  ready <- readIORef v_opt_C_ready
+  when ready $ throwGhcException (ProgramError "Too late for parseStaticFlags: call it before newSession")
 
-GLOBAL_VAR(v_unsafeGlobalDynFlags, panic "v_unsafeGlobalDynFlags: not initialised", DynFlags)
+  (leftover, errs, warns) <- processArgs flagsAvailable args
+  when (not (null errs)) $ throwGhcException $ errorsToGhcException errs
 
-unsafeGlobalDynFlags :: DynFlags
-unsafeGlobalDynFlags = unsafePerformIO $ readIORef v_unsafeGlobalDynFlags
+    -- see sanity code in staticOpts
+  writeIORef v_opt_C_ready True
+  return (leftover, warns)
+
+-- holds the static opts while they're being collected, before
+-- being unsafely read by unpacked_static_opts below.
+GLOBAL_VAR(v_opt_C, [], [String])
+GLOBAL_VAR(v_opt_C_ready, False, Bool)
 
-setUnsafeGlobalDynFlags :: DynFlags -> IO ()
-setUnsafeGlobalDynFlags = writeIORef v_unsafeGlobalDynFlags
 
------------------------------------------------------------------------------
--- Static flags
+staticFlags :: [String]
+staticFlags = unsafePerformIO $ do
+  ready <- readIORef v_opt_C_ready
+  if (not ready)
+        then panic "Static flags have not been initialised!\n        Please call GHC.newSession or GHC.parseStaticFlags early enough."
+        else readIORef v_opt_C
+
+-- All the static flags should appear in this list.  It describes how each
+-- static flag should be processed.  Two main purposes:
+-- (a) if a command-line flag doesn't appear in the list, GHC can complain
+-- (b) a command-line flag may remove, or add, other flags; e.g. the "-fno-X" 
+--     things
+--
+-- The common (PassFlag addOpt) action puts the static flag into the bunch of
+-- things that are searched up by the top-level definitions like
+--      opt_foo = lookUp (fsLit "-dfoo")
+
+-- Note that ordering is important in the following list: any flag which
+-- is a prefix flag (i.e. HasArg, Prefix, OptPrefix, AnySuffix) will override
+-- flags further down the list with the same prefix.
+
+flagsStatic :: [Flag IO]
+flagsStatic = [
+  ------ Debugging ----------------------------------------------------
+    Flag "dppr-debug"       (PassFlag addOptEwM)
+  , Flag "dno-debug-output" (PassFlag addOptEwM)
+  -- rest of the debugging flags are dynamic
+
+  ----- RTS opts ------------------------------------------------------
+  , Flag "H"           (HasArg (\s -> liftEwM (setHeapSize (fromIntegral (decodeSize s)))))
+
+  , Flag "Rghc-timing" (NoArg (liftEwM enableTimingStats))
+
+  ------ Compiler flags -----------------------------------------------
+  -- All other "-fno-<blah>" options cancel out "-f<blah>" on the hsc cmdline
+  , Flag "fno-"
+         (PrefixPred (\s -> isStaticFlag ("f"++s)) (\s -> removeOptEwM ("-f"++s)))
+
+  -- Pass all remaining "-f<blah>" options to hsc
+  , Flag "f" (AnySuffixPred isStaticFlag addOptEwM)
+  ]
+
+
+isStaticFlag :: String -> Bool
+isStaticFlag f =
+  f `elem` [
+    "fdicts-strict",
+    "fspec-inline-join-points",
+    "fno-hi-version-check",
+    "dno-black-holing",
+    "fno-state-hack",
+    "fruntime-types",
+    "fno-opt-coercion",
+    "fno-flat-cache",
+    "fhardwire-lib-paths",
+    "fcpr-off"
+    ]
+
 
 initStaticOpts :: IO ()
 initStaticOpts = writeIORef v_opt_C_ready True
@@ -90,24 +174,79 @@ removeOpt f = do
   fs <- readIORef v_opt_C
   writeIORef v_opt_C $! filter (/= f) fs
 
-lookUp	       	 :: FastString -> Bool
+type StaticP = EwM IO
 
--- holds the static opts while they're being collected, before
--- being unsafely read by unpacked_static_opts below.
-GLOBAL_VAR(v_opt_C, [], [String])
-GLOBAL_VAR(v_opt_C_ready, False, Bool)
+addOptEwM :: String -> StaticP ()
+addOptEwM = liftEwM . addOpt
 
-staticFlags :: [String]
-staticFlags = unsafePerformIO $ do
-  ready <- readIORef v_opt_C_ready
-  if (not ready)
-        then panic "Static flags have not been initialised!\n        Please call GHC.newSession or GHC.parseStaticFlags early enough."
-        else readIORef v_opt_C
+removeOptEwM :: String -> StaticP ()
+removeOptEwM = liftEwM . removeOpt
 
 packed_static_opts :: [FastString]
 packed_static_opts   = map mkFastString staticFlags
 
-lookUp     sw = sw `elem` packed_static_opts
+lookUp :: FastString -> Bool
+lookUp sw = sw `elem` packed_static_opts
+
+-- debugging options
+
+opt_PprStyle_Debug :: Bool
+opt_PprStyle_Debug = lookUp  (fsLit "-dppr-debug")
+
+opt_NoDebugOutput  :: Bool
+opt_NoDebugOutput  = lookUp  (fsLit "-dno-debug-output")
+
+-- language opts
+opt_DictsStrict    :: Bool
+opt_DictsStrict	   = lookUp  (fsLit "-fdicts-strict")
+
+opt_NoStateHack    :: Bool
+opt_NoStateHack	   = lookUp  (fsLit "-fno-state-hack")
+
+-- Switch off CPR analysis in the new demand analyser
+opt_CprOff         :: Bool
+opt_CprOff         = lookUp  (fsLit "-fcpr-off")
+
+opt_NoOptCoercion  :: Bool
+opt_NoOptCoercion  = lookUp  (fsLit "-fno-opt-coercion")
+
+opt_NoFlatCache    :: Bool
+opt_NoFlatCache     = lookUp  (fsLit "-fno-flat-cache")
+
+
+-----------------------------------------------------------------------------
+-- Convert sizes like "3.5M" into integers
+
+decodeSize :: String -> Integer
+decodeSize str
+  | c == ""      = truncate n
+  | c == "K" || c == "k" = truncate (n * 1000)
+  | c == "M" || c == "m" = truncate (n * 1000 * 1000)
+  | c == "G" || c == "g" = truncate (n * 1000 * 1000 * 1000)
+  | otherwise            = throwGhcException (CmdLineError ("can't decode size: " ++ str))
+  where (m, c) = span pred str
+        n      = readRational m
+        pred c = isDigit c || c == '.'
+
+
+-----------------------------------------------------------------------------
+-- Tunneling our global variables into a new instance of the GHC library
+
+saveStaticFlagGlobals :: IO (Bool, [String])
+saveStaticFlagGlobals = liftM2 (,) (readIORef v_opt_C_ready) (readIORef v_opt_C)
+
+restoreStaticFlagGlobals :: (Bool, [String]) -> IO ()
+restoreStaticFlagGlobals (c_ready, c) = do
+    writeIORef v_opt_C_ready c_ready
+    writeIORef v_opt_C c
+
+
+-----------------------------------------------------------------------------
+-- RTS Hooks
+
+foreign import ccall unsafe "setHeapSize"       setHeapSize       :: Int -> IO ()
+foreign import ccall unsafe "enableTimingStats" enableTimingStats :: IO ()
+
 
 {-
 -- (lookup_str "foo") looks for the flag -foo=X or -fooX,
@@ -157,39 +296,3 @@ unpacked_opts =
    expandAts l = [l]
 -}
 
--- debugging options
-
-opt_PprStyle_Debug  :: Bool
-opt_PprStyle_Debug              = lookUp  (fsLit "-dppr-debug")
-
-opt_NoDebugOutput   :: Bool
-opt_NoDebugOutput               = lookUp  (fsLit "-dno-debug-output")
-
--- language opts
-opt_DictsStrict :: Bool
-opt_DictsStrict			= lookUp  (fsLit "-fdicts-strict")
-
-opt_NoStateHack :: Bool
-opt_NoStateHack			= lookUp  (fsLit "-fno-state-hack")
-
-opt_CprOff :: Bool
-opt_CprOff			= lookUp  (fsLit "-fcpr-off")
-	-- Switch off CPR analysis in the new demand analyser
-
-opt_NoOptCoercion :: Bool
-opt_NoOptCoercion    	        = lookUp  (fsLit "-fno-opt-coercion")
-
-opt_NoFlatCache :: Bool
-opt_NoFlatCache    	        = lookUp  (fsLit "-fno-flat-cache")
-
------------------------------------------------------------------------------
--- Tunneling our global variables into a new instance of the GHC library
-
-saveStaticFlagGlobals :: IO (Bool, [String])
-saveStaticFlagGlobals = liftM2 (,) (readIORef v_opt_C_ready) (readIORef v_opt_C)
-
-restoreStaticFlagGlobals :: (Bool, [String]) -> IO ()
-restoreStaticFlagGlobals (c_ready, c) = do
-    writeIORef v_opt_C_ready c_ready
-    writeIORef v_opt_C c
-
diff --git a/compiler/main/StaticFlags.hs-boot b/compiler/main/StaticFlags.hs-boot
new file mode 100644
index 0000000000..53ee13bf15
--- /dev/null
+++ b/compiler/main/StaticFlags.hs-boot
@@ -0,0 +1,4 @@
+module StaticFlags where
+
+opt_PprStyle_Debug :: Bool
+opt_NoDebugOutput  :: Bool
diff --git a/compiler/main/TidyPgm.lhs b/compiler/main/TidyPgm.lhs
index 990f6cd8ec..884f6ab61f 100644
--- a/compiler/main/TidyPgm.lhs
+++ b/compiler/main/TidyPgm.lhs
@@ -29,6 +29,7 @@ import Id
 import IdInfo
 import InstEnv
 import FamInstEnv
+import Type             ( tidyTopType )
 import Demand           ( appIsBottom, isTopSig, isBottomingSig )
 import BasicTypes
 import Name hiding (varName)
@@ -39,7 +40,6 @@ import PrelNames
 import IfaceEnv
 import TcEnv
 import TcRnMonad
-import TcType
 import DataCon
 import TyCon
 import Class
diff --git a/compiler/rename/RnSource.lhs b/compiler/rename/RnSource.lhs
index 54cd9a2bcb..81344fe2d5 100644
--- a/compiler/rename/RnSource.lhs
+++ b/compiler/rename/RnSource.lhs
@@ -578,15 +578,10 @@ Renaming of the associated types in instances.
 \begin{code}
 -- rename associated type family decl in class
 rnATDecls :: Name      -- Class
-          -> LHsTyVarBndrs Name
           -> [LFamilyDecl RdrName] 
           -> RnM ([LFamilyDecl Name], FreeVars)
-rnATDecls cls hs_tvs at_decls
-  = rnList (rnFamDecl (Just (cls, tv_ns))) at_decls
-  where
-    tv_ns = hsLTyVarNames hs_tvs
-    -- Type variable binders (but NOT kind variables)
-    -- See Note [Renaming associated types] in RnTypes
+rnATDecls cls at_decls
+  = rnList (rnFamDecl (Just cls)) at_decls
 
 rnATInstDecls :: (Maybe (Name, [Name]) ->    -- The function that renames
                   decl RdrName ->            -- an instance. rnTyFamInstDecl
@@ -950,7 +945,7 @@ rnTyClDecl (ClassDecl {tcdCtxt = context, tcdLName = lcls,
              { (context', cxt_fvs) <- rnContext cls_doc context
              ; fds'  <- rnFds (docOfHsDocContext cls_doc) fds
                          -- The fundeps have no free variables
-             ; (ats',     fv_ats)     <- rnATDecls cls' tyvars' ats
+             ; (ats',     fv_ats)     <- rnATDecls cls' ats
              ; (at_defs', fv_at_defs) <- rnATInstDecls rnTyFamInstDecl cls' tyvars' at_defs
              ; (sigs', sig_fvs) <- renameSigs (ClsDeclCtxt cls') sigs
              ; let fvs = cxt_fvs     `plusFV`
@@ -1045,8 +1040,8 @@ badGadtStupidTheta _
   = vcat [ptext (sLit "No context is allowed on a GADT-style data declaration"),
           ptext (sLit "(You can put a context on each contructor, though.)")]
 
-rnFamDecl :: Maybe (Name, [Name])
-                    -- Just (cls,tvs) => this FamilyDecl is nested 
+rnFamDecl :: Maybe Name
+                    -- Just cls => this FamilyDecl is nested 
                     --             inside an *class decl* for cls
                     --             used for associated types
           -> FamilyDecl RdrName
@@ -1062,7 +1057,6 @@ rnFamDecl mb_cls (FamilyDecl { fdLName = tycon, fdTyVars = tyvars
   where 
      fmly_doc = TyFamilyCtx tycon
      kvs = extractRdrKindSigVars kind
-
 \end{code}
 
 Note [Stupid theta]
diff --git a/compiler/rename/RnTypes.lhs b/compiler/rename/RnTypes.lhs
index 7a44731ccf..bc66eea923 100644
--- a/compiler/rename/RnTypes.lhs
+++ b/compiler/rename/RnTypes.lhs
@@ -360,7 +360,8 @@ bindHsTyVars :: HsDocContext
              -> (LHsTyVarBndrs Name -> RnM (b, FreeVars))
              -> RnM (b, FreeVars)
 -- (a) Bring kind variables into scope 
---     both (i) passed in (kv_bndrs) and (ii) mentioned in the kinds of tv_bndrs
+--     both (i)  passed in (kv_bndrs) 
+--     and  (ii) mentioned in the kinds of tv_bndrs
 -- (b) Bring type variables into scope
 bindHsTyVars doc mb_assoc kv_bndrs tv_bndrs thing_inside
   = do { rdr_env <- getLocalRdrEnv
diff --git a/compiler/simplCore/OccurAnal.lhs b/compiler/simplCore/OccurAnal.lhs
index db652c38f4..63d3329c9b 100644
--- a/compiler/simplCore/OccurAnal.lhs
+++ b/compiler/simplCore/OccurAnal.lhs
@@ -710,7 +710,7 @@ occAnalRec :: SCC (Node Details)
 occAnalRec (AcyclicSCC (ND { nd_bndr = bndr, nd_rhs = rhs, nd_uds = rhs_uds}, _, _))
            (body_uds, binds)
   | not (bndr `usedIn` body_uds)
-  = (body_uds, binds)
+  = (body_uds, binds)           -- See Note [Dead code]
 
   | otherwise                   -- It's mentioned in the body
   = (body_uds' +++ rhs_uds,
@@ -722,7 +722,7 @@ occAnalRec (AcyclicSCC (ND { nd_bndr = bndr, nd_rhs = rhs, nd_uds = rhs_uds}, _,
         -- See Note [Loop breaking]
 occAnalRec (CyclicSCC nodes) (body_uds, binds)
   | not (any (`usedIn` body_uds) bndrs) -- NB: look at body_uds, not total_uds
-  = (body_uds, binds)                           -- Dead code
+  = (body_uds, binds)                   -- See Note [Dead code]
 
   | otherwise   -- At this point we always build a single Rec
   = -- pprTrace "occAnalRec" (vcat
diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs
index f667cd5aeb..2f81ca6088 100644
--- a/compiler/typecheck/FamInst.lhs
+++ b/compiler/typecheck/FamInst.lhs
@@ -1,6 +1,7 @@
 The @FamInst@ type: family instance heads
 
 \begin{code}
+{-# LANGUAGE GADTs #-}
 {-# OPTIONS -fno-warn-tabs #-}
 -- The above warning supression flag is a temporary kludge.
 -- While working on this module you are encouraged to remove it and
@@ -12,20 +13,19 @@ module FamInst (
         checkFamInstConsistency, tcExtendLocalFamInstEnv,
 	tcLookupFamInst, tcLookupDataFamInst,
         tcGetFamInstEnvs,
-
-        freshenFamInstEqn, freshenFamInstEqnLoc,
-        mkFreshenedSynInst, mkFreshenedSynInstLoc
+        newFamInst
     ) where
 
 import HscTypes
 import FamInstEnv
+import InstEnv( roughMatchTcs )
+import Coercion( pprCoAxBranchHdr )
 import LoadIface
 import TypeRep
 import TcRnMonad
 import TyCon
 import CoAxiom
 import DynFlags
-import SrcLoc
 import Module
 import Outputable
 import UniqFM
@@ -33,7 +33,7 @@ import FastString
 import Util
 import Maybes
 import TcMType
-import Type
+import TcType
 import Name
 import Control.Monad
 import Data.Map (Map)
@@ -42,6 +42,47 @@ import qualified Data.Map as Map
 #include "HsVersions.h"
 \end{code}
 
+%************************************************************************
+%*									*
+                 Making a FamInst
+%*									*
+%************************************************************************
+
+\begin{code}
+-- All type variables in a FamInst must be fresh. This function
+-- creates the fresh variables and applies the necessary substitution
+-- It is defined here to avoid a dependency from FamInstEnv on the monad
+-- code.
+newFamInst :: FamFlavor -> Bool -> CoAxiom br -> TcRnIf gbl lcl(FamInst br)
+-- Freshen the type variables of the FamInst branches
+-- Called from the vectoriser monad too, hence the rather general type
+newFamInst flavor is_group axiom@(CoAxiom { co_ax_tc       = fam_tc
+                                          , co_ax_branches = ax_branches })
+  = do { fam_branches <- go ax_branches
+       ; return (FamInst { fi_fam      = tyConName fam_tc
+                         , fi_flavor   = flavor
+                         , fi_branches = fam_branches
+                         , fi_group    = is_group
+                         , fi_axiom    = axiom }) }
+  where
+    go :: BranchList CoAxBranch br -> TcRnIf gbl lcl (BranchList FamInstBranch br)
+    go (FirstBranch br) = do { br' <- go_branch br
+                             ; return (FirstBranch br') }
+    go (NextBranch br brs) = do { br' <- go_branch br
+                                ; brs' <- go brs
+                                ;return (NextBranch br' brs') }
+    go_branch :: CoAxBranch -> TcRnIf gbl lcl FamInstBranch 
+    go_branch (CoAxBranch { cab_tvs = tvs1
+                          , cab_lhs = lhs
+                          , cab_loc = loc
+                          , cab_rhs = rhs })
+       = do { (subst, tvs2) <- tcInstSkolTyVarsLoc loc tvs1
+            ; return (FamInstBranch { fib_tvs   = tvs2
+                                    , fib_lhs   = substTys subst lhs
+                                    , fib_rhs   = substTy  subst rhs
+                                    , fib_tcs   = roughMatchTcs lhs }) }
+\end{code}
+
 
 %************************************************************************
 %*									*
@@ -348,53 +389,3 @@ tcGetFamInstEnvs
   = do { eps <- getEps; env <- getGblEnv
        ; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }
 \end{code}
-
-%************************************************************************
-%*									*
-	Freshening type variables
-%*									*
-%************************************************************************
-
-\begin{code}
-
--- All type variables in a FamInst/CoAxiom must be fresh. This function
--- creates the fresh variables and applies the necessary substitution
--- It is defined here to avoid a dependency from FamInstEnv on the monad
--- code.
-freshenFamInstEqn :: [TyVar] -- original, possibly stale, tyvars
-                  -> [Type]  -- LHS patterns
-                  -> Type    -- RHS
-                  -> TcM ([TyVar], [Type], Type)
-freshenFamInstEqn tvs lhs rhs
-  = do { loc <- getSrcSpanM
-       ; freshenFamInstEqnLoc loc tvs lhs rhs }
-
--- freshenFamInstEqn needs to be called outside the TcM monad:
-freshenFamInstEqnLoc :: SrcSpan
-                     -> [TyVar] -> [Type] -> Type
-                     -> TcRnIf gbl lcl ([TyVar], [Type], Type)
-freshenFamInstEqnLoc loc tvs lhs rhs
-  = do { (subst, tvs') <- tcInstSkolTyVarsLoc loc tvs
-       ; let lhs' = substTys subst lhs
-             rhs' = substTy  subst rhs
-       ; return (tvs', lhs', rhs') }
-
--- Makes an unbranched synonym FamInst, with freshened tyvars
-mkFreshenedSynInst :: Name    -- Unique name for the coercion tycon
-                   -> [TyVar] -- possibly stale tyvars of the coercion
-                   -> TyCon   -- Family tycon
-                   -> [Type]  -- LHS patterns
-                   -> Type    -- RHS
-                   -> TcM (FamInst Unbranched)
-mkFreshenedSynInst name tvs fam_tc inst_tys rep_ty
-  = do { loc <- getSrcSpanM
-       ; mkFreshenedSynInstLoc loc name tvs fam_tc inst_tys rep_ty }
-
-mkFreshenedSynInstLoc :: SrcSpan
-                      -> Name -> [TyVar] -> TyCon -> [Type] -> Type
-                      -> TcRnIf gbl lcl (FamInst Unbranched)
-mkFreshenedSynInstLoc loc name tvs fam_tc inst_tys rep_ty
-  = do { (tvs', inst_tys', rep_ty') <- freshenFamInstEqnLoc loc tvs inst_tys rep_ty
-       ; return $ mkSingleSynFamInst name tvs' fam_tc inst_tys' rep_ty' }
-
-\end{code}
\ No newline at end of file
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index e34b139bfb..b34e58ae15 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -26,6 +26,7 @@ import TcEvidence
 import TcHsType
 import TcPat
 import TcMType
+import Type( tidyOpenType )
 import FunDeps( growThetaTyVars )
 import TyCon
 import TcType
diff --git a/compiler/typecheck/TcGenGenerics.lhs b/compiler/typecheck/TcGenGenerics.lhs
index 3095dac07c..2c752434f8 100644
--- a/compiler/typecheck/TcGenGenerics.lhs
+++ b/compiler/typecheck/TcGenGenerics.lhs
@@ -28,7 +28,8 @@ import TcGenDeriv
 import DataCon
 import TyCon
 import CoAxiom
-import FamInstEnv       ( FamInst )
+import Coercion         ( mkSingleCoAxiom )
+import FamInstEnv       ( FamInst, FamFlavor(..) )
 import FamInst
 import Module           ( Module, moduleName, moduleNameString )
 import IfaceEnv         ( newGlobalBinder )
@@ -419,7 +420,7 @@ tc_mkRepFamInsts gk tycon metaDts mod =
        -- Also consider `R:DInt`, where { data family D x y :: * -> *
        --                               ; data instance D Int a b = D_ a }
   do { -- `rep` = GHC.Generics.Rep or GHC.Generics.Rep1 (type family)
-       rep <- case gk of
+       fam_tc <- case gk of
          Gen0 -> tcLookupTyCon repTyConName
          Gen1 -> tcLookupTyCon rep1TyConName
 
@@ -432,6 +433,7 @@ tc_mkRepFamInsts gk tycon metaDts mod =
 
            tyvar_args = mkTyVarTys tyvars
 
+           appT :: [Type]
            appT = case tyConFamInst_maybe tycon of
                      -- `appT` = D Int a b (data families case)
                      Just (famtycon, apps) ->
@@ -452,8 +454,8 @@ tc_mkRepFamInsts gk tycon metaDts mod =
                    in newGlobalBinder mod (mkGen (nameOccName (tyConName tycon)))
                         (nameSrcSpan (tyConName tycon))
 
-     ; mkFreshenedSynInst rep_name tyvars rep appT repTy
-     }
+     ; let axiom = mkSingleCoAxiom rep_name tyvars fam_tc appT repTy
+     ; newFamInst SynFamilyInst False axiom  }
 
 --------------------------------------------------------------------------------
 -- Type representation
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index cd5e029c61..69b97ce850 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -886,7 +886,7 @@ tcScopedKindVars kv_ns thing_inside
   = tcExtendTyVarEnv (map mkKindSigVar kv_ns) thing_inside
 
 tcHsTyVarBndrs :: LHsTyVarBndrs Name 
-	       -> ([TyVar] -> TcM r)
+	       -> ([TcTyVar] -> TcM r)
 	       -> TcM r
 -- Bind the type variables to skolems, each with a meta-kind variable kind
 tcHsTyVarBndrs (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
@@ -895,7 +895,7 @@ tcHsTyVarBndrs (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
        ; traceTc "tcHsTyVarBndrs" (ppr hs_tvs $$ ppr tvs)
        ; tcExtendTyVarEnv tvs (thing_inside tvs) }
 
-tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TyVar
+tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TcTyVar
 -- Return a type variable 
 -- initialised with a kind variable.
 -- Typically the Kind inside the KindedTyVar will be a tyvar with a mutable kind 
@@ -907,7 +907,7 @@ tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TyVar
 --   instance C (a,b) where
 --     type F (a,b) c = ...
 -- Here a,b will be in scope when processing the associated type instance for F.
--- See Note [Associated type tyvar names] in TyCon
+-- See Note [Associated type tyvar names] in Class
 tcHsTyVarBndr (L _ hs_tv)
   = do { let name = hsTyVarName hs_tv
        ; mb_tv <- tcLookupLcl_maybe name
@@ -915,7 +915,7 @@ tcHsTyVarBndr (L _ hs_tv)
            Just (ATyVar _ tv) -> return tv ;
            _ -> do
        { kind <- case hs_tv of
-                   UserTyVar {} -> newMetaKindVar
+                   UserTyVar {}       -> newMetaKindVar
                    KindedTyVar _ kind -> tcLHsKind kind
        ; return (mkTcTyVar name kind (SkolemTv False)) } } }
 
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index 26b6c755d0..b721a4b93b 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -31,6 +31,7 @@ import TcRnMonad
 import TcValidity
 import TcMType
 import TcType
+import Coercion( mkSingleCoAxiom, mkBranchedCoAxiom, pprCoAxBranch )
 import BuildTyCl
 import Inst
 import InstEnv
@@ -40,6 +41,7 @@ import TcDeriv
 import TcEnv
 import TcHsType
 import TcUnify
+import Unify      ( tcMatchTyX )
 import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
 import CoreSyn    ( DFunArg(..) )
 import Type
@@ -531,14 +533,15 @@ tcClsInstDecl (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                  --            instance C [x]
                  -- Then we want to generate the decl:   type F [x] b = ()
                 | otherwise 
-                = forM defs $ \(ATD _tvs pat_tys rhs _loc) ->
+                = forM defs $ \(CoAxBranch { cab_lhs = pat_tys, cab_rhs = rhs }) ->
                   do { let pat_tys' = substTys mini_subst pat_tys
                            rhs'     = substTy  mini_subst rhs
                            tv_set'  = tyVarsOfTypes pat_tys'
                            tvs'     = varSetElems tv_set'
                      ; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
+                     ; let axiom = mkSingleCoAxiom rep_tc_name tvs' fam_tc pat_tys' rhs'
                      ; ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' ) 
-                       mkFreshenedSynInst rep_tc_name tvs' fam_tc pat_tys' rhs' }
+                       newFamInst SynFamilyInst False {- group -} axiom }
 
         ; tyfam_insts1 <- mapM mk_deflt_at_instances (classATItems clas)
         
@@ -556,6 +559,29 @@ tcClsInstDecl (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
               inst_info = InstInfo { iSpec  = ispec, iBinds = VanillaInst binds uprags False }
 
         ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts) }
+
+--------------
+tcAssocTyDecl :: Class                   -- Class of associated type
+              -> VarEnv Type             -- Instantiation of class TyVars
+              -> LTyFamInstDecl Name     
+              -> TcM (FamInst Unbranched)
+tcAssocTyDecl clas mini_env ldecl@(L loc decl)
+  = setSrcSpan loc $
+    tcAddTyFamInstCtxt decl $
+    do { fam_tc <- tcFamInstDeclCombined NotTopLevel (tyFamInstDeclLName decl)
+       ; fam_inst <- tcTyFamInstDecl (Just (clas, mini_env)) fam_tc ldecl
+       ; return $ toUnbranchedFamInst fam_inst }
+
+--------------
+tcAssocDataDecl :: Class                 -- ^ Class of associated type
+                -> VarEnv Type           -- ^ Instantiation of class TyVars
+                -> LDataFamInstDecl Name -- ^ RHS
+                -> TcM (FamInst Unbranched)
+tcAssocDataDecl clas mini_env ldecl@(L loc decl)
+  = setSrcSpan loc $
+    tcAddDataFamInstCtxt decl $
+    do { fam_tc <- tcFamInstDeclCombined NotTopLevel (dfid_tycon decl)
+       ; tcDataFamInstDecl (Just (clas, mini_env)) fam_tc ldecl }
 \end{code}
 
 %************************************************************************
@@ -569,29 +595,6 @@ class instance heads, but can contain data constructors and hence they share a
 lot of kinding and type checking code with ordinary algebraic data types (and
 GADTs).
 
-Note [Associated type consistency check]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-According to the invariant stated in FamInstEnv, all FamInsts are created
-with *fresh* variables. This is all well and good for matching instances --
-when we don't want a spurious variable collision -- but bad for type checking
-the instance declarations. Consider this example:
-
-  class Cls a where
-    type Typ a
-
-  instance Cls (Maybe b) where
-    type Typ (Maybe b) = Int
-
-When we're checking the class instance, we build the mini_env [a |-> Maybe b].
-Then, we wish to check that the pattern used in the type instance matches.
-If we build the FamInst for the associated type instance before doing this
-check, the check always fails. This is because the FamInst will be built with
-a *fresh* b, which won't be the same as the old, stale b.
-
-Bottom line: we must perform this check before creating the FamInst, even
-though it's a little awkward to do so. (The FamInst packages everything
-nicely, and we have to push around all pieces independently.)
-
 \begin{code}
 tcFamInstDeclCombined :: TopLevelFlag -> Located Name -> TcM TyCon
 tcFamInstDeclCombined top_lvl fam_tc_lname
@@ -622,51 +625,38 @@ tcTyFamInstDecl mb_clsinfo fam_tc (L loc decl@(TyFamInstDecl { tfid_group = grou
                  (notOpenFamily fam_tc)
 
          -- (1) do the work of verifying the synonym group
-       ; quads <- tcSynFamInstDecl fam_tc decl
+       ; co_ax_branches <- tcSynFamInstDecl fam_tc decl
 
-         -- (2) create the branches
-       ; co_ax_branches <- mapM check_valid_mk_branch quads
+         -- (2) check for validity and inaccessibility
+       ; foldlM_ check_valid_branch [] co_ax_branches
 
-         -- (3) construct coercion tycon
+         -- (3) construct coercion axiom
        ; rep_tc_name <- newFamInstAxiomName loc
                                             (tyFamInstDeclName decl)
-                                            (get_typats quads)
-
-         -- (4) check to see if earlier equations dominate a later one
-       ; foldlM_ check_inaccessible_branches [] co_ax_branches
-
-         -- now, build the FamInst
-       ; return $ mkSynFamInst rep_tc_name fam_tc group co_ax_branches }
-
+                                            (map cab_lhs co_ax_branches)
+       ; let axiom = mkBranchedCoAxiom rep_tc_name fam_tc co_ax_branches
+       ; newFamInst SynFamilyInst group axiom }
     where 
-      check_valid_mk_branch :: ([TyVar], [Type], Type, SrcSpan)
-                            -> TcM CoAxBranch
-      check_valid_mk_branch (t_tvs, t_typats, t_rhs, loc)
+      check_valid_branch :: [CoAxBranch]     -- previous
+                         -> CoAxBranch       -- current
+                         -> TcM [CoAxBranch] -- current : previous
+      check_valid_branch prev_branches
+          cur_branch@(CoAxBranch { cab_tvs = t_tvs, cab_lhs = t_typats
+                                 , cab_rhs = t_rhs, cab_loc = loc })
         = setSrcSpan loc $
-          do { -- check the well-formedness of the instance
+          do { -- Check the well-formedness of the instance
                checkValidTyFamInst fam_tc t_tvs t_typats t_rhs
 
-               -- check that type patterns match the class instance head
-             ; tcAssocFamInst mb_clsinfo loc (ptext (sLit "type")) fam_tc t_typats
-
-               -- make fresh tyvars for axiom
-             ; (t_tvs', t_typats', t_rhs')
-                 <- freshenFamInstEqn t_tvs t_typats t_rhs
+               -- Check that type patterns match the class instance head
+             ; checkConsistentFamInst mb_clsinfo (ptext (sLit "type")) fam_tc t_tvs t_typats
 
-             ; return $ mkCoAxBranch loc t_tvs' t_typats' t_rhs' }
+               -- Check whether the branch is dominated by earlier
+               -- ones and hence is inaccessible
+             ; when (t_typats `isDominatedBy` prev_branches) $
+               addErrTc $ inaccessibleCoAxBranch fam_tc cur_branch
 
-      check_inaccessible_branches :: [CoAxBranch]     -- previous
-                                  -> CoAxBranch       -- current
-                                  -> TcM [CoAxBranch] -- current : previous
-      check_inaccessible_branches prev_branches
-                                  cur_branch@(CoAxBranch { cab_lhs = tys })
-        = setSrcSpan (coAxBranchSpan cur_branch) $
-          do { when (tys `isDominatedBy` prev_branches) $
-                    addErrTc $ inaccessibleCoAxBranch fam_tc cur_branch
              ; return $ cur_branch : prev_branches }
 
-      get_typats = map (\(_, tys, _, _) -> tys)
-
 tcDataFamInstDecl :: Maybe (Class, VarEnv Type)
                   -> TyCon -> LDataFamInstDecl Name -> TcM (FamInst Unbranched)
   -- "newtype instance" and "data instance"
@@ -676,7 +666,8 @@ tcDataFamInstDecl mb_clsinfo fam_tc
              , dfid_tycon = fam_tc_name
              , dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                                            , dd_ctxt = ctxt, dd_cons = cons } }))
-  = do { -- Check that the family declaration is for the right kind
+  = setSrcSpan loc $
+    do { -- Check that the family declaration is for the right kind
          checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
        ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
 
@@ -684,18 +675,18 @@ tcDataFamInstDecl mb_clsinfo fam_tc
        ; tcFamTyPats fam_tc pats (kcDataDefn defn) $ 
            \tvs' pats' res_kind -> do
 
-         -- Check that left-hand side contains no type family applications
+       { -- Check that left-hand side contains no type family applications
          -- (vanilla synonyms are fine, though, and we checked for
-         -- foralls earlier)
-       { checkValidFamPats fam_tc tvs' pats'
+         --  foralls earlier)
+         checkValidFamPats fam_tc tvs' pats'
+         -- Check that type patterns match class instance head, if any
+       ; checkConsistentFamInst mb_clsinfo (ppr new_or_data) fam_tc tvs' pats'
          
          -- Result kind must be '*' (otherwise, we have too few patterns)
        ; checkTc (isLiftedTypeKind res_kind) $ tooFewParmsErr (tyConArity fam_tc)
 
        ; stupid_theta <- tcHsContext ctxt
        ; h98_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta cons
-         -- Check that type patterns match class instance head, if any
-       ; tcAssocFamInst mb_clsinfo loc (ppr new_or_data) fam_tc pats'
 
          -- Construct representation tycon
        ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
@@ -710,11 +701,10 @@ tcDataFamInstDecl mb_clsinfo fam_tc
                      NewType  -> ASSERT( not (null data_cons) )
                                  mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
               -- freshen tyvars
-              ; (subst, tvs'') <- tcInstSkolTyVars tvs'
-              ; let pats''   = substTys subst pats'
-                    fam_inst = mkDataFamInst axiom_name tvs'' fam_tc pats'' rep_tc
-                    parent   = FamInstTyCon (famInstAxiom fam_inst) fam_tc pats''
-                    rep_tc   = buildAlgTyCon rep_tc_name tvs'' cType stupid_theta tc_rhs 
+              ; let axiom    = mkSingleCoAxiom axiom_name tvs' fam_tc pats' 
+                                               (mkTyConApp rep_tc (mkTyVarTys tvs'))
+                    parent   = FamInstTyCon axiom fam_tc pats'
+                    rep_tc   = buildAlgTyCon rep_tc_name tvs' cType stupid_theta tc_rhs 
                                              Recursive 
                                              False      -- No promotable to the kind level
                                              h98_syntax parent
@@ -723,65 +713,135 @@ tcDataFamInstDecl mb_clsinfo fam_tc
                  -- further instance might not introduce a new recursive
                  -- dependency.  (2) They are always valid loop breakers as
                  -- they involve a coercion.
+              ; fam_inst <- newFamInst (DataFamilyInst rep_tc) False axiom
               ; return (rep_tc, fam_inst) }
 
          -- Remember to check validity; no recursion to worry about here
        ; checkValidTyCon rep_tc
        ; return fam_inst } }
+\end{code}
+
+
+Note [Associated type instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We allow this:
+  class C a where
+    type T x a
+  instance C Int where
+    type T (S y) Int = y
+    type T Z     Int = Char
 
+Note that 
+  a) The variable 'x' is not bound by the class decl
+  b) 'x' is instantiated to a non-type-variable in the instance
+  c) There are several type instance decls for T in the instance
 
-----------------
--- See Note [Associated type consistency check]
-tcAssocFamInst :: Maybe (Class
-               ,  VarEnv Type)       -- ^ Class of associated type
-                                     -- and instantiation of class TyVars
-               -> SrcSpan            -- ^ Of the family instance
+All this is fine.  Of course, you can't give any *more* instances
+for (T ty Int) elsewhere, becuase it's an *associated* type.
+
+Note [Checking consistent instantiation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  class C a b where
+    type T a x b
+
+  instance C [p] Int
+    type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
+                                --    type TR p y = (p,y,y)
+
+So we 
+  * Form the mini-envt from the class type variables a,b
+    to the instance decl types [p],Int:   [a->[p], b->Int]
+
+  * Look at the tyvars a,x,b of the type family constructor T
+    (it shares tyvars with the class C)
+
+  * Apply the mini-evnt to them, and check that the result is
+    consistent with the instance types [p] y Int
+
+We do *not* assume (at this point) the the bound variables of 
+the assoicated type instance decl are the same as for the parent
+instance decl. So, for example,
+
+  instance C [p] Int
+    type T [q] y Int = ...
+
+would work equally well. Reason: making the *kind* variables line
+up is much harder. Example (Trac #7282):
+  class Foo (xs :: [k]) where
+     type Bar xs :: *
+
+   instance Foo '[] where
+     type Bar '[] = Int
+Here the instance decl really looks like
+   instance Foo k ('[] k) where
+     type Bar k ('[] k) = Int
+but the k's are not scoped, and hence won't match Uniques.
+
+So instead we just match structure, with tcMatchTyX, and check
+that distinct type variales match 1-1 with distinct type variables.
+
+HOWEVER, we *still* make the instance type variables scope over the
+type instances, to pick up non-obvious kinds.  Eg
+   class Foo (a :: k) where
+      type F a
+   instance Foo (b :: k -> k) where
+      type F b = Int
+Here the instance is kind-indexed and really looks like
+      type F (k->k) (b::k->k) = Int
+But if the 'b' didn't scope, we would make F's instance too
+poly-kinded.
+
+\begin{code}
+checkConsistentFamInst 
+               :: Maybe ( Class
+                        , VarEnv Type )  -- ^ Class of associated type
+                                         -- and instantiation of class TyVars
                -> SDoc               -- ^ "flavor" of the instance
                -> TyCon              -- ^ Family tycon
+               -> [TyVar]            -- ^ Type variables of the family instance
                -> [Type]             -- ^ Type patterns from instance
                -> TcM ()
-tcAssocFamInst Nothing _ _ _ _ = return ()
-tcAssocFamInst (Just (clas, mini_env)) loc flav fam_tc at_tys
-  = setSrcSpan loc $
-    tcAddFamInstCtxt flav (tyConName fam_tc) $
-    do {
-       -- Check that the associated type comes from this class
+-- See Note [Checking consistent instantiation]
+
+checkConsistentFamInst Nothing _ _ _ _ = return ()
+checkConsistentFamInst (Just (clas, mini_env)) flav fam_tc at_tvs at_tys
+  = tcAddFamInstCtxt flav (tyConName fam_tc) $
+    do { -- Check that the associated type indeed comes from this class
          checkTc (Just clas == tyConAssoc_maybe fam_tc)
                  (badATErr (className clas) (tyConName fam_tc))
 
-       -- See Note [Checking consistent instantiation] in TcTyClsDecls
-       ; zipWithM_ check_arg (tyConTyVars fam_tc) at_tys }
+         -- See Note [Checking consistent instantiation] in TcTyClsDecls
+         -- Check right to left, so that we spot type variable
+         -- inconsistencies before (more confusing) kind variables
+       ; discardResult $ foldrM check_arg emptyTvSubst $
+                         tyConTyVars fam_tc `zip` at_tys }
   where
-    check_arg fam_tc_tv at_ty
+    at_tv_set = mkVarSet at_tvs
+
+    check_arg :: (TyVar, Type) -> TvSubst -> TcM TvSubst
+    check_arg (fam_tc_tv, at_ty) subst
       | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
-      = checkTc (inst_ty `eqType` at_ty) 
-                (wrongATArgErr at_ty inst_ty)
+      = case tcMatchTyX at_tv_set subst at_ty inst_ty of
+           Just subst | all_distinct subst -> return subst
+           _ -> failWithTc $ wrongATArgErr at_ty inst_ty
                 -- No need to instantiate here, becuase the axiom
                 -- uses the same type variables as the assocated class
       | otherwise
-      = return ()   -- Allow non-type-variable instantiation
-                    -- See Note [Associated type instances]
+      = return subst   -- Allow non-type-variable instantiation
+                       -- See Note [Associated type instances]
 
-tcAssocTyDecl :: Class                   -- Class of associated type
-              -> VarEnv Type             -- Instantiation of class TyVars
-              -> LTyFamInstDecl Name     
-              -> TcM (FamInst Unbranched)
-tcAssocTyDecl clas mini_env ldecl@(L loc decl)
-  = setSrcSpan loc $
-    tcAddTyFamInstCtxt decl $
-    do { fam_tc <- tcFamInstDeclCombined NotTopLevel (tyFamInstDeclLName decl)
-       ; fam_inst <- tcTyFamInstDecl (Just (clas, mini_env)) fam_tc ldecl
-       ; return $ toUnbranchedFamInst fam_inst }
-
-tcAssocDataDecl :: Class                 -- ^ Class of associated type
-                -> VarEnv Type           -- ^ Instantiation of class TyVars
-                -> LDataFamInstDecl Name -- ^ RHS
-                -> TcM (FamInst Unbranched)
-tcAssocDataDecl clas mini_env ldecl@(L loc decl)
-  = setSrcSpan loc $
-    tcAddDataFamInstCtxt decl $
-    do { fam_tc <- tcFamInstDeclCombined NotTopLevel (dfid_tycon decl)
-       ; tcDataFamInstDecl (Just (clas, mini_env)) fam_tc ldecl }
+    all_distinct :: TvSubst -> Bool
+    -- True if all the variables mapped the substitution 
+    -- map to *distinct* type *variables*
+    all_distinct subst = go [] at_tvs
+       where
+         go _   []       = True
+         go acc (tv:tvs) = case lookupTyVar subst tv of
+                             Nothing -> go acc tvs
+                             Just ty | Just tv' <- tcGetTyVar_maybe ty
+                                     , tv' `notElem` acc
+                                     -> go (tv' : acc) tvs
+                             _other -> False
 \end{code}
 
 
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 8af1e4c57e..f0dd6e9ddd 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -547,9 +547,12 @@ defaultKindVarToStar kv
 
 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
 -- A kind variable k may occur *after* a tyvar mentioning k in its kind
+-- Can be given a mixture of TcTyVars and TyVars, in the case of
+-- associated type declarations
 zonkQuantifiedTyVars tyvars
   = do { let (kvs, tvs) = partition isKindVar tyvars
-             (meta_kvs, skolem_kvs) = partition isMetaTyVar kvs
+             (meta_kvs, skolem_kvs) 
+                  = partition (\kv -> isTcTyVar kv && isMetaTyVar kv) kvs
 
              -- In the non-PolyKinds case, default the kind variables
              -- to *, and zonk the tyvars as usual.  Notice that this
@@ -562,10 +565,16 @@ zonkQuantifiedTyVars tyvars
                       do { mapM_ defaultKindVarToStar meta_kvs
                          ; return skolem_kvs }  -- Should be empty
 
-       ; mapM zonkQuantifiedTyVar (qkvs ++ tvs) }
+       ; mapM zonk_quant (qkvs ++ tvs) }
            -- Because of the order, any kind variables
            -- mentioned in the kinds of the type variables refer to
            -- the now-quantified versions
+  where
+    zonk_quant tkv
+      | isTcTyVar tkv = zonkQuantifiedTyVar tkv
+      | otherwise     = return tkv
+      -- For associated types, we have the class variables 
+      -- in scope, and they are TyVars not TcTyVars
 
 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 -- The quantified type variables often include meta type variables
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index 2da70231f2..db4902bbf8 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -42,7 +42,6 @@ import FamInstEnv
 import TcAnnotations
 import TcBinds
 import HeaderInfo       ( mkPrelImports )
-import TcType   ( tidyTopType )
 import TcDefaults
 import TcEnv
 import TcRules
@@ -77,6 +76,7 @@ import Outputable
 import DataCon
 import Type
 import Class
+import CoAxiom  ( CoAxBranch(..) )
 import TcType   ( orphNamesOfDFunHead )
 import Inst     ( tcGetInstEnvs )
 import Data.List ( sortBy )
@@ -748,7 +748,8 @@ checkBootTyCon tc1 tc2
            eqListBy eqATDef def_ats1 def_ats2
 
        -- Ignore the location of the defaults
-       eqATDef (ATD tvs1 ty_pats1 ty1 _loc1) (ATD tvs2 ty_pats2 ty2 _loc2)
+       eqATDef (CoAxBranch { cab_tvs = tvs1, cab_lhs =  ty_pats1, cab_rhs = ty1 })
+               (CoAxBranch { cab_tvs = tvs2, cab_lhs =  ty_pats2, cab_rhs = ty2 })
          | Just env <- eqTyVarBndrs emptyRnEnv2 tvs1 tvs2
          = eqListBy (eqTypeX env) ty_pats1 ty_pats2 &&
            eqTypeX env ty1 ty2
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 24ca540dbc..1d0748da8d 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -43,9 +43,11 @@ import TcMType
 import TcType
 import TysWiredIn( unitTy )
 import FamInst
+import Coercion( mkCoAxBranch )
 import Type
 import Kind
 import Class
+import CoAxiom( CoAxBranch(..) )
 import TyCon
 import DataCon
 import Id
@@ -596,49 +598,40 @@ tcTyClDecl1 _parent rec_info
 	    , tcdFDs = fundeps, tcdSigs = sigs
             , tcdATs = ats, tcdATDefs = at_defs })
   = ASSERT( isNoParent _parent )
-    do 
-  { (tvs', ctxt', fds', sig_stuff, gen_dm_env)
-       <- tcTyClTyVars class_name tvs $ \ tvs' kind -> do
-          { MASSERT( isConstraintKind kind )
-
-          ; ctxt' <- tcHsContext ctxt
-          ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'  
-                  -- Squeeze out any kind unification variables
-          ; fds'  <- mapM (addLocM tc_fundep) fundeps
-          ; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
-          ; env <- getLclTypeEnv
-          ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds' $$  ppr env)
-          ; return (tvs', ctxt', fds', sig_stuff, gen_dm_env) }
-
-
-
-  ; clas <- fixM $ \ clas -> do
-	    { let 	-- This little knot is just so we can get
+    do { (clas, tvs', gen_dm_env) <- fixM $ \ ~(clas,_,_) ->
+	    tcTyClTyVars class_name tvs $ \ tvs' kind ->
+            do { MASSERT( isConstraintKind kind )
+               ; let 	-- This little knot is just so we can get
 			-- hold of the name of the class TyCon, which we
 			-- need to look up its recursiveness
 		    tycon_name = tyConName (classTyCon clas)
 		    tc_isrec = rti_is_rec rec_info tycon_name
 
-            ; at_stuff <- tcClassATs class_name (AssocFamilyTyCon clas) ats at_defs
-
-            ; buildClass False {- Must include unfoldings for selectors -}
-			 class_name tvs' ctxt' fds' at_stuff
-			 sig_stuff tc_isrec }
-
-  ; let gen_dm_ids = [ AnId (mkExportedLocalId gen_dm_name gen_dm_ty)
-                     | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
-                     , let gen_dm_tau = expectJust "tcTyClDecl1" $
-                                        lookupNameEnv gen_dm_env (idName sel_id)
-		     , let gen_dm_ty = mkSigmaTy tvs' 
-                                                 [mkClassPred clas (mkTyVarTys tvs')] 
-                                                 gen_dm_tau
-                     ]
-        class_ats = map ATyCon (classATs clas)
-
-  ; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats )
-      -- NB: Order is important due to the call to `mkGlobalThings' when
-      --     tying the the type and class declaration type checking knot.
-  }
+               ; ctxt' <- tcHsContext ctxt
+               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'  
+                       -- Squeeze out any kind unification variables
+               ; fds'  <- mapM (addLocM tc_fundep) fundeps
+               ; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
+               ; at_stuff <- tcClassATs class_name (AssocFamilyTyCon clas) ats at_defs
+               ; clas <- buildClass False {- Must include unfoldings for selectors -}
+	                    class_name tvs' ctxt' fds' at_stuff
+	       		    sig_stuff tc_isrec 
+               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds')
+               ; return (clas, tvs', gen_dm_env) }
+
+       ; let { gen_dm_ids = [ AnId (mkExportedLocalId gen_dm_name gen_dm_ty)
+                            | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
+                     	    , let gen_dm_tau = expectJust "tcTyClDecl1" $
+                     	                       lookupNameEnv gen_dm_env (idName sel_id)
+		     	    , let gen_dm_ty = mkSigmaTy tvs' 
+                     	                              [mkClassPred clas (mkTyVarTys tvs')] 
+                     	                              gen_dm_tau
+                     	    ]
+             ; class_ats = map ATyCon (classATs clas) }
+
+       ; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats ) }
+         -- NB: Order is important due to the call to `mkGlobalThings' when
+         --     tying the the type and class declaration type checking knot.
   where
     tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tc_fd_tyvar tvs1 ;
 				; tvs2' <- mapM tc_fd_tyvar tvs2 ;
@@ -788,19 +781,16 @@ tcClassATs class_name parent ats at_defs
 -------------------------
 tcDefaultAssocDecl :: TyCon                -- ^ Family TyCon
                    -> LTyFamInstDecl Name  -- ^ RHS
-                   -> TcM [ATDefault]      -- ^ Type checked RHS and free TyVars
+                   -> TcM [CoAxBranch]     -- ^ Type checked RHS and free TyVars
 tcDefaultAssocDecl fam_tc (L loc decl)
   = setSrcSpan loc $
     tcAddTyFamInstCtxt decl $
     do { traceTc "tcDefaultAssocDecl" (ppr decl)
-       ; quads <- tcSynFamInstDecl fam_tc decl
-       ; return $ map (uncurry4 ATD) quads }
--- We check for well-formedness and validity later, in checkValidClass
-    where uncurry4 :: (a -> b -> c -> d -> e) -> (a, b, c, d) -> e
-          uncurry4 f (a, b, c, d) = f a b c d
+       ; tcSynFamInstDecl fam_tc decl }
+    -- We check for well-formedness and validity later, in checkValidClass
 
 -------------------------
-tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM [([TyVar], [Type], Type, SrcSpan)]
+tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM [CoAxBranch]
 -- Placed here because type family instances appear as 
 -- default decls in class declarations 
 tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqns = eqns })
@@ -823,7 +813,7 @@ tcSynFamInstNames (L _ first) names
       = setSrcSpan loc $
         failWithTc (msg_fun name)
 
-tcTyFamInstEqn :: TyCon -> LTyFamInstEqn Name -> TcM ([TyVar], [Type], Type, SrcSpan)
+tcTyFamInstEqn :: TyCon -> LTyFamInstEqn Name -> TcM CoAxBranch
 tcTyFamInstEqn fam_tc 
     (L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
   = setSrcSpan loc $
@@ -832,7 +822,7 @@ tcTyFamInstEqn fam_tc
     do { rhs_ty <- tcCheckLHsType hs_ty res_kind
        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
        ; traceTc "tcSynFamInstEqn" (ppr fam_tc <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty))
-       ; return (tvs', pats', rhs_ty, loc) }
+       ; return (mkCoAxBranch tvs' pats' rhs_ty loc) }
 
 kcDataDefn :: HsDataDefn Name -> TcKind -> TcM ()
 -- Used for 'data instance' only
@@ -966,42 +956,6 @@ type variables (a,b), but also over the implicitly mentioned kind varaibles
 none. The role of the kind signature (a :: Maybe k) is to add a constraint
 that 'a' must have that kind, and to bring 'k' into scope.
 
-Note [Associated type instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We allow this:
-  class C a where
-    type T x a
-  instance C Int where
-    type T (S y) Int = y
-    type T Z     Int = Char
-
-Note that 
-  a) The variable 'x' is not bound by the class decl
-  b) 'x' is instantiated to a non-type-variable in the instance
-  c) There are several type instance decls for T in the instance
-
-All this is fine.  Of course, you can't give any *more* instances
-for (T ty Int) elsewhere, becuase it's an *associated* type.
-
-Note [Checking consistent instantiation]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  class C a b where
-    type T a x b
-
-  instance C [p] Int
-    type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
-                                --    type TR p y = (p,y,y)
-
-So we 
-  * Form the mini-envt from the class type variables a,b
-    to the instance decl types [p],Int:   [a->[p], b->Int]
-
-  * Look at the tyvars a,x,b of the type family constructor T
-    (it shares tyvars with the class C)
-
-  * Apply the mini-evnt to them, and check that the result is
-    consistent with the instance types [p] y Int
-
 
 %************************************************************************
 %*                                                                      *
@@ -1459,7 +1413,6 @@ checkValidClass cls
 	; mapM_ (check_op constrained_class_methods) op_stuff
 
         -- Check the associated type defaults are well-formed and instantiated
-        -- See Note [Checking consistent instantiation]
         ; mapM_ check_at_defs at_stuff	}
   where
     (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
@@ -1505,7 +1458,8 @@ checkValidClass cls
 		-- type variable.  What a mess!
 
     check_at_defs (fam_tc, defs)
-      = do { mapM_ (\(ATD tvs pats rhs _loc) -> checkValidTyFamInst fam_tc tvs pats rhs) defs
+      = do { mapM_ (\(CoAxBranch { cab_tvs = tvs, cab_lhs = pats, cab_rhs = rhs })
+                    -> checkValidTyFamInst fam_tc tvs pats rhs) defs
            ; tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $ 
              mapM_ (check_loc_at_def fam_tc) defs }
 
@@ -1520,7 +1474,7 @@ checkValidClass cls
     --  the (C Int Bool)  header
     -- This is not to do with soundness; it's just checking that the
     -- type instance arg is the sam
-    check_loc_at_def fam_tc (ATD _tvs pats _rhs loc)
+    check_loc_at_def fam_tc (CoAxBranch { cab_lhs = pats, cab_loc = loc })
       -- Set the location for each of the default declarations
       = setSrcSpan loc $ zipWithM_ check_arg (tyConTyVars fam_tc) pats
 
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index ba2fa0dc0b..7a69b4b250 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -90,17 +90,6 @@ module TcType (
   -- * Finding "exact" (non-dead) type variables
   exactTyVarsOfType, exactTyVarsOfTypes,
 
-  -- * Tidying type related things up for printing
-  tidyType,      tidyTypes,
-  tidyOpenType,  tidyOpenTypes,
-  tidyOpenKind,
-  tidyTyVarBndr, tidyTyVarBndrs, tidyFreeTyVars,
-  tidyOpenTyVar, tidyOpenTyVars,
-  tidyTyVarOcc,
-  tidyTopType,
-  tidyKind, 
-  tidyCo, tidyCos,
-
   ---------------------------------
   -- Foreign import and export
   isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
@@ -192,7 +181,6 @@ import ListSetOps
 import Outputable
 import FastString
 
-import Data.List( mapAccumL )
 import Data.IORef
 \end{code}
 
@@ -521,149 +509,6 @@ pprUserTypeCtxt (DataTyCtxt tc)   = ptext (sLit "the context of the data type de
 
 
 %************************************************************************
-%*									*
-\subsection{TidyType}
-%*									*
-%************************************************************************
-
-Tidying is here becuase it has a special case for FlatSkol
-
-\begin{code}
--- | This tidies up a type for printing in an error message, or in
--- an interface file.
--- 
--- It doesn't change the uniques at all, just the print names.
-tidyTyVarBndrs :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
-tidyTyVarBndrs env tvs = mapAccumL tidyTyVarBndr env tvs
-
-tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
-tidyTyVarBndr tidy_env@(occ_env, subst) tyvar
-  = case tidyOccName occ_env occ1 of
-      (tidy', occ') -> ((tidy', subst'), tyvar')
-	where
-          subst' = extendVarEnv subst tyvar tyvar'
-          tyvar' = setTyVarKind (setTyVarName tyvar name') kind'
-          name'  = tidyNameOcc name occ'
-          kind'  = tidyKind tidy_env (tyVarKind tyvar)
-  where
-    name = tyVarName tyvar
-    occ  = getOccName name
-    -- System Names are for unification variables;
-    -- when we tidy them we give them a trailing "0" (or 1 etc)
-    -- so that they don't take precedence for the un-modified name
-    occ1 | isSystemName name = mkTyVarOcc (occNameString occ ++ "0")
-         | otherwise         = occ
-
-
----------------
-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 (full_occ_env, var_env) (varSetElems tyvars))
-
-        ---------------
-tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
-tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
-
----------------
-tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
--- ^ Treat a new 'TyVar' as a binder, and give it a fresh tidy name
--- using the environment if one has not already been allocated. See
--- also 'tidyTyVarBndr'
-tidyOpenTyVar env@(_, subst) tyvar
-  = case lookupVarEnv subst tyvar of
-	Just tyvar' -> (env, tyvar')		-- Already substituted
-	Nothing	    -> tidyTyVarBndr env tyvar	-- Treat it as a binder
-
----------------
-tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar
-tidyTyVarOcc (_, subst) tv
-  = case lookupVarEnv subst tv of
-	Nothing  -> tv
-	Just tv' -> tv'
-
----------------
-tidyTypes :: TidyEnv -> [Type] -> [Type]
-tidyTypes env tys = map (tidyType env) tys
-
----------------
-tidyType :: TidyEnv -> Type -> Type
-tidyType _   (LitTy n)            = LitTy n
-tidyType env (TyVarTy tv)	  = TyVarTy (tidyTyVarOcc env tv)
-tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
- 		                    in args `seqList` TyConApp tycon args
-tidyType env (AppTy fun arg)	  = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
-tidyType env (FunTy fun arg)	  = (FunTy $! (tidyType env fun)) $! (tidyType env arg)
-tidyType env (ForAllTy tv ty)	  = ForAllTy tvp $! (tidyType envp ty)
-			          where
-			            (envp, tvp) = tidyTyVarBndr env tv
-
----------------
--- | Grabs the free type variables, tidies them
--- and then uses 'tidyType' to work over the type itself
-tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
-tidyOpenType env ty
-  = (env', tidyType (trimmed_occ_env, var_env) ty)
-  where
-    (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])
-tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
-
----------------
--- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
-tidyTopType :: Type -> Type
-tidyTopType ty = tidyType emptyTidyEnv ty
-
----------------
-tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
-tidyOpenKind = tidyOpenType
-
-tidyKind :: TidyEnv -> Kind -> Kind
-tidyKind = tidyType
-\end{code}
-
-%************************************************************************
-%*									*
-                            Tidying coercions
-%*									*
-%************************************************************************
-
-\begin{code}
-tidyCo :: TidyEnv -> Coercion -> Coercion
-tidyCo env@(_, subst) co
-  = go co
-  where
-    go (Refl ty)             = Refl (tidyType env ty)
-    go (TyConAppCo tc cos)   = let args = map go cos
-                               in args `seqList` TyConAppCo tc args
-    go (AppCo co1 co2)       = (AppCo $! go co1) $! go co2
-    go (ForAllCo tv co)      = ForAllCo tvp $! (tidyCo envp co)
-                               where
-                                 (envp, tvp) = tidyTyVarBndr env tv
-    go (CoVarCo cv)          = case lookupVarEnv subst cv of
-                                 Nothing  -> CoVarCo cv
-                                 Just cv' -> CoVarCo cv'
-    go (AxiomInstCo con ind cos) = let args = tidyCos env cos
-                               in  args `seqList` AxiomInstCo con ind args
-    go (UnsafeCo ty1 ty2)    = (UnsafeCo $! tidyType env ty1) $! tidyType env ty2
-    go (SymCo co)            = SymCo $! go co
-    go (TransCo co1 co2)     = (TransCo $! go co1) $! go co2
-    go (NthCo d co)          = NthCo d $! go co
-    go (LRCo lr co)          = LRCo lr $! go co
-    go (InstCo co ty)        = (InstCo $! go co) $! tidyType env ty
-
-tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
-tidyCos env = map (tidyCo env)
-\end{code}
-
-%************************************************************************
 %*                  *
     Finding type family instances
 %*                  *
diff --git a/compiler/types/Class.lhs b/compiler/types/Class.lhs
index 6ceb7799cd..312ce84525 100644
--- a/compiler/types/Class.lhs
+++ b/compiler/types/Class.lhs
@@ -16,7 +16,7 @@ The @Class@ datatype
 module Class (
 	Class,
         ClassOpItem, DefMeth (..),
-        ClassATItem, ATDefault (..),
+        ClassATItem,
 	defMethSpecOfDefMeth,
 
 	FunDep,	pprFundeps, pprFunDep,
@@ -31,15 +31,14 @@ module Class (
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TyCon	( TyCon, tyConName, tyConUnique )
-import {-# SOURCE #-} TypeRep	( Type, PredType )
-
+import {-# SOURCE #-} TypeRep	( PredType )
+import CoAxiom
 import Var
 import Name
 import BasicTypes
 import Unique
 import Util
 import Outputable
-import SrcLoc
 import FastString
 
 import Data.Typeable (Typeable)
@@ -97,21 +96,10 @@ data DefMeth = NoDefMeth 		-- No default method
              deriving Eq
 
 type ClassATItem = (TyCon,           -- See Note [Associated type tyvar names]
-                    [ATDefault])     -- Default associated types from these templates 
+                    [CoAxBranch])    -- Default associated types from these templates 
   -- We can have more than one default per type; see
   -- Note [Associated type defaults] in TcTyClsDecls
 
--- Each associated type default template is a quad of:
-data ATDefault = ATD { -- TyVars of the RHS and family arguments 
-                       -- (including, but perhaps more than, the class TVs)
-                       atDefaultTys     :: [TyVar],
-                       -- The instantiated family arguments
-                       atDefaultPats    :: [Type],
-                       -- The RHS of the synonym
-                       atDefaultRhs     :: Type,
-                       -- The source location of the synonym
-                       atDefaultSrcSpan :: SrcSpan }
-
 -- | Convert a `DefMethSpec` to a `DefMeth`, which discards the name field in
 --   the `DefMeth` constructor of the `DefMeth`.
 defMethSpecOfDefMeth :: DefMeth -> DefMethSpec
diff --git a/compiler/types/CoAxiom.lhs b/compiler/types/CoAxiom.lhs
index 04e63ef25c..bf432cae49 100644
--- a/compiler/types/CoAxiom.lhs
+++ b/compiler/types/CoAxiom.lhs
@@ -16,7 +16,7 @@ module CoAxiom (
        brListLength, brListNth, brListMap, brListFoldr,
        brListZipWith, brListIndices,
 
-       CoAxiom(..), CoAxBranch(..), mkCoAxBranch,
+       CoAxiom(..), CoAxBranch(..), 
 
        toBranchedAxiom, toUnbranchedAxiom,
        coAxiomName, coAxiomArity, coAxiomBranches,
@@ -219,7 +219,8 @@ data CoAxBranch
   = CoAxBranch
     { cab_loc      :: SrcSpan      -- Location of the defining equation
                                    -- See Note [CoAxiom locations]
-    , cab_tvs      :: [TyVar]      -- Bound type variables
+    , cab_tvs      :: [TyVar]      -- Bound type variables; not necessarily fresh
+                                   -- See Note [CoAxBranch type variables]
     , cab_lhs      :: [Type]       -- Type patterns to match against
     , cab_rhs      :: Type         -- Right-hand side of the equality
     }
@@ -275,12 +276,30 @@ coAxBranchSpan = cab_loc
 isImplicitCoAxiom :: CoAxiom br -> Bool
 isImplicitCoAxiom = co_ax_implicit
 
--- The tyvars must be *fresh*. This CoAxBranch will be put into a
--- FamInst. See Note [Template tyvars are fresh] in InstEnv
-mkCoAxBranch :: SrcSpan -> [TyVar] -> [Type] -> Type -> CoAxBranch
-mkCoAxBranch = CoAxBranch
 \end{code}
 
+Note [CoAxBranch type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In the case of a CoAxBranch of an associated type-family instance, 
+we use the *same* type variables (where possible) as the
+enclosing class or instance.  Consider
+   class C a b where
+     type F x b 
+     type F [y] b = ...     -- Second param must be b
+
+   instance C Int [z] where
+     type F Int [z] = ...   -- Second param must be [z]
+
+In the CoAxBranch in the instance decl (F Int [z]) we use the
+same 'z', so that it's easy to check that that type is the same
+as that in the instance header.  
+
+Similarly in the CoAxBranch for the default decl for F in the
+class decl, we use the same 'b' to make the same check easy.
+
+So, unlike FamInsts, there is no expectation that the cab_tvs
+are fresh wrt each other, or any other CoAxBranch.
+
 Note [CoAxiom locations]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 The source location of a CoAxiom is stored in two places in the
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 3129df378a..3de9c21951 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -15,6 +15,9 @@
 -- more on System FC and how coercions fit into it.
 --
 module Coercion (
+        -- * CoAxioms
+        mkCoAxBranch, mkBranchedCoAxiom, mkSingleCoAxiom,
+
         -- * Main data type
         Coercion(..), Var, CoVar,
         LeftOrRight(..), pickLR,
@@ -70,7 +73,11 @@ module Coercion (
         seqCo,
         
         -- * Pretty-printing
-        pprCo, pprParendCo, pprCoAxiom, 
+        pprCo, pprParendCo, 
+        pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr, 
+
+        -- * Tidying
+        tidyCo, tidyCos,
 
         -- * Other
         applyCo
@@ -88,7 +95,7 @@ import Var
 import VarEnv
 import VarSet
 import Maybes   ( orElse )
-import Name	( Name, NamedThing(..), nameUnique, getSrcSpan )
+import Name	( Name, NamedThing(..), nameUnique, nameModule, getSrcSpan )
 import NameSet
 import OccName 	( parenSymOcc )
 import Util
@@ -96,6 +103,7 @@ import BasicTypes
 import Outputable
 import Unique
 import Pair
+import SrcLoc
 import PrelNames	( funTyConKey, eqPrimTyConKey )
 import Control.Applicative
 import Data.Traversable (traverse, sequenceA)
@@ -105,6 +113,58 @@ import FastString
 import qualified Data.Data as Data hiding ( TyCon )
 \end{code}
 
+
+%************************************************************************
+%*                                                                      *
+           Constructing axioms
+    These functions are here because tidyType etc 
+    are not available in CoAxiom
+%*                                                                      *
+%************************************************************************
+
+Note [Tidy axioms when we build them]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We print out axioms and don't want to print stuff like
+    F k k a b = ...
+Instead we must tidy those kind variables.  See Trac #7524.
+
+
+\begin{code}
+mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
+             -> [Type]  -- LHS patterns
+             -> Type    -- RHS
+             -> SrcSpan
+             -> CoAxBranch
+mkCoAxBranch tvs lhs rhs loc
+  = CoAxBranch { cab_tvs = tvs1
+               , cab_lhs = tidyTypes env lhs
+               , cab_rhs = tidyType  env rhs
+               , cab_loc = loc }
+  where
+    (env, tvs1) = tidyTyVarBndrs emptyTidyEnv tvs
+    -- See Note [Tidy axioms when we build them]
+  
+
+mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
+mkBranchedCoAxiom ax_name fam_tc branches
+  = CoAxiom { co_ax_unique   = nameUnique ax_name
+            , co_ax_name     = ax_name
+            , co_ax_tc       = fam_tc
+            , co_ax_implicit = False
+            , co_ax_branches = toBranchList branches }
+
+mkSingleCoAxiom :: Name -> [TyVar] -> TyCon -> [Type] -> Type -> CoAxiom Unbranched
+mkSingleCoAxiom ax_name tvs fam_tc lhs_tys rhs_ty
+  = CoAxiom { co_ax_unique   = nameUnique ax_name
+            , co_ax_name     = ax_name
+            , co_ax_tc       = fam_tc
+            , co_ax_implicit = False
+            , co_ax_branches = FirstBranch branch }
+  where
+    branch = mkCoAxBranch tvs lhs_tys rhs_ty (getSrcSpan ax_name)
+\end{code}
+
+
 %************************************************************************
 %*									*
             Coercions
@@ -390,6 +450,40 @@ coercionSize (InstCo co ty)      = 1 + coercionSize co + typeSize ty
 
 %************************************************************************
 %*									*
+                            Tidying coercions
+%*									*
+%************************************************************************
+
+\begin{code}
+tidyCo :: TidyEnv -> Coercion -> Coercion
+tidyCo env@(_, subst) co
+  = go co
+  where
+    go (Refl ty)             = Refl (tidyType env ty)
+    go (TyConAppCo tc cos)   = let args = map go cos
+                               in args `seqList` TyConAppCo tc args
+    go (AppCo co1 co2)       = (AppCo $! go co1) $! go co2
+    go (ForAllCo tv co)      = ForAllCo tvp $! (tidyCo envp co)
+                               where
+                                 (envp, tvp) = tidyTyVarBndr env tv
+    go (CoVarCo cv)          = case lookupVarEnv subst cv of
+                                 Nothing  -> CoVarCo cv
+                                 Just cv' -> CoVarCo cv'
+    go (AxiomInstCo con ind cos) = let args = tidyCos env cos
+                               in  args `seqList` AxiomInstCo con ind args
+    go (UnsafeCo ty1 ty2)    = (UnsafeCo $! tidyType env ty1) $! tidyType env ty2
+    go (SymCo co)            = SymCo $! go co
+    go (TransCo co1 co2)     = (TransCo $! go co1) $! go co2
+    go (NthCo d co)          = NthCo d $! go co
+    go (LRCo lr co)          = LRCo lr $! go co
+    go (InstCo co ty)        = (InstCo $! go co) $! tidyType env ty
+
+tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
+tidyCos env = map (tidyCo env)
+\end{code}
+
+%************************************************************************
+%*									*
                    Pretty-printing coercions
 %*                                                                      *
 %************************************************************************
@@ -472,10 +566,25 @@ pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
        2 (vcat (map (pprCoAxBranch tc) $ fromBranchList branches))
 
 pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
-pprCoAxBranch tc (CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs })
-  = ptext (sLit "forall") <+> pprTvBndrs tvs <> dot <+> 
-      pprEqPred (Pair (mkTyConApp tc lhs) rhs)
-
+pprCoAxBranch fam_tc (CoAxBranch { cab_tvs = tvs
+                                 , cab_lhs = lhs
+                                 , cab_rhs = rhs })
+  = hang (ifPprDebug (pprForAll tvs))
+       2 (hang (pprTypeApp fam_tc lhs) 2 (equals <+> (ppr rhs)))
+
+pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
+pprCoAxBranchHdr ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_name = name }) index
+  | CoAxBranch { cab_lhs = tys, cab_loc = loc } <- coAxiomNthBranch ax index
+  = hang (pprTypeApp fam_tc tys)
+       2 (ptext (sLit "-- Defined") <+> ppr_loc loc)
+  where
+        ppr_loc loc
+          | isGoodSrcSpan loc
+          = ptext (sLit "at") <+> ppr (srcSpanStart loc)
+    
+          | otherwise
+          = ptext (sLit "in") <+>
+              quotes (ppr (nameModule name))
 \end{code}
 
 %************************************************************************
@@ -595,7 +704,6 @@ mkAxInstLHS ax index tys
   , (tys1, tys2) <- splitAtList tvs tys
   = ASSERT( tvs `equalLength` tys1 ) 
     mkTyConApp (coAxiomTyCon ax) (substTysWith tvs tys1 lhs ++ tys2)
-  where
 
 mkAxInstRHS ax index tys
   | CoAxBranch { cab_tvs = tvs, cab_rhs = rhs } <- coAxiomNthBranch ax index
diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index f657b5bff6..b0dd91dfad 100644
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -17,9 +17,7 @@ module FamInstEnv (
         famInstTyCon, famInstRepTyCon_maybe, dataFamInstRepTyCon, 
         pprFamInst, pprFamInsts, 
         pprFamFlavor, 
-        pprCoAxBranch, pprCoAxBranchHdr, 
-        mkSynFamInst, mkSingleSynFamInst,
-        mkDataFamInst, mkImportedFamInst, 
+        mkImportedFamInst, 
 
         FamInstEnv, FamInstEnvs,
         emptyFamInstEnvs, emptyFamInstEnv, famInstEnvElts, familyInstances,
@@ -53,13 +51,12 @@ import Outputable
 import Maybes
 import Util
 import FastString
-import SrcLoc
 \end{code}
 
 
 %************************************************************************
 %*                                                                      *
-\subsection{Type checked family instance heads}
+           Type checked family instance heads
 %*                                                                      *
 %************************************************************************
 
@@ -131,8 +128,8 @@ data FamInst br -- See Note [FamInsts and CoAxioms], Note [Branched axioms] in C
 
 data FamInstBranch
   = FamInstBranch
-    { fib_tvs    :: [TyVar]      -- bound type variables
-                                 -- like ClsInsts, these variables are always
+    { fib_tvs    :: [TyVar]      -- Bound type variables
+                                 -- Like ClsInsts, these variables are always
                                  -- fresh. See Note [Template tyvars are fresh]
                                  -- in InstEnv
     , fib_lhs    :: [Type]       -- type patterns
@@ -242,123 +239,8 @@ pprFamFlavor flavor
         | isAbstractTyCon tycon -> ptext (sLit "data")
         | otherwise             -> ptext (sLit "WEIRD") <+> ppr tycon
 
--- defined here to avoid bad dependencies
-pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
-pprCoAxBranch fam_tc (CoAxBranch { cab_lhs = lhs
-                                 , cab_rhs = rhs })
-  = pprTypeApp fam_tc lhs <+> equals <+> (ppr rhs)
-
-pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
-pprCoAxBranchHdr ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_name = name }) index
-  | CoAxBranch { cab_lhs = tys, cab_loc = loc } <- coAxiomNthBranch ax index
-  = hang (pprTypeApp fam_tc tys)
-       2 (ptext (sLit "-- Defined") <+> ppr_loc loc)
-  where
-        ppr_loc loc
-          | isGoodSrcSpan loc
-          = ptext (sLit "at") <+> ppr (srcSpanStart loc)
-    
-          | otherwise
-          = ptext (sLit "in") <+>
-              quotes (ppr (nameModule name))
-
-
 pprFamInsts :: [FamInst br] -> SDoc
 pprFamInsts finsts = vcat (map pprFamInst finsts)
-
-mk_fam_inst_branch :: CoAxBranch -> FamInstBranch
-mk_fam_inst_branch (CoAxBranch { cab_tvs = tvs
-                               , cab_lhs = lhs
-                               , cab_rhs = rhs })
-  = FamInstBranch { fib_tvs   = tvs
-                  , fib_lhs   = lhs
-                  , fib_rhs   = rhs
-                  , fib_tcs   = roughMatchTcs lhs }
-
--- | Create a coercion identifying a @type@ family instance.
--- It has the form @Co tvs :: F ts ~ R@, where @Co@ is
--- the coercion constructor built here, @F@ the family tycon and @R@ the
--- right-hand side of the type family instance.
-mkSynFamInst :: Name            -- ^ Unique name for the coercion tycon
-             -> TyCon           -- ^ Family tycon (@F@)
-             -> Bool            -- ^ Was this declared as a branched group?
-             -> [CoAxBranch]    -- ^ the branches of the CoAxiom
-             -> FamInst Branched
-mkSynFamInst name fam_tc group branches
-  = ASSERT( length branches >= 1 )
-    FamInst { fi_fam      = tyConName fam_tc
-            , fi_flavor   = SynFamilyInst
-            , fi_branches = toBranchList (map mk_fam_inst_branch branches)
-            , fi_group    = group
-            , fi_axiom    = axiom }
-  where
-    axiom = CoAxiom { co_ax_unique   = nameUnique name
-                    , co_ax_name     = name
-                    , co_ax_tc       = fam_tc
-                    , co_ax_implicit = False
-                    , co_ax_branches = toBranchList branches }
-
-
--- | Create a coercion identifying a @type@ family instance, but with only
--- one equation (branch).
-mkSingleSynFamInst :: Name        -- ^ Unique name for the coercion tycon
-                   -> [TyVar]     -- ^ *Fresh* tyvars of the coercion (@tvs@)
-                   -> TyCon       -- ^ Family tycon (@F@)
-                   -> [Type]      -- ^ Type instance (@ts@)
-                   -> Type        -- ^ right-hand side
-                   -> FamInst Unbranched
--- See note [Branched axioms] in CoAxiom.lhs
-mkSingleSynFamInst name tvs fam_tc inst_tys rep_ty
-  = FamInst { fi_fam      = tyConName fam_tc
-            , fi_flavor   = SynFamilyInst
-            , fi_branches = FirstBranch branch
-            , fi_group    = False
-            , fi_axiom    = axiom }
-  where
-    -- See note [FamInst Locations]
-    branch = mk_fam_inst_branch axBranch
-    axiom = CoAxiom { co_ax_unique   = nameUnique name
-                    , co_ax_name     = name
-                    , co_ax_tc       = fam_tc
-                    , co_ax_implicit = False
-                    , co_ax_branches = FirstBranch axBranch }
-    axBranch = CoAxBranch { cab_loc = getSrcSpan name
-                          , cab_tvs = tvs
-                          , cab_lhs = inst_tys
-                          , cab_rhs = rep_ty }
-    
--- | Create a coercion identifying a @data@ or @newtype@ representation type
--- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@,
--- where @Co@ is the coercion constructor built here, @F@ the family tycon
--- and @R@ the (derived) representation tycon.
-mkDataFamInst :: Name         -- ^ Unique name for the coercion tycon
-              -> [TyVar]      -- ^ *Fresh* parameters of the coercion (@tvs@)
-              -> TyCon        -- ^ Family tycon (@F@)
-              -> [Type]       -- ^ Type instance (@ts@)
-              -> TyCon        -- ^ Representation tycon (@R@)
-              -> FamInst Unbranched
-mkDataFamInst name tvs fam_tc inst_tys rep_tc
-  = FamInst { fi_fam      = tyConName fam_tc
-            , fi_flavor   = DataFamilyInst rep_tc
-            , fi_group    = False
-            , fi_branches = FirstBranch branch
-            , fi_axiom    = axiom }
-  where
-    rhs = mkTyConApp rep_tc (mkTyVarTys tvs)
-
-                               -- See Note [FamInst locations]
-    branch = mk_fam_inst_branch axBranch
-    axiom = CoAxiom { co_ax_unique   = nameUnique name
-                    , co_ax_name     = name
-                    , co_ax_tc       = fam_tc
-                    , co_ax_branches = FirstBranch axBranch
-                    , co_ax_implicit = False }
-
-    axBranch = CoAxBranch { cab_loc = getSrcSpan name
-                          , cab_tvs = tvs
-                          , cab_lhs = inst_tys
-                          , cab_rhs = rhs }
-
 \end{code}
 
 Note [Lazy axiom match]
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index a2fab854b5..1add302eb0 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -136,6 +136,16 @@ module Type (
         pprTvBndr, pprTvBndrs, pprForAll, pprSigmaType,
 	pprEqPred, pprTheta, pprThetaArrowTy, pprClassPred, 
         pprKind, pprParendKind, pprSourceTyCon,
+
+        -- * Tidying type related things up for printing
+        tidyType,      tidyTypes,
+        tidyOpenType,  tidyOpenTypes,
+        tidyOpenKind,
+        tidyTyVarBndr, tidyTyVarBndrs, tidyFreeTyVars,
+        tidyOpenTyVar, tidyOpenTyVars,
+        tidyTyVarOcc,
+        tidyTopType,
+        tidyKind, 
     ) where
 
 #include "HsVersions.h"
diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs
index c8235d4146..f83ed38145 100644
--- a/compiler/types/TypeRep.lhs
+++ b/compiler/types/TypeRep.lhs
@@ -47,6 +47,16 @@ module TypeRep (
         -- Free variables
         tyVarsOfType, tyVarsOfTypes,
 
+        -- * Tidying type related things up for printing
+        tidyType,      tidyTypes,
+        tidyOpenType,  tidyOpenTypes,
+        tidyOpenKind,
+        tidyTyVarBndr, tidyTyVarBndrs, tidyFreeTyVars,
+        tidyOpenTyVar, tidyOpenTyVars,
+        tidyTyVarOcc,
+        tidyTopType,
+        tidyKind, 
+
         -- Substitutions
         TvSubst(..), TvSubstEnv
     ) where
@@ -75,6 +85,7 @@ import StaticFlags( opt_PprStyle_Debug )
 import Util
 
 -- libraries
+import Data.List( mapAccumL )
 import qualified Data.Data        as Data hiding ( TyCon )
 \end{code}
 
@@ -730,3 +741,111 @@ pprArrowChain p (arg:args) = maybeParen p FunPrec $
                              sep [arg, sep (map (arrow <+>) args)]
 \end{code}
 
+%************************************************************************
+%*									*
+\subsection{TidyType}
+%*									*
+%************************************************************************
+
+Tidying is here becuase it has a special case for FlatSkol
+
+\begin{code}
+-- | This tidies up a type for printing in an error message, or in
+-- an interface file.
+-- 
+-- It doesn't change the uniques at all, just the print names.
+tidyTyVarBndrs :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
+tidyTyVarBndrs env tvs = mapAccumL tidyTyVarBndr env tvs
+
+tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
+tidyTyVarBndr tidy_env@(occ_env, subst) tyvar
+  = case tidyOccName occ_env occ1 of
+      (tidy', occ') -> ((tidy', subst'), tyvar')
+	where
+          subst' = extendVarEnv subst tyvar tyvar'
+          tyvar' = setTyVarKind (setTyVarName tyvar name') kind'
+          name'  = tidyNameOcc name occ'
+          kind'  = tidyKind tidy_env (tyVarKind tyvar)
+  where
+    name = tyVarName tyvar
+    occ  = getOccName name
+    -- System Names are for unification variables;
+    -- when we tidy them we give them a trailing "0" (or 1 etc)
+    -- so that they don't take precedence for the un-modified name
+    occ1 | isSystemName name = mkTyVarOcc (occNameString occ ++ "0")
+         | otherwise         = occ
+
+
+---------------
+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 (full_occ_env, var_env) (varSetElems tyvars))
+
+        ---------------
+tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
+tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
+
+---------------
+tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
+-- ^ Treat a new 'TyVar' as a binder, and give it a fresh tidy name
+-- using the environment if one has not already been allocated. See
+-- also 'tidyTyVarBndr'
+tidyOpenTyVar env@(_, subst) tyvar
+  = case lookupVarEnv subst tyvar of
+	Just tyvar' -> (env, tyvar')		-- Already substituted
+	Nothing	    -> tidyTyVarBndr env tyvar	-- Treat it as a binder
+
+---------------
+tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar
+tidyTyVarOcc (_, subst) tv
+  = case lookupVarEnv subst tv of
+	Nothing  -> tv
+	Just tv' -> tv'
+
+---------------
+tidyTypes :: TidyEnv -> [Type] -> [Type]
+tidyTypes env tys = map (tidyType env) tys
+
+---------------
+tidyType :: TidyEnv -> Type -> Type
+tidyType _   (LitTy n)            = LitTy n
+tidyType env (TyVarTy tv)	  = TyVarTy (tidyTyVarOcc env tv)
+tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
+ 		                    in args `seqList` TyConApp tycon args
+tidyType env (AppTy fun arg)	  = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
+tidyType env (FunTy fun arg)	  = (FunTy $! (tidyType env fun)) $! (tidyType env arg)
+tidyType env (ForAllTy tv ty)	  = ForAllTy tvp $! (tidyType envp ty)
+			          where
+			            (envp, tvp) = tidyTyVarBndr env tv
+
+---------------
+-- | Grabs the free type variables, tidies them
+-- and then uses 'tidyType' to work over the type itself
+tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
+tidyOpenType env ty
+  = (env', tidyType (trimmed_occ_env, var_env) ty)
+  where
+    (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])
+tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
+
+---------------
+-- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
+tidyTopType :: Type -> Type
+tidyTopType ty = tidyType emptyTidyEnv ty
+
+---------------
+tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
+tidyOpenKind = tidyOpenType
+
+tidyKind :: TidyEnv -> Kind -> Kind
+tidyKind = tidyType
+\end{code}
diff --git a/compiler/utils/Outputable.lhs b/compiler/utils/Outputable.lhs
index 76555eb7ea..4e741b44fb 100644
--- a/compiler/utils/Outputable.lhs
+++ b/compiler/utils/Outputable.lhs
@@ -71,11 +71,12 @@ module Outputable (
     ) where
 
 import {-# SOURCE #-}   DynFlags( DynFlags,
-                                  targetPlatform, pprUserLength, pprCols )
+                                  targetPlatform, pprUserLength, pprCols,
+                                  unsafeGlobalDynFlags )
 import {-# SOURCE #-}   Module( Module, ModuleName, moduleName )
 import {-# SOURCE #-}   Name( Name, nameModule )
+import {-# SOURCE #-}   StaticFlags( opt_PprStyle_Debug, opt_NoDebugOutput )
 
-import StaticFlags
 import FastString
 import FastTypes
 import qualified Pretty
diff --git a/compiler/utils/Panic.lhs b/compiler/utils/Panic.lhs
index c02de1c3de..fc04668ae1 100644
--- a/compiler/utils/Panic.lhs
+++ b/compiler/utils/Panic.lhs
@@ -9,7 +9,9 @@ some unnecessary loops in the module dependency graph.
 
 \begin{code}
 module Panic (
-     GhcException(..), showGhcException, throwGhcException, handleGhcException,
+     GhcException(..), showGhcException,
+     throwGhcException, throwGhcExceptionIO,
+     handleGhcException,
      progName,
      pgmError,
 
@@ -176,6 +178,9 @@ showGhcException exception
 throwGhcException :: GhcException -> a
 throwGhcException = Exception.throw
 
+throwGhcExceptionIO :: GhcException -> IO a
+throwGhcExceptionIO = Exception.throwIO
+
 handleGhcException :: ExceptionMonad m => (GhcException -> m a) -> m a -> m a
 handleGhcException = ghandle
 
diff --git a/compiler/vectorise/Vectorise/Generic/PAMethods.hs b/compiler/vectorise/Vectorise/Generic/PAMethods.hs
index f5cbf93434..af815c9294 100644
--- a/compiler/vectorise/Vectorise/Generic/PAMethods.hs
+++ b/compiler/vectorise/Vectorise/Generic/PAMethods.hs
@@ -23,7 +23,6 @@ import Type
 import OccName
 import Coercion
 import MkId
-import Name
 import FamInst
 
 import DynFlags
@@ -38,7 +37,8 @@ buildPReprTyCon orig_tc vect_tc repr
  = do name      <- mkLocalisedName mkPReprTyConOcc (tyConName orig_tc)
       rhs_ty    <- sumReprType repr
       prepr_tc  <- builtin preprTyCon
-      liftDs $ mkFreshenedSynInstLoc (getSrcSpan name) name tyvars prepr_tc instTys rhs_ty
+      let axiom = mkSingleCoAxiom name tyvars prepr_tc instTys rhs_ty
+      liftDs $ newFamInst SynFamilyInst False axiom
   where
     tyvars = tyConTyVars vect_tc
     instTys = [mkTyConApp vect_tc . mkTyVarTys $ tyConTyVars vect_tc]
diff --git a/compiler/vectorise/Vectorise/Generic/PData.hs b/compiler/vectorise/Vectorise/Generic/PData.hs
index cbedf8d8e0..893f1559be 100644
--- a/compiler/vectorise/Vectorise/Generic/PData.hs
+++ b/compiler/vectorise/Vectorise/Generic/PData.hs
@@ -14,11 +14,13 @@ import Vectorise.Generic.Description
 import Vectorise.Utils
 import Vectorise.Env( GlobalEnv( global_fam_inst_env ) )
 
+import Coercion( mkSingleCoAxiom )
 import BasicTypes
 import BuildTyCl
 import DataCon
 import TyCon
 import Type
+import FamInst
 import FamInstEnv
 import TcMType
 import Name
@@ -45,9 +47,10 @@ buildDataFamInst name' fam_tc vect_tc rhs
  = do { axiom_name <- mkDerivedName mkInstTyCoOcc name'
 
       ; (_, tyvars') <- liftDs $ tcInstSkolTyVarsLoc (getSrcSpan name') tyvars
-      ; let fam_inst = mkDataFamInst axiom_name tyvars' fam_tc pat_tys rep_tc
-            ax       = famInstAxiom fam_inst
-            pat_tys  = [mkTyConApp vect_tc (mkTyVarTys tyvars')]
+      ; let ax       = mkSingleCoAxiom axiom_name tyvars' fam_tc pat_tys rep_ty
+            tys'     = mkTyVarTys tyvars'
+            rep_ty   = mkTyConApp rep_tc tys'
+            pat_tys  = [mkTyConApp vect_tc tys']
             rep_tc   = buildAlgTyCon name'
                            tyvars'
                            Nothing
@@ -57,7 +60,7 @@ buildDataFamInst name' fam_tc vect_tc rhs
                            False       -- Not promotable
                            False       -- not GADT syntax
                            (FamInstTyCon ax fam_tc pat_tys)
-      ; return fam_inst }
+      ; liftDs $ newFamInst (DataFamilyInst rep_tc) False ax }
  where
     tyvars    = tyConTyVars vect_tc
     rec_flag  = boolToRecFlag (isRecursiveTyCon vect_tc)