Merge branch 'master' of http://darcs.haskell.org/ghc into ghc-generics
authorJose Pedro Magalhaes <jpm@cs.uu.nl>
Thu, 12 May 2011 11:26:03 +0000 (13:26 +0200)
committerJose Pedro Magalhaes <jpm@cs.uu.nl>
Thu, 12 May 2011 11:26:03 +0000 (13:26 +0200)
Resolved conflicts:
compiler/typecheck/TcTyClsDecls.lhs

27 files changed:
1  2 
compiler/basicTypes/MkId.lhs
compiler/deSugar/Check.lhs
compiler/hsSyn/HsBinds.lhs
compiler/hsSyn/HsPat.lhs
compiler/hsSyn/HsUtils.lhs
compiler/iface/BinIface.hs
compiler/iface/BuildTyCl.lhs
compiler/iface/IfaceSyn.lhs
compiler/iface/MkIface.lhs
compiler/iface/TcIface.lhs
compiler/main/DynFlags.hs
compiler/prelude/PrelNames.lhs
compiler/prelude/TysWiredIn.lhs
compiler/rename/RnBinds.lhs
compiler/rename/RnTypes.lhs
compiler/typecheck/TcDeriv.lhs
compiler/typecheck/TcEnv.lhs
compiler/typecheck/TcGenDeriv.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcPat.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/types/TyCon.lhs
compiler/types/Type.lhs
docs/users_guide/flags.xml

@@@ -13,7 -13,7 +13,7 @@@ have a standard form, namely
  
  \begin{code}
  module MkId (
 -        mkDictFunId, mkDictFunTy, mkDefaultMethodId, mkDictSelId,
 +        mkDictFunId, mkDictFunTy, mkDictSelId,
  
          mkDataConIds,
          mkPrimOpId, mkFCallId, mkTickBoxOpId, mkBreakPointOpId,
          -- And some particular Ids; see below for why they are wired in
          wiredInIds, ghcPrimIds,
          unsafeCoerceName, unsafeCoerceId, realWorldPrimId, 
-         voidArgId, nullAddrId, seqId, lazyId, lazyIdKey
+         voidArgId, nullAddrId, seqId, lazyId, lazyIdKey,
+         coercionTokenId,
+       -- Re-export error Ids
+       module PrelRules
      ) where
  
  #include "HsVersions.h"
  
  import Rules
  import TysPrim
+ import TysWiredIn     ( unitTy )
  import PrelRules
  import Type
  import Coercion
@@@ -48,7 -53,7 +53,7 @@@ import PrimO
  import ForeignCall
  import DataCon
  import Id
- import Var              ( Var, TyVar, mkCoVar, mkExportedLocalVar )
+ import Var              ( mkExportedLocalVar )
  import IdInfo
  import Demand
  import CoreSyn
@@@ -56,6 -61,7 +61,7 @@@ import Uniqu
  import PrelNames
  import BasicTypes       hiding ( SuccessFlag(..) )
  import Util
+ import Pair
  import Outputable
  import FastString
  import ListSetOps
@@@ -224,7 -230,7 +230,7 @@@ mkDataConIds wrap_name wkr_name data_co
    = DCIds Nothing wrk_id
    where
      (univ_tvs, ex_tvs, eq_spec, 
-      eq_theta, dict_theta, orig_arg_tys, res_ty) = dataConFullSig data_con
+      other_theta, orig_arg_tys, res_ty) = dataConFullSig data_con
      tycon = dataConTyCon data_con       -- The representation TyCon (not family)
  
          ----------- Worker (algebraic data types only) --------------
          -- extra constraints where necessary.
      wrap_tvs    = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
      res_ty_args = substTyVars (mkTopTvSubst eq_spec) univ_tvs
-     eq_tys   = mkPredTys eq_theta
-     dict_tys = mkPredTys dict_theta
-     wrap_ty  = mkForAllTys wrap_tvs $ mkFunTys eq_tys $ mkFunTys dict_tys $
-                mkFunTys orig_arg_tys $ res_ty
-         -- NB: watch out here if you allow user-written equality 
-         --     constraints in data constructor signatures
+     ev_tys      = mkPredTys other_theta
+     wrap_ty     = mkForAllTys wrap_tvs $ 
+                   mkFunTys ev_tys $
+                   mkFunTys orig_arg_tys $ res_ty
  
          ----------- Wrappers for algebraic data types -------------- 
      alg_wrap_id = mkGlobalId (DataConWrapId data_con) wrap_name wrap_ty alg_wrap_info
                      `setStrictnessInfo` Just wrap_sig
  
      all_strict_marks = dataConExStricts data_con ++ dataConStrictMarks data_con
-     wrap_sig = mkStrictSig (mkTopDmdType arg_dmds cpr_info)
-     arg_dmds = map mk_dmd all_strict_marks
+     wrap_sig = mkStrictSig (mkTopDmdType wrap_arg_dmds cpr_info)
+     wrap_stricts = dropList eq_spec all_strict_marks
+     wrap_arg_dmds = map mk_dmd wrap_stricts
      mk_dmd str | isBanged str = evalDmd
                 | otherwise    = lazyDmd
          -- The Cpr info can be important inside INLINE rhss, where the
          --      ...(let w = C x in ...(w p q)...)...
          -- we want to see that w is strict in its two arguments
  
-     wrap_unf = mkInlineUnfolding (Just (length dict_args + length id_args)) wrap_rhs
+     wrap_unf = mkInlineUnfolding (Just (length ev_args + length id_args)) wrap_rhs
      wrap_rhs = mkLams wrap_tvs $ 
-                mkLams eq_args $
-                mkLams dict_args $ mkLams id_args $
+                mkLams ev_args $
+                mkLams id_args $
                 foldr mk_case con_app 
-                      (zip (dict_args ++ id_args) all_strict_marks)
+                      (zip (ev_args ++ id_args) wrap_stricts)
                       i3 []
+            -- The ev_args is the evidence arguments *other than* the eq_spec
+            -- Because we are going to apply the eq_spec args manually in the
+            -- wrapper
  
      con_app _ rep_ids = wrapFamInstBody tycon res_ty_args $
                            Var wrk_id `mkTyApps`  res_ty_args
                                       `mkVarApps` ex_tvs                 
-                                      -- Equality evidence:
-                                      `mkTyApps`  map snd eq_spec
-                                      `mkVarApps` eq_args
+                                      `mkCoApps`  map (mkReflCo . snd) eq_spec
                                       `mkVarApps` reverse rep_ids
  
-     (dict_args,i2) = mkLocals 1  dict_tys
-     (id_args,i3)   = mkLocals i2 orig_arg_tys
-     wrap_arity     = i3-1
-     (eq_args,_)    = mkCoVarLocals i3 eq_tys
-     mkCoVarLocals i []     = ([],i)
-     mkCoVarLocals i (x:xs) = let (ys,j) = mkCoVarLocals (i+1) xs
-                                  y      = mkCoVar (mkSysTvName (mkBuiltinUnique i) 
-                                                   (fsLit "dc_co")) x
-                              in (y:ys,j)
+     (ev_args,i2) = mkLocals 1  ev_tys
+     (id_args,i3) = mkLocals i2 orig_arg_tys
+     wrap_arity   = i3-1
  
      mk_case 
             :: (Id, HsBang)      -- Arg, strictness
@@@ -458,7 -457,7 +457,7 @@@ mkDictSelId no_unf name cla
                                     occNameFS (getOccName name)
                         , ru_fn    = name
                       , ru_nargs = n_ty_args + 1
-                        , ru_try   = dictSelRule val_index n_ty_args n_eq_args }
+                        , ru_try   = dictSelRule val_index n_ty_args }
  
          -- The strictness signature is of the form U(AAAVAAAA) -> T
          -- where the V depends on which item we are selecting
      [data_con]           = tyConDataCons tycon
      tyvars               = dataConUnivTyVars data_con
      arg_tys              = dataConRepArgTys data_con  -- Includes the dictionary superclasses
-     eq_theta             = dataConEqTheta data_con
-     n_eq_args      = length eq_theta
  
      -- 'index' is a 0-index into the *value* arguments of the dictionary
      val_index      = assoc "MkId.mkDictSelId" sel_index_prs name
      pred                 = mkClassPred clas (mkTyVarTys tyvars)
      dict_id              = mkTemplateLocal 1 $ mkPredTy pred
      arg_ids              = mkTemplateLocalsNum 2 arg_tys
-     eq_ids               = map mkWildEvBinder eq_theta
  
      rhs = mkLams tyvars  (Lam dict_id   rhs_body)
      rhs_body | new_tycon = unwrapNewTypeBody tycon (map mkTyVarTy tyvars) (Var dict_id)
               | otherwise = Case (Var dict_id) dict_id (idType the_arg_id)
-                                 [(DataAlt data_con, eq_ids ++ arg_ids, Var the_arg_id)]
+                                 [(DataAlt data_con, arg_ids, Var the_arg_id)]
  
- dictSelRule :: Int -> Arity -> Arity 
+ dictSelRule :: Int -> Arity 
              -> IdUnfoldingFun -> [CoreExpr] -> Maybe CoreExpr
  -- Tries to persuade the argument to look like a constructor
  -- application, using exprIsConApp_maybe, and then selects
  -- from it
  --       sel_i t1..tk (D t1..tk op1 ... opm) = opi
  --
- dictSelRule val_index n_ty_args n_eq_args id_unf args
+ dictSelRule val_index n_ty_args id_unf args
    | (dict_arg : _) <- drop n_ty_args args
    , Just (_, _, con_args) <- exprIsConApp_maybe id_unf dict_arg
-   , let val_args = drop n_eq_args con_args
-   = Just (val_args !! val_index)
+   = Just (con_args !! val_index)
    | otherwise
    = Nothing
  \end{code}
@@@ -607,7 -602,7 +602,7 @@@ mkProductBox arg_ids t
  mkReboxingAlt
    :: [Unique] -- Uniques for the new Ids
    -> DataCon
-   -> [Var]    -- Source-level args, including existential dicts
+   -> [Var]    -- Source-level args, *including* all evidence vars 
    -> CoreExpr -- RHS
    -> CoreAlt
  
@@@ -628,15 -623,14 +623,14 @@@ mkReboxingAlt us con args rh
  
      -- Type variable case
      go (arg:args) stricts us 
-       | isTyCoVar arg
+       | isTyVar arg
        = let (binds, args') = go args stricts us
          in  (binds, arg:args')
  
          -- Term variable case
      go (arg:args) (str:stricts) us
        | isMarkedUnboxed str
-       = 
-         let (binds, unpacked_args')        = go args stricts us'
+       = let (binds, unpacked_args')        = go args stricts us'
              (us', bind_rhs, unpacked_args) = reboxProduct us (idType arg)
          in
              (NonRec arg bind_rhs : binds, unpacked_args ++ unpacked_args')
@@@ -674,13 -668,11 +668,11 @@@ wrapNewTypeBody :: TyCon -> [Type] -> C
  -- coercion constructor of the newtype or applied by itself).
  
  wrapNewTypeBody tycon args result_expr
-   = wrapFamInstBody tycon args inner
+   = ASSERT( isNewTyCon tycon )
+     wrapFamInstBody tycon args $
+     mkCoerce (mkSymCo co) result_expr
    where
-     inner
-       | Just co_con <- newTyConCo_maybe tycon
-       = mkCoerce (mkSymCoercion (mkTyConApp co_con args)) result_expr
-       | otherwise
-       = result_expr
+     co = mkAxInstCo (newTyConCo tycon) args
  
  -- When unwrapping, we do *not* apply any family coercion, because this will
  -- be done via a CoPat by the type checker.  We have to do it this way as
  
  unwrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
  unwrapNewTypeBody tycon args result_expr
-   | Just co_con <- newTyConCo_maybe tycon
-   = mkCoerce (mkTyConApp co_con args) result_expr
-   | otherwise
-   = result_expr
+   = ASSERT( isNewTyCon tycon )
+     mkCoerce (mkAxInstCo (newTyConCo tycon) args) result_expr
  
  -- If the type constructor is a representation type of a data instance, wrap
  -- the expression into a cast adjusting the expression type, which is an
  wrapFamInstBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
  wrapFamInstBody tycon args body
    | Just co_con <- tyConFamilyCoercion_maybe tycon
-   = mkCoerce (mkSymCoercion (mkTyConApp co_con args)) body
+   = mkCoerce (mkSymCo (mkAxInstCo co_con args)) body
    | otherwise
    = body
  
  unwrapFamInstScrut :: TyCon -> [Type] -> CoreExpr -> CoreExpr
  unwrapFamInstScrut tycon args scrut
    | Just co_con <- tyConFamilyCoercion_maybe tycon
-   = mkCoerce (mkTyConApp co_con args) scrut
+   = mkCoerce (mkAxInstCo co_con args) scrut
    | otherwise
    = scrut
  \end{code}
@@@ -826,6 -816,11 +816,6 @@@ BUT make sure they are *exported* Local
  that they aren't discarded by the occurrence analyser.
  
  \begin{code}
 -mkDefaultMethodId :: Id               -- Selector Id
 -                -> Name       -- Default method name
 -                -> Id         -- Default method Id
 -mkDefaultMethodId sel_id dm_name = mkExportedLocalId dm_name (idType sel_id)
 -
  mkDictFunId :: Name      -- Name to use for the dict fun;
              -> [TyVar]
              -> ThetaType
@@@ -853,7 -848,7 +843,7 @@@ mkDictFunTy tvs theta clas ty
                                (classSCTheta clas)
                     -- See Note [Silent Superclass Arguments]
      discard pred = isEmptyVarSet (tyVarsOfPred pred)
-                  || any (`tcEqPred` pred) theta
+                  || any (`eqPred` pred) theta
                   -- See the DFun Superclass Invariant in TcInstDcls
  \end{code}
  
@@@ -880,12 -875,13 +870,13 @@@ they can unify with both unlifted and l
  another gun with which to shoot yourself in the foot.
  
  \begin{code}
- lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName :: Name
- unsafeCoerceName = mkWiredInIdName gHC_PRIM (fsLit "unsafeCoerce#") unsafeCoerceIdKey  unsafeCoerceId
- nullAddrName     = mkWiredInIdName gHC_PRIM (fsLit "nullAddr#")     nullAddrIdKey      nullAddrId
- seqName          = mkWiredInIdName gHC_PRIM (fsLit "seq")           seqIdKey           seqId
- realWorldName    = mkWiredInIdName gHC_PRIM (fsLit "realWorld#")    realWorldPrimIdKey realWorldPrimId
- lazyIdName       = mkWiredInIdName gHC_BASE (fsLit "lazy")         lazyIdKey           lazyId
+ lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName :: Name
+ unsafeCoerceName  = mkWiredInIdName gHC_PRIM (fsLit "unsafeCoerce#") unsafeCoerceIdKey  unsafeCoerceId
+ nullAddrName      = mkWiredInIdName gHC_PRIM (fsLit "nullAddr#")     nullAddrIdKey      nullAddrId
+ seqName           = mkWiredInIdName gHC_PRIM (fsLit "seq")           seqIdKey           seqId
+ realWorldName     = mkWiredInIdName gHC_PRIM (fsLit "realWorld#")    realWorldPrimIdKey realWorldPrimId
+ lazyIdName        = mkWiredInIdName gHC_BASE (fsLit "lazy")         lazyIdKey           lazyId
+ coercionTokenName = mkWiredInIdName gHC_PRIM (fsLit "coercionToken#") coercionTokenIdKey coercionTokenId
  \end{code}
  
  \begin{code}
@@@ -903,7 -899,7 +894,7 @@@ unsafeCoerceI
                        (mkFunTy argAlphaTy openBetaTy)
      [x] = mkTemplateLocals [argAlphaTy]
      rhs = mkLams [argAlphaTyVar,openBetaTyVar,x] $
-           Cast (Var x) (mkUnsafeCoercion argAlphaTy openBetaTy)
+           Cast (Var x) (mkUnsafeCo argAlphaTy openBetaTy)
  
  ------------------------------------------------
  nullAddrId :: Id
@@@ -939,7 -935,7 +930,7 @@@ seqId = pcMiscPrelId seqName ty inf
  match_seq_of_cast :: IdUnfoldingFun -> [CoreExpr] -> Maybe CoreExpr
      -- See Note [Built-in RULES for seq]
  match_seq_of_cast _ [Type _, Type res_ty, Cast scrut co, expr]
-   = Just (Var seqId `mkApps` [Type (fst (coercionKind co)), Type res_ty,
+   = Just (Var seqId `mkApps` [Type (pFst (coercionKind co)), Type res_ty,
                                scrut, expr])
  match_seq_of_cast _ _ = Nothing
  
@@@ -1049,6 -1045,12 +1040,12 @@@ realWorldPrimId -- :: State# RealWorl
  voidArgId :: Id
  voidArgId       -- :: State# RealWorld
    = mkSysLocal (fsLit "void") voidArgIdKey realWorldStatePrimTy
+ coercionTokenId :: Id               -- :: () ~ ()
+ coercionTokenId -- Used to replace Coercion terms when we go to STG
+   = pcMiscPrelId coercionTokenName 
+                  (mkTyConApp eqPredPrimTyCon [unitTy, unitTy])
+                  noCafIdInfo
  \end{code}
  
  
@@@ -27,7 -27,6 +27,6 @@@ import TysWiredI
  import PrelNames
  import TyCon
  import Type
- import Unify( dataConCannotMatch )
  import SrcLoc
  import UniqSet
  import Util
@@@ -644,7 -643,7 +643,7 @@@ might_fail_pat (ConPatOut { pat_args = 
  
  -- Finally the ones that are sure to succeed, or which are covered by the checking algorithm
  might_fail_pat (LazyPat _)                   = False -- Always succeeds
 -might_fail_pat _                             = False -- VarPat, WildPat, LitPat, NPat, TypePat
 +might_fail_pat _                             = False -- VarPat, WildPat, LitPat, NPat
  
  --------------
  might_fail_lpat :: LPat Id -> Bool
@@@ -357,7 -357,7 +357,7 @@@ data IPBind i
  
  instance (OutputableBndr id) => Outputable (HsIPBinds id) where
    ppr (IPBinds bs ds) = pprDeeperList vcat (map ppr bs) 
-                       $$ ifPprDebug (ppr ds)
+                         $$ ifPprDebug (ppr ds)
  
  instance (OutputableBndr id) => Outputable (IPBind id) where
    ppr (IPBind id rhs) = pprBndr LetBind id <+> equals <+> pprExpr (unLoc rhs)
@@@ -457,7 -457,7 +457,7 @@@ data EvTer
    deriving( Data, Typeable)
  
  evVarTerm :: EvVar -> EvTerm
- evVarTerm v | isCoVar v = EvCoercion (mkCoVarCoercion v)
+ evVarTerm v | isCoVar v = EvCoercion (mkCoVarCo v)
              | otherwise = EvId v
  \end{code}
  
@@@ -546,7 -546,7 +546,7 @@@ pprHsWrapper doc wra
      help it WpHole             = it
      help it (WpCompose f1 f2)  = help (help it f2) f1
      help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>") 
-                                                  <+> pprParendType co)]
+                                               <+> pprParendCo co)]
      help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]
      help it (WpTyApp ty)  = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
      help it (WpEvLam id)  = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
@@@ -572,8 -572,8 +572,8 @@@ instance Outputable EvBind wher
  
  instance Outputable EvTerm where
    ppr (EvId v)                 = ppr v
-   ppr (EvCast v co)            = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendType co
-   ppr (EvCoercion co)    = ppr co
+   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendCo co
+   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co
    ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
    ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
  \end{code}
@@@ -597,10 -597,6 +597,10 @@@ data Sig name    -- Signatures and pragma
        -- f :: Num a => a -> a
      TypeSig (Located name) (LHsType name)
  
 +        -- A type signature for a default method inside a class
 +        -- default eq :: (Representable0 a, GEq (Rep0 a)) => a -> a -> Bool
 +  | GenericSig (Located name) (LHsType name)
 +
        -- A type signature in generated code, notably the code
        -- generated for record selectors.  We simply record
        -- the desired Id itself, replete with its name, type
@@@ -670,20 -666,18 +670,20 @@@ okBindSig :: Sig a -> Boo
  okBindSig _ = True
  
  okHsBootSig :: Sig a -> Bool
 -okHsBootSig (TypeSig  _ _) = True
 -okHsBootSig (FixSig _)           = True
 -okHsBootSig _              = False
 +okHsBootSig (TypeSig  _ _)    = True
 +okHsBootSig (GenericSig  _ _) = False
 +okHsBootSig (FixSig _)              = True
 +okHsBootSig _                 = False
  
  okClsDclSig :: Sig a -> Bool
  okClsDclSig (SpecInstSig _) = False
  okClsDclSig _               = True        -- All others OK
  
  okInstDclSig :: Sig a -> Bool
 -okInstDclSig (TypeSig _ _)   = False
 -okInstDclSig (FixSig _)      = False
 -okInstDclSig _                     = True
 +okInstDclSig (TypeSig _ _)    = False
 +okInstDclSig (GenericSig _ _) = False
 +okInstDclSig (FixSig _)       = False
 +okInstDclSig _                      = True
  
  sigName :: LSig name -> Maybe name
  -- Used only in Haddock
@@@ -708,10 -702,9 +708,10 @@@ isVanillaLSig (L _(TypeSig {})) = Tru
  isVanillaLSig _                 = False
  
  isTypeLSig :: LSig name -> Bool        -- Type signatures
 -isTypeLSig (L _(TypeSig {})) = True
 -isTypeLSig (L _(IdSig {}))   = True
 -isTypeLSig _                 = False
 +isTypeLSig (L _(TypeSig {}))    = True
 +isTypeLSig (L _(GenericSig {})) = True
 +isTypeLSig (L _(IdSig {}))      = True
 +isTypeLSig _                    = False
  
  isSpecLSig :: LSig name -> Bool
  isSpecLSig (L _(SpecSig {})) = True
@@@ -734,7 -727,6 +734,7 @@@ isInlineLSig _                    = Fal
  
  hsSigDoc :: Sig name -> SDoc
  hsSigDoc (TypeSig {})                 = ptext (sLit "type signature")
 +hsSigDoc (GenericSig {})      = ptext (sLit "default type signature")
  hsSigDoc (IdSig {})           = ptext (sLit "id signature")
  hsSigDoc (SpecSig {})         = ptext (sLit "SPECIALISE pragma")
  hsSigDoc (InlineSig {})         = ptext (sLit "INLINE pragma")
@@@ -749,7 -741,6 +749,7 @@@ eqHsSig :: Eq a => LSig a -> LSig a -> 
  eqHsSig (L _ (FixSig (FixitySig n1 _))) (L _ (FixSig (FixitySig n2 _))) = unLoc n1 == unLoc n2
  eqHsSig (L _ (IdSig n1))              (L _ (IdSig n2))                = n1 == n2
  eqHsSig (L _ (TypeSig n1 _))          (L _ (TypeSig n2 _))            = unLoc n1 == unLoc n2
 +eqHsSig (L _ (GenericSig n1 _))               (L _ (GenericSig n2 _))         = unLoc n1 == unLoc n2
  eqHsSig (L _ (InlineSig n1 _))          (L _ (InlineSig n2 _))          = unLoc n1 == unLoc n2
        -- For specialisations, we don't have equality over
        -- HsType, so it's not convenient to spot duplicate 
@@@ -763,7 -754,6 +763,7 @@@ instance (OutputableBndr name) => Outpu
  
  ppr_sig :: OutputableBndr name => Sig name -> SDoc
  ppr_sig (TypeSig var ty)        = pprVarSig (unLoc var) (ppr ty)
 +ppr_sig (GenericSig var ty)     = ptext (sLit "default") <+> pprVarSig (unLoc var) (ppr ty)
  ppr_sig (IdSig id)              = pprVarSig id (ppr (varType id))
  ppr_sig (FixSig fix_sig)        = ppr fix_sig
  ppr_sig (SpecSig var ty inl)    = pragBrackets (pprSpec var (ppr ty) inl)
diff --combined compiler/hsSyn/HsPat.lhs
@@@ -24,7 -24,7 +24,7 @@@ module HsPat 
  
          isBangHsBind, isLiftedPatBind,
          isBangLPat, hsPatNeedsParens,
-       isIrrefutableHsPat,
+         isIrrefutableHsPat,
  
        pprParendLPat
      ) where
@@@ -65,7 -65,7 +65,7 @@@ data Pat i
        -- support hsPatType :: Pat Id -> Type
  
    | VarPat    id                      -- Variable
-   | LazyPat   (LPat id)               -- Lazy pattern
+   | LazyPat     (LPat id)               -- Lazy pattern
    | AsPat     (Located id) (LPat id)  -- As pattern
    | ParPat      (LPat id)             -- Parenthesised pattern
    | BangPat   (LPat id)               -- Bang pattern
                    (SyntaxExpr id)     -- (>=) function, of type t->t->Bool
                    (SyntaxExpr id)     -- Name of '-' (see RnEnv.lookupSyntaxName)
  
 -      ------------ Generics ---------------
 -  | TypePat       (LHsType id)        -- Type pattern for generic definitions
 -                                        -- e.g  f{| a+b |} = ...
 -                                        -- These show up only in class declarations,
 -                                        -- and should be a top-level pattern
 -
        ------------ Pattern type signatures ---------------
    | SigPatIn      (LPat id)           -- Pattern with a type signature
                    (LHsType id)
@@@ -277,6 -283,7 +277,6 @@@ pprPat (NPat l Nothing  _)  = ppr 
  pprPat (NPat l (Just _) _)  = char '-' <> ppr l
  pprPat (NPlusKPat n k _ _)  = hcat [ppr n, char '+', ppr k]
  pprPat (QuasiQuotePat qq)   = ppr qq
 -pprPat (TypePat ty)       = ptext (sLit "{|") <> ppr ty <> ptext (sLit "|}")
  pprPat (CoPat co pat _)           = pprHsWrapper (ppr pat) co
  pprPat (SigPatIn pat ty)    = ppr pat <+> dcolon <+> ppr ty
  pprPat (SigPatOut pat ty)   = ppr pat <+> dcolon <+> ppr ty
@@@ -434,6 -441,7 +434,6 @@@ isIrrefutableHsPat pa
  
      go1 (QuasiQuotePat {}) = urk pat  -- Gotten rid of by renamer, before
                                        -- isIrrefutablePat is called
 -    go1 (TypePat {})       = urk pat
  
      urk pat = pprPanic "isIrrefutableHsPat:" (ppr pat)
  
@@@ -457,6 -465,7 +457,6 @@@ hsPatNeedsParens (LitPat {})            = 
  hsPatNeedsParens (NPat {})         = False
  hsPatNeedsParens (NPlusKPat {})      = True
  hsPatNeedsParens (QuasiQuotePat {})  = True
 -hsPatNeedsParens (TypePat {})        = False
  
  conPatNeedsParens :: HsConDetails a b -> Bool
  conPatNeedsParens (PrefixCon args) = not (null args)
@@@ -19,15 -19,15 +19,15 @@@ module HsUtils
    mkHsPar, mkHsApp, mkHsConApp, mkSimpleHsAlt,
    mkSimpleMatch, unguardedGRHSs, unguardedRHS, 
    mkMatchGroup, mkMatch, mkHsLam, mkHsIf,
-   mkHsWrap, mkLHsWrap, mkHsWrapCoI, mkLHsWrapCoI,
-   coiToHsWrapper, mkHsLams, mkHsDictLet,
-   mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCoI, 
+   mkHsWrap, mkLHsWrap, mkHsWrapCo, mkLHsWrapCo,
+   coToHsWrapper, mkHsDictLet, mkHsLams,
+   mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCo,
  
    nlHsTyApp, nlHsVar, nlHsLit, nlHsApp, nlHsApps, nlHsIntLit, nlHsVarApps, 
    nlHsDo, nlHsOpApp, nlHsLam, nlHsPar, nlHsIf, nlHsCase, nlList,
    mkLHsTupleExpr, mkLHsVarTuple, missingTupArg,
  
 -  -- Bindigns
 +  -- Bindings
    mkFunBind, mkVarBind, mkHsVarBind, mk_easy_FunBind, 
  
    -- Literals
@@@ -77,7 -77,7 +77,7 @@@ import HsLi
  import RdrName
  import Var
  import Coercion
- import Type
+ import TypeRep
  import DataCon
  import Name
  import NameSet
@@@ -137,25 -137,25 +137,25 @@@ mkHsWrap :: HsWrapper -> HsExpr id -> H
  mkHsWrap co_fn e | isIdHsWrapper co_fn = e
                 | otherwise           = HsWrap co_fn e
  
- mkHsWrapCoI :: CoercionI -> HsExpr id -> HsExpr id
- mkHsWrapCoI (IdCo _) e = e
- mkHsWrapCoI (ACo co) e = mkHsWrap (WpCast co) e
+ mkHsWrapCo :: Coercion -> HsExpr id -> HsExpr id
+ mkHsWrapCo (Refl _) e = e
+ mkHsWrapCo co       e = mkHsWrap (WpCast co) e
  
- mkLHsWrapCoI :: CoercionI -> LHsExpr id -> LHsExpr id
- mkLHsWrapCoI (IdCo _) e         = e
- mkLHsWrapCoI (ACo co) (L loc e) = L loc (mkHsWrap (WpCast co) e)
+ mkLHsWrapCo :: Coercion -> LHsExpr id -> LHsExpr id
+ mkLHsWrapCo (Refl _) e         = e
+ mkLHsWrapCo co       (L loc e) = L loc (mkHsWrap (WpCast co) e)
  
- coiToHsWrapper :: CoercionI -> HsWrapper
- coiToHsWrapper (IdCo _) = idHsWrapper
- coiToHsWrapper (ACo co) = WpCast co
+ coToHsWrapper :: Coercion -> HsWrapper
+ coToHsWrapper (Refl _) = idHsWrapper
+ coToHsWrapper co       = WpCast co
  
  mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id
  mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
                       | otherwise           = CoPat co_fn p ty
  
- mkHsWrapPatCoI :: CoercionI -> Pat id -> Type -> Pat id
- mkHsWrapPatCoI (IdCo _) pat _  = pat
- mkHsWrapPatCoI (ACo co) pat ty = CoPat (WpCast co) pat ty
+ mkHsWrapPatCo :: Coercion -> Pat id -> Type -> Pat id
+ mkHsWrapPatCo (Refl _) pat _  = pat
+ mkHsWrapPatCo co       pat ty = CoPat (WpCast co) pat ty
  
  mkHsLam :: [LPat id] -> LHsExpr id -> LHsExpr id
  mkHsLam pats body = mkHsPar (L (getLoc body) (HsLam matches))
@@@ -548,6 -548,7 +548,6 @@@ collect_lpat (L _ pat) bndr
      go (SigPatIn pat _)                 = collect_lpat pat bndrs
      go (SigPatOut pat _)        = collect_lpat pat bndrs
      go (QuasiQuotePat _)          = bndrs
 -    go (TypePat _)                = bndrs
      go (CoPat _ pat _)            = go pat
  \end{code}
  
@@@ -723,6 -724,7 +723,6 @@@ collect_sig_lpat pat acc = collect_sig_
  
  collect_sig_pat :: Pat name -> [LHsType name] -> [LHsType name]
  collect_sig_pat (SigPatIn pat ty)     acc = collect_sig_lpat pat (ty:acc)
 -collect_sig_pat (TypePat ty)          acc = ty:acc
  
  collect_sig_pat (LazyPat pat)       acc = collect_sig_lpat pat acc
  collect_sig_pat (BangPat pat)       acc = collect_sig_lpat pat acc
@@@ -1,4 -1,3 +1,3 @@@
  {-# OPTIONS_GHC -O #-}
  -- We always optimise this, otherwise performance of a non-optimised
  -- compiler is severely affected
@@@ -903,10 -902,11 +902,11 @@@ instance Binary IfaceType wher
      put_ bh (IfaceTyConApp (IfaceAnyTc k) [])                = do { putByte bh 17; put_ bh k }
  
        -- Generic cases
      put_ bh (IfaceTyConApp (IfaceTc tc) tys) = do { putByte bh 18; put_ bh tc; put_ bh tys }
      put_ bh (IfaceTyConApp tc tys)         = do { putByte bh 19; put_ bh tc; put_ bh tys }
  
+     put_ bh (IfaceCoConApp cc tys) = do { putByte bh 20; put_ bh cc; put_ bh tys }
      get bh = do
            h <- getByte bh
            case h of
                17 -> do { k <- get bh; return (IfaceTyConApp (IfaceAnyTc k) []) }
  
              18 -> do { tc <- get bh; tys <- get bh; return (IfaceTyConApp (IfaceTc tc) tys) }
-             _  -> do { tc <- get bh; tys <- get bh; return (IfaceTyConApp tc tys) }
+             19  -> do { tc <- get bh; tys <- get bh; return (IfaceTyConApp tc tys) }
+             _  -> do { cc <- get bh; tys <- get bh; return (IfaceCoConApp cc tys) }
  
  instance Binary IfaceTyCon where
        -- Int,Char,Bool can't show up here because they can't not be saturated
     put_ bh IfaceIntTc               = putByte bh 1
     put_ bh IfaceBoolTc              = putByte bh 2
     put_ bh IfaceCharTc              = putByte bh 3
     put_ bh IfaceUnliftedTypeKindTc = putByte bh 8
     put_ bh IfaceUbxTupleKindTc     = putByte bh 9
     put_ bh IfaceArgTypeKindTc      = putByte bh 10
-    put_ bh (IfaceTupTc bx ar) = do { putByte bh 11; put_ bh bx; put_ bh ar }
-    put_ bh (IfaceTc ext)      = do { putByte bh 12; put_ bh ext }
-    put_ bh (IfaceAnyTc k)     = do { putByte bh 13; put_ bh k }
+    put_ bh (IfaceTupTc bx ar)  = do { putByte bh 11; put_ bh bx; put_ bh ar }
+    put_ bh (IfaceTc ext)       = do { putByte bh 12; put_ bh ext }
+    put_ bh (IfaceAnyTc k)      = do { putByte bh 13; put_ bh k }
  
     get bh = do
        h <- getByte bh
            10 -> return IfaceArgTypeKindTc
          11 -> do { bx <- get bh; ar <- get bh; return (IfaceTupTc bx ar) }
          12 -> do { ext <- get bh; return (IfaceTc ext) }
-         _  -> do { k <- get bh; return (IfaceAnyTc k) }
+         _ -> do { k <- get bh; return (IfaceAnyTc k) }
+ instance Binary IfaceCoCon where
+    put_ bh (IfaceCoAx n)       = do { putByte bh 0; put_ bh n }
+    put_ bh IfaceReflCo         = putByte bh 1
+    put_ bh IfaceUnsafeCo       = putByte bh 2
+    put_ bh IfaceSymCo          = putByte bh 3
+    put_ bh IfaceTransCo        = putByte bh 4
+    put_ bh IfaceInstCo         = putByte bh 5
+    put_ bh (IfaceNthCo d)      = do { putByte bh 6; put_ bh d }
+   
+    get bh = do
+       h <- getByte bh
+       case h of
+           0 -> do { n <- get bh; return (IfaceCoAx n) }
+         1 -> return IfaceReflCo 
+         2 -> return IfaceUnsafeCo
+         3 -> return IfaceSymCo
+         4 -> return IfaceTransCo
+         5 -> return IfaceInstCo
+           _ -> do { d <- get bh; return (IfaceNthCo d) }
  
  instance Binary IfacePredType where
      put_ bh (IfaceClassP aa ab) = do
@@@ -1013,50 -1033,50 +1033,50 @@@ instance Binary IfaceExpr wher
      put_ bh (IfaceType ab) = do
            putByte bh 1
            put_ bh ab
-     put_ bh (IfaceTuple ac ad) = do
+     put_ bh (IfaceCo ab) = do
            putByte bh 2
+           put_ bh ab
+     put_ bh (IfaceTuple ac ad) = do
+           putByte bh 3
            put_ bh ac
            put_ bh ad
      put_ bh (IfaceLam ae af) = do
-           putByte bh 3
+           putByte bh 4
            put_ bh ae
            put_ bh af
      put_ bh (IfaceApp ag ah) = do
-           putByte bh 4
+           putByte bh 5
            put_ bh ag
            put_ bh ah
- -- gaw 2004
-     put_ bh (IfaceCase ai aj al ak) = do
-           putByte bh 5
+     put_ bh (IfaceCase ai aj ak) = do
+           putByte bh 6
            put_ bh ai
            put_ bh aj
- -- gaw 2004
-             put_ bh al
            put_ bh ak
      put_ bh (IfaceLet al am) = do
-           putByte bh 6
+           putByte bh 7
            put_ bh al
            put_ bh am
      put_ bh (IfaceNote an ao) = do
-           putByte bh 7
+           putByte bh 8
            put_ bh an
            put_ bh ao
      put_ bh (IfaceLit ap) = do
-           putByte bh 8
+           putByte bh 9
            put_ bh ap
      put_ bh (IfaceFCall as at) = do
-           putByte bh 9
+           putByte bh 10
            put_ bh as
            put_ bh at
      put_ bh (IfaceExt aa) = do
-           putByte bh 10
+           putByte bh 11
            put_ bh aa
      put_ bh (IfaceCast ie ico) = do
-             putByte bh 11
+             putByte bh 12
              put_ bh ie
              put_ bh ico
      put_ bh (IfaceTick m ix) = do
-             putByte bh 12
+             putByte bh 13
              put_ bh m
              put_ bh ix
      get bh = do
                      return (IfaceLcl aa)
              1 -> do ab <- get bh
                      return (IfaceType ab)
-             2 -> do ac <- get bh
+             2 -> do ab <- get bh
+                     return (IfaceCo ab)
+             3 -> do ac <- get bh
                      ad <- get bh
                      return (IfaceTuple ac ad)
-             3 -> do ae <- get bh
+             4 -> do ae <- get bh
                      af <- get bh
                      return (IfaceLam ae af)
-             4 -> do ag <- get bh
+             5 -> do ag <- get bh
                      ah <- get bh
                      return (IfaceApp ag ah)
-             5 -> do ai <- get bh
+             6 -> do ai <- get bh
                      aj <- get bh
- -- gaw 2004
-                       al <- get bh                   
                      ak <- get bh
- -- gaw 2004
-                     return (IfaceCase ai aj al ak)
-             6 -> do al <- get bh
+                     return (IfaceCase ai aj ak)
+             7 -> do al <- get bh
                      am <- get bh
                      return (IfaceLet al am)
-             7 -> do an <- get bh
+             8 -> do an <- get bh
                      ao <- get bh
                      return (IfaceNote an ao)
-             8 -> do ap <- get bh
+             9 -> do ap <- get bh
                      return (IfaceLit ap)
-             9 -> do as <- get bh
-                     at <- get bh
-                     return (IfaceFCall as at)
-             10 -> do aa <- get bh
+             10 -> do as <- get bh
+                      at <- get bh
+                      return (IfaceFCall as at)
+             11 -> do aa <- get bh
                       return (IfaceExt aa)
-               11 -> do ie <- get bh
+               12 -> do ie <- get bh
                         ico <- get bh
                         return (IfaceCast ie ico)
-               12 -> do m <- get bh
+               13 -> do m <- get bh
                         ix <- get bh
                         return (IfaceTick m ix)
                _ -> panic ("get IfaceExpr " ++ show h)
@@@ -1291,7 -1310,7 +1310,7 @@@ instance Binary IfaceDecl wher
            put_ bh idinfo
      put_ _ (IfaceForeign _ _) = 
        error "Binary.put_(IfaceDecl): IfaceForeign"
 -    put_ bh (IfaceData a1 a2 a3 a4 a5 a6 a7 a8) = do
 +    put_ bh (IfaceData a1 a2 a3 a4 a5 a6 a7) = do
            putByte bh 2
            put_ bh (occNameFS a1)
            put_ bh a2
            put_ bh a5
            put_ bh a6
            put_ bh a7
 -          put_ bh a8
      put_ bh (IfaceSyn a1 a2 a3 a4 a5) = do
            putByte bh 3
            put_ bh (occNameFS a1)
                    a5 <- get bh
                    a6 <- get bh
                    a7 <- get bh
 -                  a8 <- get bh
                      occ <- return $! mkOccNameFS tcName a1
 -                  return (IfaceData occ a2 a3 a4 a5 a6 a7 a8)
 +                  return (IfaceData occ a2 a3 a4 a5 a6 a7)
              3 -> do
                    a1 <- get bh
                    a2 <- get bh
@@@ -59,12 -59,13 +59,12 @@@ buildAlgTyCon :: Name -> [TyVar
              -> ThetaType              -- ^ Stupid theta
              -> AlgTyConRhs
              -> RecFlag
 -            -> Bool                   -- ^ True <=> want generics functions
              -> Bool                   -- ^ True <=> was declared in GADT syntax
                -> TyConParent
              -> Maybe (TyCon, [Type])  -- ^ family instance if applicable
              -> TcRnIf m n TyCon
  
 -buildAlgTyCon tc_name tvs stupid_theta rhs is_rec want_generics gadt_syn
 +buildAlgTyCon tc_name tvs stupid_theta rhs is_rec gadt_syn
              parent mb_family
    | Just fam_inst_info <- mb_family
    = -- We need to tie a knot as the coercion of a data instance depends
      fixM $ \ tycon_rec -> do 
      { fam_parent <- mkFamInstParentInfo tc_name tvs fam_inst_info tycon_rec
      ; return (mkAlgTyCon tc_name kind tvs stupid_theta rhs
 -                       fam_parent is_rec want_generics gadt_syn) }
 +                       fam_parent is_rec gadt_syn) }
  
    | otherwise
    = return (mkAlgTyCon tc_name kind tvs stupid_theta rhs
 -                     parent is_rec want_generics gadt_syn)
 +                     parent is_rec gadt_syn)
    where
      kind = mkArrowKinds (map tyVarKind tvs) liftedTypeKind
  
@@@ -99,8 -100,8 +99,8 @@@ mkFamInstParentInfo :: Name -> [TyVar
  mkFamInstParentInfo tc_name tvs (family, instTys) rep_tycon
    = do { -- Create the coercion
         ; co_tycon_name <- newImplicitBinder tc_name mkInstTyCoOcc
-        ; let co_tycon = mkFamInstCoercion co_tycon_name tvs
-                                         family instTys rep_tycon
+        ; let co_tycon = mkFamInstCo co_tycon_name tvs
+                                     family instTys rep_tycon
         ; return $ FamInstTyCon family instTys co_tycon }
      
  ------------------------------------------------------
@@@ -126,23 -127,15 +126,15 @@@ mkNewTyConRhs :: Name -> TyCon -> DataC
  --   because the latter is part of a knot, whereas the former is not.
  mkNewTyConRhs tycon_name tycon con 
    = do        { co_tycon_name <- newImplicitBinder tycon_name mkNewTyCoOcc
-       ; let co_tycon = mkNewTypeCoercion co_tycon_name tycon etad_tvs etad_rhs
-               cocon_maybe | all_coercions || isRecursiveTyCon tycon 
-                         = Just co_tycon
-                         | otherwise              
-                         = Nothing
-       ; traceIf (text "mkNewTyConRhs" <+> ppr cocon_maybe)
+       ; let co_tycon = mkNewTypeCo co_tycon_name tycon etad_tvs etad_rhs
+       ; traceIf (text "mkNewTyConRhs" <+> ppr co_tycon)
        ; return (NewTyCon { data_con    = con, 
                             nt_rhs      = rhs_ty,
                             nt_etad_rhs = (etad_tvs, etad_rhs),
-                            nt_co       = cocon_maybe } ) }
+                            nt_co       = co_tycon } ) }
                               -- Coreview looks through newtypes with a Nothing
                               -- for nt_co, or uses explicit coercions otherwise
    where
-         -- If all_coercions is True then we use coercions for all newtypes
-         -- otherwise we use coercions for recursive newtypes and look through
-         -- non-recursive newtypes
-     all_coercions = True
      tvs    = tyConTyVars tycon
      inst_con_ty = applyTys (dataConUserType con) (mkTyVarTys tvs)
      rhs_ty = ASSERT( isFunTy inst_con_ty ) funArgTy inst_con_ty
        -- has a single argument (Foo a) that is a *type class*, so
        -- dataConInstOrigArgTys returns [].
  
-     etad_tvs :: [TyVar]       -- Matched lazily, so that mkNewTypeCoercion can
+     etad_tvs :: [TyVar]       -- Matched lazily, so that mkNewTypeCo can
      etad_rhs :: Type  -- return a TyCon without pulling on rhs_ty
                        -- See Note [Tricky iface loop] in LoadIface
      (etad_tvs, etad_rhs) = eta_reduce (reverse tvs) rhs_ty
@@@ -228,9 -221,8 +220,9 @@@ mkDataConStupidTheta tycon arg_tys univ
  
  ------------------------------------------------------
  \begin{code}
 -type TcMethInfo = (Name, DefMethSpec, Type)  -- A temporary intermediate, to communicate 
 -                                           -- between tcClassSigs and buildClass
 +type TcMethInfo = (Name, DefMethSpec, Type)  
 +        -- A temporary intermediate, to communicate between tcClassSigs and
 +        -- buildClass.
  
  buildClass :: Bool            -- True <=> do not include unfoldings 
                                --          on dict selectors
@@@ -332,8 -324,7 +324,8 @@@ buildClass no_unf class_name tvs sc_the
      mk_op_item rec_clas (op_name, dm_spec, _) 
        = do { dm_info <- case dm_spec of
                            NoDM      -> return NoDefMeth
 -                          GenericDM -> return GenDefMeth
 +                          GenericDM -> do { dm_name <- newImplicitBinder op_name mkGenDefMethodOcc
 +                                        ; return (GenDefMeth dm_name) }
                            VanillaDM -> do { dm_name <- newImplicitBinder op_name mkDefaultMethodOcc
                                          ; return (DefMeth dm_name) }
             ; return (mkDictSelId no_unf op_name rec_clas, dm_info) }
@@@ -67,6 -67,14 +67,6 @@@ data IfaceDec
                  ifRec        :: RecFlag,        -- Recursive or not?
                  ifGadtSyntax :: Bool,           -- True <=> declared using
                                                  -- GADT syntax
 -                ifGeneric    :: Bool,           -- True <=> generic converter
 -                                                --          functions available
 -                                                -- We need this for imported
 -                                                -- data decls, since the
 -                                                -- imported modules may have
 -                                                -- been compiled with
 -                                                -- different flags to the
 -                                                -- current compilation unit
                  ifFamInst    :: Maybe (IfaceTyCon, [IfaceType])
                                                  -- Just <=> instance of family
                                                  -- Invariant:
@@@ -227,12 -235,13 +227,13 @@@ data IfaceExp
    = IfaceLcl    IfLclName
    | IfaceExt    IfExtName
    | IfaceType   IfaceType
-   | IfaceTuple  Boxity [IfaceExpr]              -- Saturated; type arguments omitted
-   | IfaceLam    IfaceBndr IfaceExpr
-   | IfaceApp    IfaceExpr IfaceExpr
-   | IfaceCase   IfaceExpr IfLclName IfaceType [IfaceAlt]
-   | IfaceLet    IfaceBinding  IfaceExpr
-   | IfaceNote   IfaceNote IfaceExpr
+   | IfaceCo     IfaceType             -- We re-use IfaceType for coercions
+   | IfaceTuple        Boxity [IfaceExpr]      -- Saturated; type arguments omitted
+   | IfaceLam  IfaceBndr IfaceExpr
+   | IfaceApp  IfaceExpr IfaceExpr
+   | IfaceCase IfaceExpr IfLclName [IfaceAlt]
+   | IfaceLet  IfaceBinding  IfaceExpr
+   | IfaceNote IfaceNote IfaceExpr
    | IfaceCast   IfaceExpr IfaceCoercion
    | IfaceLit    Literal
    | IfaceFCall  ForeignCall IfaceType
@@@ -464,11 -473,11 +465,11 @@@ pprIfaceDecl (IfaceSyn {ifName = tycon
    = hang (ptext (sLit "type family") <+> pprIfaceDeclHead [] tycon tyvars)
         4 (dcolon <+> ppr kind)
  
 -pprIfaceDecl (IfaceData {ifName = tycon, ifGeneric = gen, ifCtxt = context,
 +pprIfaceDecl (IfaceData {ifName = tycon, ifCtxt = context,
                           ifTyVars = tyvars, ifCons = condecls,
                           ifRec = isrec, ifFamInst = mbFamInst})
    = hang (pp_nd <+> pprIfaceDeclHead context tycon tyvars)
 -       4 (vcat [pprRec isrec, pprGen gen, pp_condecls tycon condecls,
 +       4 (vcat [pprRec isrec, pp_condecls tycon condecls,
                  pprFamily mbFamInst])
    where
      pp_nd = case condecls of
@@@ -488,6 -497,10 +489,6 @@@ pprIfaceDecl (IfaceClass {ifCtxt = cont
  pprRec :: RecFlag -> SDoc
  pprRec isrec = ptext (sLit "RecFlag") <+> ppr isrec
  
 -pprGen :: Bool -> SDoc
 -pprGen True  = ptext (sLit "Generics: yes")
 -pprGen False = ptext (sLit "Generics: no")
 -
  pprFamily :: Maybe (IfaceTyCon, [IfaceType]) -> SDoc
  pprFamily Nothing        = ptext (sLit "FamilyInstance: none")
  pprFamily (Just famInst) = ptext (sLit "FamilyInstance:") <+> ppr famInst
@@@ -588,6 -601,7 +589,7 @@@ pprIfaceExpr _       (IfaceLit l
  pprIfaceExpr _       (IfaceFCall cc ty) = braces (ppr cc <+> ppr ty)
  pprIfaceExpr _       (IfaceTick m ix)   = braces (text "tick" <+> ppr m <+> ppr ix)
  pprIfaceExpr _       (IfaceType ty)     = char '@' <+> pprParendIfaceType ty
+ pprIfaceExpr _       (IfaceCo co)       = text "@~" <+> pprParendIfaceType co
  
  pprIfaceExpr add_par app@(IfaceApp _ _) = add_par (pprIfaceApp app [])
  pprIfaceExpr _       (IfaceTuple c as)  = tupleParens c (interpp'SP as)
@@@ -600,17 -614,17 +602,17 @@@ pprIfaceExpr add_par i@(IfaceLam _ _
      collect bs (IfaceLam b e) = collect (b:bs) e
      collect bs e              = (reverse bs, e)
  
- pprIfaceExpr add_par (IfaceCase scrut bndr ty [(con, bs, rhs)])
-   = add_par (sep [ptext (sLit "case") <+> char '@' <+> pprParendIfaceType ty
-                         <+> pprIfaceExpr noParens scrut <+> ptext (sLit "of")
-                         <+> ppr bndr <+> char '{' <+> ppr_con_bs con bs <+> arrow,
-                   pprIfaceExpr noParens rhs <+> char '}'])
+ pprIfaceExpr add_par (IfaceCase scrut bndr [(con, bs, rhs)])
+   = add_par (sep [ptext (sLit "case") 
+                       <+> pprIfaceExpr noParens scrut <+> ptext (sLit "of") 
+                       <+> ppr bndr <+> char '{' <+> ppr_con_bs con bs <+> arrow,
+                 pprIfaceExpr noParens rhs <+> char '}'])
  
- pprIfaceExpr add_par (IfaceCase scrut bndr ty alts)
-   = add_par (sep [ptext (sLit "case") <+> char '@' <+> pprParendIfaceType ty
-                         <+> pprIfaceExpr noParens scrut <+> ptext (sLit "of")
-                         <+> ppr bndr <+> char '{',
-                   nest 2 (sep (map ppr_alt alts)) <+> char '}'])
+ pprIfaceExpr add_par (IfaceCase scrut bndr alts)
+   = add_par (sep [ptext (sLit "case") 
+                       <+> pprIfaceExpr noParens scrut <+> ptext (sLit "of") 
+                       <+> ppr bndr <+> char '{',
+                 nest 2 (sep (map ppr_alt alts)) <+> char '}'])
  
  pprIfaceExpr _       (IfaceCast expr co)
    = sep [pprParendIfaceExpr expr,
@@@ -786,6 -800,8 +788,8 @@@ freeNamesIfType (IfaceTyConApp tc ts) 
  freeNamesIfType (IfaceForAllTy tv t)  =
     freeNamesIfTvBndr tv &&& freeNamesIfType t
  freeNamesIfType (IfaceFunTy s t)      = freeNamesIfType s &&& freeNamesIfType t
+ freeNamesIfType (IfaceCoConApp tc ts) = 
+    freeNamesIfCo tc &&& fnList freeNamesIfType ts
  
  freeNamesIfTvBndrs :: [IfaceTvBndr] -> NameSet
  freeNamesIfTvBndrs = fnList freeNamesIfTvBndr
@@@ -828,16 -844,16 +832,16 @@@ freeNamesIfExpr :: IfaceExpr -> NameSe
  freeNamesIfExpr (IfaceExt v)      = unitNameSet v
  freeNamesIfExpr (IfaceFCall _ ty) = freeNamesIfType ty
  freeNamesIfExpr (IfaceType ty)    = freeNamesIfType ty
+ freeNamesIfExpr (IfaceCo co)      = freeNamesIfType co
  freeNamesIfExpr (IfaceTuple _ as) = fnList freeNamesIfExpr as
  freeNamesIfExpr (IfaceLam b body) = freeNamesIfBndr b &&& freeNamesIfExpr body
  freeNamesIfExpr (IfaceApp f a)    = freeNamesIfExpr f &&& freeNamesIfExpr a
  freeNamesIfExpr (IfaceCast e co)  = freeNamesIfExpr e &&& freeNamesIfType co
  freeNamesIfExpr (IfaceNote _n r)  = freeNamesIfExpr r
  
- freeNamesIfExpr (IfaceCase s _ ty alts)
-   = freeNamesIfExpr s
+ freeNamesIfExpr (IfaceCase s _ alts)
+   = freeNamesIfExpr s 
      &&& fnList fn_alt alts &&& fn_cons alts
-     &&& freeNamesIfType ty
    where
      fn_alt (_con,_bs,r) = freeNamesIfExpr r
  
@@@ -863,6 -879,10 +867,10 @@@ freeNamesIfTc (IfaceTc tc) = unitNameSe
  -- ToDo: shouldn't we include IfaceIntTc & co.?
  freeNamesIfTc _ = emptyNameSet
  
+ freeNamesIfCo :: IfaceCoCon -> NameSet
+ freeNamesIfCo (IfaceCoAx tc) = unitNameSet tc
+ freeNamesIfCo _ = emptyNameSet
  freeNamesIfRule :: IfaceRule -> NameSet
  freeNamesIfRule (IfaceRule { ifRuleBndrs = bs, ifRuleHead = f
                             , ifRuleArgs = es, ifRuleRhs = rhs })
@@@ -59,10 -59,10 +59,10 @@@ import Annotation
  import CoreSyn
  import CoreFVs
  import Class
+ import Kind
  import TyCon
  import DataCon
  import Type
- import Coercion
  import TcType
  import InstEnv
  import FamInstEnv
@@@ -1335,9 -1335,9 +1335,9 @@@ tyThingToIfaceDecl (AClass clas
          (sel_tyvars, rho_ty) = splitForAllTys (idType sel_id)
          op_ty                = funResultTy rho_ty
  
 -    toDmSpec NoDefMeth   = NoDM
 -    toDmSpec GenDefMeth  = GenericDM
 -    toDmSpec (DefMeth _) = VanillaDM
 +    toDmSpec NoDefMeth      = NoDM
 +    toDmSpec (GenDefMeth _) = GenericDM
 +    toDmSpec (DefMeth _)    = VanillaDM
  
      toIfaceFD (tvs1, tvs2) = (map getFS tvs1, map getFS tvs2)
  
@@@ -1357,6 -1357,7 +1357,6 @@@ tyThingToIfaceDecl (ATyCon tycon
                ifCons    = ifaceConDecls (algTyConRhs tycon),
                ifRec     = boolToRecFlag (isRecursiveTyCon tycon),
                ifGadtSyntax = isGadtSyntaxTyCon tycon,
 -              ifGeneric = tyConHasGenerics tycon,
                ifFamInst = famInstToIface (tyConFamInst_maybe tycon)}
  
    | isForeignTyCon tycon
        = IfCon   { ifConOcc     = getOccName (dataConName data_con),
                    ifConInfix   = dataConIsInfix data_con,
                    ifConWrapper = isJust (dataConWrapId_maybe data_con),
-                   ifConUnivTvs = toIfaceTvBndrs (dataConUnivTyVars data_con),
-                   ifConExTvs   = toIfaceTvBndrs (dataConExTyVars data_con),
-                   ifConEqSpec  = to_eq_spec (dataConEqSpec data_con),
-                   ifConCtxt    = toIfaceContext (dataConEqTheta data_con ++ dataConDictTheta data_con),
-                   ifConArgTys  = map toIfaceType (dataConOrigArgTys data_con),
+                   ifConUnivTvs = toIfaceTvBndrs univ_tvs,
+                   ifConExTvs   = toIfaceTvBndrs ex_tvs,
+                   ifConEqSpec  = to_eq_spec eq_spec,
+                   ifConCtxt    = toIfaceContext theta,
+                   ifConArgTys  = map toIfaceType arg_tys,
                    ifConFields  = map getOccName 
                                       (dataConFieldLabels data_con),
                    ifConStricts = dataConStrictMarks data_con }
+         where
+           (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) = dataConFullSig data_con
  
      to_eq_spec spec = [(getOccName tv, toIfaceType ty) | (tv,ty) <- spec]
  
      famInstToIface (Just (famTyCon, instTys)) = 
        Just (toIfaceTyCon famTyCon, map toIfaceType instTys)
  
+ tyThingToIfaceDecl c@(ACoAxiom _) = pprPanic "tyThingToIfaceDecl (ACoCon _)" (ppr c)
  tyThingToIfaceDecl (ADataCon dc)
   = pprPanic "toIfaceDecl" (ppr dc)    -- Should be trimmed out earlier
  
@@@ -1565,6 -1570,8 +1569,8 @@@ coreRuleToIfaceRule mod rule@(Rule { ru
        -- construct the same ru_rough field as we have right now;
        -- see tcIfaceRule
      do_arg (Type ty) = IfaceType (toIfaceType (deNoteType ty))
+     do_arg (Coercion co) = IfaceType (coToIfaceType co)
+                            
      do_arg arg       = toIfaceExpr arg
  
        -- Compute orphanhood.  See Note [Orphans] in IfaceSyn
@@@ -1584,15 -1591,16 +1590,16 @@@ bogusIfaceRule id_nam
  
  ---------------------
  toIfaceExpr :: CoreExpr -> IfaceExpr
- toIfaceExpr (Var v)       = toIfaceVar v
- toIfaceExpr (Lit l)       = IfaceLit l
- toIfaceExpr (Type ty)     = IfaceType (toIfaceType ty)
- toIfaceExpr (Lam x b)     = IfaceLam (toIfaceBndr x) (toIfaceExpr b)
- toIfaceExpr (App f a)     = toIfaceApp f [a]
- toIfaceExpr (Case s x ty as) = IfaceCase (toIfaceExpr s) (getFS x) (toIfaceType ty) (map toIfaceAlt as)
- toIfaceExpr (Let b e)     = IfaceLet (toIfaceBind b) (toIfaceExpr e)
- toIfaceExpr (Cast e co)   = IfaceCast (toIfaceExpr e) (toIfaceType co)
- toIfaceExpr (Note n e)    = IfaceNote (toIfaceNote n) (toIfaceExpr e)
+ toIfaceExpr (Var v)         = toIfaceVar v
+ toIfaceExpr (Lit l)         = IfaceLit l
+ toIfaceExpr (Type ty)       = IfaceType (toIfaceType ty)
+ toIfaceExpr (Coercion co)   = IfaceCo   (coToIfaceType co)
+ toIfaceExpr (Lam x b)       = IfaceLam (toIfaceBndr x) (toIfaceExpr b)
+ toIfaceExpr (App f a)       = toIfaceApp f [a]
+ toIfaceExpr (Case s x _ as) = IfaceCase (toIfaceExpr s) (getFS x) (map toIfaceAlt as)
+ toIfaceExpr (Let b e)       = IfaceLet (toIfaceBind b) (toIfaceExpr e)
+ toIfaceExpr (Cast e co)     = IfaceCast (toIfaceExpr e) (coToIfaceType co)
+ toIfaceExpr (Note n e)      = IfaceNote (toIfaceNote n) (toIfaceExpr e)
  
  ---------------------
  toIfaceNote :: Note -> IfaceNote
@@@ -21,6 -21,7 +21,7 @@@ import BuildTyC
  import TcRnMonad
  import TcType
  import Type
+ import Coercion
  import TypeRep
  import HscTypes
  import Annotations
@@@ -39,7 -40,6 +40,6 @@@ import TyCo
  import DataCon
  import TysWiredIn
  import TysPrim                ( anyTyConOfKind )
- import Var              ( Var, TyVar )
  import BasicTypes     ( Arity, nonRuleLoopBreaker )
  import qualified Var
  import VarEnv
@@@ -433,6 -433,7 +433,6 @@@ tc_iface_decl parent _ (IfaceData {ifNa
                          ifCtxt = ctxt, ifGadtSyntax = gadt_syn,
                          ifCons = rdr_cons, 
                          ifRec = is_rec, 
 -                        ifGeneric = want_generic,
                          ifFamInst = mb_family })
    = bindIfaceTyVars_AT tv_bndrs $ \ tyvars -> do
      { tc_name <- lookupIfaceTop occ_name
            ; cons <- tcIfaceDataCons tc_name tycon tyvars rdr_cons
            ; mb_fam_inst  <- tcFamInst mb_family
            ; buildAlgTyCon tc_name tyvars stupid_theta cons is_rec
 -                          want_generic gadt_syn parent mb_fam_inst
 +                          gadt_syn parent mb_fam_inst
            })
      ; traceIf (text "tcIfaceDecl4" <+> ppr tycon)
      ; return (ATyCon tycon) }
@@@ -790,20 -791,56 +790,56 @@@ tcIfaceType (IfaceAppTy t1 t2)    = do 
  tcIfaceType (IfaceFunTy t1 t2)    = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2; return (FunTy t1' t2') }
  tcIfaceType (IfaceTyConApp tc ts) = do { tc' <- tcIfaceTyCon tc; ts' <- tcIfaceTypes ts; return (mkTyConApp tc' ts') }
  tcIfaceType (IfaceForAllTy tv t)  = bindIfaceTyVar tv $ \ tv' -> do { t' <- tcIfaceType t; return (ForAllTy tv' t') }
- tcIfaceType (IfacePredTy st)      = do { st' <- tcIfacePredType st; return (PredTy st') }
+ tcIfaceType (IfacePredTy st)      = do { st' <- tcIfacePred tcIfaceType st; return (PredTy st') }
+ tcIfaceType t@(IfaceCoConApp {})  = pprPanic "tcIfaceType" (ppr t)
  
  tcIfaceTypes :: [IfaceType] -> IfL [Type]
  tcIfaceTypes tys = mapM tcIfaceType tys
  
  -----------------------------------------
- tcIfacePredType :: IfacePredType -> IfL PredType
- tcIfacePredType (IfaceClassP cls ts) = do { cls' <- tcIfaceClass cls; ts' <- tcIfaceTypes ts; return (ClassP cls' ts') }
- tcIfacePredType (IfaceIParam ip t)   = do { ip' <- newIPName ip; t' <- tcIfaceType t; return (IParam ip' t') }
- tcIfacePredType (IfaceEqPred t1 t2)  = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2; return (EqPred t1' t2') }
+ tcIfacePred :: (IfaceType -> IfL a) -> IfacePredType -> IfL (Pred a)
+ tcIfacePred tc (IfaceClassP cls ts)
+   = do { cls' <- tcIfaceClass cls; ts' <- mapM tc ts; return (ClassP cls' ts') }
+ tcIfacePred tc (IfaceIParam ip t)
+   = do { ip' <- newIPName ip; t' <- tc t; return (IParam ip' t') }
+ tcIfacePred tc (IfaceEqPred t1 t2)
+   = do { t1' <- tc t1; t2' <- tc t2; return (EqPred t1' t2') }
  
  -----------------------------------------
  tcIfaceCtxt :: IfaceContext -> IfL ThetaType
- tcIfaceCtxt sts = mapM tcIfacePredType sts
+ tcIfaceCtxt sts = mapM (tcIfacePred tcIfaceType) sts
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
+                       Coercions
+ %*                                                                    *
+ %************************************************************************
+ \begin{code}
+ tcIfaceCo :: IfaceType -> IfL Coercion
+ tcIfaceCo (IfaceTyVar n)        = mkCoVarCo <$> tcIfaceCoVar n
+ tcIfaceCo (IfaceAppTy t1 t2)    = mkAppCo <$> tcIfaceCo t1 <*> tcIfaceCo t2
+ tcIfaceCo (IfaceFunTy t1 t2)    = mkFunCo <$> tcIfaceCo t1 <*> tcIfaceCo t2
+ tcIfaceCo (IfaceTyConApp tc ts) = mkTyConAppCo <$> tcIfaceTyCon tc <*> mapM tcIfaceCo ts
+ tcIfaceCo (IfaceCoConApp tc ts) = tcIfaceCoApp tc ts
+ tcIfaceCo (IfaceForAllTy tv t)  = bindIfaceTyVar tv $ \ tv' ->
+                                   mkForAllCo tv' <$> tcIfaceCo t
+ -- tcIfaceCo (IfacePredTy co)      = mkPredCo <$> tcIfacePred tcIfaceCo co
+ tcIfaceCo (IfacePredTy _)      = panic "tcIfaceCo"
+ tcIfaceCoApp :: IfaceCoCon -> [IfaceType] -> IfL Coercion
+ tcIfaceCoApp IfaceReflCo    [t]     = Refl         <$> tcIfaceType t
+ tcIfaceCoApp (IfaceCoAx n)  ts      = AxiomInstCo  <$> tcIfaceCoAxiom n <*> mapM tcIfaceCo ts
+ tcIfaceCoApp IfaceUnsafeCo  [t1,t2] = UnsafeCo     <$> tcIfaceType t1 <*> tcIfaceType t2
+ tcIfaceCoApp IfaceSymCo     [t]     = SymCo        <$> tcIfaceCo t
+ tcIfaceCoApp IfaceTransCo   [t1,t2] = TransCo      <$> tcIfaceCo t1 <*> tcIfaceCo t2
+ tcIfaceCoApp IfaceInstCo    [t1,t2] = InstCo       <$> tcIfaceCo t1 <*> tcIfaceType t2
+ tcIfaceCoApp (IfaceNthCo d) [t]     = NthCo d      <$> tcIfaceCo t
+ tcIfaceCoApp cc ts = pprPanic "toIfaceCoApp" (ppr cc <+> ppr ts)
+ tcIfaceCoVar :: FastString -> IfL CoVar
+ tcIfaceCoVar = tcIfaceLclId
  \end{code}
  
  
@@@ -818,6 -855,12 +854,12 @@@ tcIfaceExpr :: IfaceExpr -> IfL CoreExp
  tcIfaceExpr (IfaceType ty)
    = Type <$> tcIfaceType ty
  
+ tcIfaceExpr (IfaceCo co)
+   = Coercion <$> tcIfaceCo co
+ tcIfaceExpr (IfaceCast expr co)
+   = Cast <$> tcIfaceExpr expr <*> tcIfaceCo co
  tcIfaceExpr (IfaceLcl name)
    = Var <$> tcIfaceLclId name
  
@@@ -852,7 -895,7 +894,7 @@@ tcIfaceExpr (IfaceLam bndr body
  tcIfaceExpr (IfaceApp fun arg)
    = App <$> tcIfaceExpr fun <*> tcIfaceExpr arg
  
- tcIfaceExpr (IfaceCase scrut case_bndr ty alts)  = do
+ tcIfaceExpr (IfaceCase scrut case_bndr alts)  = do
      scrut' <- tcIfaceExpr scrut
      case_bndr_name <- newIfaceName (mkVarOccFS case_bndr)
      let
  
      extendIfaceIdEnv [case_bndr'] $ do
       alts' <- mapM (tcIfaceAlt scrut' tc_app) alts
-      ty' <- tcIfaceType ty
-      return (Case scrut' case_bndr' ty' alts')
+      return (Case scrut' case_bndr' (coreAltsType alts') alts')
  
  tcIfaceExpr (IfaceLet (IfaceNonRec (IfLetBndr fs ty info) rhs) body)
    = do        { name    <- newIfaceName (mkVarOccFS fs)
@@@ -897,11 -939,6 +938,6 @@@ tcIfaceExpr (IfaceLet (IfaceRec pairs) 
                                  (idName id) (idType id) info
            ; return (setIdInfo id id_info, rhs') }
  
- tcIfaceExpr (IfaceCast expr co) = do
-     expr' <- tcIfaceExpr expr
-     co' <- tcIfaceType co
-     return (Cast expr' co')
  tcIfaceExpr (IfaceNote note expr) = do
      expr' <- tcIfaceExpr expr
      case note of
@@@ -941,14 -978,13 +977,13 @@@ tcIfaceDataAlt :: DataCon -> [Type] -> 
  tcIfaceDataAlt con inst_tys arg_strs rhs
    = do        { us <- newUniqueSupply
        ; let uniqs = uniqsFromSupply us
-       ; let (ex_tvs, co_tvs, arg_ids)
+       ; let (ex_tvs, arg_ids)
                      = dataConRepFSInstPat arg_strs uniqs con inst_tys
-               all_tvs = ex_tvs ++ co_tvs
  
-       ; rhs' <- extendIfaceTyVarEnv all_tvs   $
+       ; rhs' <- extendIfaceTyVarEnv ex_tvs    $
                  extendIfaceIdEnv arg_ids      $
                  tcIfaceExpr rhs
-       ; return (DataAlt con, all_tvs ++ arg_ids, rhs') }
+       ; return (DataAlt con, ex_tvs ++ arg_ids, rhs') }
  \end{code}
  
  
@@@ -1216,6 -1252,10 +1251,10 @@@ tcIfaceClass :: Name -> IfL Clas
  tcIfaceClass name = do { thing <- tcIfaceGlobal name
                       ; return (tyThingClass thing) }
  
+ tcIfaceCoAxiom :: Name -> IfL CoAxiom
+ tcIfaceCoAxiom name = do { thing <- tcIfaceGlobal name
+                        ; return (tyThingCoAxiom thing) }
  tcIfaceDataCon :: Name -> IfL DataCon
  tcIfaceDataCon name = do { thing <- tcIfaceGlobal name
                         ; case thing of
@@@ -320,6 -320,7 +320,6 @@@ data ExtensionFla
     | Opt_TemplateHaskell
     | Opt_QuasiQuotes
     | Opt_ImplicitParams
 -   | Opt_Generics                     -- "Derivable type classes"
     | Opt_ImplicitPrelude
     | Opt_ScopedTypeVariables
     | Opt_UnboxedTuples
     | Opt_DeriveFunctor
     | Opt_DeriveTraversable
     | Opt_DeriveFoldable
 +   | Opt_DeriveGeneric            -- Allow deriving Generic/1
 +   | Opt_DefaultSignatures        -- Allow extra signatures for defmeths
 +   | Opt_Generics                 -- Old generic classes, now deprecated
  
     | Opt_TypeSynonymInstances
     | Opt_FlexibleContexts
@@@ -1628,8 -1626,7 +1628,8 @@@ xFlags = 
    ( "ParallelArrays",                   Opt_ParallelArrays, nop ),
    ( "TemplateHaskell",                  Opt_TemplateHaskell, checkTemplateHaskellOk ),
    ( "QuasiQuotes",                      Opt_QuasiQuotes, nop ),
 -  ( "Generics",                         Opt_Generics, nop ),
 +  ( "Generics",                         Opt_Generics,
 +    \ _ -> deprecate "it does nothing; look into -XDefaultSignatures and -XDeriveGeneric for generic programming support." ),
    ( "ImplicitPrelude",                  Opt_ImplicitPrelude, nop ),
    ( "RecordWildCards",                  Opt_RecordWildCards, nop ),
    ( "NamedFieldPuns",                   Opt_RecordPuns, nop ),
    ( "DeriveFunctor",                    Opt_DeriveFunctor, nop ),
    ( "DeriveTraversable",                Opt_DeriveTraversable, nop ),
    ( "DeriveFoldable",                   Opt_DeriveFoldable, nop ),
 +  ( "DeriveGeneric",                    Opt_DeriveGeneric, nop ),
 +  ( "DefaultSignatures",                Opt_DefaultSignatures, nop ),
    ( "TypeSynonymInstances",             Opt_TypeSynonymInstances, nop ),
    ( "FlexibleContexts",                 Opt_FlexibleContexts, nop ),
    ( "FlexibleInstances",                Opt_FlexibleInstances, nop ),
@@@ -1853,7 -1848,6 +1853,7 @@@ glasgowExtsFlags = 
             , Opt_DeriveFunctor
             , Opt_DeriveFoldable
             , Opt_DeriveTraversable
 +           , Opt_DeriveGeneric
             , Opt_FlexibleContexts
             , Opt_FlexibleInstances
             , Opt_ConstrainedClassMethods
@@@ -1985,14 -1979,13 +1985,13 @@@ forceRecompile :: DynP (
  -- recompiled which probably isn't what you want
  forceRecompile = do { dfs <- liftEwM getCmdLineState
                    ; when (force_recomp dfs) (setDynFlag Opt_ForceRecomp) }
-       where
+         where
          force_recomp dfs = isOneShot (ghcMode dfs)
  
  setVerboseCore2Core :: DynP ()
  setVerboseCore2Core = do forceRecompile
                           setDynFlag Opt_D_verbose_core2core 
                           upd (\dfs -> dfs { shouldDumpSimplPhase = Nothing })
-                        
  
  setDumpSimplPhases :: String -> DynP ()
  setDumpSimplPhases s = do forceRecompile
@@@ -2133,7 -2126,6 +2132,6 @@@ addImportPath, addLibraryPath, addInclu
  addImportPath "" = upd (\s -> s{importPaths = []})
  addImportPath p  = upd (\s -> s{importPaths = importPaths s ++ splitPathList p})
  
  addLibraryPath p =
    upd (\s -> s{libraryPaths = libraryPaths s ++ splitPathList p})
  
@@@ -94,7 -94,7 +94,7 @@@ isUnboundName name = name `hasKey` unbo
  %*                                                                      *
  %************************************************************************
  
 -This section tells what the compiler knows about the assocation of
 +This section tells what the compiler knows about the association of
  names with uniques.  These ones are the *non* wired-in ones.  The
  wired in ones are defined in TysWiredIn etc.
  
@@@ -222,11 -222,7 +222,11 @@@ basicKnownKeyName
        -- dotnet interop
        , objectTyConName, marshalObjectName, unmarshalObjectName
        , marshalStringName, unmarshalStringName, checkDotnetResName
 -
 +      
 +      -- Generics
 +      , genClassName, gen1ClassName
 +      , datatypeClassName, constructorClassName, selectorClassName
 +      
          -- Monad comprehensions
          , guardMName
          , liftMName
      ]
  
  genericTyConNames :: [Name]
 -genericTyConNames = [crossTyConName, plusTyConName, genUnitTyConName]
 +genericTyConNames = [
 +    v1TyConName, u1TyConName, par1TyConName, rec1TyConName,
 +    k1TyConName, m1TyConName, sumTyConName, prodTyConName,
 +    compTyConName, rTyConName, pTyConName, dTyConName,
 +    cTyConName, sTyConName, rec0TyConName, par0TyConName,
 +    d1TyConName, c1TyConName, s1TyConName, noSelTyConName,
 +    repTyConName, rep1TyConName
 +  ]
  
  -- Know names from the DPH package which vary depending on the selected DPH backend.
  --
@@@ -274,7 -263,7 +274,7 @@@ pRELUDE            = mkBaseModule_ pRELUDE_NAM
  
  gHC_PRIM, gHC_TYPES, gHC_UNIT, gHC_ORDERING, gHC_GENERICS,
      gHC_MAGIC,
 -    gHC_CLASSES, gHC_BASE, gHC_ENUM,
 +    gHC_CLASSES, gHC_BASE, gHC_ENUM, gHC_CSTRING,
      gHC_SHOW, gHC_READ, gHC_NUM, gHC_INTEGER, gHC_INTEGER_TYPE, gHC_LIST,
      gHC_TUPLE, dATA_TUPLE, dATA_EITHER, dATA_STRING, dATA_FOLDABLE, dATA_TRAVERSABLE,
      gHC_PACK, gHC_CONC, gHC_IO, gHC_IO_Exception,
@@@ -290,7 -279,6 +290,7 @@@ gHC_UNIT   = mkPrimModule (fsLit "GHC.Uni
  gHC_ORDERING  = mkPrimModule (fsLit "GHC.Ordering")
  gHC_GENERICS  = mkPrimModule (fsLit "GHC.Generics")
  gHC_MAGIC     = mkPrimModule (fsLit "GHC.Magic")
 +gHC_CSTRING   = mkPrimModule (fsLit "GHC.CString")
  
  gHC_CLASSES   = mkBaseModule (fsLit "GHC.Classes")
  gHC_BASE      = mkBaseModule (fsLit "GHC.Base")
@@@ -547,59 -535,12 +547,59 @@@ mkTyConRep_RDR = varQual_RDR tYPEABLE (
  undefined_RDR :: RdrName
  undefined_RDR = varQual_RDR gHC_ERR (fsLit "undefined")
  
 +error_RDR :: RdrName
 +error_RDR = varQual_RDR gHC_ERR (fsLit "error")
 +
 +-- Old Generics (constructors and functions)
  crossDataCon_RDR, inlDataCon_RDR, inrDataCon_RDR, genUnitDataCon_RDR :: RdrName
  crossDataCon_RDR   = dataQual_RDR gHC_GENERICS (fsLit ":*:")
  inlDataCon_RDR     = dataQual_RDR gHC_GENERICS (fsLit "Inl")
  inrDataCon_RDR     = dataQual_RDR gHC_GENERICS (fsLit "Inr")
  genUnitDataCon_RDR = dataQual_RDR gHC_GENERICS (fsLit "Unit")
  
 +-- Generics (constructors and functions)
 +u1DataCon_RDR, par1DataCon_RDR, rec1DataCon_RDR,
 +  k1DataCon_RDR, m1DataCon_RDR, l1DataCon_RDR, r1DataCon_RDR,
 +  prodDataCon_RDR, comp1DataCon_RDR, from_RDR, from1_RDR,
 +  to_RDR, to1_RDR, datatypeName_RDR, moduleName_RDR, conName_RDR,
 +  conFixity_RDR, conIsRecord_RDR,
 +  noArityDataCon_RDR, arityDataCon_RDR, selName_RDR,
 +  prefixDataCon_RDR, infixDataCon_RDR, leftAssocDataCon_RDR,
 +  rightAssocDataCon_RDR, notAssocDataCon_RDR :: RdrName
 +
 +u1DataCon_RDR    = dataQual_RDR gHC_GENERICS (fsLit "U1")
 +par1DataCon_RDR  = dataQual_RDR gHC_GENERICS (fsLit "Par1")
 +rec1DataCon_RDR  = dataQual_RDR gHC_GENERICS (fsLit "Rec1")
 +k1DataCon_RDR    = dataQual_RDR gHC_GENERICS (fsLit "K1")
 +m1DataCon_RDR    = dataQual_RDR gHC_GENERICS (fsLit "M1")
 +
 +l1DataCon_RDR     = dataQual_RDR gHC_GENERICS (fsLit "L1")
 +r1DataCon_RDR     = dataQual_RDR gHC_GENERICS (fsLit "R1")
 +
 +prodDataCon_RDR   = dataQual_RDR gHC_GENERICS (fsLit ":*:")
 +comp1DataCon_RDR  = dataQual_RDR gHC_GENERICS (fsLit "Comp1")
 +
 +from_RDR  = varQual_RDR gHC_GENERICS (fsLit "from")
 +from1_RDR = varQual_RDR gHC_GENERICS (fsLit "from1")
 +to_RDR    = varQual_RDR gHC_GENERICS (fsLit "to")
 +to1_RDR   = varQual_RDR gHC_GENERICS (fsLit "to1")
 +
 +datatypeName_RDR  = varQual_RDR gHC_GENERICS (fsLit "datatypeName")
 +moduleName_RDR    = varQual_RDR gHC_GENERICS (fsLit "moduleName")
 +selName_RDR       = varQual_RDR gHC_GENERICS (fsLit "selName")
 +conName_RDR       = varQual_RDR gHC_GENERICS (fsLit "conName")
 +conFixity_RDR     = varQual_RDR gHC_GENERICS (fsLit "conFixity")
 +conIsRecord_RDR   = varQual_RDR gHC_GENERICS (fsLit "conIsRecord")
 +
 +noArityDataCon_RDR    = dataQual_RDR gHC_GENERICS (fsLit "NoArity")
 +arityDataCon_RDR      = dataQual_RDR gHC_GENERICS (fsLit "Arity")
 +prefixDataCon_RDR     = dataQual_RDR gHC_GENERICS (fsLit "Prefix")
 +infixDataCon_RDR      = dataQual_RDR gHC_GENERICS (fsLit "Infix")
 +leftAssocDataCon_RDR  = dataQual_RDR gHC_GENERICS (fsLit "LeftAssociative")
 +rightAssocDataCon_RDR = dataQual_RDR gHC_GENERICS (fsLit "RightAssociative")
 +notAssocDataCon_RDR   = dataQual_RDR gHC_GENERICS (fsLit "NotAssociative")
 +
 +
  fmap_RDR, pure_RDR, ap_RDR, foldable_foldr_RDR, traverse_RDR :: RdrName
  fmap_RDR              = varQual_RDR gHC_BASE (fsLit "fmap")
  pure_RDR              = varQual_RDR cONTROL_APPLICATIVE (fsLit "pure")
@@@ -645,48 -586,19 +645,48 @@@ eitherTyConName   = tcQual  dATA_EITHE
  leftDataConName   = conName dATA_EITHER (fsLit "Left")   leftDataConKey
  rightDataConName  = conName dATA_EITHER (fsLit "Right")  rightDataConKey
  
 --- Generics
 -crossTyConName, plusTyConName, genUnitTyConName :: Name
 -crossTyConName     = tcQual   gHC_GENERICS (fsLit ":*:") crossTyConKey
 -plusTyConName      = tcQual   gHC_GENERICS (fsLit ":+:") plusTyConKey
 -genUnitTyConName   = tcQual   gHC_GENERICS (fsLit "Unit") genUnitTyConKey
 +-- Generics (types)
 +v1TyConName, u1TyConName, par1TyConName, rec1TyConName,
 +  k1TyConName, m1TyConName, sumTyConName, prodTyConName,
 +  compTyConName, rTyConName, pTyConName, dTyConName, 
 +  cTyConName, sTyConName, rec0TyConName, par0TyConName,
 +  d1TyConName, c1TyConName, s1TyConName, noSelTyConName,
 +  repTyConName, rep1TyConName :: Name
 +
 +v1TyConName  = tcQual gHC_GENERICS (fsLit "V1") v1TyConKey
 +u1TyConName  = tcQual gHC_GENERICS (fsLit "U1") u1TyConKey
 +par1TyConName  = tcQual gHC_GENERICS (fsLit "Par1") par1TyConKey
 +rec1TyConName  = tcQual gHC_GENERICS (fsLit "Rec1") rec1TyConKey
 +k1TyConName  = tcQual gHC_GENERICS (fsLit "K1") k1TyConKey
 +m1TyConName  = tcQual gHC_GENERICS (fsLit "M1") m1TyConKey
 +
 +sumTyConName    = tcQual gHC_GENERICS (fsLit ":+:") sumTyConKey
 +prodTyConName   = tcQual gHC_GENERICS (fsLit ":*:") prodTyConKey
 +compTyConName   = tcQual gHC_GENERICS (fsLit ":.:") compTyConKey
 +
 +rTyConName  = tcQual gHC_GENERICS (fsLit "R") rTyConKey
 +pTyConName  = tcQual gHC_GENERICS (fsLit "P") pTyConKey
 +dTyConName  = tcQual gHC_GENERICS (fsLit "D") dTyConKey
 +cTyConName  = tcQual gHC_GENERICS (fsLit "C") cTyConKey
 +sTyConName  = tcQual gHC_GENERICS (fsLit "S") sTyConKey
 +
 +rec0TyConName  = tcQual gHC_GENERICS (fsLit "Rec0") rec0TyConKey
 +par0TyConName  = tcQual gHC_GENERICS (fsLit "Par0") par0TyConKey
 +d1TyConName  = tcQual gHC_GENERICS (fsLit "D1") d1TyConKey
 +c1TyConName  = tcQual gHC_GENERICS (fsLit "C1") c1TyConKey
 +s1TyConName  = tcQual gHC_GENERICS (fsLit "S1") s1TyConKey
 +noSelTyConName = tcQual gHC_GENERICS (fsLit "NoSelector") noSelTyConKey
 +
 +repTyConName  = tcQual gHC_GENERICS (fsLit "Rep")  repTyConKey
 +rep1TyConName = tcQual gHC_GENERICS (fsLit "Rep1") rep1TyConKey
  
  -- Base strings Strings
  unpackCStringName, unpackCStringAppendName, unpackCStringFoldrName,
      unpackCStringUtf8Name, eqStringName, stringTyConName :: Name
 -unpackCStringName       = varQual gHC_BASE (fsLit "unpackCString#") unpackCStringIdKey
 -unpackCStringAppendName = varQual gHC_BASE (fsLit "unpackAppendCString#") unpackCStringAppendIdKey
 -unpackCStringFoldrName  = varQual gHC_BASE (fsLit "unpackFoldrCString#") unpackCStringFoldrIdKey
 -unpackCStringUtf8Name   = varQual gHC_BASE (fsLit "unpackCStringUtf8#") unpackCStringUtf8IdKey
 +unpackCStringName       = varQual gHC_CSTRING (fsLit "unpackCString#") unpackCStringIdKey
 +unpackCStringAppendName = varQual gHC_CSTRING (fsLit "unpackAppendCString#") unpackCStringAppendIdKey
 +unpackCStringFoldrName  = varQual gHC_CSTRING (fsLit "unpackFoldrCString#") unpackCStringFoldrIdKey
 +unpackCStringUtf8Name   = varQual gHC_CSTRING (fsLit "unpackCStringUtf8#") unpackCStringUtf8IdKey
  eqStringName          = varQual gHC_BASE (fsLit "eqString")  eqStringIdKey
  stringTyConName         = tcQual  gHC_BASE (fsLit "String") stringTyConKey
  
@@@ -854,16 -766,6 +854,16 @@@ showClassName      = clsQual gHC_SHOW (fsL
  readClassName :: Name
  readClassName    = clsQual gHC_READ (fsLit "Read") readClassKey
  
 +-- Classes Generic and Generic1, Datatype, Constructor and Selector
 +genClassName, gen1ClassName, datatypeClassName, constructorClassName,
 +  selectorClassName :: Name
 +genClassName  = clsQual gHC_GENERICS (fsLit "Generic")  genClassKey
 +gen1ClassName = clsQual gHC_GENERICS (fsLit "Generic1") gen1ClassKey
 +
 +datatypeClassName = clsQual gHC_GENERICS (fsLit "Datatype") datatypeClassKey
 +constructorClassName = clsQual gHC_GENERICS (fsLit "Constructor") constructorClassKey
 +selectorClassName = clsQual gHC_GENERICS (fsLit "Selector") selectorClassKey
 +
  -- parallel array types and functions
  enumFromToPName, enumFromThenToPName, nullPName, lengthPName,
      singletonPName, replicatePName, mapPName, filterPName,
@@@ -1061,15 -963,6 +1061,15 @@@ applicativeClassKey, foldableClassKey, 
  applicativeClassKey   = mkPreludeClassUnique 34
  foldableClassKey      = mkPreludeClassUnique 35
  traversableClassKey   = mkPreludeClassUnique 36
 +
 +genClassKey, gen1ClassKey, datatypeClassKey, constructorClassKey,
 +  selectorClassKey :: Unique
 +genClassKey   = mkPreludeClassUnique 37
 +gen1ClassKey  = mkPreludeClassUnique 38
 +
 +datatypeClassKey    = mkPreludeClassUnique 39
 +constructorClassKey = mkPreludeClassUnique 40
 +selectorClassKey    = mkPreludeClassUnique 41
  \end{code}
  
  %************************************************************************
@@@ -1129,11 -1022,12 +1129,12 @@@ statePrimTyConKey, stableNamePrimTyConK
      word32PrimTyConKey, word32TyConKey, word64PrimTyConKey, word64TyConKey,
      liftedConKey, unliftedConKey, anyBoxConKey, kindConKey, boxityConKey,
      typeConKey, threadIdPrimTyConKey, bcoPrimTyConKey, ptrTyConKey,
-     funPtrTyConKey, tVarPrimTyConKey :: Unique
+     funPtrTyConKey, tVarPrimTyConKey, eqPredPrimTyConKey :: Unique
  statePrimTyConKey                     = mkPreludeTyConUnique 50
  stableNamePrimTyConKey                        = mkPreludeTyConUnique 51
- stableNameTyConKey                    = mkPreludeTyConUnique 52
- mutVarPrimTyConKey                    = mkPreludeTyConUnique 55
+ stableNameTyConKey                      = mkPreludeTyConUnique 52
+ eqPredPrimTyConKey                      = mkPreludeTyConUnique 53
+ mutVarPrimTyConKey                      = mkPreludeTyConUnique 55
  ioTyConKey                            = mkPreludeTyConUnique 56
  wordPrimTyConKey                      = mkPreludeTyConUnique 58
  wordTyConKey                          = mkPreludeTyConUnique 59
@@@ -1155,6 -1049,12 +1156,6 @@@ ptrTyConKey                            = mkPreludeTyConUnique 7
  funPtrTyConKey                                = mkPreludeTyConUnique 75
  tVarPrimTyConKey                      = mkPreludeTyConUnique 76
  
 --- Generic Type Constructors
 -crossTyConKey, plusTyConKey, genUnitTyConKey :: Unique
 -crossTyConKey                         = mkPreludeTyConUnique 79
 -plusTyConKey                          = mkPreludeTyConUnique 80
 -genUnitTyConKey                               = mkPreludeTyConUnique 81
 -
  -- Parallel array type constructor
  parrTyConKey :: Unique
  parrTyConKey                          = mkPreludeTyConUnique 82
@@@ -1167,9 -1067,8 +1168,8 @@@ eitherTyConKey :: Uniqu
  eitherTyConKey                                = mkPreludeTyConUnique 84
  
  -- Super Kinds constructors
- tySuperKindTyConKey, coSuperKindTyConKey :: Unique
+ tySuperKindTyConKey :: Unique
  tySuperKindTyConKey                    = mkPreludeTyConUnique 85
- coSuperKindTyConKey                    = mkPreludeTyConUnique 86
  
  -- Kind constructors
  liftedTypeKindTyConKey, openTypeKindTyConKey, unliftedTypeKindTyConKey,
@@@ -1206,41 -1105,6 +1206,41 @@@ opaqueTyConKe
  stringTyConKey :: Unique
  stringTyConKey                                = mkPreludeTyConUnique 134
  
 +-- Generics (Unique keys)
 +v1TyConKey, u1TyConKey, par1TyConKey, rec1TyConKey,
 +  k1TyConKey, m1TyConKey, sumTyConKey, prodTyConKey,
 +  compTyConKey, rTyConKey, pTyConKey, dTyConKey,
 +  cTyConKey, sTyConKey, rec0TyConKey, par0TyConKey,
 +  d1TyConKey, c1TyConKey, s1TyConKey, noSelTyConKey,
 +  repTyConKey, rep1TyConKey :: Unique
 +
 +v1TyConKey    = mkPreludeTyConUnique 135
 +u1TyConKey    = mkPreludeTyConUnique 136
 +par1TyConKey  = mkPreludeTyConUnique 137
 +rec1TyConKey  = mkPreludeTyConUnique 138
 +k1TyConKey    = mkPreludeTyConUnique 139
 +m1TyConKey    = mkPreludeTyConUnique 140
 +
 +sumTyConKey   = mkPreludeTyConUnique 141
 +prodTyConKey  = mkPreludeTyConUnique 142
 +compTyConKey  = mkPreludeTyConUnique 143
 +
 +rTyConKey = mkPreludeTyConUnique 144
 +pTyConKey = mkPreludeTyConUnique 145
 +dTyConKey = mkPreludeTyConUnique 146
 +cTyConKey = mkPreludeTyConUnique 147
 +sTyConKey = mkPreludeTyConUnique 148
 +
 +rec0TyConKey  = mkPreludeTyConUnique 149
 +par0TyConKey  = mkPreludeTyConUnique 150
 +d1TyConKey    = mkPreludeTyConUnique 151
 +c1TyConKey    = mkPreludeTyConUnique 152
 +s1TyConKey    = mkPreludeTyConUnique 153
 +noSelTyConKey = mkPreludeTyConUnique 154
 +
 +repTyConKey  = mkPreludeTyConUnique 155
 +rep1TyConKey = mkPreludeTyConUnique 156
 +
  ---------------- Template Haskell -------------------
  --    USES TyConUniques 200-299
  -----------------------------------------------------
@@@ -1393,6 -1257,9 +1393,9 @@@ mapIdKey              = mkPreludeMiscIdUnique 
  groupWithIdKey        = mkPreludeMiscIdUnique 70
  dollarIdKey           = mkPreludeMiscIdUnique 71
  
+ coercionTokenIdKey :: Unique
+ coercionTokenIdKey    = mkPreludeMiscIdUnique 72
  -- Parallel array functions
  singletonPIdKey, nullPIdKey, lengthPIdKey, replicatePIdKey, mapPIdKey,
      filterPIdKey, zipPIdKey, crossMapPIdKey, indexPIdKey, toPIdKey,
@@@ -64,23 -64,14 +64,14 @@@ import TysPri
  -- others:
  import Constants      ( mAX_TUPLE_SIZE )
  import Module         ( Module )
+ import DataCon          ( DataCon, mkDataCon, dataConWorkId, dataConSourceArity )
+ import Var
+ import TyCon
+ import TypeRep
  import RdrName
  import Name
- import DataCon                ( DataCon, mkDataCon, dataConWorkId, dataConSourceArity )
- import Var
- import TyCon          ( TyCon, AlgTyConRhs(DataTyCon), tyConDataCons,
-                         mkTupleTyCon, mkAlgTyCon, tyConName,
-                         TyConParent(NoParentTyCon) )
- import BasicTypes     ( Arity, RecFlag(..), Boxity(..), isBoxed, HsBang(..) )
- import Type           ( Type, mkTyConTy, mkTyConApp, mkTyVarTy, mkTyVarTys,
-                         TyThing(..) )
- import Coercion         ( unsafeCoercionTyCon, symCoercionTyCon,
-                           transCoercionTyCon, leftCoercionTyCon, 
-                           rightCoercionTyCon, instCoercionTyCon )
- import TypeRep          ( mkArrowKinds, liftedTypeKind, ubxTupleKind )
- import Unique         ( incrUnique, mkTupleTyConUnique,
+ import BasicTypes       ( Arity, RecFlag(..), Boxity(..), isBoxed, HsBang(..) )
+ import Unique           ( incrUnique, mkTupleTyConUnique,
                          mkTupleDataConUnique, mkPArrDataConUnique )
  import Data.Array
  import FastString
@@@ -124,12 -115,6 +115,6 @@@ wiredInTyCons = [ unitTyCon       -- Not trea
              , intTyCon
              , listTyCon
              , parrTyCon
-               , unsafeCoercionTyCon
-               , symCoercionTyCon
-               , transCoercionTyCon
-               , leftCoercionTyCon
-               , rightCoercionTyCon
-               , instCoercionTyCon
              ]
  \end{code}
  
@@@ -211,6 -196,7 +196,6 @@@ pcTyCon is_enum is_rec name tyvars con
                (DataTyCon cons is_enum)
                NoParentTyCon
                  is_rec
 -              True            -- All the wired-in tycons have generics
                False           -- Not in GADT syntax
  
  pcDataCon :: Name -> [TyVar] -> [Type] -> TyCon -> DataCon
@@@ -275,7 -261,7 +260,7 @@@ unboxedTupleArr = listArray (0,mAX_TUPL
  mk_tuple :: Boxity -> Int -> (TyCon,DataCon)
  mk_tuple boxity arity = (tycon, tuple_con)
    where
 -      tycon   = mkTupleTyCon tc_name tc_kind arity tyvars tuple_con boxity gen_info 
 +      tycon   = mkTupleTyCon tc_name tc_kind arity tyvars tuple_con boxity 
        modu    = mkTupleModule boxity arity
        tc_name = mkWiredInName modu (mkTupleOcc tcName boxity arity) tc_uniq
                                (ATyCon tycon) BuiltInSyntax
                                  (ADataCon tuple_con) BuiltInSyntax
        tc_uniq   = mkTupleTyConUnique   boxity arity
        dc_uniq   = mkTupleDataConUnique boxity arity
 -      gen_info  = True                -- Tuples all have generics..
 -                                      -- hmm: that's a *lot* of code
  
  unitTyCon :: TyCon
  unitTyCon     = tupleTyCon Boxed 0
@@@ -607,5 -595,3 +592,3 @@@ mkPArrFakeCon arity  = data_co
  isPArrFakeCon      :: DataCon -> Bool
  isPArrFakeCon dcon  = dcon == parrFakeCon (dataConSourceArity dcon)
  \end{code}
@@@ -26,6 -26,7 +26,6 @@@ module RnBinds 
  import {-# SOURCE #-} RnExpr( rnLExpr, rnStmts )
  
  import HsSyn
 -import RdrHsSyn
  import RnHsSyn
  import TcRnMonad
  import RnTypes        ( rnHsSigType, rnLHsType, checkPrecMatch)
@@@ -457,7 -458,7 +457,7 @@@ rnBind :: (Name -> [Name])         -- Signatur
  rnBind _ trim (L loc bind@(PatBind { pat_lhs = pat
                                     , pat_rhs = grhss 
                                        -- pat fvs were stored in bind_fvs
-                                       -- after processing the LHS          
+                                       -- after processing the LHS
                                     , bind_fvs = pat_fvs }))
    = setSrcSpan loc $ 
      do        { let bndrs = collectPatBinders pat
@@@ -477,7 -478,7 +477,7 @@@ rnBind sig_fn tri
                              , fun_infix = is_infix 
                              , fun_matches = matches })) 
         -- invariant: no free vars here when it's a FunBind
-   = setSrcSpan loc $ 
+   = setSrcSpan loc $
      do        { let plain_name = unLoc name
  
        ; (matches', fvs) <- bindSigTyVarsFV (sig_fn plain_name) $
@@@ -585,33 -586,23 +585,33 @@@ a binder
  \begin{code}
  rnMethodBinds :: Name                 -- Class name
              -> (Name -> [Name])       -- Signature tyvar function
              -> LHsBinds RdrName
              -> RnM (LHsBinds Name, FreeVars)
  
 -rnMethodBinds cls sig_fn gen_tyvars binds
 -  = foldlM do_one (emptyBag,emptyFVs) (bagToList binds)
 +rnMethodBinds cls sig_fn binds
 +  = do { checkDupRdrNames meth_names
 +           -- Check that the same method is not given twice in the
 +           -- same instance decl      instance C T where
 +           --                       f x = ...
 +           --                       g y = ...
 +           --                       f x = ...
 +           -- We must use checkDupRdrNames because the Name of the
 +           -- method is the Name of the class selector, whose SrcSpan
 +           -- points to the class declaration; and we use rnMethodBinds
 +           -- for instance decls too
 +
 +       ; foldlM do_one (emptyBag, emptyFVs) (bagToList binds) }
    where 
 +    meth_names  = collectMethodBinders binds
      do_one (binds,fvs) bind 
 -       = do { (bind', fvs_bind) <- rnMethodBind cls sig_fn gen_tyvars bind
 +       = do { (bind', fvs_bind) <- rnMethodBind cls sig_fn bind
            ; return (binds `unionBags` bind', fvs_bind `plusFV` fvs) }
  
  rnMethodBind :: Name
              -> (Name -> [Name])
 -            -> [Name]
              -> LHsBindLR RdrName RdrName
              -> RnM (Bag (LHsBindLR Name Name), FreeVars)
 -rnMethodBind cls sig_fn gen_tyvars 
 +rnMethodBind cls sig_fn 
               (L loc bind@(FunBind { fun_id = name, fun_infix = is_infix 
                                  , fun_matches = MatchGroup matches _ }))
    = setSrcSpan loc $ do
          -- We use the selector name as the binder
  
      (new_matches, fvs) <- bindSigTyVarsFV (sig_fn plain_name) $
 -                          mapFvRn (rn_match (FunRhs plain_name is_infix)) matches
 +                          mapFvRn (rnMatch (FunRhs plain_name is_infix)) matches
      let new_group = MatchGroup new_matches placeHolderType
  
      when is_infix $ checkPrecMatch plain_name new_group
                                   , bind_fvs    = fvs })),
               fvs `addOneFV` plain_name)
          -- The 'fvs' field isn't used for method binds
 -  where
 -      -- Truly gruesome; bring into scope the correct members of the generic 
 -      -- type variables.  See comments in RnSource.rnSourceDecl(ClassDecl)
 -    rn_match info match@(L _ (Match (L _ (TypePat ty) : _) _ _))
 -      = extendTyVarEnvFVRn gen_tvs    $
 -        rnMatch info match
 -      where
 -        tvs     = map (rdrNameOcc.unLoc) (extractHsTyRdrTyVars ty)
 -        gen_tvs = [tv | tv <- gen_tyvars, nameOccName tv `elem` tvs] 
 -
 -    rn_match info match = rnMatch info match
  
  -- Can't handle method pattern-bindings which bind multiple methods.
 -rnMethodBind _ _ _ (L loc bind@(PatBind {})) = do
 +rnMethodBind _ _ (L loc bind@(PatBind {})) = do
      addErrAt loc (methodBindErr bind)
      return (emptyBag, emptyFVs)
  
 -rnMethodBind _ _ _ b = pprPanic "rnMethodBind" (ppr b)
 +rnMethodBind _ _ b = pprPanic "rnMethodBind" (ppr b)
  \end{code}
  
  
@@@ -666,12 -668,7 +666,12 @@@ renameSigs mb_names ok_sig sig
                -- Check for duplicates on RdrName version, 
                -- because renamed version has unboundName for
                -- not-in-scope binders, which gives bogus dup-sig errors
 -
 +              -- NB: in a class decl, a 'generic' sig is not considered 
 +              --     equal to an ordinary sig, so we allow, say
 +              --           class C a where
 +              --             op :: a -> a
 +              --             default op :: Eq a => a -> a
 +              
        ; sigs' <- mapM (wrapLocM (renameSig mb_names)) sigs
  
        ; let (good_sigs, bad_sigs) = partition (ok_sig . unLoc) sigs'
@@@ -698,13 -695,6 +698,13 @@@ renameSig mb_names sig@(TypeSig v ty
        ; new_ty <- rnHsSigType (quotes (ppr v)) ty
        ; return (TypeSig new_v new_ty) }
  
 +renameSig mb_names sig@(GenericSig v ty)
 +  = do        { defaultSigs_on <- xoptM Opt_DefaultSignatures
 +        ; unless defaultSigs_on (addErr (defaultSigErr sig))
 +        ; new_v <- lookupSigOccRn mb_names sig v
 +      ; new_ty <- rnHsSigType (quotes (ppr v)) ty
 +      ; return (GenericSig new_v new_ty) }
 +
  renameSig _ (SpecInstSig ty)
    = do        { new_ty <- rnLHsType (text "A SPECIALISE instance pragma") ty
        ; return (SpecInstSig new_ty) }
@@@ -826,11 -816,6 +826,11 @@@ misplacedSigErr (L loc sig
    = addErrAt loc $
      sep [ptext (sLit "Misplaced") <+> hsSigDoc sig <> colon, ppr sig]
  
 +defaultSigErr :: Sig RdrName -> SDoc
 +defaultSigErr sig = vcat [ hang (ptext (sLit "Unexpected default signature:"))
 +                              2 (ppr sig)
 +                         , ptext (sLit "Use -XDefaultSignatures to enable default signatures") ] 
 +
  methodBindErr :: HsBindLR RdrName RdrName -> SDoc
  methodBindErr mbind
   =  hang (ptext (sLit "Pattern bindings (except simple variables) not allowed in instance declarations"))
@@@ -845,5 -830,4 +845,5 @@@ nonStdGuardErr :: [LStmtLR Name Name] -
  nonStdGuardErr guards
    = hang (ptext (sLit "accepting non-standard pattern guards (use -XPatternGuards to suppress this message)"))
         4 (interpp'SP guards)
 +
  \end{code}
@@@ -31,7 -31,7 +31,7 @@@ import RnEn
  import TcRnMonad
  import RdrName
  import PrelNames
- import TypeRep                ( funTyConName )
+ import TysPrim          ( funTyConName )
  import Name
  import SrcLoc
  import NameSet
@@@ -139,6 -139,13 +139,6 @@@ rnHsType doc (HsRecTy flds
    = do { flds' <- rnConDeclFields doc flds
         ; return (HsRecTy flds') }
  
 -rnHsType _ (HsNumTy i)
 -  | i == 1    = return (HsNumTy i)
 -  | otherwise = addErr err_msg >> return (HsNumTy i)
 -  where
 -    err_msg = ptext (sLit "Only unit numeric type pattern is valid")
 -                         
 -
  rnHsType doc (HsFunTy ty1 ty2) = do
      ty1' <- rnLHsType doc ty1
        -- Might find a for-all as the arg of a function type
@@@ -40,13 -40,10 +40,13 @@@ import Nam
  import NameSet
  import TyCon
  import TcType
 +import BuildTyCl
 +import BasicTypes
  import Var
  import VarSet
  import PrelNames
  import SrcLoc
 +import UniqSupply
  import Util
  import ListSetOps
  import Outputable
@@@ -128,9 -125,6 +128,9 @@@ pprDerivSpec (DS { ds_loc = l, ds_name 
                   ds_cls = c, ds_tys = tys, ds_theta = rhs })
    = parens (hsep [ppr l, ppr n, ppr tvs, ppr c, ppr tys]
            <+> equals <+> ppr rhs)
 +
 +instance Outputable DerivSpec where
 +  ppr = pprDerivSpec
  \end{code}
  
  
@@@ -298,21 -292,17 +298,21 @@@ both of them.  So we gather defs/uses f
  tcDeriving  :: [LTyClDecl Name]  -- All type constructors
              -> [LInstDecl Name]  -- All instance declarations
              -> [LDerivDecl Name] -- All stand-alone deriving declarations
 -          -> TcM ([InstInfo Name],    -- The generated "instance decls"
 -                  HsValBinds Name,    -- Extra generated top-level bindings
 -                    DefUses)
 +            -> TcM ([InstInfo Name] -- The generated "instance decls"
 +                   ,HsValBinds Name -- Extra generated top-level bindings
 +                   ,DefUses
 +                   ,[TyCon]         -- Extra generated top-level types
 +                   ,[TyCon])        -- Extra generated type family instances
  
  tcDeriving tycl_decls inst_decls deriv_decls
 -  = recoverM (return ([], emptyValBindsOut, emptyDUs)) $
 +  = recoverM (return ([], emptyValBindsOut, emptyDUs, [], [])) $
      do        {       -- Fish the "deriving"-related information out of the TcEnv
                -- And make the necessary "equations".
          is_boot <- tcIsHsBoot
        ; traceTc "tcDeriving" (ppr is_boot)
 -      ; early_specs <- makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
 +      ; (early_specs, genericsExtras) 
 +                <- makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
 +        ; let (repMetaTys, repTyCons, metaInsts) = unzip3 genericsExtras
  
        ; overlap_flag <- getOverlapFlag
        ; let (infer_specs, given_specs) = splitEithers early_specs
  
        ; insts2 <- mapM (genInst False overlap_flag) final_specs
  
 -               -- Generate the generic to/from functions from each type declaration
 -      ; gen_binds <- mkGenericBinds is_boot tycl_decls
 -      ; (inst_info, rn_binds, rn_dus) <- renameDeriv is_boot gen_binds (insts1 ++ insts2)
 +      -- We no longer generate the old generic to/from functions
 +        -- from each type declaration, so this is emptyBag
 +      ; gen_binds <- return emptyBag -- mkGenericBinds is_boot tycl_decls
 +      
 +      ; (inst_info, rn_binds, rn_dus)
 +                <- renameDeriv is_boot gen_binds (insts1 ++ insts2 ++ concat metaInsts)
  
 +      ; dflags <- getDOpts
 +      ; liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Derived instances"
 +               (ddump_deriving inst_info rn_binds))
 +{-
          ; when (not (null inst_info)) $
            dumpDerivingInfo (ddump_deriving inst_info rn_binds)
 -
 -      ; return (inst_info, rn_binds, rn_dus) }
 +-}
 +      ; return ( inst_info, rn_binds, rn_dus
 +                 , concat (map metaTyCons2TyCons repMetaTys), repTyCons) }
    where
      ddump_deriving :: [InstInfo Name] -> HsValBinds Name -> SDoc
      ddump_deriving inst_infos extra_binds
             2 (vcat (map (\i -> pprInstInfoDetails i $$ text "") inst_infos)
                $$ ppr extra_binds)
  
 +
  renameDeriv :: Bool -> LHsBinds RdrName
            -> [(InstInfo RdrName, DerivAuxBinds)]
            -> TcM ([InstInfo Name], HsValBinds Name, DefUses)
@@@ -398,12 -379,26 +398,12 @@@ renameDeriv is_boot gen_binds inst
                -- scope (yuk), and rename the method binds
           ASSERT( null sigs )
           bindLocalNames (map Var.varName tyvars) $
 -         do { (rn_binds, fvs) <- rnMethodBinds clas_nm (\_ -> []) [] binds
 +         do { (rn_binds, fvs) <- rnMethodBinds clas_nm (\_ -> []) binds
              ; let binds' = VanillaInst rn_binds [] standalone_deriv
                ; return (inst_info { iBinds = binds' }, fvs) }
        where
          (tyvars,_, clas,_) = instanceHead inst
          clas_nm            = className clas
 -
 ------------------------------------------
 -mkGenericBinds :: Bool -> [LTyClDecl Name] -> TcM (LHsBinds RdrName)
 -mkGenericBinds is_boot tycl_decls
 -  | is_boot 
 -  = return emptyBag
 -  | otherwise
 -  = do        { tcs <- mapM tcLookupTyCon [ tcdName d 
 -                                  | L _ d <- tycl_decls, isDataDecl d ]
 -      ; return (unionManyBags [ mkTyConGenericBinds tc
 -                              | tc <- tcs, tyConHasGenerics tc ]) }
 -              -- We are only interested in the data type declarations,
 -              -- and then only in the ones whose 'has-generics' flag is on
 -              -- The predicate tyConHasGenerics finds both of these
  \end{code}
  
  Note [Newtype deriving and unused constructors]
@@@ -435,81 -430,34 +435,81 @@@ stored in NewTypeDerived
  @makeDerivSpecs@ fishes around to find the info about needed derived instances.
  
  \begin{code}
 +-- Make the "extras" for the generic representation
 +mkGenDerivExtras :: TyCon 
 +                 -> TcRn (MetaTyCons, TyCon, [(InstInfo RdrName, DerivAuxBinds)])
 +mkGenDerivExtras tc = do
 +        { (metaTyCons, rep0TyInst) <- genGenericRepExtras tc
 +        ; metaInsts                <- genDtMeta (tc, metaTyCons)
 +        ; return (metaTyCons, rep0TyInst, metaInsts) }
 +
  makeDerivSpecs :: Bool 
               -> [LTyClDecl Name] 
 -               -> [LInstDecl Name]
 +             -> [LInstDecl Name]
               -> [LDerivDecl Name] 
 -             -> TcM [EarlyDerivSpec]
 -
 +             -> TcM ( [EarlyDerivSpec]
 +                      , [(MetaTyCons, TyCon, [(InstInfo RdrName, DerivAuxBinds)])])
  makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
 -  | is_boot   -- No 'deriving' at all in hs-boot files
 -  = do        { mapM_ add_deriv_err deriv_locs 
 -      ; return [] }
 +  | is_boot     -- No 'deriving' at all in hs-boot files
 +  = do  { mapM_ add_deriv_err deriv_locs 
 +        ; return ([],[]) }
    | otherwise
 -  = do        { eqns1 <- mapAndRecoverM deriveTyData all_tydata
 -      ; eqns2 <- mapAndRecoverM deriveStandalone deriv_decls
 -      ; return (eqns1 ++ eqns2) }
 +  = do  { eqns1 <- mapAndRecoverM deriveTyData all_tydata
 +        ; eqns2 <- mapAndRecoverM deriveStandalone deriv_decls
 +
 +        -- Generic representation stuff: we might need to add some "extras"
 +        -- to the instances
 +        ; xDerRep <- getDOpts >>= return . xopt Opt_DeriveGeneric
 +        ; generic_extras_deriv <- if not xDerRep
 +                                   -- No extras if the flag is off
 +                                   then (return [])
 +                                    else do {
 +          let allTyNames = [ tcdName d | L _ d <- tycl_decls, isDataDecl d ]
 +        -- Select only those types that derive Generic
 +        ; let sel_tydata = [ tcdName t | (L _ c, L _ t) <- all_tydata
 +                                       , getClassName c == Just genClassName ]
 +        ; let sel_deriv_decls = catMaybes [ getTypeName t
 +                                  | L _ (DerivDecl (L _ t)) <- deriv_decls
 +                                  , getClassName t == Just genClassName ] 
 +        ; derTyDecls <- mapM tcLookupTyCon $ 
 +                         filter (needsExtras xDerRep
 +                                  (sel_tydata ++ sel_deriv_decls)) allTyNames
 +        -- We need to generate the extras to add to what has
 +        -- already been derived
 +        ; mapM mkGenDerivExtras derTyDecls }
 +
 +        -- Merge and return
 +        ; return ( eqns1 ++ eqns2, generic_extras_deriv) }
    where
 +      -- We need extras if the flag DeriveGeneric is on and this type is 
 +      -- deriving Generic
 +    needsExtras xDerRep tydata tc_name = xDerRep && tc_name `elem` tydata
 +
 +    -- Extracts the name of the class in the deriving
 +    getClassName :: HsType Name -> Maybe Name
 +    getClassName (HsPredTy (HsClassP n _)) = Just n
 +    getClassName _                         = Nothing
 +
 +    -- Extracts the name of the type in the deriving
 +    getTypeName :: HsType Name -> Maybe Name
 +    getTypeName (HsTyVar n)                     = Just n
 +    getTypeName (HsOpTy _ (L _ n) _)            = Just n
 +    getTypeName (HsPredTy (HsClassP _ [L _ n])) = getTypeName n
 +    getTypeName _                               = Nothing
 +
      extractTyDataPreds decls
        = [(p, d) | d@(L _ (TyData {tcdDerivs = Just preds})) <- decls, p <- preds]
  
      all_tydata :: [(LHsType Name, LTyClDecl Name)]
 -      -- Derived predicate paired with its data type declaration
 +        -- Derived predicate paired with its data type declaration
      all_tydata = extractTyDataPreds (instDeclATs inst_decls ++ tycl_decls)
  
      deriv_locs = map (getLoc . snd) all_tydata
 -               ++ map getLoc deriv_decls
 +                 ++ map getLoc deriv_decls
  
      add_deriv_err loc = setSrcSpan loc $
 -                      addErr (hang (ptext (sLit "Deriving not permitted in hs-boot file"))
 -                                 2 (ptext (sLit "Use an instance declaration instead")))
 +                        addErr (hang (ptext (sLit "Deriving not permitted in hs-boot file"))
 +                                   2 (ptext (sLit "Use an instance declaration instead")))
  
  ------------------------------------------------------------------
  deriveStandalone :: LDerivDecl Name -> TcM EarlyDerivSpec
@@@ -779,11 -727,6 +779,11 @@@ inferConstraints :: [TyVar] -> Class -
  -- generated method definitions should succeed.   This set will be simplified
  -- before being used in the instance declaration
  inferConstraints _ cls inst_tys rep_tc rep_tc_args
 +  -- Generic constraints are easy
 +  | cls `hasKey` genClassKey
 +  = []
 +  -- The others are a bit more complicated
 +  | otherwise
    = ASSERT2( equalLength rep_tc_tvs all_rep_tc_args, ppr cls <+> ppr rep_tc )
      stupid_constraints ++ extra_constraints
      ++ sc_constraints ++ con_arg_constraints
@@@ -887,8 -830,6 +887,8 @@@ sideConditions mtheta cl
                                           cond_functorOK False) -- Functor/Fold/Trav works ok for rank-n types
    | cls_key == traversableClassKey = Just (checkFlag Opt_DeriveTraversable `andCond`
                                           cond_functorOK False)
 +  | cls_key == genClassKey         = Just (cond_RepresentableOk `andCond`
 +                                           checkFlag Opt_DeriveGeneric)
    | otherwise = Nothing
    where
      cls_key = getUnique cls
@@@ -907,7 -848,7 +907,7 @@@ orCond c1 c2 t
        Nothing -> Nothing          -- c1 succeeds
        Just x  -> case c2 tc of    -- c1 fails
                     Nothing -> Nothing
 -                   Just y  -> Just (x $$ ptext (sLit "  and") $$ y)
 +                   Just y  -> Just (x $$ ptext (sLit "  or") $$ y)
                                    -- Both fail
  
  andCond :: Condition -> Condition -> Condition
@@@ -933,14 -874,11 +933,14 @@@ cond_stdOK Nothing (_, rep_tc
      check_con con 
        | isVanillaDataCon con
        , all isTauTy (dataConOrigArgTys con) = Nothing
 -      | otherwise = Just (badCon con (ptext (sLit "does not have a Haskell-98 type")))
 +      | otherwise = Just (badCon con (ptext (sLit "must have a Haskell-98 type")))
    
  no_cons_why :: TyCon -> SDoc
  no_cons_why rep_tc = quotes (pprSourceTyCon rep_tc) <+> 
 -                   ptext (sLit "has no data constructors")
 +                   ptext (sLit "must have at least one data constructor")
 +
 +cond_RepresentableOk :: Condition
 +cond_RepresentableOk (_,t) = canDoGenerics t
  
  cond_enumOrProduct :: Condition
  cond_enumOrProduct = cond_isEnumeration `orCond` 
@@@ -955,7 -893,7 +955,7 @@@ cond_noUnliftedArgs (_, tc
    where
      bad_cons = [ con | con <- tyConDataCons tc
                     , any isUnLiftedType (dataConOrigArgTys con) ]
 -    why = badCon (head bad_cons) (ptext (sLit "has arguments of unlifted type"))
 +    why = badCon (head bad_cons) (ptext (sLit "must have only arguments of lifted type"))
  
  cond_isEnumeration :: Condition
  cond_isEnumeration (_, rep_tc)
    | otherwise                 = Just why
    where
      why = sep [ quotes (pprSourceTyCon rep_tc) <+> 
 -                ptext (sLit "is not an enumeration type")
 +                ptext (sLit "must be an enumeration type")
                , ptext (sLit "(an enumeration consists of one or more nullary, non-GADT constructors)") ]
                  -- See Note [Enumeration types] in TyCon
  
@@@ -973,7 -911,7 +973,7 @@@ cond_isProduct (_, rep_tc
    | otherwise           = Just why
    where
      why = quotes (pprSourceTyCon rep_tc) <+> 
 -        ptext (sLit "does not have precisely one constructor")
 +        ptext (sLit "must have precisely one constructor")
  
  cond_typeableOK :: Condition
  -- OK for Typeable class
@@@ -986,9 -924,9 +986,9 @@@ cond_typeableOK (_, tc
    | otherwise       = Nothing
    where
      too_many = quotes (pprSourceTyCon tc) <+> 
 -             ptext (sLit "has too many arguments")
 +             ptext (sLit "must have 7 or fewer arguments")
      bad_kind = quotes (pprSourceTyCon tc) <+> 
 -             ptext (sLit "has arguments of kind other than `*'")
 +             ptext (sLit "must only have arguments of kind `*'")
  
  functorLikeClassKeys :: [Unique]
  functorLikeClassKeys = [functorClassKey, foldableClassKey, traversableClassKey]
@@@ -1003,11 -941,11 +1003,11 @@@ cond_functorOK :: Bool -> Conditio
  cond_functorOK allowFunctions (_, rep_tc)
    | null tc_tvs
    = Just (ptext (sLit "Data type") <+> quotes (ppr rep_tc) 
 -          <+> ptext (sLit "has no parameters"))
 +          <+> ptext (sLit "must have some type parameters"))
  
    | not (null bad_stupid_theta)
    = Just (ptext (sLit "Data type") <+> quotes (ppr rep_tc) 
 -          <+> ptext (sLit "has a class context") <+> pprTheta bad_stupid_theta)
 +          <+> ptext (sLit "must not have a class context") <+> pprTheta bad_stupid_theta)
  
    | otherwise
    = msum (map check_con data_cons)    -- msum picks the first 'Just', if any
                        , ft_bad_app = Just (badCon con wrong_arg)
                        , ft_forall = \_ x   -> x }
                      
 -    existential = ptext (sLit "has existential arguments")
 -    covariant         = ptext (sLit "uses the type variable in a function argument")
 -    functions         = ptext (sLit "contains function types")
 -    wrong_arg         = ptext (sLit "uses the type variable in an argument other than the last")
 +    existential = ptext (sLit "must not have existential arguments")
 +    covariant         = ptext (sLit "must not use the type variable in a function argument")
 +    functions         = ptext (sLit "must not contain function types")
 +    wrong_arg         = ptext (sLit "must not use the type variable in an argument other than the last")
  
  checkFlag :: ExtensionFlag -> Condition
  checkFlag flag (dflags, _)
@@@ -1061,11 -999,11 +1061,11 @@@ std_class_via_iso cla
  
  
  non_iso_class :: Class -> Bool
 --- *Never* derive Read,Show,Typeable,Data by isomorphism,
 +-- *Never* derive Read, Show, Typeable, Data, Generic by isomorphism,
  -- even with -XGeneralizedNewtypeDeriving
  non_iso_class cls 
 -  = classKey cls `elem` ([readClassKey, showClassKey, dataClassKey] ++
 -                       typeableClassKeys)
 +  = classKey cls `elem` ([ readClassKey, showClassKey, dataClassKey
 +                         , genClassKey] ++ typeableClassKeys)
  
  typeableClassKeys :: [Unique]
  typeableClassKeys = map getUnique typeableClassNames
@@@ -1356,7 -1294,7 +1356,7 @@@ inferInstanceContexts oflag infer_spec
                  
           ; let tv_set = mkVarSet tyvars
                 weird_preds = [pred | pred <- deriv_rhs
-                                      , not (tyVarsOfPred pred `subVarSet` tv_set)]  
+                                      , not (tyVarsOfPred pred `subVarSet` tv_set)]
           ; mapM_ (addErrTc . badDerivedPred) weird_preds      
  
             ; theta <- simplifyDeriv orig the_pred tyvars deriv_rhs
@@@ -1487,14 -1425,12 +1487,12 @@@ genInst standalone_deriv ofla
    where
      inst_spec = mkInstance oflag theta spec
      co1 = case tyConFamilyCoercion_maybe rep_tycon of
-             Just co_con -> ACo (mkTyConApp co_con rep_tc_args)
+               Just co_con -> mkAxInstCo co_con rep_tc_args
              Nothing     -> id_co
              -- Not a family => rep_tycon = main tycon
-     co2 = case newTyConCo_maybe rep_tycon of
-             Just co_con -> ACo (mkTyConApp co_con rep_tc_args)
-               Nothing     -> id_co  -- The newtype is transparent; no need for a cast
-     co = co1 `mkTransCoI` co2
-     id_co = IdCo (mkTyConApp rep_tycon rep_tc_args)
+     co2 = mkAxInstCo (newTyConCo rep_tycon) rep_tc_args
+     co  = co1 `mkTransCo` co2
+     id_co = mkReflCo (mkTyConApp rep_tycon rep_tc_args)
  
  -- Example: newtype instance N [a] = N1 (Tree a) 
  --          deriving instance Eq b => Eq (N [(b,b)])
@@@ -1515,158 -1451,20 +1513,158 @@@ genDerivBinds loc fix_env clas tyco
        Nothing     -> pprPanic "genDerivBinds: bad derived class" (ppr clas)
    where
      gen_list :: [(Unique, SrcSpan -> TyCon -> (LHsBinds RdrName, DerivAuxBinds))]
 -    gen_list = [(eqClassKey,       gen_Eq_binds)
 -             ,(ordClassKey,      gen_Ord_binds)
 -             ,(enumClassKey,     gen_Enum_binds)
 -             ,(boundedClassKey,  gen_Bounded_binds)
 -             ,(ixClassKey,       gen_Ix_binds)
 -             ,(showClassKey,     gen_Show_binds fix_env)
 -             ,(readClassKey,     gen_Read_binds fix_env)
 -             ,(dataClassKey,     gen_Data_binds)
 -             ,(functorClassKey,  gen_Functor_binds)
 -             ,(foldableClassKey, gen_Foldable_binds)
 -             ,(traversableClassKey, gen_Traversable_binds)
 +    gen_list = [(eqClassKey,            gen_Eq_binds)
 +             ,(ordClassKey,           gen_Ord_binds)
 +             ,(enumClassKey,          gen_Enum_binds)
 +             ,(boundedClassKey,       gen_Bounded_binds)
 +             ,(ixClassKey,            gen_Ix_binds)
 +             ,(showClassKey,          gen_Show_binds fix_env)
 +             ,(readClassKey,          gen_Read_binds fix_env)
 +             ,(dataClassKey,          gen_Data_binds)
 +             ,(functorClassKey,       gen_Functor_binds)
 +             ,(foldableClassKey,      gen_Foldable_binds)
 +             ,(traversableClassKey,   gen_Traversable_binds)
 +             ,(genClassKey,           genGenericBinds)
               ]
  \end{code}
  
 +%************************************************************************
 +%*                                                                    *
 +\subsection[TcDeriv-generic-binds]{Bindings for the new generic deriving mechanism}
 +%*                                                                    *
 +%************************************************************************
 +
 +For the generic representation we need to generate:
 +\begin{itemize}
 +\item A Generic instance
 +\item A Rep type instance 
 +\item Many auxiliary datatypes and instances for them (for the meta-information)
 +\end{itemize}
 +
 +@genGenericBinds@ does (1)
 +@genGenericRepExtras@ does (2) and (3)
 +@genGenericAll@ does all of them
 +
 +\begin{code}
 +genGenericBinds :: SrcSpan -> TyCon -> (LHsBinds RdrName, DerivAuxBinds)
 +genGenericBinds _ tc = (mkBindsRep tc, [ {- No DerivAuxBinds -} ])
 +
 +genGenericRepExtras :: TyCon -> TcM (MetaTyCons, TyCon)
 +genGenericRepExtras tc =
 +  do  uniqS <- newUniqueSupply
 +      let
 +        -- Uniques for everyone
 +        (uniqD:uniqs) = uniqsFromSupply uniqS
 +        (uniqsC,us) = splitAt (length tc_cons) uniqs
 +        uniqsS :: [[Unique]] -- Unique supply for the S datatypes
 +        uniqsS = mkUniqsS tc_arits us
 +        mkUniqsS []    _  = []
 +        mkUniqsS (n:t) us = case splitAt n us of
 +                              (us1,us2) -> us1 : mkUniqsS t us2
 +
 +        tc_name   = tyConName tc
 +        tc_cons   = tyConDataCons tc
 +        tc_arits  = map dataConSourceArity tc_cons
 +        
 +        tc_occ    = nameOccName tc_name
 +        d_occ     = mkGenD tc_occ
 +        c_occ m   = mkGenC tc_occ m
 +        s_occ m n = mkGenS tc_occ m n
 +        mod_name  = nameModule (tyConName tc)
 +        d_name    = mkExternalName uniqD mod_name d_occ wiredInSrcSpan
 +        c_names   = [ mkExternalName u mod_name (c_occ m) wiredInSrcSpan
 +                      | (u,m) <- zip uniqsC [0..] ]
 +        s_names   = [ [ mkExternalName u mod_name (s_occ m n) wiredInSrcSpan 
 +                        | (u,n) <- zip us [0..] ] | (us,m) <- zip uniqsS [0..] ]
 +        
 +        mkTyCon name = ASSERT( isExternalName name )
 +                         buildAlgTyCon name [] [] mkAbstractTyConRhs
 +                           NonRecursive False NoParentTyCon Nothing
 +
 +      metaDTyCon  <- mkTyCon d_name
 +      metaCTyCons <- sequence [ mkTyCon c_name | c_name <- c_names ]
 +      metaSTyCons <- mapM sequence 
 +                       [ [ mkTyCon s_name 
 +                         | s_name <- s_namesC ] | s_namesC <- s_names ]
 +
 +      let metaDts = MetaTyCons metaDTyCon metaCTyCons metaSTyCons
 +  
 +      rep0_tycon <- tc_mkRepTyCon tc metaDts
 +
 +      return (metaDts, rep0_tycon)
 +{-
 +genGenericAll :: TyCon
 +                  -> TcM ((InstInfo RdrName, DerivAuxBinds), MetaTyCons, TyCon)
 +genGenericAll tc =
 +  do  (metaDts, rep0_tycon)     <- genGenericRepExtras tc
 +      clas                      <- tcLookupClass genClassName
 +      dfun_name                 <- new_dfun_name clas tc
 +      let
 +        mkInstRep = (InstInfo { iSpec = inst, iBinds = binds }
 +                               , [ {- No DerivAuxBinds -} ])
 +        inst  = mkLocalInstance dfun NoOverlap
 +        binds = VanillaInst (mkBindsRep tc) [] False
 +
 +        tvs   = tyConTyVars tc
 +        tc_ty = mkTyConApp tc (mkTyVarTys tvs)
 +        
 +        dfun  = mkDictFunId dfun_name (tyConTyVars tc) [] clas [tc_ty]
 +      return (mkInstRep, metaDts, rep0_tycon)
 +-}
 +genDtMeta :: (TyCon, MetaTyCons) -> TcM [(InstInfo RdrName, DerivAuxBinds)]
 +genDtMeta (tc,metaDts) =
 +  do  dClas <- tcLookupClass datatypeClassName
 +      d_dfun_name <- new_dfun_name dClas tc
 +      cClas <- tcLookupClass constructorClassName
 +      c_dfun_names <- sequence [ new_dfun_name cClas tc | _ <- metaC metaDts ]
 +      sClas <- tcLookupClass selectorClassName
 +      s_dfun_names <- sequence (map sequence [ [ new_dfun_name sClas tc 
 +                                               | _ <- x ] 
 +                                             | x <- metaS metaDts ])
 +      fix_env <- getFixityEnv
 +
 +      let
 +        (dBinds,cBinds,sBinds) = mkBindsMetaD fix_env tc
 +        
 +        -- Datatype
 +        d_metaTycon = metaD metaDts
 +        d_inst = mkLocalInstance d_dfun NoOverlap
 +        d_binds = VanillaInst dBinds [] False
 +        d_dfun  = mkDictFunId d_dfun_name (tyConTyVars tc) [] dClas 
 +                    [ mkTyConTy d_metaTycon ]
 +        d_mkInst = (InstInfo { iSpec = d_inst, iBinds = d_binds }, [])
 +        
 +        -- Constructor
 +        c_metaTycons = metaC metaDts
 +        c_insts = [ mkLocalInstance (c_dfun c ds) NoOverlap 
 +                  | (c, ds) <- myZip1 c_metaTycons c_dfun_names ]
 +        c_binds = [ VanillaInst c [] False | c <- cBinds ]
 +        c_dfun c dfun_name = mkDictFunId dfun_name (tyConTyVars tc) [] cClas 
 +                               [ mkTyConTy c ]
 +        c_mkInst = [ (InstInfo { iSpec = is, iBinds = bs }, []) 
 +                   | (is,bs) <- myZip1 c_insts c_binds ]
 +        
 +        -- Selector
 +        s_metaTycons = metaS metaDts
 +        s_insts = map (map (\(s,ds) -> mkLocalInstance (s_dfun s ds) NoOverlap))
 +                    (myZip2 s_metaTycons s_dfun_names)
 +        s_binds = [ [ VanillaInst s [] False | s <- ss ] | ss <- sBinds ]
 +        s_dfun s dfun_name = mkDictFunId dfun_name (tyConTyVars tc) [] sClas
 +                               [ mkTyConTy s ]
 +        s_mkInst = map (map (\(is,bs) -> (InstInfo {iSpec=is, iBinds=bs}, [])))
 +                     (myZip2 s_insts s_binds)
 +       
 +        myZip1 :: [a] -> [b] -> [(a,b)]
 +        myZip1 l1 l2 = ASSERT (length l1 == length l2) zip l1 l2
 +        
 +        myZip2 :: [[a]] -> [[b]] -> [[(a,b)]]
 +        myZip2 l1 l2 =
 +          ASSERT (and (zipWith (>=) (map length l1) (map length l2)))
 +            [ zip x1 x2 | (x1,x2) <- zip l1 l2 ]
 +        
 +      return (d_mkInst : c_mkInst ++ concat s_mkInst)
 +\end{code}
 +
  
  %************************************************************************
  %*                                                                    *
@@@ -211,7 -211,7 +211,7 @@@ tcLookupFamInst tycon ty
         }
  
  tcLookupDataFamInst :: TyCon -> [Type] -> TcM (TyCon, [Type])
 --- Find the instance of a data famliy
 +-- Find the instance of a data family
  -- Note [Looking up family instances for deriving]
  tcLookupDataFamInst tycon tys
    | not (isFamilyTyCon tycon)
@@@ -461,7 -461,7 +461,7 @@@ tcExtendGlobalTyVars gtv_var extra_glob
  \begin{code}
  tcExtendRules :: [LRuleDecl Id] -> TcM a -> TcM a
        -- Just pop the new rules into the EPS and envt resp
 -      -- All the rules come from an interface file, not soruce
 +      -- All the rules come from an interface file, not source
        -- Nevertheless, some may be for this module, if we read
        -- its interface instead of its source code
  tcExtendRules lcl_rules thing_inside
@@@ -626,7 -626,7 +626,7 @@@ data InstBindings 
                        -- witness dictionary is identical to the argument 
                        -- dictionary.  Hence no bindings, no pragmas.
  
-       CoercionI       -- The coercion maps from newtype to the representation type
+       Coercion        -- The coercion maps from newtype to the representation type
                        -- (mentioning type variables bound by the forall'd iSpec variables)
                        -- E.g.   newtype instance N [a] = N1 (Tree a)
                        --        co : N [a] ~ Tree a
  pprInstInfo :: InstInfo a -> SDoc
  pprInstInfo info = hang (ptext (sLit "instance"))
                        2 (sep [ ifPprDebug (pprForAll tvs)
-                              , pprThetaArrow theta, ppr tau
+                              , pprThetaArrowTy theta, ppr tau
                               , ptext (sLit "where")])
    where
      (tvs, theta, tau) = tcSplitSigmaTy (idType (iDFunId info))
@@@ -681,7 -681,7 +681,7 @@@ newDFunName clas tys lo
  \end{code}
  
  Make a name for the representation tycon of a family instance.  It's an
 -*external* name, like otber top-level names, and hence must be made with
 +*external* name, like other top-level names, and hence must be made with
  newGlobalBinder.
  
  \begin{code}
@@@ -42,7 -42,7 +42,7 @@@ import Nam
  import HscTypes
  import PrelInfo
  import MkCore ( eRROR_ID )
 -import PrelNames
 +import PrelNames hiding (error_RDR)
  import PrimOp
  import SrcLoc
  import TyCon
@@@ -50,7 -50,6 +50,6 @@@ import TcTyp
  import TysPrim
  import TysWiredIn
  import Type
- import Var( TyVar )
  import TypeRep
  import VarSet
  import State
@@@ -1837,7 -1836,7 +1836,7 @@@ assoc_ty_id cls_str _ tbl t
                                              text "for primitive type" <+> ppr ty)
    | otherwise = head res
    where
-     res = [id | (ty',id) <- tbl, ty `tcEqType` ty']
+     res = [id | (ty',id) <- tbl, ty `eqType` ty']
  
  -----------------------------------------------------------------------
  
@@@ -44,6 -44,7 +44,6 @@@ import TyCo
  import Class
  import Name
  import NameSet
 -import PrelNames
  import TysWiredIn
  import BasicTypes
  import SrcLoc
@@@ -364,6 -365,9 +364,6 @@@ kc_hs_type (HsPArrTy ty) = d
      ty' <- kcLiftedType ty
      return (HsPArrTy ty', liftedTypeKind)
  
 -kc_hs_type (HsNumTy n)
 -   = return (HsNumTy n, liftedTypeKind)
 -
  kc_hs_type (HsKindSig ty k) = do
      ty' <- kc_check_lhs_type ty (EK k EkKindSig)
      return (HsKindSig ty' k, k)
@@@ -602,6 -606,11 +602,6 @@@ ds_type (HsOpTy ty1 (L span op) ty2) = 
      tau_ty2 <- dsHsType ty2
      setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
  
 -ds_type (HsNumTy n)
 -  = ASSERT(n==1) do
 -    tc <- tcLookupTyCon genUnitTyConName
 -    return (mkTyConApp tc [])
 -
  ds_type ty@(HsAppTy _ _)
    = ds_app ty []
  
@@@ -848,7 -857,7 +848,7 @@@ tcPatSig :: UserTypeCtx
                 [(Name, TcType)], -- The new bit of type environment, binding
                                   -- the scoped type variables
                   HsWrapper)        -- Coercion due to unification with actual ty
-                                  -- Of shape:  res_ty ~ sig_ty
+                                    -- Of shape:  res_ty ~ sig_ty
  tcPatSig ctxt sig res_ty
    = do        { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
        -- sig_tvs are the type variables free in 'sig', 
                -- and hence is rigid, so use it to zap the res_ty
                    wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
                ; return (sig_ty, [], wrap)
-       } else do {
+         } else do {
                -- Type signature binds at least one scoped type variable
        
                -- A pattern binding cannot bind scoped type variables
        ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
  
        -- Now do a subsumption check of the pattern signature against res_ty
-       ; sig_tvs' <- tcInstSigTyVars sig_tvs
+         ; sig_tvs' <- tcInstSigTyVars sig_tvs
          ; let sig_ty' = substTyWith sig_tvs sig_tv_tys' sig_ty
                sig_tv_tys' = mkTyVarTys sig_tvs'
-         ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty'
+       ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty'
  
        -- Check that each is bound to a distinct type variable,
        -- and one that is not already in scope
-       ; binds_in_scope <- getScopedTyVarBinds
+         ; binds_in_scope <- getScopedTyVarBinds
        ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys'
        ; check binds_in_scope tv_binds
        
        -- Phew!
-       ; return (sig_ty', tv_binds, wrap)
-       } }
+         ; return (sig_ty', tv_binds, wrap)
+         } }
    where
      check _ [] = return ()
      check in_scope ((n,ty):rest) = do { check_one in_scope n ty
                -- Must not bind to the same type variable
                -- as some other in-scope type variable
        where
-         dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
+         dups = [n' | (n',ty') <- in_scope, eqType ty' ty]
  \end{code}
  
  
@@@ -16,22 -16,24 +16,24 @@@ import TcPat( addInlinePrags 
  import TcRnMonad
  import TcMType
  import TcType
+ import BuildTyCl
  import Inst
  import InstEnv
  import FamInst
  import FamInstEnv
- import MkCore ( nO_METHOD_BINDING_ERROR_ID )
  import TcDeriv
  import TcEnv
  import RnSource ( addTcgDUs )
  import TcHsType
  import TcUnify
+ import MkCore ( nO_METHOD_BINDING_ERROR_ID )
  import Type
  import Coercion
  import TyCon
  import DataCon
  import Class
  import Var
+ import Pair
  import VarSet
  import CoreUtils  ( mkPiTypes )
  import CoreUnfold ( mkDFunUnfolding )
@@@ -206,7 -208,7 +208,7 @@@ Just <blah>
  Instead, we simply rely on the fact that casts are cheap:
  
     $df :: forall a. C a => C [a]
 -   {-# INLINE df #}  -- NB: INLINE this
 +   {-# INLINE df #-}  -- NB: INLINE this
     $df = /\a. \d. MkC [a] ($cop_list a d)
         = $cop_list |> forall a. C a -> (sym (Co:C [a]))
  
@@@ -370,6 -372,7 +372,6 @@@ tcInstDecls1 tycl_decls inst_decls deri
         ; let { (local_info,
                  at_tycons_s)   = unzip local_info_tycons
               ; at_idx_tycons   = concat at_tycons_s ++ idx_tycons
 -             ; clas_decls      = filter (isClassDecl . unLoc) tycl_decls
               ; implicit_things = concatMap implicitTyThings at_idx_tycons
             ; aux_binds       = mkRecSelBinds at_idx_tycons
               }
                  --     tythings to the global environment
         ; tcExtendGlobalEnv (at_idx_tycons ++ implicit_things) $ do {
  
 -                -- (3) Instances from generic class declarations
 -       ; generic_inst_info <- getGenericInstances clas_decls
  
                  -- Next, construct the instance environment so far, consisting
                  -- of
                  --   (a) local instance decls
 -                --   (b) generic instances
 -                --   (c) local family instance decls
 +                --   (b) local family instance decls
         ; addInsts local_info         $
 -         addInsts generic_inst_info  $
           addFamInsts at_idx_tycons   $ do {
  
 -                -- (4) Compute instances from "deriving" clauses;
 +                -- (3) Compute instances from "deriving" clauses;
                  -- This stuff computes a context for the derived instance
                  -- decl, so it needs to know about all the instances possible
                  -- NB: class instance declarations can contain derivings as
                  --     part of associated data type declarations
 -       failIfErrsM            -- If the addInsts stuff gave any errors, don't
 -                              -- try the deriving stuff, becuase that may give
 -                              -- more errors still
 -       ; (deriv_inst_info, deriv_binds, deriv_dus) 
 +       failIfErrsM    -- If the addInsts stuff gave any errors, don't
 +                      -- try the deriving stuff, because that may give
 +                      -- more errors still
 +       ; (deriv_inst_info, deriv_binds, deriv_dus, deriv_tys, deriv_ty_insts) 
                <- tcDeriving tycl_decls inst_decls deriv_decls
 -       ; gbl_env <- addInsts deriv_inst_info getGblEnv
 +
 +       -- Extend the global environment also with the generated datatypes for
 +       -- the generic representation
 +       ; gbl_env <- addFamInsts (map ATyCon deriv_ty_insts) $
 +                      tcExtendGlobalEnv (map ATyCon (deriv_tys ++ deriv_ty_insts)) $
 +                        addInsts deriv_inst_info getGblEnv
         ; return ( addTcgDUs gbl_env deriv_dus,
 -                  generic_inst_info ++ deriv_inst_info ++ local_info,
 +                  deriv_inst_info ++ local_info,
                    aux_binds `plusHsValBinds` deriv_binds)
      }}}
  
@@@ -549,8 -551,8 +551,8 @@@ tcLocalInstDecl1 (L loc (InstDecl poly_
        | isTyVarTy ty         = return ()
        | otherwise            = addErrTc $ mustBeVarArgErr ty
      checkIndex ty (Just instTy)
-       | ty `tcEqType` instTy = return ()
-       | otherwise            = addErrTc $ wrongATArgErr ty instTy
+       | ty `eqType` instTy = return ()
+       | otherwise          = addErrTc $ wrongATArgErr ty instTy
  
      listToNameSet = addListToNameSet emptyNameSet
  
            tv1 `sameLexeme` tv2 =
              nameOccName (tyVarName tv1) == nameOccName (tyVarName tv2)
        in
-       extendTvSubst (substSameTyVar tvs replacingTvs) tv replacement
+       TcType.extendTvSubst (substSameTyVar tvs replacingTvs) tv replacement
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
+                Type checking family instances
+ %*                                                                    *
+ %************************************************************************
+ Family instances are somewhat of a hybrid.  They are processed together with
+ 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).
+ \begin{code}
+ tcFamInstDecl :: TopLevelFlag -> LTyClDecl Name -> TcM TyThing
+ tcFamInstDecl top_lvl (L loc decl)
+   =   -- Prime error recovery, set source location
+     setSrcSpan loc                            $
+     tcAddDeclCtxt decl                                $
+     do { -- type family instances require -XTypeFamilies
+        -- and can't (currently) be in an hs-boot file
+        ; type_families <- xoptM Opt_TypeFamilies
+        ; is_boot  <- tcIsHsBoot         -- Are we compiling an hs-boot file?
+        ; checkTc type_families $ badFamInstDecl (tcdLName decl)
+        ; checkTc (not is_boot) $ badBootFamInstDeclErr
+        -- Perform kind and type checking
+        ; tc <- tcFamInstDecl1 decl
+        ; checkValidTyCon tc   -- Remember to check validity;
+                               -- no recursion to worry about here
+        -- Check that toplevel type instances are not for associated types.
+        ; when (isTopLevel top_lvl && isAssocFamily tc)
+               (addErr $ assocInClassErr (tcdName decl))
+        ; return (ATyCon tc) }
+ isAssocFamily :: TyCon -> Bool        -- Is an assocaited type
+ isAssocFamily tycon
+   = case tyConFamInst_maybe tycon of
+           Nothing       -> panic "isAssocFamily: no family?!?"
+           Just (fam, _) -> isTyConAssoc fam
+ assocInClassErr :: Name -> SDoc
+ assocInClassErr name
+  = ptext (sLit "Associated type") <+> quotes (ppr name) <+>
+    ptext (sLit "must be inside a class instance")
+ tcFamInstDecl1 :: TyClDecl Name -> TcM TyCon
+   -- "type instance"
+ tcFamInstDecl1 (decl@TySynonym {tcdLName = L loc tc_name})
+   = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
+     do { -- check that the family declaration is for a synonym
+          checkTc (isFamilyTyCon family) (notFamily family)
+        ; checkTc (isSynTyCon family) (wrongKindOfFamily family)
+        ; -- (1) kind check the right-hand side of the type equation
+        ; k_rhs <- kcCheckLHsType (tcdSynRhs decl) (EK resKind EkUnk)
+                         -- ToDo: the ExpKind could be better
+          -- we need the exact same number of type parameters as the family
+          -- declaration 
+        ; let famArity = tyConArity family
+        ; checkTc (length k_typats == famArity) $ 
+            wrongNumberOfParmsErr famArity
+          -- (2) type check type equation
+        ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
+        ; t_typats <- mapM tcHsKindedType k_typats
+        ; t_rhs    <- tcHsKindedType k_rhs
+          -- (3) check the well-formedness of the instance
+        ; checkValidTypeInst t_typats t_rhs
+          -- (4) construct representation tycon
+        ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc
+        ; buildSynTyCon rep_tc_name t_tvs (SynonymTyCon t_rhs) 
+                        (typeKind t_rhs) 
+                        NoParentTyCon (Just (family, t_typats))
+        }}
+   -- "newtype instance" and "data instance"
+ tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
+                            tcdCons = cons})
+   = kcIdxTyPats decl $ \k_tvs k_typats resKind fam_tycon ->
+     do { -- check that the family declaration is for the right kind
+          checkTc (isFamilyTyCon fam_tycon) (notFamily fam_tycon)
+        ; checkTc (isAlgTyCon fam_tycon) (wrongKindOfFamily fam_tycon)
+        ; -- (1) kind check the data declaration as usual
+        ; k_decl <- kcDataDecl decl k_tvs
+        ; let k_ctxt = tcdCtxt k_decl
+            k_cons = tcdCons k_decl
+          -- result kind must be '*' (otherwise, we have too few patterns)
+        ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr (tyConArity fam_tycon)
+          -- (2) type check indexed data type declaration
+        ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
+        ; unbox_strict <- doptM Opt_UnboxStrictFields
+          -- kind check the type indexes and the context
+        ; t_typats     <- mapM tcHsKindedType k_typats
+        ; stupid_theta <- tcHsKindedContext k_ctxt
+          -- (3) Check that
+          --     (a) left-hand side contains no type family applications
+          --         (vanilla synonyms are fine, though, and we checked for
+          --         foralls earlier)
+        ; mapM_ checkTyFamFreeness t_typats
+        ; dataDeclChecks tc_name new_or_data stupid_theta k_cons
+          -- (4) construct representation tycon
+        ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc
+        ; let ex_ok = True     -- Existentials ok for type families!
+        ; fixM (\ rep_tycon -> do 
+            { let orig_res_ty = mkTyConApp fam_tycon t_typats
+            ; data_cons <- tcConDecls unbox_strict ex_ok rep_tycon
+                                      (t_tvs, orig_res_ty) k_cons
+            ; tc_rhs <-
+                case new_or_data of
+                  DataType -> return (mkDataTyConRhs data_cons)
+                  NewType  -> ASSERT( not (null data_cons) )
+                              mkNewTyConRhs rep_tc_name rep_tycon (head data_cons)
+            ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
+                            False h98_syntax NoParentTyCon (Just (fam_tycon, t_typats))
+                  -- We always assume that indexed types are recursive.  Why?
+                  -- (1) Due to their open nature, we can never be sure that a
+                  -- further instance might not introduce a new recursive
+                  -- dependency.  (2) They are always valid loop breakers as
+                  -- they involve a coercion.
+            })
+        }}
+        where
+        h98_syntax = case cons of      -- All constructors have same shape
+                       L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
+                       _ -> True
+ tcFamInstDecl1 d = pprPanic "tcFamInstDecl1" (ppr d)
+ -- Kind checking of indexed types
+ -- -
+ -- Kind check type patterns and kind annotate the embedded type variables.
+ --
+ -- * Here we check that a type instance matches its kind signature, but we do
+ --   not check whether there is a pattern for each type index; the latter
+ --   check is only required for type synonym instances.
+ kcIdxTyPats :: TyClDecl Name
+           -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TyCon -> TcM a)
+              -- ^^kinded tvs         ^^kinded ty pats  ^^res kind
+           -> TcM a
+ kcIdxTyPats decl thing_inside
+   = kcHsTyVars (tcdTyVars decl) $ \tvs -> 
+     do { let tc_name = tcdLName decl
+        ; fam_tycon <- tcLookupLocatedTyCon tc_name
+        ; let { (kinds, resKind) = splitKindFunTys (tyConKind fam_tycon)
+            ; hs_typats        = fromJust $ tcdTyPats decl }
+          -- we may not have more parameters than the kind indicates
+        ; checkTc (length kinds >= length hs_typats) $
+          tooManyParmsErr (tcdLName decl)
+          -- type functions can have a higher-kinded result
+        ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
+        ; typats <- zipWithM kcCheckLHsType hs_typats 
+                                   [ EK kind (EkArg (ppr tc_name) n) 
+                             | (kind,n) <- kinds `zip` [1..]]
+        ; thing_inside tvs typats resultKind fam_tycon
+        }
  \end{code}
  
  
@@@ -718,8 -896,8 +896,8 @@@ tcSuperClass n_ty_args ev_vars pre
         ; return (sc_dict, DFunConstArg (Var sc_dict)) }
    where
      find _ [] = Nothing
-     find i (ev:evs) | pred `tcEqPred` evVarPred ev = Just (ev, i)
-                     | otherwise                    = find (i+1) evs
+     find i (ev:evs) | pred `eqPred` evVarPred ev = Just (ev, i)
+                     | otherwise                  = find (i+1) evs
  
  ------------------------------
  tcSpecInstPrags :: DFunId -> InstBindings Name
@@@ -917,15 -1095,10 +1095,15 @@@ tcInstanceMethods dfun_id clas tyvars d
  
      ----------------------
      tc_default :: Id -> DefMeth -> TcM (TcId, LHsBind Id)
 +
 +    tc_default sel_id (GenDefMeth dm_name)
 +      = do { meth_bind <- mkGenericDefMethBind clas inst_tys sel_id dm_name
 +           ; tc_body sel_id False {- Not generated code? -} meth_bind }
 +{-
      tc_default sel_id GenDefMeth    -- Derivable type classes stuff
        = do { meth_bind <- mkGenericDefMethBind clas inst_tys sel_id
             ; tc_body sel_id False {- Not generated code? -} meth_bind }
 -        
 +-}
      tc_default sel_id NoDefMeth           -- No default method at all
        = do { warnMissingMethod sel_id
           ; (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars 
@@@ -1047,13 -1220,12 +1225,12 @@@ tcInstanceMethods dfun_id clas tyvars d
  
       inst_tvs = fst (tcSplitForAllTys (idType dfun_id))
       Just (init_inst_tys, _) = snocView inst_tys
-      rep_ty   = fst (coercionKind co)  -- [p]
+      rep_ty   = pFst (coercionKind co)  -- [p]
       rep_pred = mkClassPred clas (init_inst_tys ++ [rep_ty])
  
       -- co : [p] ~ T p
-      co = substTyWith inst_tvs (mkTyVarTys tyvars) $
-           case coi of { IdCo ty -> ty ;
-                         ACo co  -> mkSymCoercion co }
+      co = substCoWithTys inst_tvs (mkTyVarTys tyvars) $
+           mkSymCo coi
  
       ----------------
       tc_item :: (TcEvBinds, EvVar) -> (Id, DefMeth) -> TcM (TcId, LHsBind TcId)
       ----------------
       mk_op_wrapper :: Id -> EvVar -> HsWrapper
       mk_op_wrapper sel_id rep_d 
-        = WpCast (substTyWith sel_tvs (init_inst_tys ++ [co]) local_meth_ty)
+        = WpCast (liftCoSubstWith sel_tvs (map mkReflCo init_inst_tys ++ [co])
+                                local_meth_ty)
           <.> WpEvApp (EvId rep_d)
           <.> mkWpTyApps (init_inst_tys ++ [rep_ty]) 
         where
@@@ -1267,4 -1440,37 +1445,37 @@@ wrongATArgErr ty instTy 
        , ptext (sLit "Found") <+> quotes (ppr ty)
          <+> ptext (sLit "but expected") <+> quotes (ppr instTy)
        ]
+ tooManyParmsErr :: Located Name -> SDoc
+ tooManyParmsErr tc_name
+   = ptext (sLit "Family instance has too many parameters:") <+> 
+     quotes (ppr tc_name)
+ tooFewParmsErr :: Arity -> SDoc
+ tooFewParmsErr arity
+   = ptext (sLit "Family instance has too few parameters; expected") <+> 
+     ppr arity
+ wrongNumberOfParmsErr :: Arity -> SDoc
+ wrongNumberOfParmsErr exp_arity
+   = ptext (sLit "Number of parameters must match family declaration; expected")
+     <+> ppr exp_arity
+ badBootFamInstDeclErr :: SDoc
+ badBootFamInstDeclErr
+   = ptext (sLit "Illegal family instance in hs-boot file")
+ notFamily :: TyCon -> SDoc
+ notFamily tycon
+   = vcat [ ptext (sLit "Illegal family instance for") <+> quotes (ppr tycon)
+          , nest 2 $ parens (ppr tycon <+> ptext (sLit "is not an indexed type family"))]
+   
+ wrongKindOfFamily :: TyCon -> SDoc
+ wrongKindOfFamily family
+   = ptext (sLit "Wrong category of family instance; declaration was for a")
+     <+> kindOfFamily
+   where
+     kindOfFamily | isSynTyCon family = ptext (sLit "type synonym")
+                | isAlgTyCon family = ptext (sLit "data type")
+                | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
  \end{code}
@@@ -148,7 -148,7 +148,7 @@@ data TcSigInf
  
  instance Outputable TcSigInfo where
      ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
-         = ppr id <+> ptext (sLit "::") <+> ppr tyvars <+> pprThetaArrow theta <+> ppr tau
+         = ppr id <+> ptext (sLit "::") <+> ppr tyvars <+> pprThetaArrowTy theta <+> ppr tau
  \end{code}
  
  Note [sig_tau may be polymorphic]
@@@ -192,7 -192,7 +192,7 @@@ res_ty free vars
  %************************************************************************
  
  \begin{code}
- tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (CoercionI, TcId)
+ tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (Coercion, TcId)
  -- (coi, xp) = tcPatBndr penv x pat_ty
  -- Then coi : pat_ty ~ typeof(xp)
  --
@@@ -204,11 -204,11 +204,11 @@@ tcPatBndr (PE { pe_ctxt = LetPat lookup
        
    | otherwise
    = do { bndr_id <- newNoSigLetBndr no_gen bndr_name pat_ty
-        ; return (IdCo pat_ty, bndr_id) }
+        ; return (mkReflCo pat_ty, bndr_id) }
  
  tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
    = do { bndr <- mkLocalBinder bndr_name pat_ty
-        ; return (IdCo pat_ty, bndr) }
+        ; return (mkReflCo pat_ty, bndr) }
  
  ------------
  newSigLetBndr :: LetBndrSpec -> Name -> TcSigInfo -> TcM TcId
@@@ -372,7 -372,7 +372,7 @@@ tc_pat     :: PatEn
  tc_pat penv (VarPat name) pat_ty thing_inside
    = do        { (coi, id) <- tcPatBndr penv name pat_ty
        ; res <- tcExtendIdEnv1 name id thing_inside
-         ; return (mkHsWrapPatCoI coi (VarPat id) pat_ty, res) }
+         ; return (mkHsWrapPatCo coi (VarPat id) pat_ty, res) }
  
  tc_pat penv (ParPat pat) pat_ty thing_inside
    = do        { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
@@@ -422,7 -422,7 +422,7 @@@ tc_pat penv (AsPat (L nm_loc name) pat
            -- perhaps be fixed, but only with a bit more work.
            --
            -- If you fix it, don't forget the bindInstsOfPatIds!
-       ; return (mkHsWrapPatCoI coi (AsPat (L nm_loc bndr_id) pat') pat_ty, res) }
+       ; return (mkHsWrapPatCo coi (AsPat (L nm_loc bndr_id) pat') pat_ty, res) }
  
  tc_pat penv vpat@(ViewPat expr pat _) overall_pat_ty thing_inside 
    = do        { checkUnboxedTuple overall_pat_ty $
           -- pattern must have pat_ty
          ; (pat', res) <- tc_lpat pat pat_ty penv thing_inside
  
-       ; return (ViewPat (mkLHsWrapCoI expr_coi expr') pat' overall_pat_ty, res) }
+       ; return (ViewPat (mkLHsWrapCo expr_coi expr') pat' overall_pat_ty, res) }
  
  -- Type signatures in patterns
  -- See Note [Pattern coercions] below
@@@ -458,6 -458,9 +458,6 @@@ tc_pat penv (SigPatIn pat sig_ty) pat_t
  
          ; return (mkHsWrapPat wrap (SigPatOut pat' inner_ty) pat_ty, res) }
  
 -tc_pat _ pat@(TypePat _) _ _
 -  = failWithTc (badTypePat pat)
 -
  ------------------------
  -- Lists, tuples, arrays
  tc_pat penv (ListPat pats _) pat_ty thing_inside
@@@ -507,7 -510,7 +507,7 @@@ tc_pat _ (LitPat simple_lit) pat_ty thi
        ; coi <- unifyPatType lit_ty pat_ty
                -- coi is of kind: pat_ty ~ lit_ty
        ; res <- thing_inside 
-       ; return ( mkHsWrapPatCoI coi (LitPat simple_lit) pat_ty 
+       ; return ( mkHsWrapPatCo coi (LitPat simple_lit) pat_ty 
                   , res) }
  
  ------------------------
@@@ -542,19 -545,19 +542,19 @@@ tc_pat penv (NPlusKPat (L nm_loc name) 
        ; instStupidTheta orig [mkClassPred icls [pat_ty']]     
      
        ; res <- tcExtendIdEnv1 name bndr_id thing_inside
-       ; return (mkHsWrapPatCoI coi pat' pat_ty, res) }
+       ; return (mkHsWrapPatCo coi pat' pat_ty, res) }
  
  tc_pat _ _other_pat _ _ = panic "tc_pat"      -- ConPatOut, SigPatOut
  
  ----------------
- unifyPatType :: TcType -> TcType -> TcM CoercionI
+ unifyPatType :: TcType -> TcType -> TcM Coercion
  -- In patterns we want a coercion from the
  -- context type (expected) to the actual pattern type
  -- But we don't want to reverse the args to unifyType because
  -- that controls the actual/expected stuff in error messages
  unifyPatType actual_ty expected_ty
    = do { coi <- unifyType actual_ty expected_ty
-        ; return (mkSymCoI coi) }
+        ; return (mkSymCo coi) }
  \end{code}
  
  Note [Hopping the LIE in lazy patterns]
@@@ -653,7 -656,7 +653,7 @@@ tcConPat penv (L con_span con_name) pat
    = do        { data_con <- tcLookupDataCon con_name
        ; let tycon = dataConTyCon data_con
                  -- For data families this is the representation tycon
-             (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _)
+             (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
                  = dataConFullSig data_con
  
          -- Instantiate the constructor type variables [a->ty]
              tenv     = zipTopTvSubst (univ_tvs     ++ ex_tvs)
                                       (ctxt_res_tys ++ mkTyVarTys ex_tvs')
              arg_tys' = substTys tenv arg_tys
-             full_theta = eq_theta ++ dict_theta
  
-       ; if null ex_tvs && null eq_spec && null full_theta
+       ; if null ex_tvs && null eq_spec && null theta
          then do { -- The common case; no class bindings etc 
                      -- (see Note [Arrows and patterns])
                    (arg_pats', res) <- tcConArgs data_con arg_tys' 
  
          else do   -- The general case, with existential, 
                      -- and local equality constraints
-       { let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
-             theta'   = substTheta tenv (eq_preds ++ full_theta)
+       { let theta'   = substTheta tenv (eqSpecPreds eq_spec ++ theta)
                             -- order is *important* as we generate the list of
                             -- dictionary binders from theta'
              no_equalities = not (any isEqPred theta')
        } }
  
  ----------------------------
- matchExpectedPatTy :: (TcRhoType -> TcM (CoercionI, a))
+ matchExpectedPatTy :: (TcRhoType -> TcM (Coercion, a))
                      -> TcRhoType -> TcM (HsWrapper, a) 
  -- See Note [Matching polytyped patterns]
  -- Returns a wrapper : pat_ty ~ inner_ty
  matchExpectedPatTy inner_match pat_ty
    | null tvs && null theta
    = do { (coi, res) <- inner_match pat_ty
-        ; return (coiToHsWrapper (mkSymCoI coi), res) }
+        ; return (coToHsWrapper (mkSymCo coi), res) }
                 -- The Sym is because the inner_match returns a coercion
         -- that is the other way round to matchExpectedPatTy
  
    | otherwise
    = do { (_, tys, subst) <- tcInstTyVars tvs
         ; wrap1 <- instCall PatOrigin tys (substTheta subst theta)
-        ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (substTy subst tau)
+        ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau)
         ; return (wrap2 <.> wrap1 , arg_tys) }
    where
      (tvs, theta, tau) = tcSplitSigmaTy pat_ty
  matchExpectedConTy :: TyCon    -- The TyCon that this data 
                                 -- constructor actually returns
                   -> TcRhoType  -- The type of the pattern
-                  -> TcM (CoercionI, [TcSigmaType])
+                  -> TcM (Coercion, [TcSigmaType])
  -- See Note [Matching constructor patterns]
  -- Returns a coercion : T ty1 ... tyn ~ pat_ty
  -- This is the same way round as matchExpectedListTy etc
@@@ -760,10 -761,10 +758,10 @@@ matchExpectedConTy data_tc pat_t
         ; coi1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
                     -- coi1 : T (ty1,ty2) ~ pat_ty
  
-        ; let coi2 = ACo (mkTyConApp co_tc tys)
+        ; let coi2 = mkAxInstCo co_tc tys
                     -- coi2 : T (ty1,ty2) ~ T7 ty1 ty2
  
-        ; return (mkTransCoI (mkSymCoI coi2) coi1, tys) }
+        ; return (mkTransCo (mkSymCo coi2) coi1, tys) }
  
    | otherwise
    = matchExpectedTyConApp data_tc pat_ty
@@@ -1048,6 -1049,9 +1046,6 @@@ polyPatSig sig_t
    = hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
         2 (ppr sig_ty)
  
 -badTypePat :: Pat Name -> SDoc
 -badTypePat pat = ptext (sLit "Illegal type pattern") <+> ppr pat
 -
  lazyUnliftedPatErr :: OutputableBndr name => Pat name -> TcM ()
  lazyUnliftedPatErr pat
    = failWithTc $
@@@ -65,7 -65,6 +65,6 @@@ import Nam
  import NameEnv
  import NameSet
  import TyCon
- import TysPrim
  import SrcLoc
  import HscTypes
  import ListSetOps
@@@ -300,7 -299,7 +299,7 @@@ tcRnExtCore hsc_env (HsExtCore this_mo
        -- any mutually recursive types are done right
        -- Just discard the auxiliary bindings; they are generated 
        -- only for Haskell source code, and should already be in Core
 -   (tcg_env, _aux_binds, _dm_ids) <- tcTyAndClassDecls emptyModDetails rn_decls ;
 +   (tcg_env, _aux_binds, _dm_ids, _) <- tcTyAndClassDecls emptyModDetails rn_decls ;
  
     setGblEnv tcg_env $ do {
        -- Make the new type env available to stuff slurped from interface files
@@@ -501,7 -500,7 +500,7 @@@ tcRnHsBootDecls decl
  
                -- Typecheck type/class decls
        ; traceTc "Tc2" empty
 -      ; (tcg_env, aux_binds, dm_ids) 
 +      ; (tcg_env, aux_binds, dm_ids, _) 
                 <- tcTyAndClassDecls emptyModDetails tycl_decls
        ; setGblEnv tcg_env    $ 
            tcExtendIdEnv dm_ids $ do {
@@@ -645,7 -644,7 +644,7 @@@ checkHiBootIfac
      check_inst boot_inst
        = case [dfun | inst <- local_insts, 
                       let dfun = instanceDFunId inst,
-                      idType dfun `tcEqType` boot_inst_ty ] of
+                      idType dfun `eqType` boot_inst_ty ] of
            [] -> do { traceTc "check_inst" (vcat [ text "local_insts" <+> vcat (map (ppr . idType . instanceDFunId) local_insts)
                                                    , text "boot_inst"   <+> ppr boot_inst
                                                    , text "boot_inst_ty" <+> ppr boot_inst_ty
@@@ -669,7 -668,7 +668,7 @@@ checkBootDecl :: TyThing -> TyThing -> 
  
  checkBootDecl (AnId id1) (AnId id2)
    = ASSERT(id1 == id2) 
-     (idType id1 `tcEqType` idType id2)
+     (idType id1 `eqType` idType id2)
  
  checkBootDecl (ATyCon tc1) (ATyCon tc2)
    = checkBootTyCon tc1 tc2
@@@ -686,7 -685,7 +685,7 @@@ checkBootDecl (AClass c1)  (AClass c2
  
         eqSig (id1, def_meth1) (id2, def_meth2)
           = idName id1 == idName id2 &&
-            tcEqTypeX env op_ty1 op_ty2 &&
+            eqTypeX env op_ty1 op_ty2 &&
             def_meth1 == def_meth2
           where
          (_, rho_ty1) = splitForAllTys (idType id1)
            op_ty2 = funResultTy rho_ty2
  
         eqFD (as1,bs1) (as2,bs2) = 
-          eqListBy (tcEqTypeX env) (mkTyVarTys as1) (mkTyVarTys as2) &&
-          eqListBy (tcEqTypeX env) (mkTyVarTys bs1) (mkTyVarTys bs2)
+          eqListBy (eqTypeX env) (mkTyVarTys as1) (mkTyVarTys as2) &&
+          eqListBy (eqTypeX env) (mkTyVarTys bs1) (mkTyVarTys bs2)
  
         same_kind tv1 tv2 = eqKind (tyVarKind tv1) (tyVarKind tv2)
      in
         eqListBy eqFD clas_fds1 clas_fds2 &&
         (null sc_theta1 && null op_stuff1 && null ats1
          ||   -- Above tests for an "abstract" class
-         eqListBy (tcEqPredX env) sc_theta1 sc_theta2 &&
+         eqListBy (eqPredX env) sc_theta1 sc_theta2 &&
          eqListBy eqSig op_stuff1 op_stuff2 &&
          eqListBy checkBootTyCon ats1 ats2)
  
@@@ -728,7 -727,7 +727,7 @@@ checkBootTyCon tc1 tc
          eqSynRhs SynFamilyTyCon SynFamilyTyCon
              = True
          eqSynRhs (SynonymTyCon t1) (SynonymTyCon t2)
-             = tcEqTypeX env t1 t2
+             = eqTypeX env t1 t2
          eqSynRhs _ _ = False
      in
      equalLength tvs1 tvs2 &&
    | isAlgTyCon tc1 && isAlgTyCon tc2
    = ASSERT(tc1 == tc2)
      eqKind (tyConKind tc1) (tyConKind tc2) &&
-     eqListBy tcEqPred (tyConStupidTheta tc1) (tyConStupidTheta tc2) &&
+     eqListBy eqPred (tyConStupidTheta tc1) (tyConStupidTheta tc2) &&
      eqAlgRhs (algTyConRhs tc1) (algTyConRhs tc2)
  
    | isForeignTyCon tc1 && isForeignTyCon tc2
            && dataConIsInfix c1 == dataConIsInfix c2
            && dataConStrictMarks c1 == dataConStrictMarks c2
            && dataConFieldLabels c1 == dataConFieldLabels c2
-           && let tvs1 = dataConUnivTyVars c1 ++ dataConExTyVars c1
-                  tvs2 = dataConUnivTyVars c2 ++ dataConExTyVars c2
-                  env = rnBndrs2 env0 tvs1 tvs2
-              in
-               equalLength tvs1 tvs2 &&              
-               eqListBy (tcEqPredX env)
-                         (dataConEqTheta c1 ++ dataConDictTheta c1)
-                         (dataConEqTheta c2 ++ dataConDictTheta c2) &&
-               eqListBy (tcEqTypeX env)
-                         (dataConOrigArgTys c1)
-                         (dataConOrigArgTys c2)
+           && eqType (dataConUserType c1) (dataConUserType c2)
  
  ----------------
  missingBootThing :: Name -> String -> SDoc
@@@ -848,7 -837,7 +837,7 @@@ tcTopSrcDecls boot_detail
                -- The latter come in via tycl_decls
          traceTc "Tc2" empty ;
  
 -      (tcg_env, aux_binds, dm_ids) <- tcTyAndClassDecls boot_details tycl_decls ;
 +      (tcg_env, aux_binds, dm_ids, kc_decls) <- tcTyAndClassDecls boot_details tycl_decls ;
                -- If there are any errors, tcTyAndClassDecls fails here
        
        setGblEnv tcg_env       $
          setLclTypeEnv tcl_env $ do {  -- Environment doesn't change now
  
                  -- Second pass over class and instance declarations, 
 +                -- now using the kind-checked decls
          traceTc "Tc6" empty ;
 -        inst_binds <- tcInstDecls2 (concat tycl_decls) inst_infos ;
 +        inst_binds <- tcInstDecls2 kc_decls inst_infos ;
  
                  -- Foreign exports
          traceTc "Tc7" empty ;
@@@ -1327,16 -1315,13 +1316,13 @@@ tcRnExpr hsc_env ictxt rdr_exp
  
        -- Now typecheck the expression; 
        -- it might have a rank-2 type (e.g. :t runST)
      uniq <- newUnique ;
      let { fresh_it  = itName uniq } ;
-     ((_tc_expr, res_ty), lie)   <- captureConstraints (tcInferRho rn_expr) ;
-     ((qtvs, dicts, _), lie_top) <- captureConstraints $
-                                    simplifyInfer TopLevel
-                                                  False {- No MR for now -}
+     ((_tc_expr, res_ty), lie) <- captureConstraints (tcInferRho rn_expr) ;
+     ((qtvs, dicts, _), lie_top) <- captureConstraints $ 
+                                    simplifyInfer TopLevel False {- No MR for now -}
                                                   [(fresh_it, res_ty)]
                                                   lie  ;
      _ <- simplifyInteractive lie_top ;       -- Ignore the dicionary bindings
  
      let { all_expr_ty = mkForAllTys qtvs (mkPiTypes dicts res_ty) } ;
@@@ -1588,6 -1573,7 +1574,6 @@@ pprTcGblEnv (TcGblEnv { tcg_type_env  
           , ppr_fam_insts fam_insts
           , vcat (map ppr rules)
           , vcat (map ppr vects)
 -         , ppr_gen_tycons (typeEnvTyCons type_env)
           , ptext (sLit "Dependent modules:") <+> 
                  ppr (sortBy cmp_mp $ eltsUFM (imp_dep_mods imports))
         , ptext (sLit "Dependent packages:") <+> 
@@@ -1622,7 -1608,10 +1608,10 @@@ ppr_types insts type_en
  
  ppr_tycons :: [FamInst] -> TypeEnv -> SDoc
  ppr_tycons fam_insts type_env
-   = text "TYPE CONSTRUCTORS" $$ nest 4 (ppr_tydecls tycons)
+   = vcat [ text "TYPE CONSTRUCTORS"
+          ,   nest 2 (ppr_tydecls tycons)
+          , text "COERCION AXIOMS" 
+          ,   nest 2 (vcat (map pprCoAxiom (typeEnvCoAxioms type_env))) ]
    where
      fi_tycons = map famInstTyCon fam_insts
      tycons = [tycon | tycon <- typeEnvTyCons type_env, want_tycon tycon]
@@@ -1654,17 -1643,17 +1643,12 @@@ ppr_tydecls tycon
    = vcat (map ppr_tycon (sortLe le_sig tycons))
    where
      le_sig tycon1 tycon2 = getOccName tycon1 <= getOccName tycon2
-     ppr_tycon tycon 
-       | isCoercionTyCon tycon 
-       = sep [ptext (sLit "coercion") <+> ppr tycon <+> ppr tvs
-             , nest 2 (dcolon <+> pprEqPred (coercionKind (mkTyConApp tycon (mkTyVarTys tvs))))]
-       | otherwise             = ppr (tyThingToIfaceDecl (ATyCon tycon))
+     ppr_tycon tycon = ppr (tyThingToIfaceDecl (ATyCon tycon))
        where
-         tvs = take (tyConArity tycon) alphaTyVars
  
  ppr_rules :: [CoreRule] -> SDoc
  ppr_rules [] = empty
  ppr_rules rs = vcat [ptext (sLit "{-# RULES"),
                      nest 2 (pprRules rs),
                      ptext (sLit "#-}")]
 -
 -ppr_gen_tycons :: [TyCon] -> SDoc
 -ppr_gen_tycons []  = empty
 -ppr_gen_tycons tcs = vcat [ptext (sLit "Tycons with generics:"),
 -                         nest 2 (fsep (map ppr (filter tyConHasGenerics tcs)))]
  \end{code}
@@@ -82,6 -82,7 +82,7 @@@ import qualified TcRnMonad as Tc
  import qualified TcMType as TcM
  import qualified TcEnv as TcM 
         ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
+ import Kind
  import TcType
  import DynFlags
  
@@@ -97,12 -98,14 +98,13 @@@ import Outputabl
  import Bag
  import MonadUtils
  import VarSet
+ import Pair
  import FastString
  
  import HsBinds               -- for TcEvBinds stuff 
  import Id 
  import TcRnTypes
  import Data.IORef
 -
  #ifdef DEBUG
  import StaticFlags( opt_PprStyle_Debug )
  import Control.Monad( when )
@@@ -206,9 -209,9 +208,9 @@@ instance Outputable CanonicalCt wher
    ppr (CIPCan ip fl ip_nm ty)     
        = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
    ppr (CTyEqCan co fl tv ty)      
-       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
+       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyVarTy tv) ty)
    ppr (CFunEqCan co fl tc tys ty) 
-       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
+       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyConApp tc tys) ty)
    ppr (CFrozenErr co fl)
        = ppr fl <+> pprEvVarWithType co
  \end{code}
@@@ -676,7 -679,7 +678,7 @@@ checkWellStagedDFun pred dfun_id lo
      bind_lvl = TcM.topIdLvl dfun_id
  
  pprEq :: TcType -> TcType -> SDoc
- pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
+ pprEq ty1 ty2 = pprPredTy $ mkEqPred (ty1,ty2)
  
  isTouchableMetaTyVar :: TcTyVar -> TcS Bool
  isTouchableMetaTyVar tv 
@@@ -7,7 -7,8 +7,8 @@@ TcTyClsDecls: Typecheck type and class 
  
  \begin{code}
  module TcTyClsDecls (
-       tcTyAndClassDecls, tcFamInstDecl, mkRecSelBinds
+       tcTyAndClassDecls, kcDataDecl, tcConDecls, mkRecSelBinds,
+         checkValidTyCon, dataDeclChecks, badFamInstDecl
      ) where
  
  #include "HsVersions.h"
@@@ -25,10 -26,12 +26,10 @@@ import TcMTyp
  import TcType
  import TysWiredIn     ( unitTy )
  import Type
 -import Generics
  import Class
  import TyCon
  import DataCon
  import Id
 -import MkId           ( mkDefaultMethodId )
  import MkCore         ( rEC_SEL_ERROR_ID )
  import IdInfo
  import Var
@@@ -59,14 -62,12 +60,14 @@@ import Data.Lis
  %************************************************************************
  
  \begin{code}
 +
  tcTyAndClassDecls :: ModDetails 
                     -> [[LTyClDecl Name]]     -- Mutually-recursive groups in dependency order
                   -> TcM (TcGblEnv,         -- Input env extended by types and classes 
                                             -- and their implicit Ids,DataCons
                           HsValBinds Name,  -- Renamed bindings for record selectors
 -                         [Id])             -- Default method ids
 +                         [Id],             -- Default method ids
 +                           [LTyClDecl Name]) -- Kind-checked declarations
  -- Fails if there are any errors
  
  tcTyAndClassDecls boot_details decls_s
@@@ -89,7 -90,7 +90,7 @@@
  
                        -- And now build the TyCons/Classes
                  ; let rec_flags = calcRecFlags boot_details rec_tyclss
 -                 ; concatMapM (tcTyClDecl rec_flags) kc_decls }
 +                ; concatMapM (tcTyClDecl rec_flags) kc_decls }
  
         ; tcExtendGlobalEnv tyclss $ do
         {  -- Perform the validity check
                ; dm_ids          = mkDefaultMethodIds tyclss }
  
        ; env <- tcExtendGlobalEnv implicit_things getGblEnv
 -      ; return (env, rec_sel_binds, dm_ids) } }
 +          -- We need the kind-checked declarations later, so we return them
 +          -- from here
 +        ; kc_decls <- kcTyClDecls tyclds_s
 +        ; return (env, rec_sel_binds, dm_ids, kc_decls) } }
                      
  zipRecTyClss :: [[LTyClDecl Name]]
               -> [TyThing]           -- Knot-tied
@@@ -140,188 -138,6 +141,6 @@@ zipRecTyClss decls_s rec_thing
  
  %************************************************************************
  %*                                                                    *
-                Type checking family instances
- %*                                                                    *
- %************************************************************************
- Family instances are somewhat of a hybrid.  They are processed together with
- 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).
- \begin{code}
- tcFamInstDecl :: TopLevelFlag -> LTyClDecl Name -> TcM TyThing
- tcFamInstDecl top_lvl (L loc decl)
-   =   -- Prime error recovery, set source location
-     setSrcSpan loc                            $
-     tcAddDeclCtxt decl                                $
-     do { -- type family instances require -XTypeFamilies
-        -- and can't (currently) be in an hs-boot file
-        ; type_families <- xoptM Opt_TypeFamilies
-        ; is_boot  <- tcIsHsBoot         -- Are we compiling an hs-boot file?
-        ; checkTc type_families $ badFamInstDecl (tcdLName decl)
-        ; checkTc (not is_boot) $ badBootFamInstDeclErr
-        -- Perform kind and type checking
-        ; tc <- tcFamInstDecl1 decl
-        ; checkValidTyCon tc   -- Remember to check validity;
-                               -- no recursion to worry about here
-        -- Check that toplevel type instances are not for associated types.
-        ; when (isTopLevel top_lvl && isAssocFamily tc)
-               (addErr $ assocInClassErr (tcdName decl))
-        ; return (ATyCon tc) }
- isAssocFamily :: TyCon -> Bool        -- Is an assocaited type
- isAssocFamily tycon
-   = case tyConFamInst_maybe tycon of
-           Nothing       -> panic "isAssocFamily: no family?!?"
-           Just (fam, _) -> isTyConAssoc fam
- assocInClassErr :: Name -> SDoc
- assocInClassErr name
-  = ptext (sLit "Associated type") <+> quotes (ppr name) <+>
-    ptext (sLit "must be inside a class instance")
- tcFamInstDecl1 :: TyClDecl Name -> TcM TyCon
-   -- "type instance"
- tcFamInstDecl1 (decl@TySynonym {tcdLName = L loc tc_name})
-   = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
-     do { -- check that the family declaration is for a synonym
-          checkTc (isFamilyTyCon family) (notFamily family)
-        ; checkTc (isSynTyCon family) (wrongKindOfFamily family)
-        ; -- (1) kind check the right-hand side of the type equation
-        ; k_rhs <- kcCheckLHsType (tcdSynRhs decl) (EK resKind EkUnk)
-                         -- ToDo: the ExpKind could be better
-          -- we need the exact same number of type parameters as the family
-          -- declaration 
-        ; let famArity = tyConArity family
-        ; checkTc (length k_typats == famArity) $ 
-            wrongNumberOfParmsErr famArity
-          -- (2) type check type equation
-        ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
-        ; t_typats <- mapM tcHsKindedType k_typats
-        ; t_rhs    <- tcHsKindedType k_rhs
-          -- (3) check the well-formedness of the instance
-        ; checkValidTypeInst t_typats t_rhs
-          -- (4) construct representation tycon
-        ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc
-        ; buildSynTyCon rep_tc_name t_tvs (SynonymTyCon t_rhs) 
-                        (typeKind t_rhs) 
-                        NoParentTyCon (Just (family, t_typats))
-        }}
-   -- "newtype instance" and "data instance"
- tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
-                            tcdCons = cons})
-   = kcIdxTyPats decl $ \k_tvs k_typats resKind fam_tycon ->
-     do { -- check that the family declaration is for the right kind
-          checkTc (isFamilyTyCon fam_tycon) (notFamily fam_tycon)
-        ; checkTc (isAlgTyCon fam_tycon) (wrongKindOfFamily fam_tycon)
-        ; -- (1) kind check the data declaration as usual
-        ; k_decl <- kcDataDecl decl k_tvs
-        ; let k_ctxt = tcdCtxt k_decl
-            k_cons = tcdCons k_decl
-          -- result kind must be '*' (otherwise, we have too few patterns)
-        ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr (tyConArity fam_tycon)
-          -- (2) type check indexed data type declaration
-        ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
-        ; unbox_strict <- doptM Opt_UnboxStrictFields
-          -- kind check the type indexes and the context
-        ; t_typats     <- mapM tcHsKindedType k_typats
-        ; stupid_theta <- tcHsKindedContext k_ctxt
-          -- (3) Check that
-          --     (a) left-hand side contains no type family applications
-          --         (vanilla synonyms are fine, though, and we checked for
-          --         foralls earlier)
-        ; mapM_ checkTyFamFreeness t_typats
-        -- Check that we don't use GADT syntax in H98 world
-        ; gadt_ok <- xoptM Opt_GADTs
-        ; checkTc (gadt_ok || consUseH98Syntax cons) (badGadtDecl tc_name)
-        --     (b) a newtype has exactly one constructor
-        ; checkTc (new_or_data == DataType || isSingleton k_cons) $
-                newtypeConError tc_name (length k_cons)
-          -- (4) construct representation tycon
-        ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc
-        ; let ex_ok = True     -- Existentials ok for type families!
-        ; fixM (\ rep_tycon -> do 
-            { let orig_res_ty = mkTyConApp fam_tycon t_typats
-            ; data_cons <- tcConDecls unbox_strict ex_ok rep_tycon
-                                      (t_tvs, orig_res_ty) k_cons
-            ; tc_rhs <-
-                case new_or_data of
-                  DataType -> return (mkDataTyConRhs data_cons)
-                  NewType  -> ASSERT( not (null data_cons) )
-                              mkNewTyConRhs rep_tc_name rep_tycon (head data_cons)
-            ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
-                            h98_syntax NoParentTyCon (Just (fam_tycon, t_typats))
-                  -- We always assume that indexed types are recursive.  Why?
-                  -- (1) Due to their open nature, we can never be sure that a
-                  -- further instance might not introduce a new recursive
-                  -- dependency.  (2) They are always valid loop breakers as
-                  -- they involve a coercion.
-            })
-        }}
-        where
-        h98_syntax = case cons of      -- All constructors have same shape
-                       L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
-                       _ -> True
- tcFamInstDecl1 d = pprPanic "tcFamInstDecl1" (ppr d)
- -- Kind checking of indexed types
- -- -
- -- Kind check type patterns and kind annotate the embedded type variables.
- --
- -- * Here we check that a type instance matches its kind signature, but we do
- --   not check whether there is a pattern for each type index; the latter
- --   check is only required for type synonym instances.
- kcIdxTyPats :: TyClDecl Name
-           -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TyCon -> TcM a)
-              -- ^^kinded tvs         ^^kinded ty pats  ^^res kind
-           -> TcM a
- kcIdxTyPats decl thing_inside
-   = kcHsTyVars (tcdTyVars decl) $ \tvs -> 
-     do { let tc_name = tcdLName decl
-        ; fam_tycon <- tcLookupLocatedTyCon tc_name
-        ; let { (kinds, resKind) = splitKindFunTys (tyConKind fam_tycon)
-            ; hs_typats        = fromJust $ tcdTyPats decl }
-          -- we may not have more parameters than the kind indicates
-        ; checkTc (length kinds >= length hs_typats) $
-          tooManyParmsErr (tcdLName decl)
-          -- type functions can have a higher-kinded result
-        ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
-        ; typats <- zipWithM kcCheckLHsType hs_typats 
-                                   [ EK kind (EkArg (ppr tc_name) n) 
-                             | (kind,n) <- kinds `zip` [1..]]
-        ; thing_inside tvs typats resultKind fam_tycon
-        }
- \end{code}
- %************************************************************************
- %*                                                                    *
                Kind checking
  %*                                                                    *
  %************************************************************************
@@@ -491,8 -307,6 +310,8 @@@ kcTyClDecl decl@(ClassDecl {tcdCtxt = c
    where
      kc_sig (TypeSig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
                                   ; return (TypeSig nm op_ty') }
 +    kc_sig (GenericSig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
 +                                    ; return (GenericSig nm op_ty') }
      kc_sig other_sig        = return other_sig
  
  kcTyClDecl decl@(ForeignType {})
@@@ -639,7 -453,7 +458,7 @@@ tcTyClDecl1 parent _calc_isre
    ; checkTc idx_tys $ badFamInstDecl tc_name
  
    ; tycon <- buildAlgTyCon tc_name final_tvs [] 
 -               DataFamilyTyCon Recursive False True 
 +               DataFamilyTyCon Recursive True 
                 parent Nothing
    ; return [ATyCon tycon]
    }
@@@ -665,35 -479,19 +484,18 @@@ tcTyClDecl1 _parent calc_isre
    { extra_tvs <- tcDataKindSig mb_ksig
    ; let final_tvs = tvs' ++ extra_tvs
    ; stupid_theta <- tcHsKindedContext ctxt
 -  ; want_generic <- xoptM Opt_Generics
    ; unbox_strict <- doptM Opt_UnboxStrictFields
    ; kind_signatures <- xoptM Opt_KindSignatures
    ; existential_ok <- xoptM Opt_ExistentialQuantification
    ; gadt_ok      <- xoptM Opt_GADTs
    ; is_boot    <- tcIsHsBoot  -- Are we compiling an hs-boot file?
    ; let ex_ok = existential_ok || gadt_ok     -- Data cons can have existential context
  
        -- Check that we don't use kind signatures without Glasgow extensions
    ; checkTc (kind_signatures || isNothing mb_ksig) (badSigTyDecl tc_name)
  
-       -- Check that the stupid theta is empty for a GADT-style declaration
-   ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
+   ; dataDeclChecks tc_name new_or_data stupid_theta cons
  
-       -- Check that a newtype has exactly one constructor
-       -- Do this before checking for empty data decls, so that
-       -- we don't suggest -XEmptyDataDecls for newtypes
-   ; checkTc (new_or_data == DataType || isSingleton cons) 
-           (newtypeConError tc_name (length cons))
-       -- Check that there's at least one condecl,
-       -- or else we're reading an hs-boot file, or -XEmptyDataDecls
-   ; checkTc (not (null cons) || empty_data_decls || is_boot)
-           (emptyConDeclsErr tc_name)
-     
    ; tycon <- fixM (\ tycon -> do 
        { let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
        ; data_cons <- tcConDecls unbox_strict ex_ok 
                   NewType  -> ASSERT( not (null data_cons) )
                                 mkNewTyConRhs tc_name tycon (head data_cons)
        ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
 -          (want_generic && canDoGenerics data_cons) (not h98_syntax) 
 -            NoParentTyCon Nothing
 +          (not h98_syntax) NoParentTyCon Nothing
        })
    ; return [ATyCon tycon]
    }
@@@ -750,6 -549,29 +552,29 @@@ tcTyClDecl1 _ 
  
  tcTyClDecl1 _ _ d = pprPanic "tcTyClDecl1" (ppr d)
  
+ dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM ()
+ dataDeclChecks tc_name new_or_data stupid_theta cons
+   = do {   -- Check that we don't use GADT syntax in H98 world
+          gadtSyntax_ok <- xoptM Opt_GADTSyntax
+        ; let h98_syntax = consUseH98Syntax cons
+        ; checkTc (gadtSyntax_ok || h98_syntax) (badGadtDecl tc_name)
+          -- Check that the stupid theta is empty for a GADT-style declaration
+        ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
+       -- Check that a newtype has exactly one constructor
+       -- Do this before checking for empty data decls, so that
+       -- we don't suggest -XEmptyDataDecls for newtypes
+       ; checkTc (new_or_data == DataType || isSingleton cons) 
+               (newtypeConError tc_name (length cons))
+       -- Check that there's at least one condecl,
+       -- or else we're reading an hs-boot file, or -XEmptyDataDecls
+       ; empty_data_decls <- xoptM Opt_EmptyDataDecls
+       ; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
+       ; checkTc (not (null cons) || empty_data_decls || is_boot)
+                 (emptyConDeclsErr tc_name) }
+     
  -----------------------------------
  tcConDecls :: Bool -> Bool -> TyCon -> ([TyVar], Type)
           -> [LConDecl Name] -> TcM [DataCon]
@@@ -1102,14 -924,14 +927,14 @@@ checkNewDataCon co
                -- One argument
        ; checkTc (null eq_spec) (newtypePredError con)
                -- Return type is (T a b c)
-       ; checkTc (null ex_tvs && null eq_theta && null dict_theta) (newtypeExError con)
+       ; checkTc (null ex_tvs && null theta) (newtypeExError con)
                -- No existentials
        ; checkTc (not (any isBanged (dataConStrictMarks con))) 
                  (newtypeStrictError con)
                -- No strictness
      }
    where
-     (_univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _res_ty) = dataConFullSig con
+     (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con
  
  -------------------------------
  checkValidClass :: Class -> TcM ()
@@@ -1137,9 -959,9 +962,9 @@@ checkValidClass cl
    where
      (tyvars, fundeps, theta, _, _, op_stuff) = classExtraBigSig cls
      unary     = isSingleton tyvars
 -    no_generics = null [() | (_, GenDefMeth) <- op_stuff]
 +    no_generics = null [() | (_, (GenDefMeth _)) <- op_stuff]
  
 -    check_op constrained_class_methods (sel_id, dm) 
 +    check_op constrained_class_methods (sel_id, _) 
        = addErrCtxt (classOpCtxt sel_id tau) $ do
        { checkValidTheta SigmaCtxt (tail theta)
                -- The 'tail' removes the initial (C a) from the
        ; let grown_tyvars = growThetaTyVars theta (mkVarSet tyvars)
        ; checkTc (tyVarsOfType tau `intersectsVarSet` grown_tyvars)
                  (noClassTyVarErr cls sel_id)
 -
 -              -- Check that for a generic method, the type of 
 -              -- the method is sufficiently simple
 -      ; checkTc (dm /= GenDefMeth || validGenericMethodType tau)
 -                (badGenericMethodType op_name op_ty)
        }
        where
          op_name = idName sel_id
  mkDefaultMethodIds :: [TyThing] -> [Id]
  -- See Note [Default method Ids and Template Haskell]
  mkDefaultMethodIds things
 -  = [ mkDefaultMethodId sel_id dm_name
 +  = [ mkExportedLocalId dm_name (idType sel_id)
      | AClass cls <- things
      , (sel_id, DefMeth dm_name) <- classOpItems cls ]
  \end{code}
@@@ -1422,6 -1249,12 +1247,6 @@@ genericMultiParamErr cla
    = ptext (sLit "The multi-parameter class") <+> quotes (ppr clas) <+> 
      ptext (sLit "cannot have generic methods")
  
 -badGenericMethodType :: Name -> Kind -> SDoc
 -badGenericMethodType op op_ty
 -  = hang (ptext (sLit "Generic method type is too complex"))
 -       2 (vcat [ppr op <+> dcolon <+> ppr op_ty,
 -              ptext (sLit "You can only use type variables, arrows, lists, and tuples")])
 -
  recSynErr :: [LTyClDecl Name] -> TcRn ()
  recSynErr syn_decls
    = setSrcSpan (getLoc (head sorted_decls)) $
@@@ -1503,39 -1336,6 +1328,6 @@@ badFamInstDecl tc_nam
           quotes (ppr tc_name)
         , nest 2 (parens $ ptext (sLit "Use -XTypeFamilies to allow indexed type families")) ]
  
- tooManyParmsErr :: Located Name -> SDoc
- tooManyParmsErr tc_name
-   = ptext (sLit "Family instance has too many parameters:") <+> 
-     quotes (ppr tc_name)
- tooFewParmsErr :: Arity -> SDoc
- tooFewParmsErr arity
-   = ptext (sLit "Family instance has too few parameters; expected") <+> 
-     ppr arity
- wrongNumberOfParmsErr :: Arity -> SDoc
- wrongNumberOfParmsErr exp_arity
-   = ptext (sLit "Number of parameters must match family declaration; expected")
-     <+> ppr exp_arity
- badBootFamInstDeclErr :: SDoc
- badBootFamInstDeclErr
-   = ptext (sLit "Illegal family instance in hs-boot file")
- notFamily :: TyCon -> SDoc
- notFamily tycon
-   = vcat [ ptext (sLit "Illegal family instance for") <+> quotes (ppr tycon)
-          , nest 2 $ parens (ppr tycon <+> ptext (sLit "is not an indexed type family"))]
-   
- wrongKindOfFamily :: TyCon -> SDoc
- wrongKindOfFamily family
-   = ptext (sLit "Wrong category of family instance; declaration was for a")
-     <+> kindOfFamily
-   where
-     kindOfFamily | isSynTyCon family = ptext (sLit "type synonym")
-                | isAlgTyCon family = ptext (sLit "data type")
-                | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
  emptyConDeclsErr :: Name -> SDoc
  emptyConDeclsErr tycon
    = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
diff --combined compiler/types/TyCon.lhs
@@@ -13,7 -13,9 +13,9 @@@ module TyCon
        AlgTyConRhs(..), visibleDataCons, 
          TyConParent(..), isNoParent,
        SynTyConRhs(..),
-         CoTyConDesc(..),
+       -- ** Coercion axiom constructors
+         CoAxiom(..), coAxiomName, coAxiomArity,
  
          -- ** Constructing TyCons
        mkAlgTyCon,
@@@ -25,7 -27,6 +27,6 @@@
        mkTupleTyCon,
        mkSynTyCon,
          mkSuperKindTyCon,
-         mkCoercionTyCon,
          mkForeignTyCon,
          mkAnyTyCon,
  
          isFunTyCon, 
          isPrimTyCon,
          isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, 
-         isSynTyCon, isClosedSynTyCon, 
+         isSynTyCon, isClosedSynTyCon,
          isSuperKindTyCon, isDecomposableTyCon,
-         isCoercionTyCon, isCoercionTyCon_maybe,
          isForeignTyCon, isAnyTyCon, tyConHasKind,
  
        isInjectiveTyCon,
        isDataTyCon, isProductTyCon, isEnumerationTyCon, 
-       isNewTyCon, isAbstractTyCon, 
+         isNewTyCon, isAbstractTyCon,
          isFamilyTyCon, isSynFamilyTyCon, isDataFamilyTyCon,
          isUnLiftedTyCon,
        isGadtSyntaxTyCon,
        isTyConAssoc,
        isRecursiveTyCon,
        isHiBootTyCon,
 -        isImplicitTyCon, tyConHasGenerics,
 +        isImplicitTyCon, 
  
          -- ** Extracting information out of TyCons
        tyConName,
          tyConParent,
        tyConClass_maybe,
        tyConFamInst_maybe, tyConFamilyCoercion_maybe,tyConFamInstSig_maybe,
-       synTyConDefn, synTyConRhs, synTyConType, 
-       tyConExtName,           -- External name for foreign types
+         synTyConDefn, synTyConRhs, synTyConType,
+         tyConExtName,           -- External name for foreign types
        algTyConRhs,
          newTyConRhs, newTyConEtadRhs, unwrapNewTyCon_maybe, 
 -        tupleTyConBoxity,
 +        tupleTyConBoxity, tupleTyConArity,
  
          -- ** Manipulating TyCons
        tcExpandTyCon_maybe, coreExpandTyCon_maybe,
        makeTyConAbstract,
-       newTyConCo_maybe,
+       newTyConCo, newTyConCo_maybe,
  
          -- * Primitive representations of Types
        PrimRep(..),
@@@ -113,7 -113,7 +113,7 @@@ Note [Type synonym families
  
  * Reply "yes" to isSynFamilyTyCon, and isFamilyTyCon
  
- * From the user's point of view (F Int) and Bool are simply 
+ * From the user's point of view (F Int) and Bool are simply
    equivalent types.
  
  * A Haskell 98 type synonym is a degenerate form of a type synonym
    TyCon.  In turn this means that type and data families can be
    treated uniformly.
  
+ * Translation of type family decl:
+       type family F a :: *
+   translates to
+     a SynTyCon 'F', whose SynTyConRhs is SynFamilyTyCon
+ * Translation of type instance decl:
+       type instance F [a] = Maybe a
+   translates to
+     A SynTyCon 'R:FList a', whose 
+        SynTyConRhs is (SynonymTyCon (Maybe a))
+        TyConParent is (FamInstTyCon F [a] co)
+          where co :: F [a] ~ R:FList a
+     Notice that we introduce a gratuitous vanilla type synonym
+        type R:FList a = Maybe a
+     solely so that type and data families can be treated more
+     uniformly, via a single FamInstTyCon descriptor        
  * In the future we might want to support
      * closed type families (esp when we have proper kinds)
      * injective type families (allow decomposition)
@@@ -169,6 -186,8 +186,8 @@@ See also Note [Wrappers for data instan
  
  * Reply "yes" to isDataFamilyTyCon, and isFamilyTyCon
  
+ * Reply "yes" to isDataFamilyTyCon, and isFamilyTyCon
  * The user does not see any "equivalent types" as he did with type
    synonym families.  He just sees constructors with types
        T1 :: T Int
  --
  -- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor of kind @*@
  --
- -- 5) Type coercions! This is because we represent a coercion from @t1@ to @t2@ 
- --    as a 'Type', where that type has kind @t1 ~ t2@. See "Coercion" for more on this
- --
  -- This data type also encodes a number of primitive, built in type constructors such as those
  -- for function and tuple types.
  data TyCon
  
        algTcRec :: RecFlag,      -- ^ Tells us whether the data type is part 
                                    -- of a mutually-recursive group or not
 -
 -      hasGenerics :: Bool,      -- ^ Whether generic (in the -XGenerics sense) 
 -                                  -- to\/from functions are available in the exports 
 -                                  -- of the data type's source module.
 -
 +      
        algTcParent :: TyConParent      -- ^ Gives the class or family declaration 'TyCon' 
                                          -- for derived 'TyCon's representing class 
                                          -- or family instances, respectively. 
        tyConArity  :: Arity,
        tyConBoxed  :: Boxity,
        tyConTyVars :: [TyVar],
 -      dataCon     :: DataCon, -- ^ Corresponding tuple data constructor
 -      hasGenerics :: Bool
 +      dataCon     :: DataCon -- ^ Corresponding tuple data constructor
      }
  
    -- | Represents type synonyms
                                             --   holds the name of the imported thing
      }
  
-   -- | Type coercions, such as @(~)@, @sym@, @trans@, @left@ and @right@.
-   -- INVARIANT: Coercion TyCons are always fully applied
-   --          But note that a CoTyCon can be *over*-saturated in a type.
-   --          E.g.  (sym g1) Int  will be represented as (TyConApp sym [g1,Int])
-   | CoTyCon { 
-       tyConUnique :: Unique,
-         tyConName   :: Name,
-       tyConArity  :: Arity,
-       coTcDesc    :: CoTyConDesc
-     }
    -- | Any types.  Like tuples, this is a potentially-infinite family of TyCons
    --   one for each distinct Kind. They have no values at all.
    --   Because there are infinitely many of them (like tuples) they are 
    | AnyTyCon {
        tyConUnique  :: Unique,
        tyConName    :: Name,
-       tc_kind    :: Kind      -- Never = *; that is done via PrimTyCon
+       tc_kind      :: Kind    -- Never = *; that is done via PrimTyCon
                                -- See Note [Any types] in TysPrim
      }
  
@@@ -470,18 -480,14 +475,14 @@@ data AlgTyConRh
                        -- shorter than the declared arity of the 'TyCon'.
                        
                        -- See Note [Newtype eta]
-       
-         nt_co :: Maybe TyCon   -- ^ A 'TyCon' (which is always a 'CoTyCon') that can 
-                                -- have a 'Coercion' extracted from it to create 
-                                -- the @newtype@ from the representation 'Type'.
-                                --
-                                -- This field is optional for non-recursive @newtype@s only.
-                                
-                              -- See Note [Newtype coercions]
-                              -- Invariant: arity = #tvs in nt_etad_rhs;
-                              --       See Note [Newtype eta]
-                              -- Watch out!  If any newtypes become transparent
-                              -- again check Trac #1072.
+         nt_co :: CoAxiom     -- The axiom coercion that creates the @newtype@ from 
+                              -- the representation 'Type'.
+                                 
+                              -- See Note [Newtype coercions]
+                              -- Invariant: arity = #tvs in nt_etad_rhs;
+                              --       See Note [Newtype eta]
+                              -- Watch out!  If any newtypes become transparent
+                              -- again check Trac #1072.
      }
  
  -- | Extract those 'DataCon's that we are able to learn about.  Note
@@@ -541,7 -547,7 +542,7 @@@ data TyConParen
                          -- and Note [Type synonym families]
        TyCon   -- The family TyCon
        [Type]  -- Argument types (mentions the tyConTyVars of this TyCon)
-       TyCon   -- The coercion constructor
+         CoAxiom   -- The coercion constructor
  
        -- E.g.  data intance T [a] = ...
        -- gives a representation tycon:
@@@ -572,20 -578,6 +573,6 @@@ data SynTyConRh
  
     -- | A type synonym family  e.g. @type family F x y :: * -> *@
     | SynFamilyTyCon
- --------------------
- data CoTyConDesc
-   = CoSym   | CoTrans
-   | CoLeft  | CoRight
-   | CoCsel1 | CoCsel2 | CoCselR
-   | CoInst
-   | CoAxiom   -- C tvs : F lhs-tys ~ rhs-ty
-       { co_ax_tvs :: [TyVar]
-       , co_ax_lhs :: Type
-       , co_ax_rhs :: Type }
-   | CoUnsafe 
  \end{code}
  
  Note [Enumeration types]
@@@ -684,6 -676,31 +671,31 @@@ so the coercion tycon CoT must hav
  
  %************************************************************************
  %*                                                                    *
+                     Coercion axioms
+ %*                                                                    *
+ %************************************************************************
+ \begin{code}
+ -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
+ data CoAxiom
+   = CoAxiom                   -- type equality axiom.
+     { co_ax_unique :: Unique   -- unique identifier
+     , co_ax_name   :: Name     -- name for pretty-printing
+     , co_ax_tvs    :: [TyVar]  -- bound type variables 
+     , co_ax_lhs    :: Type     -- left-hand side of the equality
+     , co_ax_rhs    :: Type     -- right-hand side of the equality
+     }
+ coAxiomArity :: CoAxiom -> Arity
+ coAxiomArity ax = length (co_ax_tvs ax)
+ coAxiomName :: CoAxiom -> Name
+ coAxiomName = co_ax_name
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
  \subsection{PrimRep}
  %*                                                                    *
  %************************************************************************
@@@ -771,9 -788,10 +783,9 @@@ mkAlgTyCon :: Nam
             -> AlgTyConRhs       -- ^ Information about dat aconstructors
             -> TyConParent
             -> RecFlag           -- ^ Is the 'TyCon' recursive?
 -           -> Bool              -- ^ Does it have generic functions? See 'hasGenerics'
             -> Bool              -- ^ Was the 'TyCon' declared with GADT syntax?
             -> TyCon
 -mkAlgTyCon name kind tyvars stupid rhs parent is_rec gen_info gadt_syn
 +mkAlgTyCon name kind tyvars stupid rhs parent is_rec gadt_syn
    = AlgTyCon {        
        tyConName        = name,
        tyConUnique      = nameUnique name,
        algTcRhs         = rhs,
        algTcParent      = ASSERT( okParent name parent ) parent,
        algTcRec         = is_rec,
 -      algTcGadtSyntax  = gadt_syn,
 -      hasGenerics      = gen_info
 +      algTcGadtSyntax  = gadt_syn
      }
  
  -- | Simpler specialization of 'mkAlgTyCon' for classes
  mkClassTyCon :: Name -> Kind -> [TyVar] -> AlgTyConRhs -> Class -> RecFlag -> TyCon
  mkClassTyCon name kind tyvars rhs clas is_rec =
 -  mkAlgTyCon name kind tyvars [] rhs (ClassTyCon clas) is_rec False False
 +  mkAlgTyCon name kind tyvars [] rhs (ClassTyCon clas) is_rec False
  
  mkTupleTyCon :: Name 
               -> Kind    -- ^ Kind of the resulting 'TyCon'
               -> [TyVar] -- ^ 'TyVar's scoped over: see 'tyConTyVars'
               -> DataCon 
               -> Boxity  -- ^ Whether the tuple is boxed or unboxed
 -             -> Bool    -- ^ Does it have generic functions? See 'hasGenerics'
               -> TyCon
 -mkTupleTyCon name kind arity tyvars con boxed gen_info
 +mkTupleTyCon name kind arity tyvars con boxed 
    = TupleTyCon {
        tyConUnique = nameUnique name,
        tyConName = name,
        tyConArity = arity,
        tyConBoxed = boxed,
        tyConTyVars = tyvars,
 -      dataCon = con,
 -      hasGenerics = gen_info
 +      dataCon = con
      }
  
  -- ^ Foreign-imported (.NET) type constructors are represented
@@@ -871,17 -892,6 +883,6 @@@ mkSynTyCon name kind tyvars rhs paren
          synTcParent = parent
      }
  
- -- | Create a coercion 'TyCon'
- mkCoercionTyCon :: Name -> Arity 
-                 -> CoTyConDesc
-                 -> TyCon
- mkCoercionTyCon name arity desc
-   = CoTyCon {
-         tyConName   = name,
-         tyConUnique = nameUnique name,
-         tyConArity  = arity,
-         coTcDesc    = desc }
  mkAnyTyCon :: Name -> Kind -> TyCon
  mkAnyTyCon name kind 
    = AnyTyCon {  tyConName = name,
@@@ -959,11 -969,11 +960,11 @@@ isNewTyCon 
  -- | Take a 'TyCon' apart into the 'TyVar's it scopes over, the 'Type' it expands
  -- into, and (possibly) a coercion from the representation type to the @newtype@.
  -- Returns @Nothing@ if this is not possible.
- unwrapNewTyCon_maybe :: TyCon -> Maybe ([TyVar], Type, Maybe TyCon)
+ unwrapNewTyCon_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom)
  unwrapNewTyCon_maybe (AlgTyCon { tyConTyVars = tvs, 
-                                algTcRhs = NewTyCon { nt_co = mb_co, 
+                                algTcRhs = NewTyCon { nt_co = co, 
                                                       nt_rhs = rhs }})
-                          = Just (tvs, rhs, mb_co)
+                          = Just (tvs, rhs, co)
  unwrapNewTyCon_maybe _     = Nothing
  
  isProductTyCon :: TyCon -> Bool
@@@ -995,9 -1005,8 +996,8 @@@ isSynTyCon _               = Fals
  
  isDecomposableTyCon :: TyCon -> Bool
  -- True iff we can decompose (T a b c) into ((T a b) c)
- -- Specifically NOT true of synonyms (open and otherwise) and coercions
+ -- Specifically NOT true of synonyms (open and otherwise)
  isDecomposableTyCon (SynTyCon {}) = False
- isDecomposableTyCon (CoTyCon {})  = False
  isDecomposableTyCon _other        = True
  
  -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
@@@ -1039,7 -1048,7 +1039,7 @@@ isInjectiveTyCon tc = not (isSynTyCon t
        -- Ultimately we may have injective associated types
          -- in which case this test will become more interesting
        --
-       -- It'd be unusual to call isInjectiveTyCon on a regular H98
+         -- It'd be unusual to call isInjectiveTyCon on a regular H98
        -- type synonym, because you should probably have expanded it first
        -- But regardless, it's not injective!
  
@@@ -1078,11 -1087,6 +1078,11 @@@ isBoxedTupleTyCon 
  tupleTyConBoxity :: TyCon -> Boxity
  tupleTyConBoxity tc = tyConBoxed tc
  
 +-- | Extract the arity of the given 'TyCon', if it is a 'TupleTyCon'.
 +-- Panics otherwise
 +tupleTyConArity :: TyCon -> Arity
 +tupleTyConArity tc = tyConArity tc
 +
  -- | Is this a recursive 'TyCon'?
  isRecursiveTyCon :: TyCon -> Bool
  isRecursiveTyCon (AlgTyCon {algTcRec = Recursive}) = True
@@@ -1109,19 -1113,6 +1109,6 @@@ isAnyTyCon :: TyCon -> Boo
  isAnyTyCon (AnyTyCon {}) = True
  isAnyTyCon _              = False
  
- -- | Attempt to pull a 'TyCon' apart into the arity and 'coKindFun' of
- -- a coercion 'TyCon'. Returns @Nothing@ if the 'TyCon' is not of the
- -- appropriate kind
- isCoercionTyCon_maybe :: TyCon -> Maybe (Arity, CoTyConDesc)
- isCoercionTyCon_maybe (CoTyCon {tyConArity = ar, coTcDesc = desc}) 
-   = Just (ar, desc)
- isCoercionTyCon_maybe _ = Nothing
- -- | Is this a 'TyCon' that represents a coercion?
- isCoercionTyCon :: TyCon -> Bool
- isCoercionTyCon (CoTyCon {}) = True
- isCoercionTyCon _            = False
  -- | Identifies implicit tycons that, in particular, do not go into interface
  -- files (because they are implicitly reconstructed when the interface is
  -- read).
@@@ -1151,14 -1142,15 +1138,15 @@@ isImplicitTyCon _othe
  \begin{code}
  tcExpandTyCon_maybe, coreExpandTyCon_maybe 
        :: TyCon 
-       -> [Type]                       -- ^ Arguments to 'TyCon'
-       -> Maybe ([(TyVar,Type)],       
+       -> [tyco]                 -- ^ Arguments to 'TyCon'
+       -> Maybe ([(TyVar,tyco)],       
                  Type,                 
-                 [Type])               -- ^ Returns a 'TyVar' substitution, the body type
-                                         -- of the synonym (not yet substituted) and any arguments
-                                         -- remaining from the application
+                 [tyco])         -- ^ Returns a 'TyVar' substitution, the body type
+                                   -- of the synonym (not yet substituted) and any arguments
+                                   -- remaining from the application
  
- -- ^ Used to create the view the /typechecker/ has on 'TyCon's. We expand (closed) synonyms only, cf. 'coreExpandTyCon_maybe'
+ -- ^ Used to create the view the /typechecker/ has on 'TyCon's. 
+ -- We expand (closed) synonyms only, cf. 'coreExpandTyCon_maybe'
  tcExpandTyCon_maybe (SynTyCon {tyConTyVars = tvs, 
                               synTcRhs = SynonymTyCon rhs }) tys
     = expand tvs rhs tys
@@@ -1166,31 -1158,31 +1154,26 @@@ tcExpandTyCon_maybe _ _ = Nothin
  
  ---------------
  
- -- ^ Used to create the view /Core/ has on 'TyCon's. We expand not only closed synonyms like 'tcExpandTyCon_maybe',
+ -- ^ Used to create the view /Core/ has on 'TyCon's. We expand 
+ -- not only closed synonyms like 'tcExpandTyCon_maybe',
  -- but also non-recursive @newtype@s
- coreExpandTyCon_maybe (AlgTyCon {
-          algTcRhs = NewTyCon { nt_etad_rhs = etad_rhs, nt_co = Nothing }}) tys
-    = case etad_rhs of -- Don't do this in the pattern match, lest we accidentally
-                       -- match the etad_rhs of a *recursive* newtype
-       (tvs,rhs) -> expand tvs rhs tys
  coreExpandTyCon_maybe tycon tys = tcExpandTyCon_maybe tycon tys
  
  
  ----------------
- expand        :: [TyVar] -> Type                      -- Template
-       -> [Type]                               -- Args
-       -> Maybe ([(TyVar,Type)], Type, [Type]) -- Expansion
+ expand        :: [TyVar] -> Type                 -- Template
+       -> [a]                             -- Args
+       -> Maybe ([(TyVar,a)], Type, [a])  -- Expansion
  expand tvs rhs tys
    = case n_tvs `compare` length tys of
        LT -> Just (tvs `zip` tys, rhs, drop n_tvs tys)
        EQ -> Just (tvs `zip` tys, rhs, [])
-       GT -> Nothing
+         GT -> Nothing
     where
       n_tvs = length tvs
  \end{code}
  
  \begin{code}
 --- | Does this 'TyCon' have any generic to\/from functions available? See also 'hasGenerics'
 -tyConHasGenerics :: TyCon -> Bool
 -tyConHasGenerics (AlgTyCon {hasGenerics = hg})   = hg
 -tyConHasGenerics (TupleTyCon {hasGenerics = hg}) = hg
 -tyConHasGenerics _                               = False        -- Synonyms
  
  tyConKind :: TyCon -> Kind
  tyConKind (FunTyCon   { tc_kind = k }) = k
@@@ -1203,7 -1195,6 +1186,6 @@@ tyConKind tc = pprPanic "tyConKind" (pp
  
  tyConHasKind :: TyCon -> Bool
  tyConHasKind (SuperKindTyCon {}) = False
- tyConHasKind (CoTyCon {})        = False
  tyConHasKind _                   = True
  
  -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no constructors
@@@ -1256,9 -1247,14 +1238,14 @@@ newTyConEtadRhs tycon = pprPanic "newTy
  -- | Extracts the @newtype@ coercion from such a 'TyCon', which can be used to construct something
  -- with the @newtype@s type from its representation type (right hand side). If the supplied 'TyCon'
  -- is not a @newtype@, returns @Nothing@
- newTyConCo_maybe :: TyCon -> Maybe TyCon
- newTyConCo_maybe (AlgTyCon {algTcRhs = NewTyCon { nt_co = co }}) = co
- newTyConCo_maybe _                                             = Nothing
+ newTyConCo_maybe :: TyCon -> Maybe CoAxiom
+ newTyConCo_maybe (AlgTyCon {algTcRhs = NewTyCon { nt_co = co }}) = Just co
+ newTyConCo_maybe _                                             = Nothing
+ newTyConCo :: TyCon -> CoAxiom
+ newTyConCo tc = case newTyConCo_maybe tc of
+                Just co -> co
+                  Nothing -> pprPanic "newTyConCo" (ppr tc)
  
  -- | Find the primitive representation of a 'TyCon'
  tyConPrimRep :: TyCon -> PrimRep
@@@ -1328,6 -1324,7 +1315,7 @@@ tyConParent (AlgTyCon {algTcParent = pa
  tyConParent (SynTyCon {synTcParent = parent}) = parent
  tyConParent _                                 = NoParentTyCon
  
+ ----------------------------------------------------------------------------
  -- | Is this 'TyCon' that for a family instance, be that for a synonym or an
  -- algebraic family instance?
  isFamInstTyCon :: TyCon -> Bool
@@@ -1335,7 -1332,7 +1323,7 @@@ isFamInstTyCon tc = case tyConParent t
                        FamInstTyCon {} -> True
                        _               -> False
  
- tyConFamInstSig_maybe :: TyCon -> Maybe (TyCon, [Type], TyCon)
+ tyConFamInstSig_maybe :: TyCon -> Maybe (TyCon, [Type], CoAxiom)
  tyConFamInstSig_maybe tc
    = case tyConParent tc of
        FamInstTyCon f ts co_tc -> Just (f, ts, co_tc)
@@@ -1352,7 -1349,7 +1340,7 @@@ tyConFamInst_maybe t
  -- | If this 'TyCon' is that of a family instance, return a 'TyCon' which represents 
  -- a coercion identifying the representation type with the type instance family.
  -- Otherwise, return @Nothing@
- tyConFamilyCoercion_maybe :: TyCon -> Maybe TyCon
+ tyConFamilyCoercion_maybe :: TyCon -> Maybe CoAxiom
  tyConFamilyCoercion_maybe tc
    = case tyConParent tc of
        FamInstTyCon _ _ co -> Just co
@@@ -1386,18 -1383,6 +1374,6 @@@ instance Ord TyCon wher
  instance Uniquable TyCon where
      getUnique tc = tyConUnique tc
  
- instance Outputable CoTyConDesc where
-     ppr CoSym    = ptext (sLit "SYM")
-     ppr CoTrans  = ptext (sLit "TRANS")
-     ppr CoLeft   = ptext (sLit "LEFT")
-     ppr CoRight  = ptext (sLit "RIGHT")
-     ppr CoCsel1  = ptext (sLit "CSEL1")
-     ppr CoCsel2  = ptext (sLit "CSEL2")
-     ppr CoCselR  = ptext (sLit "CSELR")
-     ppr CoInst   = ptext (sLit "INST")
-     ppr CoUnsafe = ptext (sLit "UNSAFE")
-     ppr (CoAxiom {}) = ptext (sLit "AXIOM")
  instance Outputable TyCon where
      ppr tc  = ppr (getName tc) 
  
@@@ -1412,4 -1397,34 +1388,34 @@@ instance Data.Data TyCon wher
      toConstr _   = abstractConstr "TyCon"
      gunfold _ _  = error "gunfold"
      dataTypeOf _ = mkNoRepType "TyCon"
+ -------------------
+ instance Eq CoAxiom where
+     a == b = case (a `compare` b) of { EQ -> True;   _ -> False }
+     a /= b = case (a `compare` b) of { EQ -> False;  _ -> True  }
+   
+ instance Ord CoAxiom where
+     a <= b = case (a `compare` b) of { LT -> True;  EQ -> True;  GT -> False }
+     a <  b = case (a `compare` b) of { LT -> True;  EQ -> False; GT -> False }
+     a >= b = case (a `compare` b) of { LT -> False; EQ -> True;  GT -> True  }
+     a >  b = case (a `compare` b) of { LT -> False; EQ -> False; GT -> True  }
+     compare a b = getUnique a `compare` getUnique b  
+ instance Uniquable CoAxiom where
+     getUnique = co_ax_unique
+ instance Outputable CoAxiom where
+     ppr = ppr . getName
+ instance NamedThing CoAxiom where
+     getName = co_ax_name
+ instance Data.Typeable CoAxiom where
+     typeOf _ = Data.mkTyConApp (Data.mkTyCon "CoAxiom") []
+ instance Data.Data CoAxiom where
+     -- don't traverse?
+     toConstr _   = abstractConstr "CoAxiom"
+     gunfold _ _  = error "gunfold"
+     dataTypeOf _ = mkNoRepType "CoAxiom"
  \end{code}
diff --combined compiler/types/Type.lhs
@@@ -20,7 -20,8 +20,8 @@@ module Type 
        -- $type_classification
        
          -- $representation_types
-       TyThing(..), Type, PredType(..), ThetaType,
+         TyThing(..), Type, Pred(..), PredType, ThetaType,
+         Var, TyVar, isTyVar, 
  
          -- ** Constructing and deconstructing types
          mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe,
        -- (Type families)
          tyFamInsts, predFamInsts,
  
-         -- (Source types)
-         mkPredTy, mkPredTys, mkFamilyTyConApp, isEqPred, coVarPred,
+         -- Pred types
+         mkPredTy, mkPredTys, mkFamilyTyConApp,
+       mkDictTy, isDictLikeTy, isClassPred,
+         isEqPred, allPred, mkEqPred, 
+       mkClassPred, getClassPredTys, getClassPredTys_maybe,
+       isTyVarClassPred, 
+       mkIPPred, isIPPred,
  
        -- ** Common type constructors
          funTyCon,
  
          -- ** Predicates on types
-         isTyVarTy, isFunTy, isDictTy,
+         isTyVarTy, isFunTy, isPredTy,
+       isDictTy, isEqPredTy, isReflPredTy, splitPredTy_maybe, splitEqPredTy_maybe, 
  
        -- (Lifting and boxity)
        isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
@@@ -65,8 -72,7 +72,7 @@@
          -- ** Common Kinds and SuperKinds
          liftedTypeKind, unliftedTypeKind, openTypeKind,
          argTypeKind, ubxTupleKind,
-         tySuperKind, coSuperKind, 
+         tySuperKind, 
  
          -- ** Common Kind type constructors
          liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
  
        -- * Type free variables
        tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-       expandTypeSynonyms, 
+       exactTyVarsOfType, exactTyVarsOfTypes, expandTypeSynonyms, 
        typeSize,
  
        -- * Type comparison
-       coreEqType, coreEqType2,
-         tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
-       tcEqPred, tcEqPredX, tcCmpPred, tcEqTypeX, tcPartOfType, tcPartOfPred,
+         eqType, eqTypeX, eqTypes, cmpType, cmpTypes, 
+       eqPred, eqPredX, cmpPred, eqKind,
  
        -- * Forcing evaluation of types
-       seqType, seqTypes,
+         seqType, seqTypes, seqPred,
  
          -- * Other views onto Types
-         coreView, tcView, kindView,
+         coreView, tcView, 
  
          repType, 
  
        emptyTvSubstEnv, emptyTvSubst,
        
        mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
-       getTvSubstEnv, setTvSubstEnv, zapTvSubstEnv, getTvInScope, 
+         getTvSubstEnv, setTvSubstEnv,
+         zapTvSubstEnv, getTvInScope,
          extendTvInScope, extendTvInScopeList,
-       extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
+       extendTvSubst, extendTvSubstList,
+         isInScope, composeTvSubst, zipTyEnv,
          isEmptyTvSubst, unionTvSubst,
  
        -- ** Performing substitution on types
        substTy, substTys, substTyWith, substTysWith, substTheta, 
-       substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar,
+         substPred, substTyVar, substTyVars, substTyVarBndr,
+         deShadowTy, lookupTyVar, 
  
        -- * Pretty-printing
        pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
-       pprPred, pprEqPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind,
+       pprPred, pprPredTy, pprEqPred, pprTheta, pprThetaArrowTy, pprClassPred, 
+         pprKind, pprParendKind,
        
        pprSourceTyCon
      ) where
@@@ -133,8 -142,11 +142,11 @@@ import VarSe
  
  import Class
  import TyCon
+ import TysPrim
  
  -- others
+ import BasicTypes     ( IPName )
+ import Name           ( Name )
  import StaticFlags
  import Util
  import Outputable
@@@ -219,31 -231,9 +231,9 @@@ coreView :: Type -> Maybe Typ
  -- its underlying representation type. 
  -- Returns Nothing if there is nothing to look through.
  --
- -- In the case of @newtype@s, it returns one of:
- --
- -- 1) A vanilla 'TyConApp' (recursive newtype, or non-saturated)
- -- 
- -- 2) The newtype representation (otherwise), meaning the
- --    type written in the RHS of the newtype declaration,
- --    which may itself be a newtype
- --
- -- For example, with:
- --
- -- > newtype R = MkR S
- -- > newtype S = MkS T
- -- > newtype T = MkT (T -> T)
- --
- -- 'expandNewTcApp' on:
- --
- --  * @R@ gives @Just S@
- --  * @S@ gives @Just T@
- --  * @T@ gives @Nothing@ (no expansion)
  -- By being non-recursive and inlined, this case analysis gets efficiently
  -- joined onto the case analysis that the caller is already doing
- coreView (PredTy p)
-   | isEqPred p             = Nothing
-   | otherwise            = Just (predTypeRep p)
+ coreView (PredTy p)        = Just (predTypeRep p)
  coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
                           = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
                                -- Its important to use mkAppTys, rather than (foldl AppTy),
  coreView _                 = Nothing
  
  
  -----------------------------------------------
  {-# INLINE tcView #-}
  tcView :: Type -> Maybe Type
@@@ -283,14 -272,6 +272,6 @@@ expandTypeSynonyms t
      go_pred (ClassP c ts)  = ClassP c (map go ts)
      go_pred (IParam ip t)  = IParam ip (go t)
      go_pred (EqPred t1 t2) = EqPred (go t1) (go t2)
- -----------------------------------------------
- {-# INLINE kindView #-}
- kindView :: Kind -> Maybe Kind
- -- ^ Similar to 'coreView' or 'tcView', but works on 'Kind's
- -- For the moment, we don't even handle synonyms in kinds
- kindView _            = Nothing
  \end{code}
  
  
                                TyVarTy
                                ~~~~~~~
  \begin{code}
- mkTyVarTy  :: TyVar   -> Type
- mkTyVarTy  = TyVarTy
- mkTyVarTys :: [TyVar] -> [Type]
- mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
  -- | Attempts to obtain the type variable underlying a 'Type', and panics with the
  -- given message if this is not a type variable type. See also 'getTyVar_maybe'
  getTyVar :: String -> Type -> TyVar
@@@ -384,10 -359,9 +359,9 @@@ repSplitAppTy_maybe :: Type -> Maybe (T
  repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
  repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
  repSplitAppTy_maybe (TyConApp tc tys) 
-   | isDecomposableTyCon tc || length tys > tyConArity tc 
-   = case snocView tys of       -- never create unsaturated type family apps
-       Just (tys', ty') -> Just (TyConApp tc tys', ty')
-       Nothing        -> Nothing
+   | isDecomposableTyCon tc || tys `lengthExceeds` tyConArity tc 
+   , Just (tys', ty') <- snocView tys
+   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
  repSplitAppTy_maybe _other = Nothing
  -------------
  splitAppTy :: Type -> (Type, Type)
@@@ -427,8 -401,7 +401,7 @@@ splitAppTys ty = split ty ty [
  \begin{code}
  mkFunTy :: Type -> Type -> Type
  -- ^ Creates a function type from the given argument and result type
- mkFunTy arg@(PredTy (EqPred {})) res = ForAllTy (mkWildCoVar arg) res
- mkFunTy arg                      res = FunTy    arg               res
+ mkFunTy arg res = FunTy arg res
  
  mkFunTys :: [Type] -> Type -> Type
  mkFunTys tys ty = foldr mkFunTy ty tys
@@@ -496,20 -469,6 +469,6 @@@ funArgTy ty                = pprPanic "
                                ~~~~~~~~
  
  \begin{code}
- -- | A key function: builds a 'TyConApp' or 'FunTy' as apppropriate to its arguments.
- -- Applies its arguments to the constructor from left to right
- mkTyConApp :: TyCon -> [Type] -> Type
- mkTyConApp tycon tys
-   | isFunTyCon tycon, [ty1,ty2] <- tys
-   = FunTy ty1 ty2
-   | otherwise
-   = TyConApp tycon tys
- -- | Create the plain type constructor type which has been applied to no type arguments at all.
- mkTyConTy :: TyCon -> Type
- mkTyConTy tycon = mkTyConApp tycon []
  -- splitTyConApp "looks through" synonyms, because they don't
  -- mean a distinct type, but all other type-constructor applications
  -- including functions are returned as Just ..
@@@ -612,13 -571,16 +571,16 @@@ repType t
    = go [] ty
    where
      go :: [TyCon] -> Type -> Type
-     go rec_nts ty | Just ty' <- coreView ty   -- Expand synonyms
-       = go rec_nts ty'        
-     go rec_nts (ForAllTy _ ty)                        -- Look through foralls
+     go rec_nts (ForAllTy _ ty)                -- Look through foralls
        = go rec_nts ty
  
-     go rec_nts (TyConApp tc tys)              -- Expand newtypes
+     go rec_nts (PredTy p)             -- Expand predicates
+         = go rec_nts (predTypeRep p)
+     go rec_nts (TyConApp tc tys)      -- Expand newtypes and synonyms
+       | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
+       = go rec_nts (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
        | Just (rec_nts', ty') <- carefullySplitNewType_maybe rec_nts tc tys
        = go rec_nts' ty'
  
@@@ -756,13 -718,32 +718,32 @@@ applyTysD doc orig_fun_ty arg_ty
  
  %************************************************************************
  %*                                                                    *
- \subsection{Source types}
+                          Pred
  %*                                                                    *
  %************************************************************************
  
- Source types are always lifted.
+ Polymorphic functions over Pred
  
- The key function is predTypeRep which gives the representation of a source type:
+ \begin{code}
+ allPred :: (a -> Bool) -> Pred a -> Bool
+ allPred p (ClassP _ ts)  = all p ts
+ allPred p (IParam _ t)   = p t
+ allPred p (EqPred t1 t2) = p t1 && p t2
+ isClassPred :: Pred a -> Bool
+ isClassPred (ClassP {}) = True
+ isClassPred _            = False
+ isEqPred :: Pred a -> Bool
+ isEqPred (EqPred {}) = True
+ isEqPred _           = False
+ isIPPred :: Pred a -> Bool
+ isIPPred (IParam {}) = True
+ isIPPred _           = False
+ \end{code}
+ Make PredTypes
  
  \begin{code}
  mkPredTy :: PredType -> Type
@@@ -771,91 -752,115 +752,115 @@@ mkPredTy pred = PredTy pre
  mkPredTys :: ThetaType -> [Type]
  mkPredTys preds = map PredTy preds
  
- isEqPred :: PredType -> Bool
- isEqPred (EqPred _ _) = True
- isEqPred _            = False
  predTypeRep :: PredType -> Type
  -- ^ Convert a 'PredType' to its representation type. However, it unwraps 
  -- only the outermost level; for example, the result might be a newtype application
  predTypeRep (IParam _ ty)     = ty
  predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
-       -- Result might be a newtype application, but the consumer will
-       -- look through that too if necessary
- predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
+ predTypeRep (EqPred ty1 ty2)  = mkTyConApp eqPredPrimTyCon [ty1,ty2]
  
- mkFamilyTyConApp :: TyCon -> [Type] -> Type
- -- ^ Given a family instance TyCon and its arg types, return the
- -- corresponding family type.  E.g:
- --
- -- > data family T a
- -- > data instance T (Maybe b) = MkT b
- --
- -- Where the instance tycon is :RTL, so:
- --
- -- > mkFamilyTyConApp :RTL Int  =  T (Maybe Int)
- mkFamilyTyConApp tc tys
-   | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
-   , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
-   = mkTyConApp fam_tc (substTys fam_subst fam_tys)
-   | otherwise
-   = mkTyConApp tc tys
+ splitPredTy_maybe :: Type -> Maybe PredType
+ -- Returns Just for predicates only
+ splitPredTy_maybe ty | Just ty' <- tcView ty = splitPredTy_maybe ty'
+ splitPredTy_maybe (PredTy p)    = Just p
+ splitPredTy_maybe _             = Nothing
  
- -- | Pretty prints a 'TyCon', using the family instance in case of a
- -- representation tycon.  For example:
- --
- -- > data T [a] = ...
- --
- -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
- pprSourceTyCon :: TyCon -> SDoc
- pprSourceTyCon tycon 
-   | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
-   = ppr $ fam_tc `TyConApp` tys              -- can't be FunTyCon
-   | otherwise
-   = ppr tycon
- isDictTy :: Type -> Bool
- isDictTy ty = case splitTyConApp_maybe ty of
-                 Just (tc, _) -> isClassTyCon tc
-               Nothing      -> False
+ isPredTy :: Type -> Bool
+ isPredTy ty = isJust (splitPredTy_maybe ty)
  \end{code}
  
+ --------------------- Equality types ---------------------------------
+ \begin{code}
+ isReflPredTy :: Type -> Bool
+ isReflPredTy ty = case splitPredTy_maybe ty of
+                     Just (EqPred ty1 ty2) -> ty1 `eqType` ty2
+                     _                     -> False
+ splitEqPredTy_maybe :: Type -> Maybe (Type,Type)
+ splitEqPredTy_maybe ty = case splitPredTy_maybe ty of
+                             Just (EqPred ty1 ty2) -> Just (ty1,ty2)
+                             _                     -> Nothing
+ isEqPredTy :: Type -> Bool
+ isEqPredTy ty = case splitPredTy_maybe ty of
+                   Just (EqPred {}) -> True
+                 _                -> False
+ -- | Creates a type equality predicate
+ mkEqPred :: (a, a) -> Pred a
+ mkEqPred (ty1, ty2) = EqPred ty1 ty2
+ \end{code}
  
- %************************************************************************
- %*                                                                    *
-            The free variables of a type
- %*                                                                    *
- %************************************************************************
+ --------------------- Dictionary types ---------------------------------
  \begin{code}
- tyVarsOfType :: Type -> TyVarSet
- -- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym
- tyVarsOfType (TyVarTy tv)     = unitVarSet tv
- tyVarsOfType (TyConApp _ tys) = tyVarsOfTypes tys
- tyVarsOfType (PredTy sty)     = tyVarsOfPred sty
- tyVarsOfType (FunTy arg res)  = tyVarsOfType arg `unionVarSet` tyVarsOfType res
- tyVarsOfType (AppTy fun arg)  = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
- tyVarsOfType (ForAllTy tv ty) -- The kind of a coercion binder 
-                             -- can mention type variables!
-   | isTyVar tv                      = inner_tvs `delVarSet` tv
-   | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
-                                 inner_tvs `unionVarSet` tyVarsOfType (tyVarKind tv)
-   where
-     inner_tvs = tyVarsOfType ty
+ mkClassPred :: Class -> [Type] -> PredType
+ mkClassPred clas tys = ClassP clas tys
  
- tyVarsOfTypes :: [Type] -> TyVarSet
- tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
+ isDictTy :: Type -> Bool
+ isDictTy ty = case splitPredTy_maybe ty of
+                 Just p  -> isClassPred p
+               Nothing -> False
+ isTyVarClassPred :: PredType -> Bool
+ isTyVarClassPred (ClassP _ tys) = all isTyVarTy tys
+ isTyVarClassPred _              = False
+ getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
+ getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
+ getClassPredTys_maybe _                 = Nothing
+ getClassPredTys :: PredType -> (Class, [Type])
+ getClassPredTys (ClassP clas tys) = (clas, tys)
+ getClassPredTys _ = panic "getClassPredTys"
+ mkDictTy :: Class -> [Type] -> Type
+ mkDictTy clas tys = mkPredTy (ClassP clas tys)
+ isDictLikeTy :: Type -> Bool
+ -- Note [Dictionary-like types]
+ isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty'
+ isDictLikeTy (PredTy p) = isClassPred p
+ isDictLikeTy (TyConApp tc tys) 
+   | isTupleTyCon tc     = all isDictLikeTy tys
+ isDictLikeTy _          = False
+ \end{code}
  
- tyVarsOfPred :: PredType -> TyVarSet
- tyVarsOfPred (IParam _ ty)    = tyVarsOfType ty
- tyVarsOfPred (ClassP _ tys)   = tyVarsOfTypes tys
- tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+ Note [Dictionary-like types]
+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ Being "dictionary-like" means either a dictionary type or a tuple thereof.
+ In GHC 6.10 we build implication constraints which construct such tuples,
+ and if we land up with a binding
+     t :: (C [a], Eq [a])
+     t = blah
+ then we want to treat t as cheap under "-fdicts-cheap" for example.
+ (Implication constraints are normally inlined, but sadly not if the
+ occurrence is itself inside an INLINE function!  Until we revise the 
+ handling of implication constraints, that is.)  This turned out to
+ be important in getting good arities in DPH code.  Example:
+     class C a
+     class D a where { foo :: a -> a }
+     instance C a => D (Maybe a) where { foo x = x }
+     bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
+     {-# INLINE bar #-}
+     bar x y = (foo (Just x), foo (Just y))
+ Then 'bar' should jolly well have arity 4 (two dicts, two args), but
+ we ended up with something like
+    bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
+                                 in \x,y. <blah>)
+ This is all a bit ad-hoc; eg it relies on knowing that implication
+ constraints build tuples.
+ --------------------- Implicit parameters ---------------------------------
  
- tyVarsOfTheta :: ThetaType -> TyVarSet
- tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
+ \begin{code}
+ mkIPPred :: IPName Name -> Type -> PredType
+ mkIPPred ip ty = IParam ip ty
  \end{code}
  
  %************************************************************************
  %*                                                                    *
                     Size                                                                       
@@@ -867,14 -872,9 +872,9 @@@ typeSize :: Type -> In
  typeSize (TyVarTy _)     = 1
  typeSize (AppTy t1 t2)   = typeSize t1 + typeSize t2
  typeSize (FunTy t1 t2)   = typeSize t1 + typeSize t2
- typeSize (PredTy p)      = predSize p
+ typeSize (PredTy p)      = predSize typeSize p
  typeSize (ForAllTy _ t)  = 1 + typeSize t
  typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
- predSize :: PredType -> Int
- predSize (IParam _ t)   = 1 + typeSize t
- predSize (ClassP _ ts)  = 1 + sum (map typeSize ts)
- predSize (EqPred t1 t2) = typeSize t1 + typeSize t2
  \end{code}
  
  
@@@ -904,8 -904,37 +904,37 @@@ predFamInsts :: PredType -> [(TyCon, [T
  predFamInsts (ClassP _cla tys) = concat (map tyFamInsts tys)
  predFamInsts (IParam _ ty)     = tyFamInsts ty
  predFamInsts (EqPred ty1 ty2)  = tyFamInsts ty1 ++ tyFamInsts ty2
- \end{code}
  
+ mkFamilyTyConApp :: TyCon -> [Type] -> Type
+ -- ^ Given a family instance TyCon and its arg types, return the
+ -- corresponding family type.  E.g:
+ --
+ -- > data family T a
+ -- > data instance T (Maybe b) = MkT b
+ --
+ -- Where the instance tycon is :RTL, so:
+ --
+ -- > mkFamilyTyConApp :RTL Int  =  T (Maybe Int)
+ mkFamilyTyConApp tc tys
+   | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
+   , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
+   = mkTyConApp fam_tc (substTys fam_subst fam_tys)
+   | otherwise
+   = mkTyConApp tc tys
+ -- | Pretty prints a 'TyCon', using the family instance in case of a
+ -- representation tycon.  For example:
+ --
+ -- > data T [a] = ...
+ --
+ -- In that case we want to print @T [a]@, where @T@ is the family 'TyCon'
+ pprSourceTyCon :: TyCon -> SDoc
+ pprSourceTyCon tycon 
+   | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
+   = ppr $ fam_tc `TyConApp` tys              -- can't be FunTyCon
+   | otherwise
+   = ppr tycon
+ \end{code}
  
  %************************************************************************
  %*                                                                    *
@@@ -924,6 -953,7 +953,7 @@@ isUnLiftedType :: Type -> Boo
  
  isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
  isUnLiftedType (ForAllTy _ ty)   = isUnLiftedType ty
+ isUnLiftedType (PredTy p)        = isEqPred p
  isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
  isUnLiftedType _                 = False
  
@@@ -949,9 -979,9 +979,9 @@@ isAlgType t
  isClosedAlgType :: Type -> Bool
  isClosedAlgType ty
    = case splitTyConApp_maybe ty of
 -      Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 -                          isAlgTyCon tc && not (isFamilyTyCon tc)
 -      _other           -> False
 +      Just (tc, ty_args) | isAlgTyCon tc && not (isFamilyTyCon tc)
 +             -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
 +      _other -> False
  \end{code}
  
  \begin{code}
@@@ -977,7 -1007,8 +1007,8 @@@ isStrictType _                 = Fals
  --  poking the dictionary component, which is wrong.)
  isStrictPred :: PredType -> Bool
  isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
- isStrictPred _               = False
+ isStrictPred (EqPred {})     = True
+ isStrictPred (IParam {})     = False
  \end{code}
  
  \begin{code}
@@@ -994,6 -1025,64 +1025,64 @@@ isPrimitiveType ty = case splitTyConApp
  
  %************************************************************************
  %*                                                                    *
+           The "exact" free variables of a type
+ %*                                                                    *
+ %************************************************************************
+ Note [Silly type synonym]
+ ~~~~~~~~~~~~~~~~~~~~~~~~~
+ Consider
+       type T a = Int
+ What are the free tyvars of (T x)?  Empty, of course!  
+ Here's the example that Ralf Laemmel showed me:
+       foo :: (forall a. C u a -> C u a) -> u
+       mappend :: Monoid u => u -> u -> u
+       bar :: Monoid u => u
+       bar = foo (\t -> t `mappend` t)
+ We have to generalise at the arg to f, and we don't
+ want to capture the constraint (Monad (C u a)) because
+ it appears to mention a.  Pretty silly, but it was useful to him.
+ exactTyVarsOfType is used by the type checker to figure out exactly
+ which type variables are mentioned in a type.  It's also used in the
+ smart-app checking code --- see TcExpr.tcIdApp
+ On the other hand, consider a *top-level* definition
+       f = (\x -> x) :: T a -> T a
+ If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
+ if we have an application like (f "x") we get a confusing error message 
+ involving Any.  So the conclusion is this: when generalising
+   - at top level use tyVarsOfType
+   - in nested bindings use exactTyVarsOfType
+ See Trac #1813 for example.
+ \begin{code}
+ exactTyVarsOfType :: Type -> TyVarSet
+ -- Find the free type variables (of any kind)
+ -- but *expand* type synonyms.  See Note [Silly type synonym] above.
+ exactTyVarsOfType ty
+   = go ty
+   where
+     go ty | Just ty' <- tcView ty = go ty'    -- This is the key line
+     go (TyVarTy tv)         = unitVarSet tv
+     go (TyConApp _ tys)     = exactTyVarsOfTypes tys
+     go (PredTy ty)        = go_pred ty
+     go (FunTy arg res)            = go arg `unionVarSet` go res
+     go (AppTy fun arg)            = go fun `unionVarSet` go arg
+     go (ForAllTy tyvar ty)  = delVarSet (go ty) tyvar
+     go_pred (IParam _ ty)    = go ty
+     go_pred (ClassP _ tys)   = exactTyVarsOfTypes tys
+     go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
+ exactTyVarsOfTypes :: [Type] -> TyVarSet
+ exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
  \subsection{Sequencing on types}
  %*                                                                    *
  %************************************************************************
@@@ -1003,7 -1092,7 +1092,7 @@@ seqType :: Type -> (
  seqType (TyVarTy tv)    = tv `seq` ()
  seqType (AppTy t1 t2)           = seqType t1 `seq` seqType t2
  seqType (FunTy t1 t2)           = seqType t1 `seq` seqType t2
- seqType (PredTy p)      = seqPred p
+ seqType (PredTy p)        = seqPred seqType p
  seqType (TyConApp tc tys) = tc `seq` seqTypes tys
  seqType (ForAllTy tv ty)  = tv `seq` seqType ty
  
@@@ -1011,115 -1100,40 +1100,40 @@@ seqTypes :: [Type] -> (
  seqTypes []       = ()
  seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
  
- seqPred :: PredType -> ()
- seqPred (ClassP c tys)   = c `seq` seqTypes tys
- seqPred (IParam n ty)    = n `seq` seqType ty
- seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
+ seqPred :: (a -> ()) -> Pred a -> ()
+ seqPred seqt (ClassP c tys)   = c `seq` foldr (seq . seqt) () tys
+ seqPred seqt (IParam n ty)    = n `seq` seqt ty
+ seqPred seqt (EqPred ty1 ty2) = seqt ty1 `seq` seqt ty2
  \end{code}
  
  
  %************************************************************************
  %*                                                                    *
-               Equality for Core types 
+               Comparision for types 
        (We don't use instances so that we know where it happens)
  %*                                                                    *
  %************************************************************************
  
- Note that eqType works right even for partial applications of newtypes.
- See Note [Newtype eta] in TyCon.lhs
  \begin{code}
- -- | Type equality test for Core types (i.e. ignores predicate-types, synonyms etc.)
- coreEqType :: Type -> Type -> Bool
- coreEqType t1 t2 = coreEqType2 rn_env t1 t2
-   where
-     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
- coreEqType2 :: RnEnv2 -> Type -> Type -> Bool
- coreEqType2 rn_env t1 t2
-   = eq rn_env t1 t2
-   where
-     eq env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
-     eq env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
-     eq env (AppTy s1 t1)       (AppTy s2 t2)     = eq env s1 s2 && eq env t1 t2
-     eq env (FunTy s1 t1)       (FunTy s2 t2)     = eq env s1 s2 && eq env t1 t2
-     eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
-       | tc1 == tc2, all2 (eq env) tys1 tys2 = True
-                       -- The lengths should be equal because
-                       -- the two types have the same kind
-       -- NB: if the type constructors differ that does not 
-       --     necessarily mean that the types aren't equal
-       --     (synonyms, newtypes)
-       -- Even if the type constructors are the same, but the arguments
-       -- differ, the two types could be the same (e.g. if the arg is just
-       -- ignored in the RHS).  In both these cases we fall through to an 
-       -- attempt to expand one side or the other.
-       -- Now deal with newtypes, synonyms, pred-tys
-     eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2 
-                | Just t2' <- coreView t2 = eq env t1 t2' 
-       -- Fall through case; not equal!
-     eq _ _ _ = False
- \end{code}
+ eqKind :: Kind -> Kind -> Bool
+ eqKind = eqType
  
- %************************************************************************
- %*                                                                    *
-               Comparision for source types 
-       (We don't use instances so that we know where it happens)
- %*                                                                    *
- %************************************************************************
- \begin{code}
- tcEqType :: Type -> Type -> Bool
+ eqType :: Type -> Type -> Bool
  -- ^ Type equality on source types. Does not look through @newtypes@ or 
  -- 'PredType's, but it does look through type synonyms.
- tcEqType t1 t2 = isEqual $ cmpType t1 t2
- tcEqTypes :: [Type] -> [Type] -> Bool
- tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
- tcCmpType :: Type -> Type -> Ordering
- -- ^ Type ordering on source types. Does not look through @newtypes@ or 
- -- 'PredType's, but it does look through type synonyms.
- tcCmpType t1 t2 = cmpType t1 t2
+ eqType t1 t2 = isEqual $ cmpType t1 t2
  
- tcCmpTypes :: [Type] -> [Type] -> Ordering
- tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
+ eqTypeX :: RnEnv2 -> Type -> Type -> Bool
+ eqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
  
- tcEqPred :: PredType -> PredType -> Bool
- tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
+ eqTypes :: [Type] -> [Type] -> Bool
+ eqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
  
- tcEqPredX :: RnEnv2 -> PredType -> PredType -> Bool
- tcEqPredX env p1 p2 = isEqual $ cmpPredX env p1 p2
+ eqPred :: PredType -> PredType -> Bool
+ eqPred p1 p2 = isEqual $ cmpPred p1 p2
  
- tcCmpPred :: PredType -> PredType -> Ordering
- tcCmpPred p1 p2 = cmpPred p1 p2
- tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
- tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
- \end{code}
- \begin{code}
- -- | Checks whether the second argument is a subterm of the first.  (We don't care
- -- about binders, as we are only interested in syntactic subterms.)
- tcPartOfType :: Type -> Type -> Bool
- tcPartOfType t1              t2 
-   | tcEqType t1 t2              = True
- tcPartOfType t1              t2 
-   | Just t2' <- tcView t2       = tcPartOfType t1 t2'
- tcPartOfType _  (TyVarTy _)     = False
- tcPartOfType t1 (ForAllTy _ t2) = tcPartOfType t1 t2
- tcPartOfType t1 (AppTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
- tcPartOfType t1 (FunTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
- tcPartOfType t1 (PredTy p2)     = tcPartOfPred t1 p2
- tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts
- tcPartOfPred :: Type -> PredType -> Bool
- tcPartOfPred t1 (IParam _ t2)  = tcPartOfType t1 t2
- tcPartOfPred t1 (ClassP _ ts)  = any (tcPartOfType t1) ts
- tcPartOfPred t1 (EqPred s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
+ eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
+ eqPredX env p1 p2 = isEqual $ cmpPredX env p1 p2
  \end{code}
  
  Now here comes the real worker
@@@ -1141,8 -1155,13 +1155,13 @@@ cmpPred p1 p2 = cmpPredX rn_env p1 p
      rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
  
  cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering        -- Main workhorse
- cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
-                  | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
+ cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
+                  | Just t2' <- coreView t2 = cmpTypeX env t1 t2'
+ -- We expand predicate types, because in Core-land we have
+ -- lots of definitions like
+ --      fOrdBool :: Ord Bool
+ --      fOrdBool = D:Ord .. .. ..
+ -- So the RHS has a data type
  
  cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
  cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
@@@ -1199,8 -1218,8 +1218,8 @@@ PredTypes are used as a FM key in TcSim
  so we take the easy path and make them an instance of Ord
  
  \begin{code}
- instance Eq  PredType where { (==)    = tcEqPred }
- instance Ord PredType where { compare = tcCmpPred }
+ instance Eq  PredType where { (==)    = eqPred }
+ instance Ord PredType where { compare = cmpPred }
  \end{code}
  
  
  %************************************************************************
  
  \begin{code}
- -- | Type substitution
- --
- -- #tvsubst_invariant#
- -- The following invariants must hold of a 'TvSubst':
- -- 
- -- 1. The in-scope set is needed /only/ to
- -- guide the generation of fresh uniques
- --
- -- 2. In particular, the /kind/ of the type variables in 
- -- the in-scope set is not relevant
- --
- -- 3. The substition is only applied ONCE! This is because
- -- in general such application will not reached a fixed point.
- data TvSubst          
-   = TvSubst InScopeSet        -- The in-scope type variables
-           TvSubstEnv  -- The substitution itself
-       -- See Note [Apply Once]
-       -- and Note [Extending the TvSubstEnv]
- {- ----------------------------------------------------------
- Note [Apply Once]
- ~~~~~~~~~~~~~~~~~
- We use TvSubsts to instantiate things, and we might instantiate
-       forall a b. ty
- \with the types
-       [a, b], or [b, a].
- So the substition might go [a->b, b->a].  A similar situation arises in Core
- when we find a beta redex like
-       (/\ a /\ b -> e) b a
- Then we also end up with a substition that permutes type variables. Other
- variations happen to; for example [a -> (a, b)].  
-       ***************************************************
-       *** So a TvSubst must be applied precisely once ***
-       ***************************************************
- A TvSubst is not idempotent, but, unlike the non-idempotent substitution
- we use during unifications, it must not be repeatedly applied.
- Note [Extending the TvSubst]
- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- See #tvsubst_invariant# for the invariants that must hold.
- This invariant allows a short-cut when the TvSubstEnv is empty:
- if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
- then (substTy subst ty) does nothing.
- For example, consider:
-       (/\a. /\b:(a~Int). ...b..) Int
- We substitute Int for 'a'.  The Unique of 'b' does not change, but
- nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
- This invariant has several crucial consequences:
- * In substTyVarBndr, we need extend the TvSubstEnv 
-       - if the unique has changed
-       - or if the kind has changed
- * In substTyVar, we do not need to consult the in-scope set;
-   the TvSubstEnv is enough
- * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
-   
- -------------------------------------------------------------- -}
- -- | A substitition of 'Type's for 'TyVar's
- type TvSubstEnv = TyVarEnv Type
-       -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
-       -- invariant discussed in Note [Apply Once]), and also independently
-       -- in the middle of matching, and unification (see Types.Unify)
-       -- So you have to look at the context to know if it's idempotent or
-       -- apply-once or whatever
  emptyTvSubstEnv :: TvSubstEnv
  emptyTvSubstEnv = emptyVarEnv
  
@@@ -1303,11 -1247,11 +1247,11 @@@ composeTvSubst in_scope env1 env
      subst1 = TvSubst in_scope env1
  
  emptyTvSubst :: TvSubst
- emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
+ emptyTvSubst = TvSubst emptyInScopeSet emptyTvSubstEnv
  
  isEmptyTvSubst :: TvSubst -> Bool
         -- See Note [Extending the TvSubstEnv]
- isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
+ isEmptyTvSubst (TvSubst _ tenv) = isEmptyVarEnv tenv
  
  mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
  mkTvSubst = TvSubst
@@@ -1321,34 -1265,34 +1265,34 @@@ getTvInScope (TvSubst in_scope _) = in_
  isInScope :: Var -> TvSubst -> Bool
  isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
  
- notElemTvSubst :: TyVar -> TvSubst -> Bool
- notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
+ notElemTvSubst :: TyCoVar -> TvSubst -> Bool
+ notElemTvSubst v (TvSubst _ tenv) = not (v `elemVarEnv` tenv)
  
  setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
- setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
+ setTvSubstEnv (TvSubst in_scope _) tenv = TvSubst in_scope tenv
  
  zapTvSubstEnv :: TvSubst -> TvSubst
  zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv
  
  extendTvInScope :: TvSubst -> Var -> TvSubst
- extendTvInScope (TvSubst in_scope env) var = TvSubst (extendInScopeSet in_scope var) env
+ extendTvInScope (TvSubst in_scope tenv) var = TvSubst (extendInScopeSet in_scope var) tenv
  
  extendTvInScopeList :: TvSubst -> [Var] -> TvSubst
- extendTvInScopeList (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
+ extendTvInScopeList (TvSubst in_scope tenv) vars = TvSubst (extendInScopeSetList in_scope vars) tenv
  
  extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
- extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
+ extendTvSubst (TvSubst in_scope tenv) tv ty = TvSubst in_scope (extendVarEnv tenv tv ty)
  
  extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
- extendTvSubstList (TvSubst in_scope env) tvs tys 
-   = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
+ extendTvSubstList (TvSubst in_scope tenv) tvs tys 
+   = TvSubst in_scope (extendVarEnvList tenv (tvs `zip` tys))
  
  unionTvSubst :: TvSubst -> TvSubst -> TvSubst
  -- Works when the ranges are disjoint
- unionTvSubst (TvSubst in_scope1 env1) (TvSubst in_scope2 env2)
-   = ASSERT( not (env1 `intersectsVarEnv` env2) )
+ unionTvSubst (TvSubst in_scope1 tenv1) (TvSubst in_scope2 tenv2)
+   = ASSERT( not (tenv1 `intersectsVarEnv` tenv2) )
      TvSubst (in_scope1 `unionInScope` in_scope2)
-             (env1      `plusVarEnv`   env2)
+             (tenv1     `plusVarEnv`   tenv2)
  
  -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
  -- the types given; but it's just a thunk so with a bit of luck
  -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
  -- environment, hence "open"
  mkOpenTvSubst :: TvSubstEnv -> TvSubst
- mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
+ mkOpenTvSubst tenv = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts tenv))) tenv
  
  -- | Generates the in-scope set for the 'TvSubst' from the types in the incoming
  -- environment, hence "open"
@@@ -1396,7 -1340,7 +1340,7 @@@ zipTopTvSubst tyvars ty
  zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
  zipTyEnv tyvars tys
    | debugIsOn && (length tyvars /= length tys)
-   = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
+   = pprTrace "zipTyEnv" (ppr tyvars $$ ppr tys) emptyVarEnv
    | otherwise
    = zip_ty_env tyvars tys emptyVarEnv
  
@@@ -1421,10 -1365,10 +1365,10 @@@ zip_ty_env tvs      tys      env   = pp
  -- zip_ty_env _ _ env = env
  
  instance Outputable TvSubst where
-   ppr (TvSubst ins env) 
+   ppr (TvSubst ins tenv)
      = brackets $ sep[ ptext (sLit "TvSubst"),
                      nest 2 (ptext (sLit "In scope:") <+> ppr ins), 
-                     nest 2 (ptext (sLit "Env:") <+> ppr env) ]
+                     nest 2 (ptext (sLit "Type env:") <+> ppr tenv) ]
  \end{code}
  
  %************************************************************************
@@@ -1499,29 -1443,34 +1443,34 @@@ subst_ty subst t
                                   ForAllTy tv' $! (subst_ty subst' ty)
  
  substTyVar :: TvSubst -> TyVar  -> Type
- substTyVar subst@(TvSubst _ _) tv
-   = case lookupTyVar subst tv of {
-       Nothing -> TyVarTy tv;
-               Just ty -> ty   -- See Note [Apply Once]
-     } 
+ substTyVar (TvSubst _ tenv) tv
+   | Just ty  <- lookupVarEnv tenv tv      = ty  -- See Note [Apply Once]
+   | otherwise = ASSERT( isTyVar tv ) TyVarTy tv
+   -- We do not require that the tyvar is in scope
+   -- Reason: we do quite a bit of (substTyWith [tv] [ty] tau)
+   -- and it's a nuisance to bring all the free vars of tau into
+   -- scope --- and then force that thunk at every tyvar
+   -- Instead we have an ASSERT in substTyVarBndr to check for capture
  
  substTyVars :: TvSubst -> [TyVar] -> [Type]
  substTyVars subst tvs = map (substTyVar subst) tvs
  
  lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
        -- See Note [Extending the TvSubst]
- lookupTyVar (TvSubst _ env) tv = lookupVarEnv env tv
+ lookupTyVar (TvSubst _ tenv) tv = lookupVarEnv tenv tv
  
- substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)        
- substTyVarBndr subst@(TvSubst in_scope env) old_var
-   = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
+ substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
+ substTyVarBndr subst@(TvSubst in_scope tenv) old_var
+   = ASSERT2( _no_capture, ppr old_var $$ ppr subst ) 
+     (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
    where
-     is_co_var = isCoVar old_var
+     new_env | no_change = delVarEnv tenv old_var
+           | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
  
-     new_env | no_change = delVarEnv env old_var
-           | otherwise = extendVarEnv env old_var (TyVarTy new_var)
+     _no_capture = not (new_var `elemVarSet` tyVarsOfTypes (varEnvElts tenv))
+     -- Check that we are not capturing something in the substitution
  
-     no_change = new_var == old_var && not is_co_var
+     no_change = new_var == old_var
        -- no_change means that the new_var is identical in
        -- all respects to the old_var (same unique, same kind)
        -- See Note [Extending the TvSubst]
        --      (\x.e) with id_subst = [x |-> e']
        -- Here we must simply zap the substitution for x
  
-     new_var = uniqAway in_scope subst_old_var
+     new_var = uniqAway in_scope old_var
        -- The uniqAway part makes sure the new variable is not already in scope
-     subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
-                 -- It's only worth doing the substitution for coercions,
-                 -- becuase only they can have free type variables
-       | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
-       | otherwise = old_var
  \end{code}
  
  ----------------------------------------------------
            </row>
            <row>
              <entry><option>-XGenerics</option></entry>
 -            <entry>Enable <link linkend="generic-classes">generic classes</link></entry>
 +            <entry>Deprecated, does nothing. No longer enables <link linkend="generic-classes">generic classes</link>.
 +               See also GHC's support for
 +               <link linkend="generic-programming">generic programming</link>.</entry>
              <entry>dynamic</entry>
              <entry><option>-XNoGenerics</option></entry>
            </row>
              <entry><option>-XNoDeriveDataTypeable</option></entry>
            </row>
            <row>
 +            <entry><option>-XDeriveGeneric</option></entry>
 +            <entry>Enable <link linkend="deriving-typeable">deriving for the Generic class</link>.</entry>
 +            <entry>dynamic</entry>
 +            <entry><option>-XNoDeriveGeneric</option></entry>
 +          </row>
 +          <row>
              <entry><option>-XGeneralizedNewtypeDeriving</option></entry>
              <entry>Enable <link linkend="newtype-deriving">newtype deriving</link>.</entry>
              <entry>dynamic</entry>
              <entry><option>-XNoConstrainedClassMethods</option></entry>
            </row>
            <row>
 +            <entry><option>-XDefaultSignatures</option></entry>
 +            <entry>Enable <link linkend="class-default-signatures">default signatures</link>.</entry>
 +            <entry>dynamic</entry>
 +            <entry><option>-XNoDefaultSignatures</option></entry>
 +          </row>
 +          <row>
              <entry><option>-XMultiParamTypeClasses</option></entry>
              <entry>Enable <link linkend="multi-param-type-classes">multi parameter type classes</link>.</entry>
              <entry>dynamic</entry>
@@@ -2247,6 -2233,12 +2247,12 @@@ phase <replaceable>n</replaceable></ent
              <entry>-</entry>
            </row>
            <row>
+             <entry><option>-ddump-to-file</option></entry>
+             <entry>Dump to files instead of stdout</entry>
+             <entry>dynamic</entry>
+             <entry>-</entry>
+           </row>
+           <row>
              <entry><option>-ddump-asm</option></entry>
              <entry>Dump assembly</entry>
              <entry>dynamic</entry>