(partial) Merge branch 'master' into type-nats
authorIavor S. Diatchki <iavor.diatchki@gmail.com>
Sun, 19 Jun 2011 00:25:31 +0000 (17:25 -0700)
committerIavor S. Diatchki <iavor.diatchki@gmail.com>
Sun, 19 Jun 2011 00:25:31 +0000 (17:25 -0700)
Conflicts:
compiler/coreSyn/CoreLint.lhs
compiler/coreSyn/ExternalCore.lhs
compiler/deSugar/DsBinds.lhs
compiler/hsSyn/HsTypes.lhs
compiler/iface/BinIface.hs
compiler/iface/IfaceSyn.lhs
compiler/iface/IfaceType.lhs
compiler/iface/TcIface.lhs
compiler/parser/Parser.y.pp
compiler/parser/RdrHsSyn.lhs
compiler/prelude/PrelNames.lhs
compiler/rename/RnHsSyn.lhs
compiler/rename/RnTypes.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/typecheck/TcTyDecls.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs
compiler/types/Coercion.lhs
compiler/types/OptCoercion.lhs
compiler/types/Type.lhs
compiler/types/TypeRep.lhs

44 files changed:
1  2 
compiler/basicTypes/OccName.lhs
compiler/codeGen/StgCmmClosure.hs
compiler/coreSyn/CoreLint.lhs
compiler/coreSyn/ExternalCore.lhs
compiler/coreSyn/MkExternalCore.lhs
compiler/coreSyn/PprExternalCore.lhs
compiler/deSugar/DsBinds.lhs
compiler/ghc.cabal.in
compiler/hsSyn/Convert.lhs
compiler/hsSyn/HsBinds.lhs
compiler/hsSyn/HsTypes.lhs
compiler/iface/BinIface.hs
compiler/iface/IfaceSyn.lhs
compiler/iface/IfaceType.lhs
compiler/iface/TcIface.lhs
compiler/main/DynFlags.hs
compiler/parser/Lexer.x
compiler/parser/Parser.y.pp
compiler/parser/RdrHsSyn.lhs
compiler/prelude/PrelNames.lhs
compiler/prelude/TysPrim.lhs
compiler/rename/RnHsSyn.lhs
compiler/rename/RnTypes.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcSplice.lhs
compiler/typecheck/TcTyDecls.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcTypeNats.hs
compiler/typecheck/TcUnify.lhs
compiler/types/Coercion.lhs
compiler/types/FamInstEnv.lhs
compiler/types/Kind.lhs
compiler/types/OptCoercion.lhs
compiler/types/Type.lhs
compiler/types/TypeRep.lhs
compiler/types/Unify.lhs

Simple merge
Simple merge
@@@ -768,9 -716,9 +716,11 @@@ lintType ty@(AppTy t1 t2
  lintType ty@(FunTy t1 t2)
    = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
  
 +lintType ty@(LiteralTy l) = lintTyLit l >> return (typeKind ty)
 +
  lintType ty@(TyConApp tc tys)
+   | tc `hasKey` eqPredPrimTyConKey    -- See Note [The (~) TyCon] in TysPrim
+   = lint_eq_pred ty tys
    | tyConHasKind tc
    = lint_ty_app ty (tyConKind tc) tys
    | otherwise
@@@ -786,21 -734,14 +736,26 @@@ lintType ty@(PredTy (ClassP cls tys)
  lintType (PredTy (IParam _ p_ty))
    = lintType p_ty
  
- lintType ty@(PredTy (EqPred {}))
-   = failWithL (badEq ty)
+ lintType ty@(PredTy (EqPred t1 t2))
+   = do { k1 <- lintType t1
+        ; k2 <- lintType t2
+        ; unless (k1 `eqKind` k2) 
+                 (addErrL (sep [ ptext (sLit "Kind mis-match in equality predicate:")
+                               , nest 2 (ppr ty) ]))
+        ; return unliftedTypeKind }
  
 +
 +---
 +
 +lintTyLit :: TyLit -> LintM ()
 +lintTyLit (NumberTyLit n)
 +  | n >= 0    = return ()
 +  | otherwise = failWithL msg
 +    where msg = ptext (sLit "Negative type literal:") <+> integer n
 +
 +
 +
 +
  ----------------
  lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
  lint_ty_app ty k tys 
@@@ -56,11 -58,8 +58,9 @@@ data T
    | Tcon (Qual Tcon)
    | Tapp Ty Ty
    | Tforall Tbind Ty 
- -- We distinguish primitive coercions
- -- (represented in GHC by wired-in names), because
- -- External Core treats them specially, so we have
- -- to print them out with special syntax.
 +  | Tliteral TLit
+ -- We distinguish primitive coercions because External Core treats
+ -- them specially, so we have to print them out with special syntax.
    | TransCoercion Ty Ty
    | SymCoercion Ty
    | UnsafeCoercion Ty Ty
@@@ -13,6 -13,8 +13,9 @@@ import Modul
  import CoreSyn
  import HscTypes       
  import TyCon
+ -- import Class
+ -- import TysPrim( eqPredPrimTyCon )
++import Kind (isNatKind)
  import TypeRep
  import Type
  import PprExternalCore () -- Instances
@@@ -229,25 -230,7 +232,10 @@@ make_ty' (TyConApp tc ts)         = make_tyCo
  
  make_ty' (PredTy p)   = make_ty (predTypeRep p)
  
 +make_tlit :: TyLit -> C.TLit
 +make_tlit (NumberTyLit n) = C.TLnumber n
 +
  make_tyConApp :: TyCon -> [Type] -> C.Ty
- make_tyConApp tc [t1, t2] | tc == transCoercionTyCon =
-   C.TransCoercion (make_ty t1) (make_ty t2)
- make_tyConApp tc [t]      | tc == symCoercionTyCon =
-   C.SymCoercion (make_ty t)
- make_tyConApp tc [t1, t2] | tc == unsafeCoercionTyCon =
-   C.UnsafeCoercion (make_ty t1) (make_ty t2)
- make_tyConApp tc [t]      | tc == leftCoercionTyCon =
-   C.LeftCoercion (make_ty t)
- make_tyConApp tc [t]      | tc == rightCoercionTyCon =
-   C.RightCoercion (make_ty t)
- make_tyConApp tc [t1, t2] | tc == instCoercionTyCon =
-   C.InstCoercion (make_ty t1) (make_ty t2)
- -- this fails silently if we have an application
- -- of a wired-in coercion tycon to the wrong number of args.
- -- Not great...
  make_tyConApp tc ts =
    foldl C.Tapp (C.Tcon (qtc tc)) 
            (map make_ty ts)
Simple merge
@@@ -231,14 -231,12 +232,14 @@@ dsEvBinds bs = mapM dsEvGroup scc
  
      free_vars_of :: EvTerm -> [EvVar]
      free_vars_of (EvId v)           = [v]
-     free_vars_of (EvCast v co)      = v : varSetElems (tyVarsOfType co)
-     free_vars_of (EvCoercion co)    = varSetElems (tyVarsOfType co)
+     free_vars_of (EvCast v co)      = v : varSetElems (tyCoVarsOfCo co)
+     free_vars_of (EvCoercion co)    = varSetElems (tyCoVarsOfCo co)
      free_vars_of (EvDFunApp _ _ vs) = vs
      free_vars_of (EvSuperClass d _) = [d]
 +    free_vars_of (EvInteger _)      = []
 +    free_vars_of (EvAxiom _ _)      = []
  
 -dsEvGroup :: SCC EvBind -> DsEvBind
 +dsEvGroup :: MonadThings m => SCC EvBind -> m DsEvBind
  dsEvGroup (AcyclicSCC (EvBind co_var (EvSuperClass dict n)))
    | isCoVar co_var     -- An equality superclass
    = ASSERT( null other_data_cons )
                          | otherwise = mkWildEvBinder p
      
  dsEvGroup (AcyclicSCC (EvBind v r))
 -  = LetEvBind (NonRec v (dsEvTerm r))
 +  = do d <- dsEvTerm r
 +       return (LetEvBind (NonRec v d))
  
  dsEvGroup (CyclicSCC bs)
 -  = LetEvBind (Rec (map ds_pair bs))
 +  = do ds <- mapM ds_pair bs
 +       return (LetEvBind (Rec ds))
    where
 -    ds_pair (EvBind v r) = (v, dsEvTerm r)
 -
 -dsEvTerm :: EvTerm -> CoreExpr
 -dsEvTerm (EvId v)                = Var v
 -dsEvTerm (EvCast v co)           = Cast (Var v) co
 -dsEvTerm (EvDFunApp df tys vars) = Var df `mkTyApps` tys `mkVarApps` vars
 -dsEvTerm (EvCoercion co)         = Coercion co
 +    ds_pair (EvBind v r) = do ev <- dsEvTerm r
 +                              return (v, ev)
 +
 +dsEvTerm :: MonadThings m => EvTerm -> m CoreExpr
 +dsEvTerm (EvId v)         = return (Var v)
 +dsEvTerm (EvCast v co)    = return (Cast (Var v) co)
- dsEvTerm (EvDFunApp df tys vars) =
-                             return (Var df `mkTyApps` tys `mkVarApps` vars)
- dsEvTerm (EvCoercion co)  = return (Type co)
++dsEvTerm (EvDFunApp df tys vars) = return (Var df `mkTyApps` tys `mkVarApps` vars)
++dsEvTerm (EvCoercion co)         = return (Coercion co)
 +dsEvTerm (EvInteger n)    = mkIntegerExpr n
 +dsEvTerm (EvAxiom x t)    = return (mkRuntimeErrorApp rUNTIME_ERROR_ID t x)
  dsEvTerm (EvSuperClass d n)
    = ASSERT( isClassPred (classSCTheta cls !! n) )
            -- We can only select *dictionary* superclasses
Simple merge
Simple merge
@@@ -599,13 -572,10 +599,13 @@@ 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 ]
 +  ppr (EvInteger n)      = integer n
 +  ppr (EvAxiom x t)      = parens (ptext (sLit ("axiom " ++ x)) <+> 
 +                                            ptext (sLit "::") <+> ppr t)
  \end{code}
  
  %************************************************************************
@@@ -168,13 -168,6 +168,8 @@@ data HsType nam
        -- interface files smaller), so when printing a HsType we may need to
        -- add parens.  
  
-       -- Uses a separate constructor from the generics one to avoid confusion.
-       -- In this way we could support both by just modifying the parser to
-       -- avoid the overlap between the two.
-   | HsNumTy             Integer               -- Generics only
 +  | HsNumberTy          Integer         -- Type level number
 +
    | HsPredTy          (HsPred name)   -- Only used in the type of an instance
                                        -- declaration, eg.  Eq [a] -> Eq a
                                        --                             ^^^^
@@@ -445,8 -438,6 +440,7 @@@ ppr_mono_ty _    (HsKindSig ty kind) = 
  ppr_mono_ty _    (HsListTy ty)             = brackets (ppr_mono_lty pREC_TOP ty)
  ppr_mono_ty _    (HsPArrTy ty)             = pabrackets (ppr_mono_lty pREC_TOP ty)
  ppr_mono_ty _    (HsPredTy pred)     = ppr pred
- ppr_mono_ty _    (HsNumTy n)         = integer n  -- generics only
 +ppr_mono_ty _    (HsNumberTy n)      = integer n
  ppr_mono_ty _    (HsSpliceTy s _ _)  = pprSplice s
  ppr_mono_ty _    (HsCoreTy ty)       = ppr ty
  
@@@ -885,12 -884,7 +884,10 @@@ instance Binary IfaceType wher
      put_ bh (IfacePredTy aq) = do
            putByte bh 5
            put_ bh aq
-           putByte bh 20
 +    put_ bh (IfaceLiteralTy n) = do
++          putByte bh 30
 +          put_ bh n
  
        -- Simple compression for common cases of TyConApp
      put_ bh (IfaceTyConApp IfaceIntTc  [])   = putByte bh 6
      put_ bh (IfaceTyConApp IfaceCharTc [])   = putByte bh 7
      put_ bh (IfaceTyConApp IfaceUnliftedTypeKindTc []) = putByte bh 14
      put_ bh (IfaceTyConApp IfaceUbxTupleKindTc [])     = putByte bh 15
      put_ bh (IfaceTyConApp IfaceArgTypeKindTc [])      = putByte bh 16
-     put_ bh (IfaceTyConApp IfaceNatKindTc [])          = putByte bh 21
++    put_ bh (IfaceTyConApp IfaceNatKindTc [])          = putByte bh 31
      put_ bh (IfaceTyConApp (IfaceAnyTc k) [])                = do { putByte bh 17; put_ bh k }
  
        -- Generic cases
                      return (IfaceFunTy ag ah)
              5 -> do ap <- get bh
                      return (IfacePredTy ap)
-               20 -> do n <- get bh
++              30 -> do n <- get bh
 +                       return (IfaceLiteralTy n)
  
                -- Now the special cases for TyConApp
              6 -> return (IfaceTyConApp IfaceIntTc [])
                14 -> return (IfaceTyConApp IfaceUnliftedTypeKindTc [])
                15 -> return (IfaceTyConApp IfaceUbxTupleKindTc [])
                16 -> return (IfaceTyConApp IfaceArgTypeKindTc [])
-               21 -> return (IfaceTyConApp IfaceNatKindTc [])
++              31 -> return (IfaceTyConApp IfaceNatKindTc [])
                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 IfaceTyLit where
 +  put_ bh (IfaceNumberTyLit n)  = putByte bh 1 >> put_ bh n
 +
 +  get bh =
 +    do tag <- getByte bh
 +       case tag of
 +         1 -> do n <- get bh
 +                 return (IfaceNumberTyLit n)
 +
 +
  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 IfaceNatKindTc          = putByte bh 14
+    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
            8 -> return IfaceUnliftedTypeKindTc
            9 -> return IfaceUbxTupleKindTc
            10 -> return IfaceArgTypeKindTc
 +          14 -> return IfaceNatKindTc
          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
@@@ -788,8 -788,8 +788,9 @@@ freeNamesIfType (IfaceTyConApp tc ts) 
  freeNamesIfType (IfaceForAllTy tv t)  =
     freeNamesIfTvBndr tv &&& freeNamesIfType t
  freeNamesIfType (IfaceFunTy s t)      = freeNamesIfType s &&& freeNamesIfType t
 +freeNamesIfType (IfaceLiteralTy _)    = emptyNameSet
+ freeNamesIfType (IfaceCoConApp tc ts) = 
+    freeNamesIfCo tc &&& fnList freeNamesIfType ts
  
  freeNamesIfTvBndrs :: [IfaceTvBndr] -> NameSet
  freeNamesIfTvBndrs = fnList freeNamesIfTvBndr
@@@ -9,8 -9,7 +9,8 @@@ This module defines interface types an
  module IfaceType (
        IfExtName, IfLclName,
  
-         IfaceType(..), IfaceKind, IfacePredType(..), IfaceTyCon(..),
+         IfaceType(..), IfaceKind, IfacePredType(..), IfaceTyCon(..), IfaceCoCon(..),
 +        IfaceTyLit(..),
        IfaceContext, IfaceBndr(..), IfaceTvBndr, IfaceIdBndr, IfaceCoercion,
        ifaceTyConName,
  
@@@ -60,39 -64,45 +65,50 @@@ type IfaceTvBndr  = (IfLclName, IfaceKi
  type IfaceKind     = IfaceType
  type IfaceCoercion = IfaceType
  
- data IfaceType
-   = IfaceTyVar    IfLclName                   -- Type variable only, not tycon
+ data IfaceType           -- A kind of universal type, used for types, kinds, and coercions
+   = IfaceTyVar    IfLclName                   -- Type/coercion variable only, not tycon
    | IfaceAppTy    IfaceType IfaceType
+   | IfaceFunTy    IfaceType IfaceType
    | IfaceForAllTy IfaceTvBndr IfaceType
    | IfacePredTy   IfacePredType
-   | IfaceTyConApp IfaceTyCon [IfaceType]      -- Not necessarily saturated
-                                               -- Includes newtypes, synonyms, tuples
-   | IfaceFunTy  IfaceType IfaceType
+   | IfaceTyConApp IfaceTyCon [IfaceType]  -- Not necessarily saturated
+                                         -- Includes newtypes, synonyms, tuples
+   | IfaceCoConApp IfaceCoCon [IfaceType]  -- Always saturated
 +  | IfaceLiteralTy IfaceTyLit
  
  data IfacePredType    -- NewTypes are handled as ordinary TyConApps
    = IfaceClassP IfExtName [IfaceType]
    | IfaceIParam (IPName OccName) IfaceType
    | IfaceEqPred IfaceType IfaceType
  
 +data IfaceTyLit
 +  = IfaceNumberTyLit Integer
 +
  type IfaceContext = [IfacePredType]
  
- data IfaceTyCon       -- Abbreviations for common tycons with known names
+ data IfaceTyCon       -- Encodes type consructors, kind constructors
+                       -- coercion constructors, the lot
    = IfaceTc IfExtName -- The common case
    | IfaceIntTc | IfaceBoolTc | IfaceCharTc
    | IfaceListTc | IfacePArrTc
    | IfaceTupTc Boxity Arity 
    | IfaceAnyTc IfaceKind     -- Used for AnyTyCon (see Note [Any Types] in TysPrim)
                             -- other than 'Any :: *' itself
+  
+   -- Kind constructors
    | IfaceLiftedTypeKindTc | IfaceOpenTypeKindTc | IfaceUnliftedTypeKindTc
    | IfaceUbxTupleKindTc | IfaceArgTypeKindTc 
 +  | IfaceNatKindTc 
  
- ifaceTyConName :: IfaceTyCon -> IfExtName
- ifaceTyConName IfaceIntTc            = intTyConName
+   -- Coercion constructors
+ data IfaceCoCon
+   = IfaceCoAx IfExtName
+   | IfaceReflCo    | IfaceUnsafeCo  | IfaceSymCo
+   | IfaceTransCo   | IfaceInstCo
+   | IfaceNthCo Int
+ ifaceTyConName :: IfaceTyCon -> Name
+ ifaceTyConName IfaceIntTc              = intTyConName
  ifaceTyConName IfaceBoolTc           = boolTyConName
  ifaceTyConName IfaceCharTc           = charTyConName
  ifaceTyConName IfaceListTc           = listTyConName
@@@ -280,9 -288,15 +300,18 @@@ instance Outputable IfaceTyCon wher
                             -- so we fake it.  It's only for debug printing!
    ppr other_tc       = ppr (ifaceTyConName other_tc)
  
+ instance Outputable IfaceCoCon where
+   ppr (IfaceCoAx n)  = ppr n
+   ppr IfaceReflCo    = ptext (sLit "Refl")
+   ppr IfaceUnsafeCo  = ptext (sLit "Unsafe")
+   ppr IfaceSymCo     = ptext (sLit "Sym")
+   ppr IfaceTransCo   = ptext (sLit "Trans")
+   ppr IfaceInstCo    = ptext (sLit "Inst")
+   ppr (IfaceNthCo d) = ptext (sLit "Nth:") <> int d
 +instance Outputable IfaceTyLit where
 +  ppr = ppr_tylit
 +
  -------------------
  pprIfaceContext :: IfaceContext -> SDoc
  -- Prints "(C a, D b) =>", including the arrow
@@@ -324,19 -338,15 +353,16 @@@ toIfaceKind = toIfaceTyp
  ---------------------
  toIfaceType :: Type -> IfaceType
  -- Synonyms are retained in the interface type
- toIfaceType (TyVarTy tv) =
-   IfaceTyVar (occNameFS (getOccName tv))
- toIfaceType (AppTy t1 t2) =
-   IfaceAppTy (toIfaceType t1) (toIfaceType t2)
- toIfaceType (FunTy t1 t2) =
-   IfaceFunTy (toIfaceType t1) (toIfaceType t2)
- toIfaceType (TyConApp tc tys) =
-   IfaceTyConApp (toIfaceTyCon tc) (toIfaceTypes tys)
- toIfaceType (ForAllTy tv t) =
-   IfaceForAllTy (toIfaceTvBndr tv) (toIfaceType t)
- toIfaceType (PredTy st) =
-   IfacePredTy (toIfacePred st)
- toIfaceType (LiteralTy n) = IfaceLiteralTy (toIfaceTyLit n)
+ toIfaceType (TyVarTy tv)      = IfaceTyVar (toIfaceTyCoVar tv)
+ toIfaceType (AppTy t1 t2)     = IfaceAppTy (toIfaceType t1) (toIfaceType t2)
+ toIfaceType (FunTy t1 t2)     = IfaceFunTy (toIfaceType t1) (toIfaceType t2)
+ toIfaceType (TyConApp tc tys) = IfaceTyConApp (toIfaceTyCon tc) (toIfaceTypes tys)
+ toIfaceType (ForAllTy tv t)   = IfaceForAllTy (toIfaceTvBndr tv) (toIfaceType t)
+ toIfaceType (PredTy st)       = IfacePredTy (toIfacePred toIfaceType st)
++toIfaceType (LiteralTy n)     = IfaceLiteralTy (toIfaceTyLit n)
+ toIfaceTyCoVar :: TyCoVar -> FastString
+ toIfaceTyCoVar = occNameFS . getOccName
  
  ----------------
  -- A little bit of (perhaps optional) trickiness here.  When
@@@ -381,20 -390,39 +407,43 @@@ toIfaceTypes :: [Type] -> [IfaceType
  toIfaceTypes ts = map toIfaceType ts
  
  ----------------
- toIfacePred :: PredType -> IfacePredType
- toIfacePred (ClassP cls ts) = 
-   IfaceClassP (getName cls) (toIfaceTypes ts)
- toIfacePred (IParam ip t) = 
-   IfaceIParam (mapIPName getOccName ip) (toIfaceType t)
- toIfacePred (EqPred ty1 ty2) =
-   IfaceEqPred (toIfaceType ty1) (toIfaceType ty2)
+ toIfacePred :: (a -> IfaceType) -> Pred a -> IfacePredType
+ toIfacePred to (ClassP cls ts)  = IfaceClassP (getName cls) (map to ts)
+ toIfacePred to (IParam ip t)    = IfaceIParam (mapIPName getOccName ip) (to t)
+ toIfacePred to (EqPred ty1 ty2) =  IfaceEqPred (to ty1) (to ty2)
  
 +toIfaceTyLit :: TyLit -> IfaceTyLit
 +toIfaceTyLit (NumberTyLit x) = IfaceNumberTyLit x
 +
 +
  ----------------
  toIfaceContext :: ThetaType -> IfaceContext
- toIfaceContext cs = map toIfacePred cs
+ toIfaceContext cs = map (toIfacePred toIfaceType) cs
+ ----------------
+ coToIfaceType :: Coercion -> IfaceType
+ coToIfaceType (Refl ty)             = IfaceCoConApp IfaceReflCo [toIfaceType ty]
+ coToIfaceType (TyConAppCo tc cos)   = IfaceTyConApp (toIfaceTyCon tc) 
+                                                     (map coToIfaceType cos)
+ coToIfaceType (AppCo co1 co2)       = IfaceAppTy    (coToIfaceType co1) 
+                                                     (coToIfaceType co2)
+ coToIfaceType (ForAllCo v co)       = IfaceForAllTy (toIfaceTvBndr v) 
+                                                     (coToIfaceType co)
+ coToIfaceType (CoVarCo cv)          = IfaceTyVar  (toIfaceTyCoVar cv)
+ coToIfaceType (AxiomInstCo con cos) = IfaceCoConApp (IfaceCoAx (coAxiomName con))
+                                                     (map coToIfaceType cos)
+ coToIfaceType (UnsafeCo ty1 ty2)    = IfaceCoConApp IfaceUnsafeCo 
+                                                     [ toIfaceType ty1
+                                                     , toIfaceType ty2 ]
+ coToIfaceType (SymCo co)            = IfaceCoConApp IfaceSymCo 
+                                                     [ coToIfaceType co ]
+ coToIfaceType (TransCo co1 co2)     = IfaceCoConApp IfaceTransCo
+                                                     [ coToIfaceType co1
+                                                     , coToIfaceType co2 ]
+ coToIfaceType (NthCo d co)          = IfaceCoConApp (IfaceNthCo d)
+                                                     [ coToIfaceType co ]
+ coToIfaceType (InstCo co ty)        = IfaceCoConApp IfaceInstCo 
+                                                     [ coToIfaceType co
+                                                     , toIfaceType ty ]
  \end{code}
  
@@@ -805,16 -813,39 +814,46 @@@ tcIfacePred tc (IfaceEqPred t1 t2
  
  -----------------------------------------
  tcIfaceCtxt :: IfaceContext -> IfL ThetaType
- tcIfaceCtxt sts = mapM tcIfacePredType sts
+ tcIfaceCtxt sts = mapM (tcIfacePred tcIfaceType) sts
 +
 +
 +-----------------------------------------
 +tcIfaceTyLit :: IfaceTyLit -> IfL TyLit
 +tcIfaceTyLit (IfaceNumberTyLit n) = return (NumberTyLit n)
 +
+ \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"
++tcIfaceCo t@(IfaceLiteralTy _) = mkReflCo <$> tcIfaceType t
+ 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}
  
  
Simple merge
@@@ -1875,31 -1877,30 +1881,31 @@@ mkPState flags buf loc 
        alr_justClosedExplicitLetBlock = False
      }
      where
-       bitmap = genericsBit `setBitIf` xopt Opt_Generics flags
-              .|. ffiBit            `setBitIf` xopt Opt_ForeignFunctionInterface flags
-              .|. parrBit           `setBitIf` xopt Opt_ParallelArrays  flags
-              .|. arrowsBit         `setBitIf` xopt Opt_Arrows          flags
-              .|. thBit             `setBitIf` xopt Opt_TemplateHaskell flags
-              .|. qqBit             `setBitIf` xopt Opt_QuasiQuotes     flags
-              .|. ipBit             `setBitIf` xopt Opt_ImplicitParams  flags
-              .|. explicitForallBit `setBitIf` xopt Opt_ExplicitForAll  flags
-              .|. bangPatBit        `setBitIf` xopt Opt_BangPatterns flags
-              .|. tyFamBit          `setBitIf` xopt Opt_TypeFamilies flags
-              .|. haddockBit        `setBitIf` dopt Opt_Haddock      flags
-              .|. magicHashBit      `setBitIf` xopt Opt_MagicHash    flags
-              .|. kindSigsBit       `setBitIf` xopt Opt_KindSignatures flags
-              .|. recursiveDoBit    `setBitIf` xopt Opt_RecursiveDo flags
-              .|. recBit            `setBitIf` xopt Opt_DoRec  flags
-              .|. recBit            `setBitIf` xopt Opt_Arrows flags
-              .|. unicodeSyntaxBit  `setBitIf` xopt Opt_UnicodeSyntax flags
-              .|. unboxedTuplesBit  `setBitIf` xopt Opt_UnboxedTuples flags
+       bitmap =     ffiBit            `setBitIf` xopt Opt_ForeignFunctionInterface flags
+                .|. parrBit           `setBitIf` xopt Opt_ParallelArrays  flags
+                .|. arrowsBit         `setBitIf` xopt Opt_Arrows          flags
+                .|. thBit             `setBitIf` xopt Opt_TemplateHaskell flags
+                .|. qqBit             `setBitIf` xopt Opt_QuasiQuotes     flags
+                .|. ipBit             `setBitIf` xopt Opt_ImplicitParams  flags
+                .|. explicitForallBit `setBitIf` xopt Opt_ExplicitForAll  flags
+                .|. bangPatBit        `setBitIf` xopt Opt_BangPatterns    flags
+                .|. tyFamBit          `setBitIf` xopt Opt_TypeFamilies    flags
+                .|. haddockBit        `setBitIf` dopt Opt_Haddock         flags
+                .|. magicHashBit      `setBitIf` xopt Opt_MagicHash       flags
+                .|. kindSigsBit       `setBitIf` xopt Opt_KindSignatures  flags
+                .|. recursiveDoBit    `setBitIf` xopt Opt_RecursiveDo     flags
+                .|. recBit            `setBitIf` xopt Opt_DoRec           flags
+                .|. recBit            `setBitIf` xopt Opt_Arrows          flags
+                .|. unicodeSyntaxBit  `setBitIf` xopt Opt_UnicodeSyntax   flags
+                .|. unboxedTuplesBit  `setBitIf` xopt Opt_UnboxedTuples   flags
                 .|. datatypeContextsBit `setBitIf` xopt Opt_DatatypeContexts flags
                 .|. transformComprehensionsBit `setBitIf` xopt Opt_TransformListComp flags
+                .|. transformComprehensionsBit `setBitIf` xopt Opt_MonadComprehensions flags
                 .|. rawTokenStreamBit `setBitIf` dopt Opt_KeepRawTokenStream flags
                 .|. alternativeLayoutRuleBit `setBitIf` xopt Opt_AlternativeLayoutRule flags
-                .|. relaxedLayoutBit `setBitIf` xopt Opt_RelaxedLayout flags
+                .|. relaxedLayoutBit  `setBitIf` xopt Opt_RelaxedLayout flags
                 .|. nondecreasingIndentationBit `setBitIf` xopt Opt_NondecreasingIndentation flags
 +               .|. typeNaturalsBit `setBitIf` xopt Opt_TypeNaturals flags
        --
        setBitIf :: Int -> Bool -> Int
        b `setBitIf` cond | cond      = bit b
Simple merge
@@@ -55,9 -50,10 +54,11 @@@ module RdrHsSyn 
  
  import HsSyn          -- Lots of it
  import Class            ( FunDep )
- import TypeRep          ( Kind, natKind )
+ import TypeRep          ( Kind )
++import TysPrim          ( natKind )
  import RdrName                ( RdrName, isRdrTyVar, isRdrTc, mkUnqual, rdrNameOcc, 
                          isRdrDataCon, isUnqual, getRdrName, setRdrNameSpace )
+ import Name             ( Name )
  import BasicTypes     ( maxPrecedence, Activation(..), RuleMatchInfo,
                            InlinePragma(..), InlineSpec(..) )
  import Lexer
@@@ -131,8 -127,6 +132,7 @@@ extract_lty (L loc ty) ac
        HsPredTy p              -> extract_pred p acc
        HsOpTy ty1 (L loc tv) ty2 -> extract_tv loc tv (extract_lty ty1 (extract_lty ty2 acc))
        HsParTy ty                      -> extract_lty ty acc
-       HsNumTy {}                -> acc
 +      HsNumberTy {}             -> acc
        HsCoreTy {}               -> acc  -- The type is closed
        HsQuasiQuoteTy {}               -> acc  -- Quasi quotes mention no type variables
        HsSpliceTy {}                   -> acc  -- Type splices mention no type variables
@@@ -248,15 -274,15 +281,16 @@@ pRELUDE         = mkBaseModule_ pRELUDE_NAM
  
  gHC_PRIM, gHC_TYPES, gHC_UNIT, gHC_ORDERING, gHC_GENERICS,
      gHC_MAGIC,
-     gHC_CLASSES, gHC_BASE, gHC_ENUM,
-     gHC_SHOW, gHC_READ, gHC_NUM, gHC_INTEGER, gHC_INTEGER_TYPE, gHC_LIST, gHC_PARR,
+     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,
-     gHC_ST, gHC_ARR, gHC_STABLE, gHC_ADDR, gHC_PTR, gHC_ERR, gHC_REAL,
+     gHC_CONC, gHC_IO, gHC_IO_Exception,
+     gHC_ST, gHC_ARR, gHC_STABLE, gHC_PTR, gHC_ERR, gHC_REAL,
      gHC_FLOAT, gHC_TOP_HANDLER, sYSTEM_IO, dYNAMIC, tYPEABLE, gENERICS,
-     dOTNET, rEAD_PREC, lEX, gHC_INT, gHC_WORD, mONAD, mONAD_FIX, aRROW, cONTROL_APPLICATIVE,
-     gHC_DESUGAR, rANDOM, gHC_EXTS, cONTROL_EXCEPTION_BASE,
+     dOTNET, rEAD_PREC, lEX, gHC_INT, gHC_WORD, mONAD, mONAD_FIX, mONAD_GROUP, mONAD_ZIP,
+     aRROW, cONTROL_APPLICATIVE, gHC_DESUGAR, rANDOM, gHC_EXTS,
 -    cONTROL_EXCEPTION_BASE :: Module
++    cONTROL_EXCEPTION_BASE,
 +    gHC_TYPENATS :: Module
  
  gHC_PRIM      = mkPrimModule (fsLit "GHC.Prim")   -- Primitive types and values
  gHC_TYPES       = mkPrimModule (fsLit "GHC.Types")
@@@ -311,8 -337,13 +345,14 @@@ gHC_DESUGAR = mkBaseModule (fsLit "GHC.
  rANDOM                = mkBaseModule (fsLit "System.Random")
  gHC_EXTS      = mkBaseModule (fsLit "GHC.Exts")
  cONTROL_EXCEPTION_BASE = mkBaseModule (fsLit "Control.Exception.Base")
 +gHC_TYPENATS    = mkBaseModule (fsLit "GHC.TypeNats")
  
+ gHC_PARR :: PackageId -> Module
+ gHC_PARR pkg = mkModule pkg (mkModuleNameFS (fsLit "Data.Array.Parallel"))
+ gHC_PARR' :: Module
+ gHC_PARR' = mkBaseModule (fsLit "GHC.PArr")
  mAIN, rOOT_MAIN :: Module
  mAIN          = mkMainModule_ mAIN_NAME
  rOOT_MAIN     = mkMainModule (fsLit ":Main") -- Root module for initialisation 
@@@ -943,11 -1060,14 +1078,19 @@@ applicativeClassKey   = mkPreludeClassUni
  foldableClassKey      = mkPreludeClassUnique 35
  traversableClassKey   = mkPreludeClassUnique 36
  
- typeNatClassKey, lessThanEqualClassKey :: Unique
- typeNatClassKey         = mkPreludeClassUnique 37
- lessThanEqualClassKey   = mkPreludeClassUnique 38
+ genClassKey, gen1ClassKey, datatypeClassKey, constructorClassKey,
+   selectorClassKey :: Unique
+ genClassKey   = mkPreludeClassUnique 37
+ gen1ClassKey  = mkPreludeClassUnique 38
+ datatypeClassKey    = mkPreludeClassUnique 39
+ constructorClassKey = mkPreludeClassUnique 40
+ selectorClassKey    = mkPreludeClassUnique 41
 +
++typeNatClassKey, lessThanEqualClassKey :: Unique
++typeNatClassKey         = mkPreludeClassUnique 42
++lessThanEqualClassKey   = mkPreludeClassUnique 43
 +
  \end{code}
  
  %************************************************************************
@@@ -1091,15 -1204,43 +1228,49 @@@ opaqueTyConKe
  stringTyConKey :: Unique
  stringTyConKey                                = mkPreludeTyConUnique 134
  
- addTyFamNameKey, mulTyFamNameKey, expTyFamNameKey :: Unique
- addTyFamNameKey                         = mkPreludeTyConUnique 135
- mulTyFamNameKey                         = mkPreludeTyConUnique 136
- expTyFamNameKey                         = mkPreludeTyConUnique 137
 +
+ -- 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
  
++addTyFamNameKey, mulTyFamNameKey, expTyFamNameKey :: Unique
++addTyFamNameKey                         = mkPreludeTyConUnique 160
++mulTyFamNameKey                         = mkPreludeTyConUnique 161
++expTyFamNameKey                         = mkPreludeTyConUnique 162
 +
  ---------------- Template Haskell -------------------
- --    USES TyConUniques 100-129
+ --    USES TyConUniques 200-299
  -----------------------------------------------------
  
  unitTyConKey :: Unique
@@@ -1364,9 -1518,7 +1548,9 @@@ kindKeys = [ liftedTypeKindTyConKe
           , openTypeKindTyConKey
           , unliftedTypeKindTyConKey
           , ubxTupleKindTyConKey 
 -         , argTypeKindTyConKey ]
 +         , argTypeKindTyConKey
-            , natKindTyConKey
-            ]
++         , natKindTyConKey
++       ]
  \end{code}
  
  
@@@ -14,7 -14,22 +14,25 @@@ module TysPrim
        openAlphaTy, openBetaTy, openAlphaTyVar, openBetaTyVar, openAlphaTyVars,
          argAlphaTy, argAlphaTyVar, argBetaTy, argBetaTyVar,
  
-       primTyCons,
+         -- Kind constructors...
+         tySuperKindTyCon, tySuperKind,
+         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
+         argTypeKindTyCon, ubxTupleKindTyCon,
++        natKindTyCon,
+         tySuperKindTyConName, liftedTypeKindTyConName,
+         openTypeKindTyConName, unliftedTypeKindTyConName,
+         ubxTupleKindTyConName, argTypeKindTyConName,
++        natKindTyConName,
+         -- Kinds
+       liftedTypeKind, unliftedTypeKind, openTypeKind,
+         argTypeKind, ubxTupleKind,
+         mkArrowKind, mkArrowKinds, isCoercionKind,
++        natKind,
+         funTyCon, funTyConName,
+         primTyCons,
  
        charPrimTyCon,          charPrimTy,
        intPrimTyCon,           intPrimTy,
@@@ -197,106 -214,92 +217,100 @@@ argBetaTy  = mkTyVarTy argBetaTyVa
  %*                                                                    *
  %************************************************************************
  
- Note [Any types]
- ~~~~~~~~~~~~~~~~
- The type constructor Any::* has these properties
-   * It is defined in module GHC.Prim, and exported so that it is 
-     available to users.  For this reason it's treated like any other 
-     primitive type:
-       - has a fixed unique, anyTyConKey, 
-       - lives in the global name cache
-       - built with TyCon.PrimTyCon
-   * It is lifted, and hence represented by a pointer
-   * It is inhabited by at least one value, namely bottom
-   * You can unsafely coerce any lifted type to Ayny, and back.
-   * It does not claim to be a *data* type, and that's important for
-     the code generator, because the code gen may *enter* a data value
-     but never enters a function value. 
-   * It is used to instantiate otherwise un-constrained type variables of kind *
-     For example       length Any []
-     See Note [Strangely-kinded void TyCons]
- In addition, we have a potentially-infinite family of types, one for
- each kind /other than/ *, needed to instantiate otherwise
- un-constrained type variables of kinds other than *.  This is a bit
- like tuples; there is a potentially-infinite family.  They have slightly
- different characteristics to Any::*:
-   
-   * They are built with TyCon.AnyTyCon
-   * They have non-user-writable names like "Any(*->*)" 
-   * They are not exported by GHC.Prim
-   * They are uninhabited (of course; not kind *)
-   * They have a unique derived from their OccName (see Note [Uniques of Any])
-   * Their Names do not live in the global name cache
- Note [Uniques of Any]
- ~~~~~~~~~~~~~~~~~~~~~
- Although Any(*->*), say, doesn't have a binding site, it still needs
- to have a Unique.  Unlike tuples (which are also an infinite family)
- there is no convenient way to index them, so we use the Unique from
- their OccName instead.  That should be unique, 
-   - both wrt each other, because their strings differ
-   - and wrt any other Name, because Names get uniques with 
-     various 'char' tags, but the OccName of Any will 
-     get a Unique built with mkTcOccUnique, which has a particular 'char' 
-     tag; see Unique.mkTcOccUnique!
- Note [Strangely-kinded void TyCons]
- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- See Trac #959 for more examples
- When the type checker finds a type variable with no binding, which
- means it can be instantiated with an arbitrary type, it usually
- instantiates it to Void.  Eg.
+ \begin{code}
+ funTyConName :: Name
+ funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
+ funTyCon :: TyCon
+ funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
+         -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
+       -- But if we do that we get kind errors when saying
+       --      instance Control.Arrow (->)
+       -- becuase the expected kind is (*->*->*).  The trouble is that the
+       -- expected/actual stuff in the unifier does not go contra-variant, whereas
+       -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
+       -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
+         -- because they are never in scope in the source
+ \end{code}
  
-       length []
- ===>
-       length Any (Nil Any)
  
- But in really obscure programs, the type variable might have a kind
- other than *, so we need to invent a suitably-kinded type.
- This commit uses
-       Any for kind *
-       Any(*->*) for kind *->*
-       etc
+ %************************************************************************
+ %*                                                                    *
+                 Kinds
+ %*                                                                    *
+ %************************************************************************
  
  \begin{code}
- anyTyConName :: Name
- anyTyConName = mkPrimTc (fsLit "Any") anyTyConKey anyTyCon
- anyTyCon :: TyCon
- anyTyCon = mkLiftedPrimTyCon anyTyConName liftedTypeKind 0 PtrRep
- anyTypeOfKind :: Kind -> Type
- anyTypeOfKind kind = mkTyConApp (anyTyConOfKind kind) []
+ -- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
+ tySuperKindTyCon, liftedTypeKindTyCon,
+       openTypeKindTyCon, unliftedTypeKindTyCon,
+       ubxTupleKindTyCon, argTypeKindTyCon
++    , natKindTyCon
+    :: TyCon
+ tySuperKindTyConName, liftedTypeKindTyConName,
+       openTypeKindTyConName, unliftedTypeKindTyConName,
+       ubxTupleKindTyConName, argTypeKindTyConName
++    , natKindTyConName
+    :: Name
+ tySuperKindTyCon      = mkSuperKindTyCon tySuperKindTyConName
+ liftedTypeKindTyCon   = mkKindTyCon liftedTypeKindTyConName   tySuperKind
+ openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName     tySuperKind
+ unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName tySuperKind
+ ubxTupleKindTyCon     = mkKindTyCon ubxTupleKindTyConName     tySuperKind
+ argTypeKindTyCon      = mkKindTyCon argTypeKindTyConName      tySuperKind
++natKindTyCon          = mkKindTyCon natKindTyConName          tySuperKind
++
+ --------------------------
+ -- ... and now their names
+ tySuperKindTyConName      = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
+ liftedTypeKindTyConName   = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
+ openTypeKindTyConName     = mkPrimTyConName (fsLit "?") openTypeKindTyConKey openTypeKindTyCon
+ unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
+ ubxTupleKindTyConName     = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
+ argTypeKindTyConName      = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
++natKindTyConName          = mkPrimTyConName (fsLit "Nat") natKindTyConKey natKindTyCon
++
+ mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
+ mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ) 
+                                             key 
+                                             (ATyCon tycon)
+                                             BuiltInSyntax
+       -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
+       -- because they are never in scope in the source
+ \end{code}
  
- anyTyConOfKind :: Kind -> TyCon
- -- Map all superkinds of liftedTypeKind to liftedTypeKind
- anyTyConOfKind kind 
-   | liftedTypeKind `isSubKind` kind = anyTyCon
-   | otherwise                       = tycon
-   where
-         -- Derive the name from the kind, thus:
-         --     Any(*->*), Any(*->*->*)
-         -- These are names that can't be written by the user,
-         -- and are not allocated in the global name cache
-     str = "Any" ++ showSDoc (pprParendKind kind)
  
-     occ   = mkTcOcc str
-     uniq  = getUnique occ  -- See Note [Uniques of Any]
-     name  = mkWiredInName gHC_PRIM occ uniq (ATyCon tycon) UserSyntax
-     tycon = mkAnyTyCon name kind 
+ \begin{code}
+ kindTyConType :: TyCon -> Type
+ kindTyConType kind = TyConApp kind []
+ -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
+ liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
 -
++natKind :: Kind
+ liftedTypeKind   = kindTyConType liftedTypeKindTyCon
+ unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
+ openTypeKind     = kindTyConType openTypeKindTyCon
+ argTypeKind      = kindTyConType argTypeKindTyCon
+ ubxTupleKind   = kindTyConType ubxTupleKindTyCon
++natKind          = kindTyConType natKindTyCon
++
+ -- | Given two kinds @k1@ and @k2@, creates the 'Kind' @k1 -> k2@
+ mkArrowKind :: Kind -> Kind -> Kind
+ mkArrowKind k1 k2 = FunTy k1 k2
+ -- | Iterated application of 'mkArrowKind'
+ mkArrowKinds :: [Kind] -> Kind -> Kind
+ mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
+ tySuperKind :: SuperKind
+ tySuperKind = kindTyConType tySuperKindTyCon 
  \end{code}
  
  %************************************************************************
  %*                                                                    *
  \subsection[TysPrim-basic]{Basic primitive types (@Char#@, @Int#@, etc.)}
@@@ -66,8 -64,6 +64,7 @@@ extractHsTyNames t
      get (HsParTy ty)           = getl ty
      get (HsBangTy _ ty)        = getl ty
      get (HsRecTy flds)         = extractHsTyNames_s (map cd_fld_type flds)
-     get (HsNumTy _)            = emptyNameSet
 +    get (HsNumberTy _)         = emptyNameSet
      get (HsTyVar tv)           = unitNameSet tv
      get (HsSpliceTy _ fvs _)   = fvs
      get (HsQuasiQuoteTy {})    = emptyNameSet
@@@ -139,15 -139,6 +139,8 @@@ 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 _ (HsNumberTy i) = return (HsNumberTy i)
 +
  rnHsType doc (HsFunTy ty1 ty2) = do
      ty1' <- rnLHsType doc ty1
        -- Might find a for-all as the arg of a function type
@@@ -113,10 -120,8 +120,10 @@@ flatten ctxt t
               return (xi, co, ccs) }
  
  flatten _ v@(TyVarTy _)
-   = return (v, v, emptyCCan)
+   = return (v, mkReflCo v, emptyCCan)
  
- flatten _ t@(LiteralTy _) = return (t, t, emptyCCan)
++flatten _ t@(LiteralTy _) = return (t, mkReflCo t, emptyCCan)
 +
  flatten ctxt (AppTy ty1 ty2)
    = do { (xi1,co1,c1) <- flatten ctxt ty1
         ; (xi2,co2,c2) <- flatten ctxt ty2
@@@ -992,4 -957,107 +960,107 @@@ a.  If this turns out to be impossible
  itself, and so on.
  
  
+ %************************************************************************
+ %*                                                                      *
+ %*          Functional dependencies, instantiation of equations
+ %*                                                                      *
+ %************************************************************************
+ When we spot an equality arising from a functional dependency,
+ we now use that equality (a "wanted") to rewrite the work-item
+ constraint right away.  This avoids two dangers
+  Danger 1: If we send the original constraint on down the pipeline
+            it may react with an instance declaration, and in delicate
+          situations (when a Given overlaps with an instance) that
+          may produce new insoluble goals: see Trac #4952
+  Danger 2: If we don't rewrite the constraint, it may re-react
+            with the same thing later, and produce the same equality
+            again --> termination worries.
+ To achieve this required some refactoring of FunDeps.lhs (nicer
+ now!).  
+ \begin{code}
+ rewriteWithFunDeps :: [Equation]
+                    -> [Xi] 
+                    -> WantedLoc 
+                    -> TcS (Maybe ([Xi], [Coercion], [(EvVar,WantedLoc)])) 
+                                            -- Not quite a WantedEvVar unfortunately
+                                            -- Because our intention could be to make 
+                                            -- it derived at the end of the day
+ -- NB: The flavor of the returned EvVars will be decided by the caller
+ -- Post: returns no trivial equalities (identities)
+ rewriteWithFunDeps eqn_pred_locs xis wloc
+  = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
+       ; let fd_ev_pos :: [(Int,(EvVar,WantedLoc))]
+             fd_ev_pos = concat fd_ev_poss
+             (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
+       ; if null fd_ev_pos then return Nothing
+         else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
+ instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
+ -- Post: Returns the position index as well as the corresponding FunDep equality
+ instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
+                         , fd_pred1 = d1, fd_pred2 = d2 })
+   = do { let tvs = varSetElems qtvs
+        ; tvs' <- mapM instFlexiTcS tvs
+        ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+        ; foldM (do_one subst) [] eqs }
+   where 
+     do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
+        = let sty1 = Type.substTy subst ty1 
+              sty2 = Type.substTy subst ty2 
+          in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
+             else do { ev <- newCoVar sty1 sty2
+                     ; let wl' = push_ctx wl 
+                     ; return $ (i,(ev,wl')):ievs }
+     push_ctx :: WantedLoc -> WantedLoc 
+     push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
+ mkEqnMsg :: (TcPredType, SDoc) 
+          -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
+ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
+   = do  { zpred1 <- TcM.zonkTcPredType pred1
+         ; zpred2 <- TcM.zonkTcPredType pred2
+       ; let { tpred1 = tidyPred tidy_env zpred1
+               ; tpred2 = tidyPred tidy_env zpred2 }
+       ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
+                         nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), 
+                         nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
+       ; return (tidy_env, msg) }
+ rewriteDictParams :: [(Int,(EvVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
+                   -> [Type]                    -- A sequence of types: tys
+                   -> [(Type,Coercion)]         -- Returns: [(ty', co : ty' ~ ty)]
+ rewriteDictParams param_eqs tys
+   = zipWith do_one tys [0..]
+   where
+     do_one :: Type -> Int -> (Type,Coercion)
+     do_one ty n = case lookup n param_eqs of
+                     Just wev -> (get_fst_ty wev, mkCoVarCo (fst wev))
+                     Nothing  -> (ty,             mkReflCo ty) -- Identity
+     get_fst_ty (wev,_wloc) 
+       | EqPred ty1 _ <- evVarPred wev 
+       = ty1 
+       | otherwise 
+       = panic "rewriteDictParams: non equality fundep!?"
+ mkCanonicalFDAsWanted :: [(EvVar,WantedLoc)] -> TcS WorkList
+ mkCanonicalFDAsWanted evlocs
+   = do { ws <- mapM can_as_wanted evlocs
+        ; return (unionWorkLists ws) }
+   where can_as_wanted (ev,loc) = mkCanonicalFEV (EvVarX ev (Wanted loc))
  
 -\end{code}
+ mkCanonicalFDAsDerived :: [(EvVar,WantedLoc)] -> TcS WorkList
+ mkCanonicalFDAsDerived evlocs
+   = do { ws <- mapM can_as_derived evlocs
+        ; return (unionWorkLists ws) }
+   where can_as_derived (ev,loc) = mkCanonicalFEV (EvVarX ev (Derived loc)) 
++\end{code}
Simple merge
Simple merge
@@@ -365,11 -364,6 +364,8 @@@ 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 (HsNumberTy n) = return (HsNumberTy n, natKind)
 +
  kc_hs_type (HsKindSig ty k) = do
      ty' <- kc_check_lhs_type ty (EK k EkKindSig)
      return (HsKindSig ty' k, k)
@@@ -608,13 -602,6 +604,8 @@@ 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 (HsNumberTy n) = return (mkNumberTy n)
 +
  ds_type ty@(HsAppTy _ _)
    = ds_app ty []
  
@@@ -52,6 -54,6 +54,8 @@@ import Maybes ( orElse 
  import Data.Maybe
  import Control.Monad
  import Data.List
++import PrelNames ( addTyFamName, mulTyFamName, expTyFamName )
++
  
  #include "HsVersions.h"
  \end{code}
@@@ -563,7 -561,182 +563,195 @@@ tcLocalInstDecl1 (L loc (InstDecl poly_
            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 TyCon
+ 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
++         -- Check that this in not a built-in name
++       ; when (isBuiltinFamily (tcdName decl))
++              (addErr $ builtinFamilyErr (tcdName decl))
++
+        -- 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 tc }
+ isAssocFamily :: TyCon -> Bool        -- Is an assocaited type
+ isAssocFamily tycon
+   = case tyConFamInst_maybe tycon of
+           Nothing       -> panic "isAssocFamily: no family?!?"
+           Just (fam, _) -> isTyConAssoc fam
++isBuiltinFamily :: Name -> Bool
++isBuiltinFamily tc = tc `elem`
++                        [ addTyFamName, mulTyFamName, expTyFamName ]
++
++builtinFamilyErr :: Name -> SDoc
++builtinFamilyErr name
++  = ptext (sLit "Built-in type familiy") <+> quotes (ppr name) <+>
++    ptext (sLit "may not have user-defined instances.")
++
+ 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
+          -- 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 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}
  
  
@@@ -32,7 -31,7 +32,8 @@@ import Coercio
  import Outputable
  
  import TcRnTypes
+ import TcMType ( isSilentEvVar )
 +import TcTypeNats
  import TcErrors
  import TcSMonad
  import Bag
@@@ -919,9 -1018,9 +1022,9 @@@ doInteractWithInert (CDictCan { cc_id 
    | wfl `canRewrite` ifl
    , tv `elemVarSet` tyVarsOfTypes xis
    = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
-        ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
+        ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromNonEq rewritten_dict) }
  
 --- Class constraint and given equality: use the equality to rewrite
 +-- Implicit parameter and given equality: use the equality to rewrite
  -- the class constraint.
  doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) 
                      (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty }) 
@@@ -1040,69 -1155,6 +1159,69 @@@ doInteractWithInert (CFrozenErr { cc_i
  -- Fall-through case for all other situations
  doInteractWithInert _ workItem = noInteraction workItem
  
- numericReactionsStage workItem inert | isNumWork =
 +numericReactionsStage :: SimplifierStage
-              Nothing  -> inert
++numericReactionsStage _depth workItem inert_s | isNumWork =
 +  do res <- canonicalNum grelevant drelevant wrelevant workItem
 +     return SR
 +       { sr_stop = case numNext res of
 +                     Nothing -> Stop
 +                     Just v  -> ContinueWith v
 +       , sr_new_work = numNewWork res
 +       , sr_inerts =
 +           case numInert res of
-   where (grelevant, drelevant, wrelevant, inert_residual) = getNumInerts inert
++             Nothing  -> inert_s
 +             Just ins -> foldrBag (flip updInertSet) inert_residual ins
 +       }
 +
- numericReactionsStage workItem inert = return
-   SR { sr_inerts    = inert
-      , sr_new_work  = emptyBag
++  where (grelevant, drelevant, wrelevant, inert_residual) = getNumInerts inert_s
 +        isNumWork = case workItem of
 +                      CFunEqCan { cc_fun   = f }  -> isNumFun f
 +                      CDictCan  { cc_class = c }  -> isNumClass c
 +                      _                           -> False
 +
-   in ( unionWorkLists gfuns gcls
-      , unionWorkLists dfuns dcls
-      , unionWorkLists wfuns wcls
++numericReactionsStage _ workItem inert_set = return
++  SR { sr_inerts    = inert_set
++     , sr_new_work  = emptyWorkList
 +     , sr_stop      = ContinueWith workItem
 +     }
 +
 +-- Extract constraints which may interact with numeric predicates.
 +getNumInerts :: InertSet -> (CanonicalCts, CanonicalCts, CanonicalCts, InertSet)
 +getNumInerts i =
 +  let (gfuns, dfuns, wfuns, other_funs) =
 +                                    partitionCCanMap isNumFun (inert_funeqs i)
 +      (gcls, dcls, wcls, other_cls) =
 +                                    partitionCCanMap isNumClass (inert_dicts i)
++  in ( unionBags gfuns gcls
++     , unionBags dfuns dcls
++     , unionBags wfuns wcls
 +     , i { inert_funeqs = other_funs, inert_dicts = other_cls }
 +     )
 +
 +
 +isNumFun :: TyCon -> Bool
 +isNumFun tc = tyConName tc `elem` [ addTyFamName, mulTyFamName, expTyFamName ]
 +
 +-- Does not include 'TypeNat' (it does not interact with numeric predicates).
 +isNumClass :: Class -> Bool
 +isNumClass cls  = className cls == lessThanEqualClassName
 +
 +partitionCCanMap ::
 +  Ord a => (a -> Bool) -> CCanMap a ->
 +                          (CanonicalCts, CanonicalCts, CanonicalCts, CCanMap a)
 +partitionCCanMap p cmap =
 +  let (relw,not_relw) = Map.partitionWithKey (\k _ -> p k) (cts_wanted cmap)
 +      (reld,not_reld) = Map.partitionWithKey (\k _ -> p k) (cts_derived cmap)
 +      (relg,not_relg) = Map.partitionWithKey (\k _ -> p k) (cts_given  cmap)
 +  in ( unionManyBags (Map.elems relg)   -- These our assumptions.
 +     , unionManyBags (Map.elems reld)   -- These are facts implied by the goals.
 +     , unionManyBags (Map.elems relw)   -- These are our goals.
 +     , cmap { cts_wanted  = not_relw
 +            , cts_given   = not_relg
 +            , cts_derived = not_reld
 +            }
 +     )
 +
  -------------------------
  -- Equational Rewriting 
  rewriteDict  :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
@@@ -1978,20 -2073,25 +2140,31 @@@ data LookupInstResul
    = NoInstance
    | GenInst [WantedEvVar] EvTerm 
  
- matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
+ matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
 +
- matchClassInst clas [ ty ] _
++matchClassInst _ clas [ ty ] _
 +  | className clas == typeNatClassName
 +  , Just n <- isNumberTy ty = return (GenInst [] (EvInteger n))
 +
- matchClassInst clas tys loc
++
+ matchClassInst inerts clas tys loc
     = do { let pred = mkClassPred clas tys 
          ; mb_result <- matchClass clas tys
+         ; untch <- getUntouchables
          ; case mb_result of
              MatchInstNo   -> return NoInstance
-             MatchInstMany -> return NoInstance -- defer any reactions of a multitude until 
+             MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
                                                 -- we learn more about the reagent 
-             MatchInstSingle (dfun_id, mb_inst_tys) -> 
+             MatchInstSingle (_,_)
+               | given_overlap untch -> 
+                   do { traceTcS "Delaying instance application" $ 
+                        vcat [ text "Workitem=" <+> pprPredTy (ClassP clas tys)
+                             , text "Silents and their superclasses=" <+> ppr silents_and_their_scs
+                             , text "All given dictionaries=" <+> ppr all_given_dicts ]
+                      ; return NoInstance -- see Note [Instance and Given overlap]
+                      }
+             MatchInstSingle (dfun_id, mb_inst_tys) ->
                do { checkWellStagedDFun pred dfun_id loc
  
        -- It's possible that not all the tyvars are in
Simple merge
@@@ -36,9 -41,10 +41,11 @@@ module TcSMonad 
  
      setWantedTyBind,
  
+     lookupFlatCacheMap, updateFlatCacheMap,
      getInstEnvs, getFamInstEnvs,                -- Getting the environments
      getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
 +    tcsLookupClass, tcsLookupTyCon,
      getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
  
      newFlattenSkolemTy,                         -- Flatten skolems 
@@@ -83,8 -85,8 +86,9 @@@ import FamInstEn
  import qualified TcRnMonad as TcM
  import qualified TcMType as TcM
  import qualified TcEnv as TcM 
 -       ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
 +       ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys
 +       , tcLookupClass, tcLookupTyCon )
+ import Kind
  import TcType
  import DynFlags
  
Simple merge
Simple merge
@@@ -356,9 -355,8 +355,9 @@@ tcTyConsOfType t
       go (FunTy a b)                = go a `plusNameEnv` go b
       go (PredTy (IParam _ ty))     = go ty
       go (PredTy (ClassP cls tys))  = go_tc (classTyCon cls) tys
+      go (PredTy (EqPred ty1 ty2))  = go ty1 `plusNameEnv` go ty2
       go (ForAllTy _ ty)            = go ty
-      go _                          = panic "tcTyConsOfType"
 +     go (LiteralTy _)              = emptyNameEnv
  
       go_tc tc tys = extendNameEnv (go_s tys) (tyConName tc) tc
       go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
@@@ -156,7 -157,7 +157,9 @@@ import TyCo
  
  -- others:
  import DynFlags
- import Name
 -import Name hiding (varName)
++import Name -- hiding (varName)
++            -- We use this to make dictionaries for type literals.
++            -- Perhaps there's a better way to do this?
  import NameSet
  import VarEnv
  import PrelNames
@@@ -1114,16 -1025,10 +1033,11 @@@ tcTyVarsOfType (TyVarTy tv)      = if is
  tcTyVarsOfType (TyConApp _ tys)     = tcTyVarsOfTypes tys
  tcTyVarsOfType (PredTy sty)       = tcTyVarsOfPred sty
  tcTyVarsOfType (FunTy arg res)            = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
 +tcTyVarsOfType (LiteralTy _)        = emptyVarSet
  tcTyVarsOfType (AppTy fun arg)            = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
- tcTyVarsOfType (ForAllTy tyvar ty)  = (tcTyVarsOfType ty `delVarSet` tyvar)
-                                       `unionVarSet` tcTyVarsOfTyVar tyvar
+ tcTyVarsOfType (ForAllTy tyvar ty)  = tcTyVarsOfType ty `delVarSet` tyvar
        -- We do sometimes quantify over skolem TcTyVars
  
- tcTyVarsOfTyVar :: TcTyVar -> TyVarSet
- tcTyVarsOfTyVar tv | isCoVar tv = tcTyVarsOfType (tyVarKind tv)
-                    | otherwise  = emptyVarSet
  tcTyVarsOfTypes :: [Type] -> TyVarSet
  tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
  
index 7488959,0000000..a0e7db6
mode 100644,000000..100644
--- /dev/null
@@@ -1,656 -1,0 +1,666 @@@
-                   , newWantedCoVar
-                   , setWantedCoBind, setDictBind, newDictVar
 +{-# LANGUAGE PatternGuards #-}
 +module TcTypeNats ( canonicalNum, NumericsResult(..) ) where
 +
 +import TcSMonad   ( TcS, Xi
-                   , tcEqType, tcCmpType, pprType
++                  , newCoVar, setCoBind
++                  , newDictVar, setDictBind
 +                  , getWantedLoc
 +                  , tcsLookupTyCon, tcsLookupClass
 +                  , CanonicalCt (..), CanonicalCts
 +                  , mkFrozenError
 +                  , traceTcS
++                  , WorkList, unionWorkList, emptyWorkList
 +                  )
 +import TcRnTypes  ( CtFlavor(..) )
 +import TcCanonical (mkCanonicals)
 +import HsBinds    (EvTerm(..))
 +import Class      ( Class, className, classTyCon )
 +import Type       ( tcView, mkTyConApp, mkNumberTy, isNumberTy
- import Coercion   ( mkUnsafeCoercion )
++                  , eqType, cmpType, pprType
 +                  )
 +import TypeRep    (Type(..))
 +import TyCon      (TyCon, tyConName)
 +import Var        (EvVar)
-   Var x   == Var y    = tcEqType x y
++import Coercion   ( mkUnsafeCo )
 +import Outputable
 +import PrelNames  ( lessThanEqualClassName
 +                  , addTyFamName, mulTyFamName, expTyFamName
 +                  )
 +import Bag        (bagToList, emptyBag, unionManyBags, unionBags)
 +import Data.Maybe (fromMaybe, listToMaybe, maybeToList)
 +import Data.List  (nub, partition, sort)
 +import Control.Monad (msum, mplus, zipWithM, (<=<), guard)
 +
 +import Debug.Trace
 +import Unique(getUnique)
 +import Type(getTyVar)
 +
 +
 +data Term = Var Xi | Num Integer (Maybe Xi)
 +data Op   = Add | Mul | Exp deriving Eq
 +data Prop = EqFun Op Term Term Term
 +          | Leq Term Term
 +          | Eq Term Term
 +
 +commutative :: Op -> Bool
 +commutative op = op == Add || op == Mul
 +
 +associative :: Op -> Bool
 +associative op = op == Add || op == Mul
 +
 +num :: Integer -> Term
 +num n = Num n Nothing
 +
 +opFun :: Op -> (Integer -> Integer -> Integer)
 +opFun x = case x of
 +            Add -> (+)
 +            Mul -> (*)
 +            Exp -> (^)
 +
 +
 +instance Eq Term where
-   compare (Var x)   (Var y)   = tcCmpType x y
++  Var x   == Var y    = eqType x y
 +  Num x _ == Num y _  = x == y
 +  _       == _        = False
 +
 +instance Ord Term where
 +  compare (Num x _) (Num y _) = compare x y
 +  compare (Num _ _) (Var _)   = LT
-   { numNewWork :: CanonicalCts
++  compare (Var x)   (Var y)   = cmpType x y
 +  compare (Var _)   (Num _ _) = GT
 +
 +
 +--------------------------------------------------------------------------------
 +-- Interface with the type checker
 +--------------------------------------------------------------------------------
 +
 +data NumericsResult = NumericsResult
++  { numNewWork :: WorkList
 +  , numInert   :: Maybe CanonicalCts   -- Nothing for "no change"
 +  , numNext    :: Maybe CanonicalCt
 +  }
 +
 +-- We keep the original type in numeric constants to preserve type synonyms.
 +toTerm :: Xi -> Term
 +toTerm xi = case mplus (isNumberTy xi) (isNumberTy =<< tcView xi) of
 +              Just n -> Num n (Just xi)
 +              _      -> Var xi
 +
 +fromTerm :: Term -> Xi
 +fromTerm (Num n mb) = fromMaybe (mkNumberTy n) mb
 +fromTerm (Var xi)   = xi
 +
 +toProp :: CanonicalCt -> Prop
 +toProp (CDictCan { cc_class = c, cc_tyargs = [xi1,xi2] })
 +  | className c == lessThanEqualClassName = Leq (toTerm xi1) (toTerm xi2)
 +
 +toProp (CFunEqCan { cc_fun = tc, cc_tyargs = [xi11,xi12], cc_rhs = xi2 })
 +  | tyConName tc == addTyFamName = EqFun Add t1 t2 t3
 +  | tyConName tc == mulTyFamName = EqFun Mul t1 t2 t3
 +  | tyConName tc == expTyFamName = EqFun Exp t1 t2 t3
 +
 +    where t1 = toTerm xi11
 +          t2 = toTerm xi12
 +          t3 = toTerm xi2
 +
 +toProp p = panic $
 +  "[TcTypeNats.toProp] Unexpected CanonicalCt: " ++ showSDoc (ppr p)
 +
- canonicalNum given derived wanted prop =
++-- XXX: Not doing anything, just trying to get things to compile.
 +canonicalNum :: CanonicalCts -> CanonicalCts -> CanonicalCts -> CanonicalCt ->
 +                TcS NumericsResult
-               , numNewWork = unionBags wanted goals }
++canonicalNum _given _derived _wanted prop =
++  return NumericsResult { numInert    = Nothing
++                        , numNewWork  = emptyWorkList
++                        , numNext     = Just prop
++                        }
++
++{-
 +  case cc_flavor prop of
 +    Wanted {}   -> solveNumWanted given derived wanted prop
 +    Derived {}  -> addNumDerived  given derived wanted prop
 +    Given {}    -> addNumGiven    given derived wanted prop
++-}
 +
 +
++{-
 +solveNumWanted :: CanonicalCts -> CanonicalCts -> CanonicalCts -> CanonicalCt ->
 +                TcS NumericsResult
 +solveNumWanted given derived wanted prop =
 +  do let asmps = map toProp $ bagToList $ unionManyBags [given,derived,wanted]
 +         goal  = toProp prop
 +
 +     numTrace "solveNumWanted" (vmany asmps <+> text "|-" <+> ppr goal)
 +
 +     case solve asmps goal of
 +
 +       Simplified sgs ->
 +         do numTrace "Simplified to" (vmany sgs)
 +            defineDummy (cc_id prop) =<< fromProp goal
 +            evs   <- mapM (newSubGoal <=< fromProp) sgs
 +            goals <- mkCanonicals (cc_flavor prop) evs
 +            return NumericsResult
 +              { numNext = Nothing, numInert = Nothing, numNewWork = goals }
 +
 +       -- XXX: The new wanted might imply some of the existing wanteds...
 +       Improved is ->
 +         do numTrace "Improved by" (vmany is)
 +            evs   <- mapM (newSubGoal <=< fromProp) is
 +            goals <- mkCanonicals (cc_flavor prop) evs
 +            return NumericsResult
 +              { numNext = Just prop, numInert = Nothing, numNewWork = goals }
 +
 +       Impossible -> impossible prop
 +
 +
 +-- XXX: Need to understand derived work better.
 +addNumDerived :: CanonicalCts -> CanonicalCts -> CanonicalCts -> CanonicalCt ->
 +              TcS NumericsResult
 +addNumDerived given derived wanted prop =
 +  do let asmps = map toProp $ bagToList given
 +         goal  = toProp prop
 +
 +     numTrace "addNumDerived" (vmany asmps <+> text "|-" <+> ppr goal)
 +
 +     case solve asmps goal of
 +
 +       Simplified sgs ->
 +         do numTrace "Simplified to" (vmany sgs)
 +            defineDummy (cc_id prop) =<< fromProp goal
 +            evs   <- mapM (newSubGoal <=< fromProp) sgs
 +            goals <- mkCanonicals (cc_flavor prop) evs
 +            return NumericsResult
 +              { numNext = Nothing, numInert = Nothing, numNewWork = goals }
 +
 +       -- XXX: watch out for cycles because of the wanteds being restarted:
 +       -- W => D && D => W, we could solve W by W
 +       -- if W <=> D, then we should simplify W to D, not make it derived.
 +       Improved is ->
 +         do numTrace "Improved by" (vmany is)
 +            evs   <- mapM (newSubGoal <=< fromProp) is
 +            goals <- mkCanonicals (Derived (getWantedLoc prop)) evs
 +            return NumericsResult
 +              { numNext = Just prop, numInert = Just (unionBags given derived)
-               , numNewWork = unionBags wanted facts }
++              , numNewWork = unionWorkList wanted goals }
 +
 +       Impossible -> impossible prop
 +
 +
 +addNumGiven :: CanonicalCts -> CanonicalCts -> CanonicalCts -> CanonicalCt ->
 +              TcS NumericsResult
 +addNumGiven given derived wanted prop =
 +  do let asmps = map toProp (bagToList given)
 +         goal  = toProp prop
 +
 +     numTrace "addNumGiven" (vmany asmps <+> text " /\\ " <+> ppr goal)
 +     case solve asmps goal of
 +
 +       Simplified sgs ->
 +         do numTrace "Simplified to" (vmany sgs)
 +            evs   <- mapM (newFact <=< fromProp) sgs
 +            facts <- mkCanonicals (cc_flavor prop) evs
 +            return NumericsResult
 +              { numNext = Nothing, numInert = Nothing, numNewWork = facts }
 +
 +       Improved is ->
 +         do numTrace "Improved by" (vmany is)
 +            evs <- mapM (newFact <=< fromProp) is
 +            facts <- mkCanonicals (cc_flavor prop) evs
 +            return NumericsResult
 +              { numNext = Just prop, numInert = Just (unionBags given derived)
-        { numNext = Just err, numInert = Nothing, numNewWork = emptyBag }
++              , numNewWork = unionWorkList wanted facts }
 +
 +       Impossible -> impossible prop
++-}
 +
 +impossible :: CanonicalCt -> TcS NumericsResult
 +impossible c =
 +  do numTrace "Impossible" empty
 +     let err = mkFrozenError (cc_flavor c) (cc_id c)
 +     return NumericsResult
- newSubGoal (CvtCo t1 t2)   = newWantedCoVar t1 t2
++       { numNext = Just err, numInert = Nothing, numNewWork = emptyWorkList }
 +
 +
 +
 +data CvtProp  = CvtClass Class [Type]
 +              | CvtCo Type Type
 +
 +fromProp :: Prop -> TcS CvtProp
 +fromProp (Leq t1 t2) =
 +  do cl <- tcsLookupClass lessThanEqualClassName
 +     return (CvtClass cl [ fromTerm t1, fromTerm t2 ])
 +
 +fromProp (Eq t1 t2) = return $ CvtCo (fromTerm t1) (fromTerm t2)
 +
 +fromProp (EqFun op t1 t2 t3) =
 +  do tc <- tcsLookupTyCon $ case op of
 +                              Add -> addTyFamName
 +                              Mul -> mulTyFamName
 +                              Exp -> expTyFamName
 +     return $ CvtCo (mkTyConApp tc [fromTerm t1, fromTerm t2]) (fromTerm t3)
 +
 +
 +newSubGoal :: CvtProp -> TcS EvVar
 +newSubGoal (CvtClass c ts) = newDictVar c ts
-   setWantedCoBind c $ mkUnsafeCoercion t1 t2
++newSubGoal (CvtCo t1 t2)   = newCoVar t1 t2
 +
 +newFact :: CvtProp -> TcS EvVar
 +newFact prop =
 +  do d <- newSubGoal prop
 +     defineDummy d prop
 +     return d
 +
 +
 +-- If we decided that we want to generate evidence terms,
 +-- here we would set the evidence properly.  For now, we skip this
 +-- step because evidence terms are not used for anything, and they
 +-- get quite large, at least, if we start with a small set of axioms.
 +defineDummy :: EvVar -> CvtProp -> TcS ()
 +defineDummy d (CvtClass c ts) =
 +  setDictBind d $ EvAxiom "<=" $ mkTyConApp (classTyCon c) ts
 +
 +defineDummy c (CvtCo t1 t2) =
++  setCoBind c (mkUnsafeCo t1 t2)
 +
 +
 +
 +
 +--------------------------------------------------------------------------------
 +-- The Solver
 +--------------------------------------------------------------------------------
 +
 +
 +data Result = Impossible            -- We know that the goal cannot be solved.
 +            | Simplified [Prop]     -- We reformulated the goal.
 +            | Improved   [Prop]     -- We learned some new facts.
 +
 +solve :: [Prop] -> Prop -> Result
 +solve asmps (Leq a b) =
 +  let ps = propsToOrd asmps
 +  in case isLeq ps a b of
 +       True  -> Simplified []
 +       False ->
 +         case improveLeq ps a b of
 +           Nothing -> Impossible
 +           Just ps -> Improved ps
 +
 +solve asmps prop =
 +  case solveWanted1 prop of
 +    Just sgs -> Simplified sgs
 +    Nothing ->
 +      case msum $ zipWith solveWanted2 asmps (repeat prop) of
 +        Just sgs -> Simplified sgs
 +        Nothing
 +          | solveAC asmps prop  -> Simplified []
 +          | byDistr asmps prop  -> Simplified []
 +          | otherwise ->
 +            case improve1 prop of
 +              Nothing   -> Impossible
 +              Just eqs  ->
 +                case zipWithM improve2 asmps (repeat prop) of
 +                  Nothing   -> Impossible
 +                  Just eqs1 -> Improved (concat (eqs : eqs1))
 +
 +
 +
 +
 +improve1 :: Prop -> Maybe [Prop]
 +improve1 prop =
 +  case prop of
 +
 +    EqFun Add (Num m _) (Num n _) t         -> Just [ Eq (num (m+n)) t ]
 +    EqFun Add (Num 0 _) s         t         -> Just [ Eq s t ]
 +    EqFun Add (Num m _) s         (Num n _)
 +      | m <= n                              -> Just [ Eq (num (n-m)) s ]
 +      | otherwise                           -> Nothing
 +    EqFun Add r s (Num 0 _)             -> Just [ Eq (num 0) r, Eq (num 0) s ]
 +    EqFun Add r         s         t
 +      | r == t                              -> Just [ Eq (num 0) s ]
 +      | s == t                              -> Just [ Eq (num 0) r ]
 +
 +    EqFun Mul (Num m _) (Num n _) t -> Just [ Eq (num (m*n)) t ]
 +    EqFun Mul (Num 0 _) _         t -> Just [ Eq (num 0) t ]
 +    EqFun Mul (Num 1 _) s         t -> Just [ Eq s t ]
 +    EqFun Mul (Num _ _) s         t
 +      | s == t                      -> Just [ Eq (num 0) s ]
 +
 +    EqFun Mul r         s (Num 1 _) -> Just [ Eq (num 1) r, Eq (num 1) s ]
 +    EqFun Mul (Num m _) s (Num n _)
 +      | Just a <- divide n m        -> Just [ Eq (num a) s ]
 +      | otherwise                   -> Nothing
 +
 +
 +    EqFun Exp (Num m _) (Num n _) t -> Just [ Eq (num (m ^ n)) t ]
 +
 +    EqFun Exp (Num 1 _) _         t -> Just [ Eq (num 1) t ]
 +    EqFun Exp (Num _ _) s t
 +      | s == t                      -> Nothing
 +    EqFun Exp (Num m _) s (Num n _) -> do a <- descreteLog m n
 +                                          return [ Eq (num a) s ]
 +
 +    EqFun Exp _ (Num 0 _) t         -> Just [ Eq (num 1) t ]
 +    EqFun Exp r (Num 1 _) t         -> Just [ Eq r t ]
 +    EqFun Exp r (Num m _) (Num n _) -> do a <- descreteRoot m n
 +                                          return [ Eq (num a) r ]
 +
 +    _                               -> Just []
 +
 +improve2 :: Prop -> Prop -> Maybe [ Prop ]
 +improve2 asmp prop =
 +  case asmp of
 +
 +    EqFun Add a1 b1 c1 ->
 +      case prop of
 +        EqFun Add a2 b2 c2
 +          | a1 == a2 && b1 == b2  -> Just [ Eq c1 c2 ]
 +          | a1 == b2 && b1 == a2  -> Just [ Eq c1 c2 ]
 +          | c1 == c2 && a1 == a2  -> Just [ Eq b1 b2 ]
 +          | c1 == c2 && a1 == b2  -> Just [ Eq b1 a2 ]
 +          | c1 == c2 && b1 == b2  -> Just [ Eq a1 a2 ]
 +          | c1 == c2 && b1 == a2  -> Just [ Eq a1 b2 ]
 +        _ -> Just []
 +
 +
 +    EqFun Mul a1 b1 c1 ->
 +      case prop of
 +        EqFun Mul a2 b2 c2
 +          | a1 == a2 && b1 == b2  -> Just [ Eq c1 c2 ]
 +          | a1 == b2 && b1 == a2  -> Just [ Eq c1 c2 ]
 +          | c1 == c2 && b1 == b2, Num m _ <- a1, Num n _ <- a2, m /= n
 +                                  -> Just [ Eq (num 0) b1, Eq (num 0) c1 ]
 +        _ -> Just []
 +
 +
 +    _ -> Just []
 +
 +
 +solveWanted1 :: Prop -> Maybe [ Prop ]
 +solveWanted1 prop =
 +  case prop of
 +
 +    EqFun Add (Num m _) (Num n _) (Num mn _)  | m + n == mn -> Just []
 +    EqFun Add (Num 0 _) s         t           | s == t      -> Just []
 +    EqFun Add r         s         t           | r == s      ->
 +                                                Just [ EqFun Mul (num 2) r t ]
 +
 +    EqFun Mul (Num m _) (Num n _) (Num mn _)  | m * n == mn -> Just []
 +    EqFun Mul (Num 0 _) _         (Num 0 _)                 -> Just []
 +    EqFun Mul (Num 1 _) s         t           | s == t      -> Just []
 +    EqFun Mul r         s         t           | r == s      ->
 +                                                Just [ EqFun Exp r (num 2) t ]
 +
 +    -- Simple normalization of commutative operators
 +    EqFun op  r@(Var _) s@(Num _ _) t         | commutative op ->
 +                                                Just [ EqFun op s r t ]
 +
 +    EqFun Exp (Num m _) (Num n _) (Num mn _)  | m ^ n == mn -> Just []
 +    EqFun Exp (Num 1 _) _         (Num 1 _)                 -> Just []
 +    EqFun Exp _         (Num 0 _) (Num 1 _)                 -> Just []
 +    EqFun Exp r         (Num 1 _) t           | r == t      -> Just []
 +    EqFun Exp r         (Num _ _) t           | r == t      ->
 +                                                Just  [Leq r (num 1)]
 +
 +    _ -> Nothing
 +
 +
 +solveWanted2 :: Prop -> Prop -> Maybe [Prop]
 +solveWanted2 asmp prop =
 +  case (asmp, prop) of
 +
 +    (EqFun op1 r1 s1 t1, EqFun op2 r2 s2 t2)
 +      | op1 == op2 && t1 == t2 &&
 +      (  r1 == r2 && s1 == s2
 +      || commutative op1 && r1 == s2 && s1 == r2
 +      )                         -> Just []
 +
 +    (EqFun Add (Num m _) b c1, EqFun Add (Num n _) d c2)
 +      | c1 == c2 -> if m >= n then Just [ EqFun Add (num (m - n)) b d ]
 +                              else Just [ EqFun Add (num (n - m)) d b ]
 +
 +    (EqFun Mul (Num m _) b c1, EqFun Mul (Num n _) d c2)
 +      | c1 == c2, Just x <- divide m n -> Just [ EqFun Mul (num x) b d ]
 +      | c1 == c2, Just x <- divide n m -> Just [ EqFun Mul (num x) d b ]
 +
 +    -- hm:  m * b = c |- c + b = d <=> (m + 1) * b = d
 +    (EqFun Mul (Num m _) s1 t1, EqFun Add r2 s2 t2)
 +      | t1 == r2 && s1 == s2    -> Just [ EqFun Mul (num (m + 1)) s1 t2 ]
 +      | t1 == s2 && s1 == r2    -> Just [ EqFun Mul (num (m + 1)) r2 t2 ]
 +
 +    _                           -> Nothing
 +
 +
 +--------------------------------------------------------------------------------
 +-- Reasoning about ordering.
 +--------------------------------------------------------------------------------
 +
 +-- This function assumes that the assumptions are acyclic.
 +isLeq :: [(Term, Term)] -> Term -> Term -> Bool
 +isLeq _ (Num 0 _) _         = True
 +isLeq _ (Num m _) (Num n _) = m <= n
 +isLeq _ a b | a == b        = True
 +isLeq ps (Num m _) a        = or [ isLeq ps b a  | (Num x _, b) <- ps, m <= x ]
 +isLeq ps a (Num m _)        = or [ isLeq ps a b  | (b, Num x _) <- ps, x <= m ]
 +isLeq ps a b                = or [ isLeq ps c b  | (a',c)       <- ps, a == a' ]
 +
 +isGt :: [(Term, Term)] -> Term -> Term -> Bool
 +isGt _ (Num m _) (Num n _)  = m > n
 +isGt ps (Num m _) a         = (m > 0) && isLeq ps a (num (m - 1))
 +isGt ps a (Num m _)         = isLeq ps (num (m + 1)) a
 +isGt _ _ _                  = False
 +
 +improveLeq :: [(Term,Term)] -> Term -> Term -> Maybe [Prop]
 +improveLeq ps a b | isLeq ps b a  = Just [Eq a b]
 +                  | isGt ps a b   = Nothing
 +                  | otherwise     = Just []
 +
 +-- Ordering constraints derived from numeric predicates.
 +-- We do not consider equlities because they should be substituted away.
 +propsToOrd :: [Prop] -> [(Term,Term)]
 +propsToOrd props = loop (step [] unconditional)
 +  where
 +  loop ps = let new = filter (`notElem` ps) (step ps conditional)
 +            in if null new then ps else loop (new ++ ps)
 +
 +  step ps = nub . concatMap (toOrd ps)
 +
 +  isConditional (EqFun op _ _ _)  = op == Mul || op == Exp
 +  isConditional _                 = False
 +
 +  (conditional,unconditional)     = partition isConditional props
 +
 +  toOrd _ (Leq a b) = [(a,b)]
 +  toOrd _ (Eq _ _)  = []      -- Would lead to a cycle, should be subst. away
 +  toOrd ps (EqFun op a b c) =
 +    case op of
 +      Add               -> [(a,c),(b,c)]
 +
 +      Mul               -> (guard (isLeq ps (num 1) a) >> return (b,c)) ++
 +                           (guard (isLeq ps (num 1) b) >> return (a,c))
 +      Exp
 +        | Num 0 _ <- a  -> [(c, num 1)]
 +        | a == c        -> [(a, num 1)]
 +        | otherwise     -> (guard (isLeq ps (num 2) a) >> return (b,c)) ++
 +                           (guard (isLeq ps (num 1) b) >> return (a,c))
 +
 +--------------------------------------------------------------------------------
 +-- Associative and Commutative Operators
 +--------------------------------------------------------------------------------
 +
 +-- XXX: It'd be nice to go back to a "small-step" style solve.
 +-- If we can get it to work, it is likely to be simpler,
 +-- and it would be way easier to provide proofs.
 +
 +
 +-- XXX: recursion may non-terminate: x * y = x
 +-- XXX: does not do improvements
 +
 +
 +
 +solveAC :: [Prop] -> Prop -> Bool
 +solveAC ps (EqFun op x y z)
 +  | commutative op && associative op =
 +      (xs_ys === z) || or [ add as xs_ys === r | (as,r) <- cancelCands z ]
 +
 +  where
 +  xs_ys         = add (sums x) (sums y)
 +
 +  candidates c  = [ (a,b) | (a,b,c') <- asmps, c == c' ]
 +
 +  -- (xs,e) `elem` cancelCands g    ==> xs + g = e
 +  cancelCands :: Term -> [([[Term]],Term)]
 +  cancelCands g = do (a,b,c) <- asmps
 +                     let us = filter (all mayCancel)
 +                            $ case () of
 +                                _ | a == g    -> sums b
 +                                  | b == g    -> sums a
 +                                  | otherwise -> [ ]
 +                     guard (not (null us))
 +                     (us,c) : [ (add us vs, e) | (vs,e) <- cancelCands c ]
 +
 +
 +  mayCancel x   = case op of
 +                    Add -> True
 +                    Mul -> isLeq ordProps (num 1) x
 +                    Exp -> False
 +
 +  -- xs `elem` sums a   ==>   sum xs = a
 +  sums a        = [a] : [ p | (b,c) <- candidates a, p <- add (sums b) (sums c)]
 +
 +  add :: [Terms] -> [Terms] -> [Terms]
 +  add as bs     = [ doOp2 (opFun op) u v | u <- as, v <- bs ]
 +
 +  (===) :: [[Term]] -> Term -> Bool
 +  as === b      = any (`elem` sums b) as
 +
 +  -- Facts in a more convenient from
 +  asmps         = [ (a,b,c) | EqFun op' a b c <- ps, op == op' ]
 +  ordProps      = propsToOrd ps
 +
 +
 +solveAC _ _ = False
 +
 +
 +
 +
 +-- Combining sequences of terms with the same operation.
 +-- We preserve a normal form with at most 1 constant and variables sorted.
 +-- Examples:
 +--  (1 + c + y) + (2 + b + z) = 3 + b + c + y + z
 +--  (2 * c * y) * (3 * b * z) = 6 * b * c * y * z
 +
 +type Terms = [Term]
 +
 +doOp2 :: (Integer -> Integer -> Integer) -> Terms -> Terms -> Terms
 +doOp2 op (Num m _ : as) (Num n _ : bs) = num (op m n) : merge as bs
 +doOp2 _ xs ys                          = merge xs ys
 +
 +merge :: Ord a => [a] -> [a] -> [a]
 +merge xs@(a:as) ys@(b:bs)
 +  | a <= b    = a : merge as ys
 +  | otherwise = b : merge xs bs
 +merge [] ys = ys
 +merge xs [] = xs
 +
 +
 +-- XXX: This duplicates a lot of work done by AC.
 +byDistr :: [Prop] -> Prop -> Bool
 +byDistr ps (EqFun op x y z)
 +  -- (a * b + a * c) = x |- a * (b + c) = x
 +  | op == Mul = let zs = sumsFor z
 +                    ps = sumProds x y
 +                in -- pNumTrace "Distr *" (text "zs:" <+> vmany zs <> comma <+> text "ps:" <+> vmany ps) $
 +                   any (`elem` zs) ps
 +
 +  -- a * (b + c) = x |- a * b + a * c = x
 +  | op == Add = let as = sumsFor x
 +                    bs = sumsFor y
 +                    cs = [ doOp2 (opFun op) a b | a <- as, b <- bs ]
 +                    ds = do (a,b,z') <- prods
 +                            guard (z == z')
 +                            sumProds a b
 +                in -- pNumTrace "Distr +" (text "cs:" <+> vmany cs <> comma <+> text "ds:" <+> vmany ds) $
 +                   any (`elem` cs) ds
 +
 +  where
 +  sums      = [ (a,b,c) | EqFun Add a b c <- ps ]
 +  prods     = [ (a,b,c) | EqFun Mul a b c <- ps ]
 +  sumsFor  :: Term -> [[Term]]
 +  sumsFor c = [c] : do (a,b,c') <- sums
 +                       guard (c == c')
 +                       u <- sumsFor a
 +                       v <- sumsFor b
 +                       return (doOp2 (opFun Mul) u v)
 +
 +  -- This is very ad-hock.
 +  prod (Num 1 _, a) = Just a
 +  prod (a, Num 1 _) = Just a
 +  prod (a,b)  = listToMaybe [ c | (a',b',c) <- prods, a == a', b == b' ]
 +
 +  sumProds u v  = do s1 <- sumsFor u
 +                     s2 <- sumsFor v
 +                     maybeToList $
 +                       do s3 <- mapM prod [ (a,b) | a <- s1, b <- s2 ]
 +                          return (sort s3)
 +byDistr _ _ = False
 +
 +
 +
 +
 +--------------------------------------------------------------------------------
 +-- Descrete Math
 +--------------------------------------------------------------------------------
 +
 +descreteRoot :: Integer -> Integer -> Maybe Integer
 +descreteRoot root num = search 0 num
 +  where
 +  search from to = let x = from + div (to - from) 2
 +                       a = x ^ root
 +                   in case compare a num of
 +                        EQ              -> Just x
 +                        LT | x /= from  -> search x to
 +                        GT | x /= to    -> search from x
 +                        _               -> Nothing
 +
 +descreteLog :: Integer -> Integer -> Maybe Integer
 +descreteLog _    0   = Just 0
 +descreteLog base num | base == num  = Just 1
 +descreteLog base num = case divMod num base of
 +                         (x,0) -> fmap (1+) (descreteLog base x)
 +                         _     -> Nothing
 +
 +divide :: Integer -> Integer -> Maybe Integer
 +divide _ 0  = Nothing
 +divide x y  = case divMod x y of
 +                (a,0) -> Just a
 +                _     -> Nothing
 +
 +
 +--------------------------------------------------------------------------------
 +-- Debugging
 +--------------------------------------------------------------------------------
 +
 +numTrace :: String -> SDoc -> TcS ()
 +numTrace x y = traceTcS ("[numerics] " ++ x) y
 +
 +pNumTrace :: String -> SDoc -> a -> a
 +pNumTrace x y = trace ("[numerics] " ++ x ++ " " ++ showSDoc y)
 +
 +vmany :: Outputable a => [a] -> SDoc
 +vmany xs = braces $ hcat $ punctuate comma $ map ppr xs
 +
 +instance Outputable Term where
 +  ppr (Var xi)  = pprType xi <> un
 +    where un = brackets $ text $ show $ getUnique (getTyVar "numerics dbg" xi)
 +  ppr (Num n _) = integer n
 +
 +instance Outputable Prop where
 +  ppr (EqFun op t1 t2 t3) = ppr t1 <+> ppr op <+> ppr t2 <+> char '~' <+> ppr t3
 +  ppr (Leq t1 t2)         = ppr t1 <+> text "<=" <+> ppr t2
 +  ppr (Eq t1 t2)          = ppr t1 <+> char '~'  <+> ppr t2
 +
 +instance Outputable Op where
 +  ppr op  = case op of
 +              Add -> char '+'
 +              Mul -> char '*'
 +              Exp -> char '^'
 +
@@@ -35,6 -35,6 +35,7 @@@ import TcRnMona
  import TcType
  import Type
  import Coercion
++import Kind ( isNatKind )
  import Inst
  import TyCon
  import TysWiredIn
@@@ -582,19 -581,6 +582,9 @@@ uType_np origin orig_ty1 orig_ty
          -- Predicates
      go (PredTy p1) (PredTy p2) = uPred origin p1 p2
  
-       | m == n  = return (IdCo ty1)
-         -- Coercion functions: (t1a ~ t1b) => t1c  ~  (t2a ~ t2b) => t2c
-     go ty1 ty2 
-       | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1, 
-         Just (t2a,t2b,t2c) <- splitCoPredTy_maybe ty2
-       = do { co1 <- uType origin t1a t2a 
-            ; co2 <- uType origin t1b t2b
-            ; co3 <- uType origin t1c t2c 
-            ; return $ mkCoPredCoI co1 co2 co3 }
 +    go ty1@(LiteralTy m) (LiteralTy n)
++      | m == n  = return (mkReflCo ty1)
 +
          -- Functions (or predicate functions) just check the two parts
      go (FunTy fun1 arg1) (FunTy fun2 arg2)
        = do { coi_l <- uType origin fun1 fun2
@@@ -609,102 -737,298 +737,299 @@@ coreEqCoercion2 _ _ _ = Fals
  
  %************************************************************************
  %*                                                                    *
-             CoercionI and its constructors
- %*                                                                    *
+                    Substitution of coercions
+ %*                                                                      *
  %************************************************************************
  
- --------------------------------------
- -- CoercionI smart constructors
- --    lifted smart constructors of ordinary coercions
+ \begin{code}
+ -- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
+ --   doing a \"lifting\" substitution)
+ type CvSubstEnv = VarEnv Coercion
+ emptyCvSubstEnv :: CvSubstEnv
+ emptyCvSubstEnv = emptyVarEnv
+ data CvSubst          
+   = CvSubst InScopeSet        -- The in-scope type variables
+           TvSubstEnv  -- Substitution of types
+             CvSubstEnv  -- Substitution of coercions
+ instance Outputable CvSubst where
+   ppr (CvSubst ins tenv cenv)
+     = brackets $ sep[ ptext (sLit "CvSubst"),
+                     nest 2 (ptext (sLit "In scope:") <+> ppr ins), 
+                     nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
+                     nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
+ emptyCvSubst :: CvSubst
+ emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
+ isEmptyCvSubst :: CvSubst -> Bool
+ isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
+ getCvInScope :: CvSubst -> InScopeSet
+ getCvInScope (CvSubst in_scope _ _) = in_scope
+ zapCvSubstEnv :: CvSubst -> CvSubst
+ zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
+ cvTvSubst :: CvSubst -> TvSubst
+ cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
+ tvCvSubst :: TvSubst -> CvSubst
+ tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
+ extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
+ extendTvSubst (CvSubst in_scope tenv cenv) tv ty
+   = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
+ substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
+ substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
+   = ASSERT( isCoVar old_var )
+     (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
+   where
+     -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
+     -- In that case, mkCoVarCo will return a ReflCoercion, and
+     -- we want to substitute that (not new_var) for old_var
+     new_co    = mkCoVarCo new_var
+     no_change = new_var == old_var && not (isReflCo new_co)
+     new_cenv | no_change = delVarEnv cenv old_var
+              | otherwise = extendVarEnv cenv old_var new_co
+     new_var = uniqAway in_scope subst_old_var
+     subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
+                 -- It's important to do the substitution for coercions,
+                 -- because only they can have free type variables
+ substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
+ substTyVarBndr (CvSubst in_scope tenv cenv) old_var
+   = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
+       (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
+ zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
+ zipOpenCvSubst vs cos
+   | debugIsOn && (length vs /= length cos)
+   = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
+   | otherwise 
+   = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
+ mkTopCvSubst :: [(Var,Coercion)] -> CvSubst
+ mkTopCvSubst prs = CvSubst emptyInScopeSet emptyTvSubstEnv (mkVarEnv prs)
+ substCoWithTy :: TyVar -> Type -> Coercion -> Coercion
+ substCoWithTy tv ty = substCoWithTys [tv] [ty]
+ substCoWithTys :: [TyVar] -> [Type] -> Coercion -> Coercion
+ substCoWithTys tvs tys co
+   | debugIsOn && (length tvs /= length tys)
+   = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
+   | otherwise 
+   = ASSERT( length tvs == length tys )
+     substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
+   where
+     in_scope = mkInScopeSet (tyVarsOfTypes tys)
+ -- | Substitute within a 'Coercion'
+ substCo :: CvSubst -> Coercion -> Coercion
+ substCo subst co | isEmptyCvSubst subst = co
+                  | otherwise            = subst_co subst co
+ -- | Substitute within several 'Coercion's
+ substCos :: CvSubst -> [Coercion] -> [Coercion]
+ substCos subst cos | isEmptyCvSubst subst = cos
+                    | otherwise            = map (substCo subst) cos
+ substTy :: CvSubst -> Type -> Type
+ substTy subst = Type.substTy (cvTvSubst subst)
+ subst_co :: CvSubst -> Coercion -> Coercion
+ subst_co subst co
+   = go co
+   where
+     go_ty :: Type -> Type
+     go_ty = Coercion.substTy subst
+     go :: Coercion -> Coercion
+     go (Refl ty)             = Refl $! go_ty ty
+     go (TyConAppCo tc cos)   = let args = map go cos
+                                in  args `seqList` TyConAppCo tc args
+     go (AppCo co1 co2)       = mkAppCo (go co1) $! go co2
+     go (ForAllCo tv co)      = case substTyVarBndr subst tv of
+                                  (subst', tv') ->
+                                    ForAllCo tv' $! subst_co subst' co
+     go (CoVarCo cv)          = substCoVar subst cv
+     go (AxiomInstCo con cos) = AxiomInstCo con $! map go cos
+     go (UnsafeCo ty1 ty2)    = (UnsafeCo $! go_ty ty1) $! go_ty ty2
+     go (SymCo co)            = mkSymCo (go co)
+     go (TransCo co1 co2)     = mkTransCo (go co1) (go co2)
+     go (NthCo d co)          = mkNthCo d (go co)
+     go (InstCo co ty)        = mkInstCo (go co) $! go_ty ty
+ substCoVar :: CvSubst -> CoVar -> Coercion
+ substCoVar (CvSubst in_scope _ cenv) cv
+   | Just co  <- lookupVarEnv cenv cv      = co
+   | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
+   | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv )
+                 ASSERT( isCoVar cv ) CoVarCo cv
+ substCoVars :: CvSubst -> [CoVar] -> [Coercion]
+ substCoVars subst cvs = map (substCoVar subst) cvs
+ lookupTyVar :: CvSubst -> TyVar  -> Maybe Type
+ lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
+ lookupCoVar :: CvSubst -> Var  -> Maybe Coercion
+ lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
+                    "Lifting" substitution
+          [(TyVar,Coercion)] -> Type -> Coercion
+ %*                                                                      *
+ %************************************************************************
  
  \begin{code}
- -- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
- -- can represent either one of:
- --
- -- 1. A proper 'Coercion'
+ liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
+ liftCoSubstWith tvs cos = liftCoSubst (zipOpenCvSubst tvs cos)
+ -- | The \"lifting\" operation which substitutes coercions for type
+ --   variables in a type to produce a coercion.
  --
- -- 2. The identity coercion
- data CoercionI = IdCo Type | ACo Coercion
+ --   For the inverse operation, see 'liftCoMatch' 
+ liftCoSubst :: CvSubst -> Type -> Coercion
+ -- The CvSubst maps TyVar -> Type      (mainly for cloning foralls)
+ --                  TyVar -> Coercion  (this is the payload)
+ -- The unusual thing is that the *coercion* substitution maps
+ -- some *type* variables. That's the whole point of this function!
+ liftCoSubst subst ty | isEmptyCvSubst subst = Refl ty
+                      | otherwise            = ty_co_subst subst ty
+ ty_co_subst :: CvSubst -> Type -> Coercion
+ ty_co_subst subst ty
+   = go ty
+   where
+     go (TyVarTy tv)      = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv)
+     go (AppTy ty1 ty2)   = mkAppCo (go ty1) (go ty2)
+     go (TyConApp tc tys) = mkTyConAppCo tc (map go tys)
+     go (FunTy ty1 ty2)   = mkFunCo (go ty1) (go ty2)
+     go (ForAllTy v ty)   = mkForAllCo v' $! (ty_co_subst subst' ty)
+                          where
+                            (subst', v') = liftCoSubstTyVarBndr subst v
+     go (PredTy p)        = mkPredCo (go <$> p)
++    go ty@(LiteralTy _)  = mkReflCo ty
+ liftCoSubstTyVar :: CvSubst -> TyVar -> Maybe Coercion
+ liftCoSubstTyVar subst@(CvSubst _ tenv cenv) tv
+   = case (lookupVarEnv tenv tv, lookupVarEnv cenv tv) of
+       (Nothing, Nothing) -> Nothing
+       (Just ty, Nothing) -> Just (Refl ty)
+       (Nothing, Just co) -> Just co
+       (Just {}, Just {}) -> pprPanic "ty_co_subst" (ppr tv $$ ppr subst)
+                                     
+ liftCoSubstTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
+ liftCoSubstTyVarBndr (CvSubst in_scope tenv cenv) old_var
+   = (CvSubst (in_scope `extendInScopeSet` new_var) 
+              new_tenv
+              (delVarEnv cenv old_var) -- See Note [Lifting substitutions]
+     , new_var)                
+   where
+     new_tenv | no_change = delVarEnv tenv old_var
+            | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
  
- liftCoI :: (Type -> Type) -> CoercionI -> CoercionI
- liftCoI f (IdCo ty) = IdCo (f ty)
- liftCoI f (ACo ty)  = ACo (f ty)
+     no_change = new_var == old_var
+     new_var = uniqAway in_scope old_var
+ \end{code}
+ Note [Lifting substitutions]
+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ Consider liftCoSubstWith [a] [co] (a, forall a. a)
+ Then we want to substitute for the free 'a', but obviously not for
+ the bound 'a'.  hence the (delVarEnv cent old_var) in liftCoSubstTyVarBndr.
  
- liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI
- liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2)
- liftCoI2 f coi1       coi2       = ACo (f (fromCoI coi1) (fromCoI coi2))
+ This also why we need a full CvSubst when doing lifting substitutions.
  
- liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI
- liftCoIs f cois = go_id [] cois
+ \begin{code}
+ -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
+ --   @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
+ --   That is, it matches a type against a coercion of the same
+ --   "shape", and returns a lifting substitution which could have been
+ --   used to produce the given coercion from the given type.
+ liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe CvSubst
+ liftCoMatch tmpls ty co 
+   = case ty_co_match menv (emptyVarEnv, emptyVarEnv) ty co of
+       Just (tv_env, cv_env) -> Just (CvSubst in_scope tv_env cv_env)
+       Nothing               -> Nothing
    where
-     go_id rev_tys []               = IdCo (f (reverse rev_tys))
-     go_id rev_tys (IdCo ty : cois) = go_id  (ty:rev_tys) cois
-     go_id rev_tys (ACo  co : cois) = go_aco (co:rev_tys) cois
-     go_aco rev_tys []               = ACo (f (reverse rev_tys))
-     go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois
-     go_aco rev_tys (ACo  co : cois) = go_aco (co:rev_tys) cois
- instance Outputable CoercionI where
-   ppr (IdCo _) = ptext (sLit "IdCo")
-   ppr (ACo co) = ppr co
- isIdentityCoI :: CoercionI -> Bool
- isIdentityCoI (IdCo _) = True
- isIdentityCoI (ACo _)  = False
- -- | Return either the 'Coercion' contained within the 'CoercionI' or the given
- -- 'Type' if the 'CoercionI' is the identity 'Coercion'
- fromCoI :: CoercionI -> Type
- fromCoI (IdCo ty) = ty        -- Identity coercion represented 
- fromCoI (ACo co)  = co        --      by the type itself
- -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
- mkSymCoI :: CoercionI -> CoercionI
- mkSymCoI (IdCo ty) = IdCo ty
- mkSymCoI (ACo co)  = ACo $ mkCoercion symCoercionTyCon [co] 
-                               -- the smart constructor
-                               -- is too smart with tyvars
- -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
- mkTransCoI :: CoercionI -> CoercionI -> CoercionI
- mkTransCoI (IdCo _) aco = aco
- mkTransCoI aco (IdCo _) = aco
- mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
- -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
- mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI
- mkTyConAppCoI tyCon cois = liftCoIs (mkTyConApp tyCon) cois
- -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
- mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
- mkAppTyCoI = liftCoI2 mkAppTy
- mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
- mkFunTyCoI = liftCoI2 mkFunTy
- -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
- mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
- mkForAllTyCoI tv = liftCoI (ForAllTy tv)
- -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
- --
- -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
- mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
- mkClassPPredCoI cls = liftCoIs (PredTy . ClassP cls)
+     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
+     in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
+     -- Like tcMatchTy, assume all the interesting variables 
+     -- in ty are in tmpls
+ type TyCoSubstEnv = (TvSubstEnv, CvSubstEnv)
+      -- Used locally inside ty_co_match only
+ -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
+ ty_co_match :: MatchEnv -> TyCoSubstEnv -> Type -> Coercion -> Maybe TyCoSubstEnv
+ ty_co_match menv subst ty co | Just ty' <- coreView ty = ty_co_match menv subst ty' co
+    -- Deal with the Refl case by delegating to type matching
+ ty_co_match menv (tenv, cenv) ty co
+   | Just ty' <- isReflCo_maybe co
+   = case ruleMatchTyX ty_menv tenv ty ty' of
+       Just tenv' -> Just (tenv', cenv) 
+       Nothing    -> Nothing
+   where
+     ty_menv = menv { me_tmpls = me_tmpls menv `minusUFM` cenv }
+     -- Remove from the template set any variables already bound to non-refl coercions
+   -- Match a type variable against a non-refl coercion
+ ty_co_match menv subst@(tenv, cenv) (TyVarTy tv1) co
+   | Just {} <- lookupVarEnv tenv tv1'      -- tv1' is already bound to (Refl ty)
+   = Nothing    -- The coercion 'co' is not Refl
+   | Just co1' <- lookupVarEnv cenv tv1'      -- tv1' is already bound to co1
+   = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
+     then Just subst
+     else Nothing       -- no match since tv1 matches two different coercions
+   | tv1' `elemVarSet` me_tmpls menv           -- tv1' is a template var
+   = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
+     then Nothing      -- occurs check failed
+     else return (tenv, extendVarEnv cenv tv1' co)
+         -- BAY: I don't think we need to do any kind matching here yet
+         -- (compare 'match'), but we probably will when moving to SHE.
+   | otherwise    -- tv1 is not a template ty var, so the only thing it
+                  -- can match is a reflexivity coercion for itself.
+                -- But that case is dealt with already
+   = Nothing
  
- -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
- mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI 
- mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
+   where
+     rn_env = me_env menv
+     tv1' = rnOccL rn_env tv1
+ ty_co_match menv subst (AppTy ty1 ty2) co
+   | Just (co1, co2) <- splitAppCo_maybe co    -- c.f. Unify.match on AppTy
+   = do { subst' <- ty_co_match menv subst ty1 co1 
+        ; ty_co_match menv subst' ty2 co2 }
+ ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos)
+   | tc1 == tc2 = ty_co_matches menv subst tys cos
  
- -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
- mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
- mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
+ ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
+   | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
  
- mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI 
- mkCoPredCoI coi1 coi2 coi3 =   mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3
+ ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co) 
+   = ty_co_match menv' subst ty co
+   where
+     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
  
+ ty_co_match _ _ _ _ = Nothing
  
+ ty_co_matches :: MatchEnv -> TyCoSubstEnv -> [Type] -> [Coercion] -> Maybe TyCoSubstEnv
+ ty_co_matches menv = matchList (ty_co_match menv)
  \end{code}
  
  %************************************************************************
@@@ -755,113 -1073,38 +1074,38 @@@ coercionType co = case coercionKind co 
  --
  -- > c :: (t1 ~ t2)
  --
- -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, 
- -- then @coercionKind c = (t1, t2)@.
- coercionKind :: Coercion -> (Type, Type)
- coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
-                             | otherwise = (ty, ty)
- coercionKind (AppTy ty1 ty2) 
-   = let (s1, t1) = coercionKind ty1
-         (s2, t2) = coercionKind ty2 in
-     (mkAppTy s1 s2, mkAppTy t1 t2)
- coercionKind co@(TyConApp tc args)
-   | Just (ar, desc) <- isCoercionTyCon_maybe tc 
-     -- CoercionTyCons carry their kinding rule, so we use it here
-   = WARN( not (length args >= ar), ppr co )   -- Always saturated
-     (let (ty1,  ty2)  = coTyConAppKind desc (take ar args)
-        (tys1, tys2) = coercionKinds (drop ar args)
-      in (mkAppTys ty1 tys1, mkAppTys ty2 tys2))
-   | otherwise
-   = let (lArgs, rArgs) = coercionKinds args in
-     (TyConApp tc lArgs, TyConApp tc rArgs)
- coercionKind (FunTy ty1 ty2) 
-   = let (t1, t2) = coercionKind ty1
-         (s1, s2) = coercionKind ty2 in
-     (mkFunTy t1 s1, mkFunTy t2 s2)
- coercionKind t@(LiteralTy _)  = (t,t)
- coercionKind (ForAllTy tv ty)
-   | isCoVar tv
- --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
- --    ----------------------------------------------
- --    c1~c2 => c3  ::  (s1~t1) => r1 ~ (s2~t2) => r2
- --      or
- --    forall (_:c1~c2)
-   = let (c1,c2) = coVarKind tv
-       (s1,s2) = coercionKind c1
-       (t1,t2) = coercionKind c2
-       (r1,r2) = coercionKind ty
-     in
-     (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2)
-   | otherwise
- --     c1 :: s1~s2  c2 :: t1~t2   c3 :: r1~r2
- --   ----------------------------------------------
- --    forall a:k. c :: forall a:k. t1 ~ forall a:k. t2
-   = let (ty1, ty2) = coercionKind ty in
-     (ForAllTy tv ty1, ForAllTy tv ty2)
- coercionKind (PredTy (ClassP cl args)) 
-   = let (lArgs, rArgs) = coercionKinds args in
-     (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
- coercionKind (PredTy (IParam name ty))
-   = let (ty1, ty2) = coercionKind ty in
-     (PredTy (IParam name ty1), PredTy (IParam name ty2))
- coercionKind (PredTy (EqPred c1 c2)) 
-   = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
-   -- These should not show up in coercions at all
-   -- becuase they are in the form of for-alls
-     let k1 = coercionKindPredTy c1
-         k2 = coercionKindPredTy c2 in
-     (k1,k2)
-   where
-     coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
+ -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
+ coercionKind :: Coercion -> Pair Type
+ coercionKind (Refl ty)            = Pair ty ty
+ coercionKind (TyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map coercionKind cos)
+ coercionKind (AppCo co1 co2)      = mkAppTy <$> coercionKind co1 <*> coercionKind co2
+ coercionKind (ForAllCo tv co)     = mkForAllTy tv <$> coercionKind co
+ coercionKind (CoVarCo cv)         = ASSERT( isCoVar cv ) toPair $ coVarKind cv
+ coercionKind (AxiomInstCo ax cos) = let Pair tys1 tys2 = coercionKinds cos
+                                     in  Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax)) 
+                                              (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax))
+ coercionKind (UnsafeCo ty1 ty2)   = Pair ty1 ty2
+ coercionKind (SymCo co)           = swap $ coercionKind co
+ coercionKind (TransCo co1 co2)    = Pair (pFst $ coercionKind co1) (pSnd $ coercionKind co2)
+ coercionKind (NthCo d co)         = getNth d <$> coercionKind co
+ coercionKind co@(InstCo aco ty)    | Just ks <- splitForAllTy_maybe `traverse` coercionKind aco
+                                   = (\(tv, body) -> substTyWith [tv] [ty] body) <$> ks
+                                 | otherwise = pprPanic "coercionKind" (ppr co)
  
- ------------------
  -- | Apply 'coercionKind' to multiple 'Coercion's
- coercionKinds :: [Coercion] -> ([Type], [Type])
- coercionKinds tys = unzip $ map coercionKind tys
+ coercionKinds :: [Coercion] -> Pair [Type]
+ coercionKinds tys = sequenceA $ map coercionKind tys
  
- ------------------
- -- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon',
- -- and constructs the types that the resulting coercion relates.
- -- Fails (in the monad) if ill-kinded.
- -- Typically the monad is 
- --   either the Lint monad (with the consistency-check flag = True), 
- --   or the ID monad with a panic on failure (and the consistency-check flag = False)
- coTyConAppKind 
-     :: CoTyConDesc
-     -> [Type]                 -- Exactly right number of args
-     -> (Type, Type)           -- Kind of this application
- coTyConAppKind CoUnsafe (ty1:ty2:_)
-   = (ty1,ty2)
- coTyConAppKind CoSym (co:_) 
-   | (ty1,ty2) <- coercionKind co = (ty2,ty1)
- coTyConAppKind CoTrans (co1:co2:_) 
-   = (fst (coercionKind co1), snd (coercionKind co2))
- coTyConAppKind CoLeft (co:_) 
-   | Just (res,_) <- decompLR_maybe (coercionKind co) = res
- coTyConAppKind CoRight (co:_) 
-   | Just (_,res) <- decompLR_maybe (coercionKind co) = res
- coTyConAppKind CoCsel1 (co:_) 
-   | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res
- coTyConAppKind CoCsel2 (co:_) 
-   | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res
- coTyConAppKind CoCselR (co:_) 
-   | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res
- coTyConAppKind CoInst (co:ty:_) 
-   | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co)
-   = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2) 
- coTyConAppKind (CoAxiom { co_ax_tvs = tvs 
-                         , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
-   = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
-   where
-     (tys1, tys2) = coercionKinds cos
- coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat 
-                              [ ppr co <+> dcolon <+> pprEqPred (coercionKind co)
-                              | co <- cos ])) $
-                           coercionKind (head cos)
+ getNth :: Int -> Type -> Type
+ getNth n ty | Just (_, tys) <- splitTyConApp_maybe ty
+             = ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
+ getNth n ty = pprPanic "getNth" (ppr n <+> ppr ty)
+ \end{code}
+ \begin{code}
+ applyCo :: Type -> Coercion -> Type
+ -- Gives the type of (e co) where e :: (a~b) => ty
+ applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
+ applyCo (FunTy _ ty) _ = ty
+ applyCo _            _ = panic "applyCo"
 -\end{code}
 +\end{code}
@@@ -503,7 -507,6 +507,7 @@@ normaliseType env t
    | Just ty' <- coreView ty = normaliseType env ty' 
  normaliseType env (TyConApp tc tys)
    = normaliseTcApp env tc tys
- normaliseType _env ty@(LiteralTy _) = (IdCo ty, ty)
++normaliseType _env ty@(LiteralTy _) = (Refl ty, ty)
  normaliseType env (AppTy ty1 ty2)
    = let (coi1,nty1) = normaliseType env ty1
          (coi2,nty2) = normaliseType env ty2
index 0000000,0594f7f..ebd8a53
mode 000000,100644..100644
--- /dev/null
@@@ -1,0 -1,235 +1,250 @@@
 --- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
+ %
+ % (c) The University of Glasgow 2006
+ %
+ \begin{code}
+ module Kind (
+         -- * Main data type
+         Kind, typeKind,
+       -- Kinds
+       liftedTypeKind, unliftedTypeKind, openTypeKind,
+         argTypeKind, ubxTupleKind,
+         mkArrowKind, mkArrowKinds,
+         -- Kind constructors...
+         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
+         argTypeKindTyCon, ubxTupleKindTyCon,
+         -- Super Kinds
+       tySuperKind, tySuperKindTyCon, 
+         
+       pprKind, pprParendKind,
+         -- ** Deconstructing Kinds
+         kindFunResult, kindAppResult, synTyConResKind,
+         splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
+         -- ** Predicates on Kinds
+         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
+         isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
+         isSuperKind, isCoercionKind, 
+         isLiftedTypeKindCon,
++        isNatKind, isNatKindCon,
+         isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind,
+         isSubKindCon,
+        ) where
+ #include "HsVersions.h"
+ import TypeRep
+ import TysPrim
+ import TyCon
+ import Var
+ import PrelNames
+ import Outputable
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
+         Predicates over Kinds
+ %*                                                                    *
+ %************************************************************************
+ \begin{code}
+ isTySuperKind :: SuperKind -> Bool
+ isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
+ isTySuperKind _                = False
+ -------------------
+ -- Lastly we need a few functions on Kinds
+ isLiftedTypeKindCon :: TyCon -> Bool
+ isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
++
++isNatKindCon :: TyCon -> Bool
++isNatKindCon tc           =  tc `hasKey` natKindTyConKey
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
+         The kind of a type
+ %*                                                                    *
+ %************************************************************************
+ \begin{code}
+ typeKind :: Type -> Kind
+ typeKind _ty@(TyConApp tc tys) 
+   = ASSERT2( not (tc `hasKey` eqPredPrimTyConKey) || length tys == 2, ppr _ty )
+            -- Assertion checks for unsaturated application of (~)
+            -- See Note [The (~) TyCon] in TysPrim
+     kindAppResult (tyConKind tc) tys
+ typeKind (PredTy pred)              = predKind pred
+ typeKind (AppTy fun _)        = kindFunResult (typeKind fun)
+ typeKind (ForAllTy _ ty)      = typeKind ty
+ typeKind (TyVarTy tyvar)      = tyVarKind tyvar
+ typeKind (FunTy _arg res)
+     -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*), 
+     --              not unliftedTypKind (#)
+     -- The only things that can be after a function arrow are
+     --   (a) types (of kind openTypeKind or its sub-kinds)
+     --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
+     | isTySuperKind k         = k
+     | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind 
+     where
+       k = typeKind res
++typeKind (LiteralTy x)        = tyLitKind x
+ ------------------
+ predKind :: PredType -> Kind
+ predKind (EqPred {}) = unliftedTypeKind       -- Coercions are unlifted
+ predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are
+ predKind (IParam {}) = liftedTypeKind         -- always represented by lifted types
++
++-----------------
++tyLitKind :: TyLit -> Kind
++tyLitKind (NumberTyLit _) = natKind
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
+       Functions over Kinds            
+ %*                                                                    *
+ %************************************************************************
+ \begin{code}
+ -- | Essentially 'funResultTy' on kinds
+ kindFunResult :: Kind -> Kind
+ kindFunResult (FunTy _ res) = res
+ kindFunResult k = pprPanic "kindFunResult" (ppr k)
+ kindAppResult :: Kind -> [arg] -> Kind
+ kindAppResult k []     = k
+ kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
+ -- | Essentially 'splitFunTys' on kinds
+ splitKindFunTys :: Kind -> ([Kind],Kind)
+ splitKindFunTys (FunTy a r) = case splitKindFunTys r of
+                               (as, k) -> (a:as, k)
+ splitKindFunTys k = ([], k)
+ splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
+ splitKindFunTy_maybe (FunTy a r) = Just (a,r)
+ splitKindFunTy_maybe _           = Nothing
+ -- | Essentially 'splitFunTysN' on kinds
+ splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
+ splitKindFunTysN 0 k           = ([], k)
+ splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
+                                    (as, k) -> (a:as, k)
+ splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
+ -- | Find the result 'Kind' of a type synonym, 
+ -- after applying it to its 'arity' number of type variables
+ -- Actually this function works fine on data types too, 
+ -- but they'd always return '*', so we never need to ask
+ synTyConResKind :: TyCon -> Kind
+ synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
+ -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
+ isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
+ isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
+         isUnliftedTypeKindCon, isSubArgTypeKindCon      :: TyCon -> Bool
+ isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
+ isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
+ isOpenTypeKind _               = False
+ isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
+ isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
+ isUbxTupleKind _               = False
+ isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
+ isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
+ isArgTypeKind _               = False
+ isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
+ isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
+ isUnliftedTypeKind _               = False
++isNatKind :: Kind -> Bool
++isNatKind (TyConApp tc [])        = isNatKindCon tc
++isNatKind _                       = False
++
+ isSubOpenTypeKind :: Kind -> Bool
 -\end{code}
++-- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow and Nat)
+ isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) 
+                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) 
+                                      False
++isSubOpenTypeKind k | isNatKind k  = False
+ isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
+ isSubOpenTypeKind other            = ASSERT( isKind other ) False
+          -- This is a conservative answer
+          -- It matters in the call to isSubKind in
+        -- checkExpectedKind.
+ isSubArgTypeKindCon kc
+   | isUnliftedTypeKindCon kc = True
+   | isLiftedTypeKindCon kc   = True
+   | isArgTypeKindCon kc      = True
+   | otherwise                = False
+ isSubArgTypeKind :: Kind -> Bool
+ -- ^ True of any sub-kind of ArgTypeKind 
+ isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
+ isSubArgTypeKind _                = False
+ -- | Is this a super-kind (i.e. a type-of-kinds)?
+ isSuperKind :: Type -> Bool
+ isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
+ isSuperKind _                   = False
+ -- | Is this a kind (i.e. a type-of-types)?
+ isKind :: Kind -> Bool
+ isKind k = isSuperKind (typeKind k)
+ isSubKind :: Kind -> Kind -> Bool
+ -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
+ isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
+ isSubKind (FunTy a1 r1) (FunTy a2 r2)       = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
+ isSubKind _             _                     = False
+ isSubKindCon :: TyCon -> TyCon -> Bool
+ -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
+ isSubKindCon kc1 kc2
+   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
+   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
+   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
++  | isNatKindCon kc1                                       = isNatKindCon kc2
+   | isOpenTypeKindCon kc2                                  = True 
+                            -- we already know kc1 is not a fun, its a TyCon
+   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
+   | otherwise                                              = False
+ defaultKind :: Kind -> Kind
+ -- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
+ -- information on what that means
+ -- When we generalise, we make generic type variables whose kind is
+ -- simple (* or *->* etc).  So generic type variables (other than
+ -- built-in constants like 'error') always have simple kinds.  This is important;
+ -- consider
+ --    f x = True
+ -- We want f to get type
+ --    f :: forall (a::*). a -> Bool
+ -- Not 
+ --    f :: forall (a::??). a -> Bool
+ -- because that would allow a call like (f 3#) as well as (f True),
+ --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
+ defaultKind k 
+   | isSubOpenTypeKind k = liftedTypeKind
+   | isSubArgTypeKind k  = liftedTypeKind
+   | otherwise        = k
++\end{code}
 -%
 -% (c) The University of Glasgow 2006
 -%
 -
 -\begin{code}
 +%\r
 +% (c) The University of Glasgow 2006\r
 +%\r
 +\r
 +\begin{code}\r
- {-# OPTIONS_GHC -w #-}\r
- module OptCoercion (\r
-       optCoercion\r
-    ) where \r
\r
- #include "HsVersions.h"\r
\r
- import Unify  ( tcMatchTy )\r
- import Coercion\r
- import Type\r
- import TypeRep\r
- import TyCon\r
- import Var\r
- import VarSet\r
- import VarEnv\r
- import PrelNames\r
- import Util\r
- import Outputable\r
- \end{code}\r
\r
- %************************************************************************\r
- %*                                                                      *\r
-                  Optimising coercions                                                                 \r
- %*                                                                      *\r
- %************************************************************************\r
\r
- Note [Subtle shadowing in coercions]\r
- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\r
- Supose we optimising a coercion\r
-     optCoercion (forall (co_X5:t1~t2). ...co_B1...)\r
- The co_X5 is a wild-card; the bound variable of a coercion for-all\r
- should never appear in the body of the forall. Indeed we often\r
- write it like this\r
-     optCoercion ( (t1~t2) => ...co_B1... )\r
\r
- Just because it's a wild-card doesn't mean we are free to choose\r
- whatever variable we like.  For example it'd be wrong for optCoercion\r
- to return\r
-    forall (co_B1:t1~t2). ...co_B1...\r
- because now the co_B1 (which is really free) has been captured, and\r
- subsequent substitutions will go wrong.  That's why we can't use\r
- mkCoPredTy in the ForAll case, where this note appears.  \r
\r
- \begin{code}\r
- optCoercion :: TvSubst -> Coercion -> NormalCo\r
- -- ^ optCoercion applies a substitution to a coercion, \r
- --   *and* optimises it to reduce its size\r
- optCoercion env co = opt_co env False co\r
\r
- type NormalCo = Coercion\r
-   -- Invariants: \r
-   --  * The substitution has been fully applied\r
-   --  * For trans coercions (co1 `trans` co2)\r
-   --       co1 is not a trans, and neither co1 nor co2 is identity\r
-   --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)\r
\r
- type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity\r
\r
- opt_co, opt_co' :: TvSubst\r
-                       -> Bool        -- True <=> return (sym co)\r
-                       -> Coercion\r
-                       -> NormalCo     \r
- opt_co = opt_co'\r
\r
- {-    Debuggery \r
- opt_co env sym co \r
- -- = pprTrace "opt_co {" (ppr sym <+> ppr co) $\r
- --                    co1 `seq` \r
- --               pprTrace "opt_co done }" (ppr co1) \r
- --               WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (s1,t1) \r
- --                                   $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )\r
-  =   WARN( not (coreEqType co1 simple_result), \r
-            (text "env=" <+> ppr env) $$\r
-            (text "input=" <+> ppr co) $$\r
-            (text "simple=" <+> ppr simple_result) $$\r
-            (text "opt=" <+> ppr co1) )\r
-      co1\r
-  where\r
-    co1 = opt_co' env sym co\r
-    same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2\r
-    (s,t) = coercionKind (substTy env co)\r
-    (s1,t1) | sym = (t,s)\r
-            | otherwise = (s,t)\r
-    (s2,t2) = coercionKind co1\r
\r
-    simple_result | sym = mkSymCoercion (substTy env co)\r
-                  | otherwise = substTy env co\r
- -}\r
\r
- opt_co' env sym (AppTy ty1 ty2)         = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)\r
- opt_co' env sym (FunTy ty1 ty2)         = FunTy (opt_co env sym ty1) (opt_co env sym ty2)\r
- opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))\r
- opt_co' env sym (PredTy (IParam n ty))    = PredTy (IParam n (opt_co env sym ty))\r
- opt_co' _   _   co@(PredTy (EqPred {}))   = pprPanic "optCoercion" (ppr co)\r
\r
- opt_co' env sym co@(TyVarTy tv)\r
-   | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty\r
-   | not (isCoVar tv)     = co   -- Identity; does not mention a CoVar\r
-   | ty1 `coreEqType` ty2 = ty1        -- Identity; ..ditto..\r
-   | not sym              = co\r
-   | otherwise            = mkSymCoercion co\r
-   where\r
-     (ty1,ty2) = coVarKind tv\r
\r
- opt_co' env sym (ForAllTy tv cor) \r
-   | isTyVar tv  = case substTyVarBndr env tv of\r
-                    (env', tv') -> ForAllTy tv' (opt_co' env' sym cor)\r
\r
- opt_co' env sym co@(ForAllTy co_var cor) \r
-   | isCoVar co_var \r
-   = WARN( co_var `elemVarSet` tyVarsOfType cor, ppr co )\r
-     ForAllTy co_var' cor'\r
-   where\r
-     (co1,co2) = coVarKind co_var\r
-     co1' = opt_co' env sym co1\r
-     co2' = opt_co' env sym co2\r
-     cor' = opt_co' env sym cor\r
-     co_var' = uniqAway (getTvInScope env) (mkWildCoVar (mkCoKind co1' co2'))\r
-     -- See Note [Subtle shadowing in coercions]\r
\r
- opt_co' env sym (TyConApp tc cos)\r
-   | Just (arity, desc) <- isCoercionTyCon_maybe tc\r
-   = mkAppTys (opt_co_tc_app env sym tc desc (take arity cos))\r
-              (map (opt_co env sym) (drop arity cos))\r
-   | otherwise\r
-   = TyConApp tc (map (opt_co env sym) cos)\r
\r
- opt_co' _ _ co@(LiteralTy _) = co\r
\r
- --------\r
- opt_co_tc_app :: TvSubst -> Bool -> TyCon -> CoTyConDesc -> [Coercion] -> NormalCo\r
- -- Used for CoercionTyCons only\r
- -- Arguments are *not* already simplified/substituted\r
- opt_co_tc_app env sym tc desc cos\r
-   = case desc of\r
-       CoAxiom {} -- Do *not* push sym inside top-level axioms\r
-                -- e.g. if g is a top-level axiom\r
-                --   g a : F a ~ a\r
-                -- Then (sym (g ty)) /= g (sym ty) !!\r
-         | sym       -> mkSymCoercion the_co  \r
-         | otherwise -> the_co\r
-         where\r
-            the_co = TyConApp tc (map (opt_co env False) cos)\r
-            -- Note that the_co does *not* have sym pushed into it\r
-     \r
-       CoTrans \r
-         | sym       -> opt_trans opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g\r
-         | otherwise -> opt_trans opt_co1 opt_co2\r
\r
-       CoUnsafe\r
-         | sym       -> mkUnsafeCoercion ty2' ty1'\r
-         | otherwise -> mkUnsafeCoercion ty1' ty2'\r
\r
-       CoSym   -> opt_co env (not sym) co1\r
-       CoLeft  -> opt_lr fst\r
-       CoRight -> opt_lr snd\r
-       CoCsel1 -> opt_csel fstOf3\r
-       CoCsel2 -> opt_csel sndOf3\r
-       CoCselR -> opt_csel thirdOf3\r
\r
-       CoInst        -- See if the first arg is already a forall\r
-                   -- ...then we can just extend the current substitution\r
-         | Just (tv, co1_body) <- splitForAllTy_maybe co1\r
-         -> opt_co (extendTvSubst env tv ty2') sym co1_body\r
\r
-                     -- See if is *now* a forall\r
-         | Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1\r
-         -> substTyWith [tv] [ty2'] opt_co1_body       -- An inefficient one-variable substitution\r
\r
-         | otherwise\r
-         -> TyConApp tc [opt_co1, ty2']\r
\r
-   where\r
-     (co1 : cos1) = cos\r
-     (co2 : _)    = cos1\r
\r
-     ty1' = substTy env co1\r
-     ty2' = substTy env co2\r
\r
-       -- These opt_cos have the sym pushed into them\r
-     opt_co1 = opt_co env sym co1\r
-     opt_co2 = opt_co env sym co2\r
\r
-     the_unary_opt_co = TyConApp tc [opt_co1]\r
\r
-     opt_lr   sel = case splitAppTy_maybe opt_co1 of\r
-                      Nothing -> the_unary_opt_co \r
-                      Just lr -> sel lr\r
-     opt_csel sel = case splitCoPredTy_maybe opt_co1 of\r
-                      Nothing -> the_unary_opt_co \r
-                      Just lr -> sel lr\r
\r
- -------------\r
- opt_transL :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
- opt_transL = zipWith opt_trans\r
\r
- opt_trans :: NormalCo -> NormalCo -> NormalCo\r
- opt_trans co1 co2\r
-   | isIdNormCo co1 = co2\r
-   | otherwise      = opt_trans1 co1 co2\r
\r
- opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo\r
- -- First arg is not the identity\r
- opt_trans1 co1 co2\r
-   | isIdNormCo co2 = co1\r
-   | otherwise      = opt_trans2 co1 co2\r
\r
- opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo\r
- -- Neither arg is the identity\r
- opt_trans2 (TyConApp tc [co1a,co1b]) co2\r
-   | tc `hasKey` transCoercionTyConKey\r
-   = opt_trans1 co1a (opt_trans2 co1b co2)\r
\r
- opt_trans2 co1 co2 \r
-   | Just co <- opt_trans_rule co1 co2\r
-   = co\r
\r
- opt_trans2 co1 (TyConApp tc [co2a,co2b])\r
-   | tc `hasKey` transCoercionTyConKey\r
-   , Just co1_2a <- opt_trans_rule co1 co2a\r
-   = if isIdNormCo co1_2a\r
-     then co2b\r
-     else opt_trans2 co1_2a co2b\r
\r
- opt_trans2 co1 co2\r
-   = mkTransCoercion co1 co2\r
\r
- ------\r
- opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo\r
- opt_trans_rule (TyConApp tc1 args1) (TyConApp tc2 args2)\r
-   | tc1 == tc2\r
-   = case isCoercionTyCon_maybe tc1 of\r
-       Nothing \r
-         -> Just (TyConApp tc1 (opt_transL args1 args2))\r
-       Just (arity, desc) \r
-         | arity == length args1\r
-         -> opt_trans_rule_equal_tc desc args1 args2\r
-         | otherwise\r
-         -> case opt_trans_rule_equal_tc desc \r
-                          (take arity args1) \r
-                          (take arity args2) of\r
-               Just co -> Just $ mkAppTys co $ \r
-                          opt_transL (drop arity args1) (drop arity args2)\r
-             Nothing -> Nothing \r
-  \r
- -- Push transitivity inside apply\r
- opt_trans_rule co1 co2\r
-   | Just (co1a, co1b) <- splitAppTy_maybe co1\r
-   , Just (co2a, co2b) <- etaApp_maybe co2\r
-   = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
\r
-   | Just (co2a, co2b) <- splitAppTy_maybe co2\r
-   , Just (co1a, co1b) <- etaApp_maybe co1\r
-   = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
\r
- -- Push transitivity inside (s~t)=>r\r
- -- We re-use the CoVar rather than using mkCoPredTy\r
- -- See Note [Subtle shadowing in coercions]\r
- opt_trans_rule co1 co2\r
-   | Just (cv1,r1) <- splitForAllTy_maybe co1\r
-   , isCoVar cv1\r
-   , Just (s1,t1) <- coVarKind_maybe cv1\r
-   , Just (s2,t2,r2) <- etaCoPred_maybe co2\r
-   = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
-                    (opt_trans r1 r2))\r
\r
-   | Just (cv2,r2) <- splitForAllTy_maybe co2\r
-   , isCoVar cv2\r
-   , Just (s2,t2) <- coVarKind_maybe cv2\r
-   , Just (s1,t1,r1) <- etaCoPred_maybe co1\r
-   = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
-                    (opt_trans r1 r2))\r
\r
- -- Push transitivity inside forall\r
- opt_trans_rule co1 co2\r
-   | Just (tv1,r1) <- splitTypeForAll_maybe co1\r
-   , Just (tv2,r2) <- etaForAll_maybe co2\r
-   , let r2' = substTyWith [tv2] [TyVarTy tv1] r2\r
-   = Just (ForAllTy tv1 (opt_trans2 r1 r2'))\r
\r
-   | Just (tv2,r2) <- splitTypeForAll_maybe co2\r
-   , Just (tv1,r1) <- etaForAll_maybe co1\r
-   , let r1' = substTyWith [tv1] [TyVarTy tv2] r1\r
-   = Just (ForAllTy tv1 (opt_trans2 r1' r2))\r
\r
- opt_trans_rule co1 co2\r
- {-    Omitting for now, because unsound\r
-   | Just (sym1, (ax_tc1, ax1_args, ax_tvs, ax_lhs, ax_rhs)) <- co1_is_axiom_maybe\r
-   , Just (sym2, (ax_tc2, ax2_args, _, _, _)) <- co2_is_axiom_maybe\r
-   , ax_tc1 == ax_tc2\r
-   , sym1 /= sym2\r
-   = Just $\r
-     if sym1 \r
-     then substTyWith ax_tvs (opt_transL (map mkSymCoercion ax1_args) ax2_args) ax_rhs\r
-     else substTyWith ax_tvs (opt_transL ax1_args (map mkSymCoercion ax2_args)) ax_lhs\r
- -}\r
\r
-   | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- co1_is_axiom_maybe\r
-   , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co2\r
-   = Just $ \r
-     if sym \r
-     then mkSymCoercion $ TyConApp ax_tc (opt_transL (map mkSymCoercion cos) ax_args)\r
-     else                 TyConApp ax_tc (opt_transL ax_args cos)\r
\r
-   | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- isAxiom_maybe co2\r
-   , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co1\r
-   = Just $ \r
-     if sym \r
-     then mkSymCoercion $ TyConApp ax_tc (opt_transL ax_args (map mkSymCoercion cos))\r
-     else                 TyConApp ax_tc (opt_transL cos ax_args)\r
-   where\r
-     co1_is_axiom_maybe = isAxiom_maybe co1\r
-     co2_is_axiom_maybe = isAxiom_maybe co2\r
\r
- opt_trans_rule co1 co2        -- Identity rule\r
-   | (ty1,_) <- coercionKind co1\r
-   , (_,ty2) <- coercionKind co2\r
-   , ty1 `coreEqType` ty2\r
-   = Just ty2\r
\r
- opt_trans_rule _ _ = Nothing\r
\r
- -----------  \r
- isAxiom_maybe :: Coercion -> Maybe (Bool, (TyCon, [Coercion], [TyVar], Type, Type))\r
- isAxiom_maybe co\r
-   | Just (tc, args) <- splitTyConApp_maybe co\r
-   , Just (_, desc)  <- isCoercionTyCon_maybe tc\r
-   = case desc of\r
-       CoAxiom { co_ax_tvs = tvs, co_ax_lhs = lhs, co_ax_rhs = rhs } \r
-             -> Just (False, (tc, args, tvs, lhs, rhs))\r
-       CoSym | (arg1:_) <- args  \r
-             -> case isAxiom_maybe arg1 of\r
-                  Nothing           -> Nothing\r
-                  Just (sym, stuff) -> Just (not sym, stuff)\r
-       _ -> Nothing\r
-   | otherwise\r
-   = Nothing\r
\r
- matchesAxiomLhs :: [TyVar] -> Type -> Type -> Maybe [Type]\r
- matchesAxiomLhs tvs ty_tmpl ty \r
-   = case tcMatchTy (mkVarSet tvs) ty_tmpl ty of\r
-       Nothing    -> Nothing\r
-       Just subst -> Just (map (substTyVar subst) tvs)\r
\r
- -----------  \r
- opt_trans_rule_equal_tc :: CoTyConDesc -> [Coercion] -> [Coercion] -> Maybe Coercion\r
- -- Rules for Coercion TyCons only\r
\r
- -- Push transitivity inside instantiation\r
- opt_trans_rule_equal_tc desc [co1,ty1] [co2,ty2]\r
-   | CoInst <- desc\r
-   , ty1 `coreEqType` ty2\r
-   , co1 `compatible_co` co2\r
-   = Just (mkInstCoercion (opt_trans2 co1 co2) ty1) \r
\r
- opt_trans_rule_equal_tc desc [co1] [co2]\r
-   | CoLeft  <- desc, is_compat = Just (mkLeftCoercion res_co)\r
-   | CoRight <- desc, is_compat = Just (mkRightCoercion res_co)\r
-   | CoCsel1 <- desc, is_compat = Just (mkCsel1Coercion res_co)\r
-   | CoCsel2 <- desc, is_compat = Just (mkCsel2Coercion res_co)\r
-   | CoCselR <- desc, is_compat = Just (mkCselRCoercion res_co)\r
-   where\r
-     is_compat = co1 `compatible_co` co2\r
-     res_co    = opt_trans2 co1 co2\r
\r
- opt_trans_rule_equal_tc _ _ _ = Nothing\r
\r
- -------------\r
- compatible_co :: Coercion -> Coercion -> Bool\r
- -- Check whether (co1 . co2) will be well-kinded\r
- compatible_co co1 co2\r
-   = x1 `coreEqType` x2                \r
-   where\r
-     (_,x1) = coercionKind co1\r
-     (x2,_) = coercionKind co2\r
\r
- -------------\r
- etaForAll_maybe :: Coercion -> Maybe (TyVar, Coercion)\r
- -- Try to make the coercion be of form (forall tv. co)\r
- etaForAll_maybe co\r
-   | Just (tv, r) <- splitForAllTy_maybe co\r
-   , not (isCoVar tv)  -- Check it is a *type* forall, not a (t1~t2)=>co\r
-   = Just (tv, r)\r
\r
-   | (ty1,ty2) <- coercionKind co\r
-   , Just (tv1, _) <- splitTypeForAll_maybe ty1\r
-   , Just (tv2, _) <- splitTypeForAll_maybe ty2\r
-   , tyVarKind tv1 `eqKind` tyVarKind tv2\r
-   = Just (tv1, mkInstCoercion co (mkTyVarTy tv1))\r
\r
-   | otherwise\r
-   = Nothing\r
\r
- etaCoPred_maybe :: Coercion -> Maybe (Coercion, Coercion, Coercion)\r
- etaCoPred_maybe co \r
-   | Just (s,t,r) <- splitCoPredTy_maybe co\r
-   = Just (s,t,r)\r
-   \r
-   --  co :: (s1~t1)=>r1 ~ (s2~t2)=>r2\r
-   | (ty1,ty2) <- coercionKind co      -- We know ty1,ty2 have same kind\r
-   , Just (s1,_,_) <- splitCoPredTy_maybe ty1\r
-   , Just (s2,_,_) <- splitCoPredTy_maybe ty2\r
-   , typeKind s1 `eqKind` typeKind s2  -- t1,t2 have same kinds\r
-   = Just (mkCsel1Coercion co, mkCsel2Coercion co, mkCselRCoercion co)\r
-   \r
-   | otherwise\r
-   = Nothing\r
\r
- etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)\r
- -- Split a coercion g :: t1a t1b ~ t2a t2b\r
- -- into (left g, right g) if possible\r
- etaApp_maybe co\r
-   | Just (co1, co2) <- splitAppTy_maybe co\r
-   = Just (co1, co2)\r
\r
-   | (ty1,ty2) <- coercionKind co\r
-   , Just (ty1a, _) <- splitAppTy_maybe ty1\r
-   , Just (ty2a, _) <- splitAppTy_maybe ty2\r
-   , typeKind ty1a `eqKind` typeKind ty2a\r
-   = Just (mkLeftCoercion co, mkRightCoercion co)\r
\r
-   | otherwise\r
-   = Nothing\r
\r
- -------------\r
- splitTypeForAll_maybe :: Type -> Maybe (TyVar, Type)\r
- -- Returns Just only for a *type* forall, not a (t1~t2)=>co\r
- splitTypeForAll_maybe ty\r
-   | Just (tv, rty) <- splitForAllTy_maybe ty\r
-   , not (isCoVar tv)\r
-   = Just (tv, rty)\r
\r
-   | otherwise\r
-   = Nothing\r
\r
- -------------\r
- isIdNormCo :: NormalCo -> Bool\r
- -- Cheap identity test: look for coercions with no coercion variables at all\r
- -- So it'll return False for (sym g `trans` g)\r
- isIdNormCo ty = go ty\r
-   where\r
-     go (TyVarTy tv)          = not (isCoVar tv)\r
-     go (AppTy t1 t2)         = go t1 && go t2\r
-     go (FunTy t1 t2)         = go t1 && go t2\r
-     go (ForAllTy tv ty)        = go (tyVarKind tv) && go ty\r
-     go (TyConApp tc tys)       = not (isCoercionTyCon tc) && all go tys\r
-     go (PredTy (IParam _ ty))  = go ty\r
-     go (PredTy (ClassP _ tys)) = all go tys\r
-     go (PredTy (EqPred t1 t2)) = go t1 && go t2\r
-     go (LiteralTy _)           = True\r
- \end{code}  \r
\r
+ module OptCoercion ( optCoercion ) where 
+ #include "HsVersions.h"
+ import Coercion
+ import Type hiding( substTyVarBndr, substTy, extendTvSubst )
+ import TyCon
+ import Var
+ import VarSet
+ import VarEnv
+ import StaticFlags    ( opt_NoOptCoercion )
+ import Outputable
+ import Pair
+ import Maybes( allMaybes )
+ import FastString
+ \end{code}
+ %************************************************************************
+ %*                                                                      *
+                  Optimising coercions                                                                 
+ %*                                                                      *
+ %************************************************************************
+ Note [Subtle shadowing in coercions]
+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ Supose we optimising a coercion
+     optCoercion (forall (co_X5:t1~t2). ...co_B1...)
+ The co_X5 is a wild-card; the bound variable of a coercion for-all
+ should never appear in the body of the forall. Indeed we often
+ write it like this
+     optCoercion ( (t1~t2) => ...co_B1... )
+ Just because it's a wild-card doesn't mean we are free to choose
+ whatever variable we like.  For example it'd be wrong for optCoercion
+ to return
+    forall (co_B1:t1~t2). ...co_B1...
+ because now the co_B1 (which is really free) has been captured, and
+ subsequent substitutions will go wrong.  That's why we can't use
+ mkCoPredTy in the ForAll case, where this note appears.  
+ \begin{code}
+ optCoercion :: CvSubst -> Coercion -> NormalCo
+ -- ^ optCoercion applies a substitution to a coercion, 
+ --   *and* optimises it to reduce its size
+ optCoercion env co 
+   | opt_NoOptCoercion = substCo env co
+   | otherwise         = opt_co env False co
+ type NormalCo = Coercion
+   -- Invariants: 
+   --  * The substitution has been fully applied
+   --  * For trans coercions (co1 `trans` co2)
+   --       co1 is not a trans, and neither co1 nor co2 is identity
+   --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
+ type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
+ opt_co, opt_co' :: CvSubst
+                       -> Bool        -- True <=> return (sym co)
+                       -> Coercion
+                       -> NormalCo     
+ opt_co = opt_co'
+ {-
+ opt_co env sym co
+  = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
+    co1 `seq`
+    pprTrace "opt_co done }" (ppr co1) $
+    (WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (Pair s1 t1)
+                          $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )
+     WARN( not (coreEqCoercion co1 simple_result),
+            (text "env=" <+> ppr env) $$
+            (text "input=" <+> ppr co) $$
+            (text "simple=" <+> ppr simple_result) $$
+            (text "opt=" <+> ppr co1) )
+    co1)
+  where
+    co1 = opt_co' env sym co
+    same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
+    Pair s t = coercionKind (substCo env co)
+    (s1,t1) | sym = (t,s)
+            | otherwise = (s,t)
+    Pair s2 t2 = coercionKind co1
+    simple_result | sym = mkSymCo (substCo env co)
+                  | otherwise = substCo env co
+ -}
+ opt_co' env _   (Refl ty)           = Refl (substTy env ty)
+ opt_co' env sym (SymCo co)          = opt_co env (not sym) co
+ opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)
+ opt_co' env sym (AppCo co1 co2)     = mkAppCo (opt_co env sym co1) (opt_co env sym co2)
+ opt_co' env sym (ForAllCo tv co)    = case substTyVarBndr env tv of
+                                          (env', tv') -> mkForAllCo tv' (opt_co env' sym co)
+      -- Use the "mk" functions to check for nested Refls
+ opt_co' env sym (CoVarCo cv)
+   | Just co <- lookupCoVar env cv
+   = opt_co (zapCvSubstEnv env) sym co
+   | Just cv1 <- lookupInScope (getCvInScope env) cv
+   = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)
+                 -- cv1 might have a substituted kind!
+   | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
+                 ASSERT( isCoVar cv )
+                 wrapSym sym (CoVarCo cv)
+ opt_co' env sym (AxiomInstCo con cos)
+     -- Do *not* push sym inside top-level axioms
+     -- e.g. if g is a top-level axiom
+     --   g a : f a ~ a
+     -- then (sym (g ty)) /= g (sym ty) !!
+   = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)
+       -- Note that the_co does *not* have sym pushed into it
+ opt_co' env sym (UnsafeCo ty1 ty2)
+   | ty1' `eqType` ty2' = Refl ty1'
+   | sym                = mkUnsafeCo ty2' ty1'
+   | otherwise          = mkUnsafeCo ty1' ty2'
+   where
+     ty1' = substTy env ty1
+     ty2' = substTy env ty2
+ opt_co' env sym (TransCo co1 co2)
+   | sym       = opt_trans opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
+   | otherwise = opt_trans opt_co1 opt_co2
+   where
+     opt_co1 = opt_co env sym co1
+     opt_co2 = opt_co env sym co2
+ opt_co' env sym (NthCo n co)
+   | TyConAppCo tc cos <- co'
+   , isDecomposableTyCon tc            -- Not synonym families
+   = ASSERT( n < length cos )
+     cos !! n
+   | otherwise
+   = NthCo n co'
+   where
+     co' = opt_co env sym co
+ opt_co' env sym (InstCo co ty)
+     -- See if the first arg is already a forall
+     -- ...then we can just extend the current substitution
+   | Just (tv, co_body) <- splitForAllCo_maybe co
+   = opt_co (extendTvSubst env tv ty') sym co_body
+     -- See if it is a forall after optimization
+   | Just (tv, co'_body) <- splitForAllCo_maybe co'
+   = substCoWithTy tv ty' co'_body   -- An inefficient one-variable substitution
+   | otherwise = InstCo co' ty'
+   where
+     co' = opt_co env sym co
+     ty' = substTy env ty
+ -------------
+ opt_transList :: [NormalCo] -> [NormalCo] -> [NormalCo]
+ opt_transList = zipWith opt_trans
+ opt_trans :: NormalCo -> NormalCo -> NormalCo
+ opt_trans co1 co2
+   | isReflCo co1 = co2
+   | otherwise    = opt_trans1 co1 co2
+ opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
+ -- First arg is not the identity
+ opt_trans1 co1 co2
+   | isReflCo co2 = co1
+   | otherwise    = opt_trans2 co1 co2
+ opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
+ -- Neither arg is the identity
+ opt_trans2 (TransCo co1a co1b) co2
+     -- Don't know whether the sub-coercions are the identity
+   = opt_trans co1a (opt_trans co1b co2)  
+ opt_trans2 co1 co2 
+   | Just co <- opt_trans_rule co1 co2
+   = co
+ opt_trans2 co1 (TransCo co2a co2b)
+   | Just co1_2a <- opt_trans_rule co1 co2a
+   = if isReflCo co1_2a
+     then co2b
+     else opt_trans1 co1_2a co2b
+ opt_trans2 co1 co2
+   = mkTransCo co1 co2
+ ------
+ -- Optimize coercions with a top-level use of transitivity.
+ opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
+ -- push transitivity down through matching top-level constructors.
+ opt_trans_rule in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
+   | tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $
+                  TyConAppCo tc1 (opt_transList cos1 cos2)
+ -- push transitivity through matching destructors
+ opt_trans_rule in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
+   | d1 == d2
+   , co1 `compatible_co` co2
+   = fireTransRule "PushNth" in_co1 in_co2 $
+     mkNthCo d1 (opt_trans co1 co2)
+ -- Push transitivity inside instantiation
+ opt_trans_rule in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
+   | ty1 `eqType` ty2
+   , co1 `compatible_co` co2
+   = fireTransRule "TrPushInst" in_co1 in_co2 $
+     mkInstCo (opt_trans co1 co2) ty1
+  
+ -- Push transitivity inside apply
+ opt_trans_rule in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
+   = fireTransRule "TrPushApp" in_co1 in_co2 $
+     mkAppCo (opt_trans co1a co2a) (opt_trans co1b co2b)
+ opt_trans_rule co1@(TyConAppCo tc cos1) co2
+   | Just cos2 <- etaTyConAppCo_maybe tc co2
+   = ASSERT( length cos1 == length cos2 )
+     fireTransRule "EtaCompL" co1 co2 $
+     TyConAppCo tc (zipWith opt_trans cos1 cos2)
+ opt_trans_rule co1 co2@(TyConAppCo tc cos2)
+   | Just cos1 <- etaTyConAppCo_maybe tc co1
+   = ASSERT( length cos1 == length cos2 )
+     fireTransRule "EtaCompR" co1 co2 $
+     TyConAppCo tc (zipWith opt_trans cos1 cos2)
+ -- Push transitivity inside forall
+ opt_trans_rule co1 co2
+   | Just (tv1,r1) <- splitForAllCo_maybe co1
+   , Just (tv2,r2) <- etaForAllCo_maybe co2
+   , let r2' = substCoWithTy tv2 (mkTyVarTy tv1) r2
+   = fireTransRule "EtaAllL" co1 co2 $
+     mkForAllCo tv1 (opt_trans2 r1 r2')
+   | Just (tv2,r2) <- splitForAllCo_maybe co2
+   , Just (tv1,r1) <- etaForAllCo_maybe co1
+   , let r1' = substCoWithTy tv1 (mkTyVarTy tv2) r1
+   = fireTransRule "EtaAllR" co1 co2 $
+     mkForAllCo tv1 (opt_trans2 r1' r2)
+ -- Push transitivity inside axioms
+ opt_trans_rule co1 co2
+   -- TrPushAxR/TrPushSymAxR
+   | Just (sym, con, cos1) <- co1_is_axiom_maybe
+   , Just cos2 <- matchAxiom sym con co2
+   = fireTransRule "TrPushAxR" co1 co2 $
+     if sym 
+     then SymCo $ AxiomInstCo con (opt_transList (map mkSymCo cos2) cos1)
+     else         AxiomInstCo con (opt_transList cos1 cos2)
+   -- TrPushAxL/TrPushSymAxL
+   | Just (sym, con, cos2) <- co2_is_axiom_maybe
+   , Just cos1 <- matchAxiom (not sym) con co1
+   = fireTransRule "TrPushAxL" co1 co2 $
+     if sym 
+     then SymCo $ AxiomInstCo con (opt_transList cos2 (map mkSymCo cos1))
+     else         AxiomInstCo con (opt_transList cos1 cos2)
+   -- TrPushAxSym/TrPushSymAx
+   | Just (sym1, con1, cos1) <- co1_is_axiom_maybe
+   , Just (sym2, con2, cos2) <- co2_is_axiom_maybe
+   , con1 == con2
+   , sym1 == not sym2
+   , let qtvs = co_ax_tvs con1
+         lhs  = co_ax_lhs con1 
+         rhs  = co_ax_rhs con1 
+         pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
+   , all (`elemVarSet` pivot_tvs) qtvs
+   = fireTransRule "TrPushAxSym" co1 co2 $
+     if sym2
+     then liftCoSubstWith qtvs (opt_transList cos1 (map mkSymCo cos2)) lhs  -- TrPushAxSym
+     else liftCoSubstWith qtvs (opt_transList (map mkSymCo cos1) cos2) rhs  -- TrPushSymAx
+   where
+     co1_is_axiom_maybe = isAxiom_maybe co1
+     co2_is_axiom_maybe = isAxiom_maybe co2
+ opt_trans_rule co1 co2        -- Identity rule
+   | Pair ty1 _ <- coercionKind co1
+   , Pair _ ty2 <- coercionKind co2
+   , ty1 `eqType` ty2
+   = fireTransRule "RedTypeDirRefl" co1 co2 $
+     Refl ty2
+ opt_trans_rule _ _ = Nothing
+ fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
+ fireTransRule _rule _co1 _co2 res
+   = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
+     Just res
+ -----------
+ wrapSym :: Bool -> Coercion -> Coercion
+ wrapSym sym co | sym       = SymCo co
+                | otherwise = co
+ -----------
+ isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom, [Coercion])
+ isAxiom_maybe (SymCo co) 
+   | Just (sym, con, cos) <- isAxiom_maybe co
+   = Just (not sym, con, cos)
+ isAxiom_maybe (AxiomInstCo con cos)
+   = Just (False, con, cos)
+ isAxiom_maybe _ = Nothing
+ matchAxiom :: Bool -- True = match LHS, False = match RHS
+            -> CoAxiom -> Coercion -> Maybe [Coercion]
+ -- If we succeed in matching, then *all the quantified type variables are bound*
+ -- E.g.   if tvs = [a,b], lhs/rhs = [b], we'll fail
+ matchAxiom sym (CoAxiom { co_ax_tvs = qtvs, co_ax_lhs = lhs, co_ax_rhs = rhs }) co
+   = case liftCoMatch (mkVarSet qtvs) (if sym then lhs else rhs) co of
+       Nothing    -> Nothing
+       Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)
+ -------------
+ compatible_co :: Coercion -> Coercion -> Bool
+ -- Check whether (co1 . co2) will be well-kinded
+ compatible_co co1 co2
+   = x1 `eqType` x2            
+   where
+     Pair _ x1 = coercionKind co1
+     Pair x2 _ = coercionKind co2
+ -------------
+ etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
+ -- Try to make the coercion be of form (forall tv. co)
+ etaForAllCo_maybe co
+   | Just (tv, r) <- splitForAllCo_maybe co
+   = Just (tv, r)
+   | Pair ty1 ty2  <- coercionKind co
+   , Just (tv1, _) <- splitForAllTy_maybe ty1
+   , Just (tv2, _) <- splitForAllTy_maybe ty2
+   , tyVarKind tv1 `eqKind` tyVarKind tv2
+   = Just (tv1, mkInstCo co (mkTyVarTy tv1))
+   | otherwise
+   = Nothing
+ etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
+ -- If possible, split a coercion 
+ --       g :: T s1 .. sn ~ T t1 .. tn
+ -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] 
+ etaTyConAppCo_maybe tc (TyConAppCo tc2 cos2)
+   = ASSERT( tc == tc2 ) Just cos2
+ etaTyConAppCo_maybe tc co
+   | isDecomposableTyCon tc
+   , Pair ty1 ty2     <- coercionKind co
+   , Just (tc1, tys1) <- splitTyConApp_maybe ty1
+   , Just (tc2, tys2) <- splitTyConApp_maybe ty2
+   , tc1 == tc2
+   , let n = length tys1
+   = ASSERT( tc == tc1 ) 
+     ASSERT( n == length tys2 )
+     Just (decomposeCo n co)  
+     -- NB: n might be <> tyConArity tc
+     -- e.g.   data family T a :: * -> *
+     --        g :: T a b ~ T c d
+   | otherwise
+   = Nothing
+ \end{code}  
@@@ -67,10 -72,8 +74,9 @@@ module Type 
          -- ** Common Kinds and SuperKinds
          liftedTypeKind, unliftedTypeKind, openTypeKind,
          argTypeKind, ubxTupleKind,
+         tySuperKind, 
 +        natKind,
  
-         tySuperKind, coSuperKind, 
          -- ** Common Kind type constructors
          liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
          argTypeKindTyCon, ubxTupleKindTyCon,
  
        -- * Pretty-printing
        pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
-       pprPred, pprEqPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind,
+       pprPred, pprPredTy, pprEqPred, pprTheta, pprThetaArrowTy, pprClassPred, 
+         pprKind, pprParendKind,
 +        pprTyLit,
        
        pprSourceTyCon
      ) where
@@@ -854,32 -868,13 +895,14 @@@ mkIPPred ip ty = IParam ip t
  %************************************************************************
  
  \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 (LiteralTy _)    = emptyVarSet
- 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
- tyVarsOfTypes :: [Type] -> TyVarSet
- tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
- tyVarsOfPred :: PredType -> TyVarSet
- tyVarsOfPred (IParam _ ty)    = tyVarsOfType ty
- tyVarsOfPred (ClassP _ tys)   = tyVarsOfTypes tys
- tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
- tyVarsOfTheta :: ThetaType -> TyVarSet
- tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
+ typeSize :: Type -> Int
+ typeSize (TyVarTy _)     = 1
+ typeSize (AppTy t1 t2)   = typeSize t1 + typeSize t2
+ typeSize (FunTy t1 t2)   = typeSize t1 + typeSize t2
+ typeSize (PredTy p)      = predSize typeSize p
+ typeSize (ForAllTy _ t)  = 1 + typeSize t
+ typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts)
++typeSize (LiteralTy _)   = 1
  \end{code}
  
  
@@@ -930,14 -953,8 +982,15 @@@ 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 (LiteralTy _)     = False
 +  -- Literal types are not really lifted (they are empty) but this
 +  -- probably does not matter a lot.  We return 'False' here because
 +  -- the rest of the typechecker assumes that only lifted types can be
 +  -- unified with type variables (see the note at the top of this file).
 +  -- This is a bit odd.
 +
  isUnLiftedType _                 = False
  
  isUnboxedTupleType :: Type -> Bool
@@@ -1008,6 -1025,64 +1062,65 @@@ 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 (LiteralTy _)        = emptyVarSet
+     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}
  %*                                                                    *
  %************************************************************************
@@@ -1017,22 -1092,18 +1130,22 @@@ 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
 +seqType (LiteralTy x)     = seqTyLit x
  
  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
 +
 +seqTyLit :: TyLit -> ()
 +seqTyLit (NumberTyLit x) = x `seq` ()
  \end{code}
  
  
@@@ -1524,14 -1441,16 +1488,17 @@@ subst_ty subst t
      go (ForAllTy tv ty)  = case substTyVarBndr subst tv of
                                (subst', tv') ->
                                   ForAllTy tv' $! (subst_ty subst' ty)
 +    go (LiteralTy x)     = LiteralTy x
  
  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
  module TypeRep (
        TyThing(..), 
        Type(..),
-       PredType(..),                   -- to friends
+         Pred(..),                       -- to friends
 +        TyLit(..),                      -- to friends
        
-       Kind, ThetaType,                -- Synonyms
+         Kind, SuperKind,
+         PredType, ThetaType,      -- Synonyms
  
-       funTyCon, funTyConName,
+         -- Functions over types
+         mkTyConApp, mkTyConTy, mkTyVarTy, mkTyVarTys,
+         isLiftedTypeKind, isCoercionKind, 
  
-       -- Pretty-printing
+         -- Pretty-printing
        pprType, pprParendType, pprTypeApp,
        pprTyThing, pprTyThingCategory, 
-       pprPred, pprEqPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
+       pprPredTy, pprEqPred, pprTheta, pprForAll, pprThetaArrowTy, pprClassPred,
+         pprKind, pprParendKind,
 +        pprTyLit,
+       Prec(..), maybeParen, pprTcApp, pprTypeNameApp, 
+         pprPrefixApp, pprPred, pprArrowChain, pprThetaArrow,
+         -- Free variables
+         tyVarsOfType, tyVarsOfTypes,
+         tyVarsOfPred, tyVarsOfTheta,
+       varsOfPred, varsOfTheta,
+       predSize,
  
-       -- Kinds
-       liftedTypeKind, unliftedTypeKind, openTypeKind,
-         argTypeKind, ubxTupleKind,
-         natKind,
-       isLiftedTypeKindCon, isLiftedTypeKind,
-         isNatKindCon, isNatKind,
-       mkArrowKind, mkArrowKinds, isCoercionKind,
-       coVarPred,
-         -- Kind constructors...
-         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
-         argTypeKindTyCon, ubxTupleKindTyCon,
-         natKindTyCon,
-         -- And their names
-         unliftedTypeKindTyConName, openTypeKindTyConName,
-         ubxTupleKindTyConName, argTypeKindTyConName,
-         liftedTypeKindTyConName,
-         natKindTyConName,
-         -- Super Kinds
-       tySuperKind, coSuperKind,
-         isTySuperKind, isCoSuperKind,
-       tySuperKindTyCon, coSuperKindTyCon,
-         
-       pprKind, pprParendKind
+         -- Substitutions
+         TvSubst(..), TvSubstEnv
      ) where
  
  #include "HsVersions.h"
@@@ -161,23 -156,12 +158,23 @@@ data Typ
    | PredTy
        PredType        -- ^ The type of evidence for a type predictate.
                          -- Note that a @PredTy (EqPred _ _)@ can appear only as the kind
-                       -- of a coercion variable; never as the argument or result
-                       -- of a 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
+                         -- of a coercion variable; never as the argument or result of a
+                         -- 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
                        
                        -- See Note [PredTy], and Note [Equality predicates]
-   | LiteralTy TyLit     -- Type literals are simillar to type constructors.
 +
-   deriving (Data, Typeable)
++  | LiteralTy TyLit     -- ^ Type literals are simillar to type constructors.
 +
+   deriving (Data.Data, Data.Typeable)
  
-   deriving (Eq, Ord, Data, Typeable)
 +
 +-- NOTE:  Other parts of the code assume that type literals do not contain
 +-- other types or type variables.
 +data TyLit
 +  = NumberTyLit Integer
++  deriving (Eq, Ord, Data.Data, Data.Typeable)
 +
 +
  -- | The key type representing kinds in the compiler.
  -- Invariant: a kind is always in one of these forms:
  --
@@@ -257,6 -252,89 +265,90 @@@ name (wildCoVarName), since it's not me
  
  %************************************************************************
  %*                                                                    *
+             Simple constructors
+ %*                                                                    *
+ %************************************************************************
+ These functions are here so that they can be used by TysPrim,
+ which in turn is imported by Type
+ \begin{code}
+ mkTyVarTy  :: TyVar   -> Type
+ mkTyVarTy  = TyVarTy
+ mkTyVarTys :: [TyVar] -> [Type]
+ mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
+ -- | 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 []
+ isLiftedTypeKind :: Kind -> Bool
+ -- This function is here because it's used in the pretty printer
+ isLiftedTypeKind (TyConApp tc []) = tc `hasKey` liftedTypeKindTyConKey
+ isLiftedTypeKind _                = False
+ isCoercionKind :: Kind -> Bool
+ -- All coercions are of form (ty1 ~ ty2)
+ -- This function is here rather than in Coercion, because it
+ -- is used in a knot-tied way to enforce invariants in Var
+ isCoercionKind (PredTy (EqPred {})) = True
+ isCoercionKind _                    = False
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
+                       Free variables of types and coercions
+ %*                                                                    *
+ %************************************************************************
+ \begin{code}
+ tyVarsOfPred :: PredType -> TyCoVarSet
+ tyVarsOfPred = varsOfPred tyVarsOfType
+ tyVarsOfTheta :: ThetaType -> TyCoVarSet
+ tyVarsOfTheta = varsOfTheta tyVarsOfType
+ tyVarsOfType :: Type -> VarSet
+ -- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym
+ tyVarsOfType (TyVarTy v)         = unitVarSet v
+ tyVarsOfType (TyConApp _ tys)    = tyVarsOfTypes tys
+ tyVarsOfType (PredTy sty)        = varsOfPred tyVarsOfType sty
+ tyVarsOfType (FunTy arg res)     = tyVarsOfType arg `unionVarSet` tyVarsOfType res
+ tyVarsOfType (AppTy fun arg)     = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
+ tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
++tyVarsOfType (LiteralTy _)       = emptyVarSet
+ tyVarsOfTypes :: [Type] -> TyVarSet
+ tyVarsOfTypes tys = foldr (unionVarSet . tyVarsOfType) emptyVarSet tys
+ varsOfPred :: (a -> VarSet) -> Pred a -> VarSet
+ varsOfPred f (IParam _ ty)    = f ty
+ varsOfPred f (ClassP _ tys)   = foldr (unionVarSet . f) emptyVarSet tys
+ varsOfPred f (EqPred ty1 ty2) = f ty1 `unionVarSet` f ty2
+ varsOfTheta :: (a -> VarSet) -> [Pred a] -> VarSet
+ varsOfTheta f = foldr (unionVarSet . varsOfPred f) emptyVarSet
+ predSize :: (a -> Int) -> Pred a -> Int
+ predSize size (IParam _ t)   = 1 + size t
+ predSize size (ClassP _ ts)  = 1 + sum (map size ts)
+ predSize size (EqPred t1 t2) = size t1 + size t2
+ \end{code}
+ %************************************************************************
+ %*                                                                    *
                        TyThing
  %*                                                                    *
  %************************************************************************
@@@ -450,27 -481,30 +495,33 @@@ maybeParen ctxt_prec inner_prec prett
  
  ------------------
  pprType, pprParendType :: Type -> SDoc
- pprType       ty = ppr_type TopPrec   ty
+ pprType       ty = ppr_type TopPrec ty
  pprParendType ty = ppr_type TyConPrec ty
  
- pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
- -- The first arg is the tycon, or sometimes class
- -- Print infix if the tycon/class looks like an operator
- pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
+ pprKind, pprParendKind :: Kind -> SDoc
+ pprKind       = pprType
+ pprParendKind = pprParendType
  
 +pprTyLit :: TyLit -> SDoc
 +pprTyLit = ppr_tylit TopPrec
 +
  ------------------
- pprPred :: PredType -> SDoc
- pprPred (ClassP cls tys) = pprClassPred cls tys
- pprPred (IParam ip ty)   = ppr ip <> dcolon <> pprType ty
- pprPred (EqPred ty1 ty2) = pprEqPred (ty1,ty2)
- pprEqPred :: (Type,Type) -> SDoc
- pprEqPred (ty1,ty2) = sep [ ppr_type FunPrec ty1
-                           , nest 2 (ptext (sLit "~"))
-                           , ppr_type FunPrec ty2]
+ pprPredTy :: PredType -> SDoc
+ pprPredTy = pprPred ppr_type
+ pprPred :: (Prec -> a -> SDoc) -> Pred a -> SDoc
+ pprPred pp (ClassP cls tys) = ppr_class_pred pp cls tys
+ pprPred pp (IParam ip ty)   = ppr ip <> dcolon <> pp TopPrec ty
+ pprPred pp (EqPred ty1 ty2) = ppr_eq_pred pp (Pair ty1 ty2)
+ ------------
+ pprEqPred :: Pair Type -> SDoc
+ pprEqPred = ppr_eq_pred ppr_type
+ ppr_eq_pred :: (Prec -> a -> SDoc) -> Pair a -> SDoc
+ ppr_eq_pred pp (Pair ty1 ty2) = sep [ pp FunPrec ty1
+                                     , nest 2 (ptext (sLit "~"))
+                                     , pp FunPrec ty2]
                               -- Precedence looks like (->) so that we get
                               --    Maybe a ~ Bool
                               --    (a->a) ~ Bool
@@@ -502,12 -545,10 +562,13 @@@ noParenPred (IParam {}) = Fals
  instance Outputable Type where
      ppr ty = pprType ty
  
- instance Outputable PredType where
-     ppr = pprPred
+ instance Outputable (Pred Type) where
+     ppr = pprPredTy   -- Not for arbitrary (Pred a), because the
+                     -- (Outputable a) doesn't give precedence
  
 +instance Outputable TyLit where
 +   ppr = pprTyLit
 +
  instance Outputable name => OutputableBndr (IPName name) where
      pprBndr _ n = ppr n       -- Simple for now
  
Simple merge