Substantial improvements to coercion optimisation
authorsimonpj@microsoft.com <unknown>
Mon, 4 Jan 2010 08:21:55 +0000 (08:21 +0000)
committersimonpj@microsoft.com <unknown>
Mon, 4 Jan 2010 08:21:55 +0000 (08:21 +0000)
The main purpose of this patch is to add a bunch of new rules
to the coercion optimiser.  They are documented in the (revised)
Appendix of the System FC paper.

Some code has moved about:

- OptCoercion is now a separate module, mainly because it
  now uses tcMatchTy, which is defined in Unify, so OptCoercion
  must live higehr up in the hierarchy

- Functions that manipulate Kinds has moved from
  Type.lhs to Coercion.lhs.  Reason: the function typeKind
  now needs to call coercionKind.  And in any case, a Kind is
  a flavour of Type, so it builds on top of Type; indeed Coercions
  and Kinds are both flavours of Type.

  This change required fiddling with a number of imports, hence
  the one-line changes to otherwise-unrelated modules

- The representation of CoTyCons in TyCon has changed.   Instead of
  an extensional representation (a kind checker) there is now an
  intensional representation (namely TyCon.CoTyConDesc).  This was
  needed for one of the new coercion optimisations.

17 files changed:
compiler/coreSyn/CoreLint.lhs
compiler/coreSyn/CoreSubst.lhs
compiler/ghc.cabal.in
compiler/hsSyn/Convert.lhs
compiler/hsSyn/HsTypes.lhs
compiler/main/GHC.hs
compiler/main/InteractiveEval.hs
compiler/parser/Parser.y.pp
compiler/parser/ParserCore.y
compiler/prelude/TysPrim.lhs
compiler/simplCore/Simplify.lhs
compiler/types/Coercion.lhs
compiler/types/OptCoercion.lhs [new file with mode: 0644]
compiler/types/TyCon.lhs
compiler/types/Type.lhs
compiler/types/Unify.lhs
compiler/utils/Util.lhs

index 4893885..ee6541e 100644 (file)
@@ -633,10 +633,9 @@ lintCoercion ty@(FunTy ty1 ty2)
        ; return (FunTy s1 s2, FunTy t1 t2) }
 
 lintCoercion ty@(TyConApp tc tys) 
-  | Just (ar, rule) <- isCoercionTyCon_maybe tc
+  | Just (ar, desc) <- isCoercionTyCon_maybe tc
   = do { unless (tys `lengthAtLeast` ar) (badCo ty)
-       ; (s,t)   <- rule lintType lintCoercion 
-                         True (take ar tys)
+       ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
        ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
        ; check_co_app ty (typeKind s) ss
        ; return (mkAppTys s ss, mkAppTys t ts) }
@@ -677,6 +676,70 @@ lintCoercion (ForAllTy tv ty)
 badCo :: Coercion -> LintM a
 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
 
+---------------
+lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
+-- Always called with correct number of coercion arguments
+-- First arg is just for error message
+lintCoTyConApp _ CoLeft  (co:_) = lintLR   fst             co 
+lintCoTyConApp _ CoRight (co:_) = lintLR   snd             co   
+lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3   co 
+lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3   co 
+lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co 
+
+lintCoTyConApp _ CoSym (co:_) 
+  = do { (ty1,ty2) <- lintCoercion co
+       ; return (ty2,ty1) }
+
+lintCoTyConApp co CoTrans (co1:co2:_) 
+  = do { (ty1a, ty1b) <- lintCoercion co1
+       ; (ty2a, ty2b) <- lintCoercion co2
+       ; checkL (ty1b `coreEqType` ty2a)
+                (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
+                    2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
+       ; return (ty1a, ty2b) }
+
+lintCoTyConApp _ CoInst (co:arg_ty:_) 
+  = do { co_tys <- lintCoercion co
+       ; arg_kind  <- lintType arg_ty
+       ; case decompInst_maybe co_tys of
+          Just ((tv1,tv2), (ty1,ty2)) 
+            | arg_kind `isSubKind` tyVarKind tv1
+            -> return (substTyWith [tv1] [arg_ty] ty1, 
+                       substTyWith [tv2] [arg_ty] ty2) 
+            | otherwise
+            -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
+         Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
+
+lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs 
+                          , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
+  = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
+       ; sequence_ (zipWith checkKinds tvs tys1)
+       ; return (substTyWith tvs tys1 lhs_ty,
+                 substTyWith tvs tys2 rhs_ty) }
+
+lintCoTyConApp _ CoUnsafe (ty1:ty2:_) 
+  = do { _ <- lintType ty1
+       ; _ <- lintType ty2     -- Ignore kinds; it's unsafe!
+       ; return (ty1,ty2) } 
+
+lintCoTyConApp _ _ _ = panic "lintCoTyConApp"  -- Called with wrong number of coercion args
+
+----------
+lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
+lintLR sel co
+  = do { (ty1,ty2) <- lintCoercion co
+       ; case decompLR_maybe (ty1,ty2) of
+           Just res -> return (sel res)
+           Nothing  -> failWithL (ptext (sLit "Bad argument of left/right")) }
+
+----------
+lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
+lintCsel sel co
+  = do { (ty1,ty2) <- lintCoercion co
+       ; case decompCsel_maybe (ty1,ty2) of
+           Just res -> return (sel res)
+           Nothing  -> failWithL (ptext (sLit "Bad argument of csel")) }
+
 -------------------
 lintType :: OutType -> LintM Kind
 lintType (TyVarTy tv)
index 216b636..9f1e20d 100644 (file)
@@ -39,7 +39,7 @@ import OccurAnal( occurAnalyseExpr )
 
 import qualified Type
 import Type     ( Type, TvSubst(..), TvSubstEnv )
-import Coercion ( optCoercion )
+import OptCoercion ( optCoercion )
 import VarSet
 import VarEnv
 import Id
index 8e444a8..f49d8d0 100644 (file)
@@ -326,6 +326,7 @@ Library
         HaddockUtils
         LexCore
         Lexer
+        OptCoercion
         Parser
         ParserCore
         ParserCoreUtils
index 0ff2691..91d1b90 100644 (file)
@@ -19,6 +19,7 @@ import qualified OccName
 import OccName
 import SrcLoc
 import Type
+import Coercion
 import TysWiredIn
 import BasicTypes as Hs
 import ForeignCall
index 797a8f2..4e6e5ab 100644 (file)
@@ -33,6 +33,7 @@ module HsTypes (
 import {-# SOURCE #-} HsExpr ( HsSplice, pprSplice )
 
 import Type
+import Coercion
 import HsDoc
 import BasicTypes
 import SrcLoc
index 5289f71..c01a433 100644 (file)
@@ -254,8 +254,8 @@ import NameSet
 import RdrName
 import qualified HsSyn -- hack as we want to reexport the whole module
 import HsSyn hiding ((<.>))
-import Type             hiding (typeKind)
-import TcType           hiding (typeKind)
+import Type
+import TcType          hiding( typeKind )
 import Id
 import Var
 import TysPrim         ( alphaTyVars )
index 352fbf0..d4230c7 100644 (file)
@@ -42,9 +42,9 @@ module InteractiveEval (
 import HscMain          hiding (compileExpr)
 import HscTypes
 import TcRnDriver
-import Type             hiding (typeKind)
-import TcType           hiding (typeKind)
 import InstEnv
+import Type
+import TcType          hiding( typeKind )
 import Var
 import Id
 import Name             hiding ( varName )
index 4cd637f..212a79c 100644 (file)
@@ -45,7 +45,8 @@ import SrcLoc         ( Located(..), unLoc, getLoc, noLoc, combineSrcSpans,
                          mkSrcLoc, mkSrcSpan )
 import Module
 import StaticFlags     ( opt_SccProfilingOn, opt_Hpc )
-import Type            ( Kind, mkArrowKind, liftedTypeKind, unliftedTypeKind )
+import Type            ( Kind, liftedTypeKind, unliftedTypeKind )
+import Coercion                ( mkArrowKind )
 import Class           ( FunDep )
 import BasicTypes      ( Boxity(..), Fixity(..), FixityDirection(..), IPName(..),
                          Activation(..), RuleMatchInfo(..), defaultInlinePragma )
index 6839fa2..f43e225 100644 (file)
@@ -16,8 +16,9 @@ import RdrName
 import OccName
 import Type ( Kind,
               liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
-              argTypeKindTyCon, ubxTupleKindTyCon, mkArrowKind, mkTyConApp
+              argTypeKindTyCon, ubxTupleKindTyCon, mkTyConApp
             )
+import Coercion( mkArrowKind )
 import Name( Name, nameOccName, nameModule, mkExternalName )
 import Module
 import ParserCoreUtils
index 4e1576f..18c80a4 100644 (file)
@@ -57,6 +57,7 @@ import OccName                ( mkTcOcc )
 import OccName         ( mkTyVarOccFS, mkTcOccFS )
 import TyCon           ( TyCon, mkPrimTyCon, mkLiftedPrimTyCon, mkAnyTyCon )
 import Type
+import Coercion
 import SrcLoc
 import Unique          ( mkAlphaTyVarUnique )
 import PrelNames
index 4c1b6cb..86eef46 100644 (file)
@@ -20,6 +20,7 @@ import Var
 import IdInfo
 import Name            ( mkSystemVarName, isExternalName )
 import Coercion
+import OptCoercion     ( optCoercion )
 import FamInstEnv       ( topNormaliseType )
 import DataCon          ( DataCon, dataConWorkId, dataConRepStrictness )
 import CoreMonad       ( SimplifierSwitch(..), Tick(..) )
index 2b0f1b3..bc93372 100644 (file)
@@ -3,23 +3,32 @@
 %
 
 \begin{code}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
--- | Module for type coercions, as used in System FC. See 'CoreSyn.Expr' for
+-- | Module for (a) type kinds and (b) type coercions, 
+-- as used in System FC. See 'CoreSyn.Expr' for
 -- more on System FC and how coercions fit into it.
 --
 -- Coercions are represented as types, and their kinds tell what types the 
--- coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so:
+-- coercion works on. The coercion kind constructor is a special TyCon that 
+-- must always be saturated, like so:
 --
--- > typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type]
+-- > typeKind (symCoercion type) :: TyConApp CoTyCon{...} [type, type]
 module Coercion (
         -- * Main data type
-        Coercion,
+        Coercion, Kind,
+        typeKind,
+
+        -- ** Deconstructing Kinds 
+        kindFunResult, splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
+
+        -- ** Predicates on Kinds
+        isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
+        isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
+        isCoSuperKind, isSuperKind, isCoercionKind, 
+       mkArrowKind, mkArrowKinds,
+
+        isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
+        isSubKindCon,
+
         mkCoKind, mkCoPredTy, coVarKind, coVarKind_maybe,
         coercionKind, coercionKinds, isIdentityCoercion,
 
@@ -35,7 +44,6 @@ module Coercion (
         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
         mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, 
 
-        splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
 
         unsafeCoercionTyCon, symCoercionTyCon,
         transCoercionTyCon, leftCoercionTyCon, 
@@ -44,9 +52,8 @@ module Coercion (
 
         -- ** Decomposition
         decompLR_maybe, decompCsel_maybe, decompInst_maybe,
-
-        -- ** Optimisation
-       optCoercion,
+        splitCoPredTy_maybe,
+        splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
 
         -- ** Comparison
         coreEqCoercion, coreEqCoercion2,
@@ -73,12 +80,140 @@ import VarEnv
 import Name
 import PrelNames
 import Util
-import Control.Monad
 import BasicTypes
-import MonadUtils
 import Outputable
 import FastString
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+       Functions over Kinds            
+%*                                                                     *
+%************************************************************************
 
+\begin{code}
+-- | Essentially 'funResultTy' on kinds
+kindFunResult :: Kind -> Kind
+kindFunResult k = funResultTy k
+
+-- | Essentially 'splitFunTys' on kinds
+splitKindFunTys :: Kind -> ([Kind],Kind)
+splitKindFunTys k = splitFunTys k
+
+splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
+splitKindFunTy_maybe = splitFunTy_maybe
+
+-- | Essentially 'splitFunTysN' on kinds
+splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
+splitKindFunTysN k = splitFunTysN k
+
+-- | 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
+
+isSubOpenTypeKind :: Kind -> Bool
+-- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
+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 (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 (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2')) 
+  = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
+isSubKind _             _                     = False
+
+eqKind :: Kind -> Kind -> Bool
+eqKind = tcEqType
+
+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
+  | 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}
+
+%************************************************************************
+%*                                                                     *
+            Coercions
+%*                                                                     *
+%************************************************************************
+
+
+\begin{code}
 -- | A 'Coercion' represents a 'Type' something should be coerced to.
 type Coercion     = Type
 
@@ -154,83 +289,6 @@ getEqPredTys :: PredType -> (Type,Type)
 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
 getEqPredTys other           = pprPanic "getEqPredTys" (ppr other)
 
--- | If it is the case that
---
--- > 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, rule) <- 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) = runID (rule (return . typeKind)
-                                (return . coercionKind)
-                               False (take ar args))
-                             -- Apply the rule to the right number of args
-                             -- Always succeeds (if term is well-kinded!)
-        (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 (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 (EqPred c1 c2)) 
-  = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
-    let k1 = coercionKindPredTy c1
-        k2 = coercionKindPredTy c2 in
-    (k1,k2)
-  -- These should not show up in coercions at all
-  -- becuase they are in the form of for-alls
-  where
-    coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
-
-
-
-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))
-
--- | Apply 'coercionKind' to multiple 'Coercion's
-coercionKinds :: [Coercion] -> ([Type], [Type])
-coercionKinds tys = unzip $ map coercionKind tys
-
--------------------------------------
 isIdentityCoercion :: Coercion -> Bool
 isIdentityCoercion co  
   = case coercionKind co of
@@ -322,8 +380,7 @@ mkInstsCoercion co tys = foldl mkInstCoercion co tys
 -- but it is used when we know we are dealing with bottom, which is one case in which 
 -- it is safe.  This is also used implement the @unsafeCoerce#@ primitive.
 mkUnsafeCoercion :: Type -> Type -> Coercion
-mkUnsafeCoercion ty1 ty2 
-  = mkCoercion unsafeCoercionTyCon [ty1, ty2]
+mkUnsafeCoercion ty1 ty2 = mkCoercion unsafeCoercionTyCon [ty1, ty2]
 
 
 -- See note [Newtype coercions] in TyCon
@@ -334,16 +391,12 @@ mkUnsafeCoercion ty1 ty2
 -- a subset of those 'TyVar's.
 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
 mkNewTypeCoercion name tycon tvs rhs_ty
-  = mkCoercionTyCon name co_con_arity rule
+  = mkCoercionTyCon name arity desc
   where
-    co_con_arity = length tvs
-
-    rule :: CoTyConKindChecker
-    rule kc_ty _kc_co checking args 
-      = do { ks <- mapM kc_ty args
-           ; unless (not checking || kindAppOk (tyConKind tycon) ks) 
-                    (fail "Argument kind mis-match")
-           ; return (TyConApp tycon args, substTyWith tvs args rhs_ty) }
+    arity = length tvs
+    desc = CoAxiom { co_ax_tvs = tvs 
+                   , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs)
+                   , co_ax_rhs = rhs_ty }
 
 -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
 -- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is 
@@ -355,26 +408,13 @@ mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon
                  -> [Type]     -- ^ Type instance (@ts@)
                  -> TyCon      -- ^ Representation tycon (@R@)
                  -> TyCon      -- ^ Coercion tycon (@Co@)
-mkFamInstCoercion name tvs family instTys rep_tycon
-  = mkCoercionTyCon name coArity rule
+mkFamInstCoercion name tvs family inst_tys rep_tycon
+  = mkCoercionTyCon name arity desc
   where
-    coArity = length tvs
-
-    rule :: CoTyConKindChecker
-    rule kc_ty _kc_co checking args 
-      = do { ks <- mapM kc_ty args
-           ; unless (not checking  || kindAppOk (tyConKind rep_tycon) ks)
-                    (fail "Argument kind mis-match")
-           ; return (substTyWith tvs args $         -- with sigma = [tys/tvs],
-                    TyConApp family instTys         --       sigma (F ts)
-                   , TyConApp rep_tycon args) }     --   ~ R tys
-
-kindAppOk :: Kind -> [Kind] -> Bool
-kindAppOk _   [] = True
-kindAppOk kfn (k:ks) 
-  = case splitKindFunTy_maybe kfn of
-      Just (kfa, kfb) | k `isSubKind` kfa -> kindAppOk kfb ks
-      _other                              -> False
+    arity = length tvs
+    desc = CoAxiom { co_ax_tvs = tvs
+                   , co_ax_lhs = mkTyConApp family inst_tys 
+                   , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
 \end{code}
 
 
@@ -403,137 +443,67 @@ symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon,
   rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
   csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
 
-symCoercionTyCon 
-  = mkCoercionTyCon symCoercionTyConName 1 kc_sym
-  where
-    kc_sym :: CoTyConKindChecker
-    kc_sym _kc_ty kc_co _ (co:_) 
-      = do { (ty1,ty2) <- kc_co co
-           ; return (ty2,ty1) }
-    kc_sym _ _ _ _ = panic "kc_sym"
-
-transCoercionTyCon 
-  = mkCoercionTyCon transCoercionTyConName 2 kc_trans
-  where
-    kc_trans :: CoTyConKindChecker
-    kc_trans _kc_ty kc_co checking (co1:co2:_)
-      = do { (a1, r1) <- kc_co co1
-           ; (a2, r2) <- kc_co co2 
-          ; unless (not checking || (r1 `coreEqType` a2))
-                    (fail "Trans coercion mis-match")
-           ; return (a1, r2) }
-    kc_trans _ _ _ _ = panic "kc_sym"
-
----------------------------------------------------
-leftCoercionTyCon  = mkCoercionTyCon leftCoercionTyConName  1 (kcLR_help fst)
-rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (kcLR_help snd)
-
-kcLR_help :: (forall a. (a,a)->a) -> CoTyConKindChecker
-kcLR_help select _kc_ty kc_co _checking (co : _)
-  = do { (ty1, ty2)  <- kc_co co
-       ; case decompLR_maybe ty1 ty2 of
-           Nothing  -> fail "decompLR" 
-           Just res -> return (select res) }
-kcLR_help _ _ _ _ _ = panic "kcLR_help"
-
-decompLR_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type))
+symCoercionTyCon    = mkCoercionTyCon symCoercionTyConName   1 CoSym
+transCoercionTyCon  = mkCoercionTyCon transCoercionTyConName 2 CoTrans
+leftCoercionTyCon   = mkCoercionTyCon leftCoercionTyConName  1 CoLeft
+rightCoercionTyCon  = mkCoercionTyCon rightCoercionTyConName 1 CoRight
+instCoercionTyCon   =  mkCoercionTyCon instCoercionTyConName 2 CoInst
+csel1CoercionTyCon  = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1
+csel2CoercionTyCon  = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2
+cselRCoercionTyCon  = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR
+unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe
+
+transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, 
+   rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
+   csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
+
+transCoercionTyConName         = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
+symCoercionTyConName           = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
+leftCoercionTyConName          = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
+rightCoercionTyConName         = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
+instCoercionTyConName          = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
+csel1CoercionTyConName  = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
+csel2CoercionTyConName  = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
+cselRCoercionTyConName  = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
+unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
+
+mkCoConName :: FastString -> Unique -> TyCon -> Name
+mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
+                            key (ATyCon coCon) BuiltInSyntax
+\end{code}
+
+\begin{code}
+------------
+decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type))
 -- Helper for left and right.  Finds coercion kind of its input and
 -- returns the left and right projections of the coercion...
 --
 -- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
-decompLR_maybe ty1 ty2
+decompLR_maybe (ty1,ty2)
   | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
   = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
-decompLR_maybe _ = Nothing
+decompLR_maybe _ = Nothing
 
----------------------------------------------------
-instCoercionTyCon 
-  =  mkCoercionTyCon instCoercionTyConName 2 kcInst_help
-  where
-    kcInst_help :: CoTyConKindChecker
-    kcInst_help kc_ty kc_co checking (co : ty : _)
-      = do { (t1,t2) <- kc_co co
-           ; k <- kc_ty ty
-           ; case decompInst_maybe t1 t2 of
-               Nothing -> fail "decompInst"
-               Just ((tv1,tv2), (ty1,ty2)) -> do
-           { unless (not checking || (k `isSubKind` tyVarKind tv1))
-                    (fail "Coercion instantation kind mis-match")
-           ; return (substTyWith [tv1] [ty] ty1,
-                     substTyWith [tv2] [ty] ty2) } }
-    kcInst_help _ _ _ _ = panic "kcInst_help"
-
-decompInst_maybe :: Type -> Type -> Maybe ((TyVar,TyVar), (Type,Type))
-decompInst_maybe ty1 ty2
+------------
+decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type))
+decompInst_maybe (ty1, ty2)
   | Just (tv1,r1) <- splitForAllTy_maybe ty1
   , Just (tv2,r2) <- splitForAllTy_maybe ty2
   = Just ((tv1,tv2), (r1,r2))
-decompInst_maybe _ = Nothing
+decompInst_maybe _ = Nothing
 
----------------------------------------------------
-unsafeCoercionTyCon 
-  = mkCoercionTyCon unsafeCoercionTyConName 2 kc_unsafe
-  where
-   kc_unsafe kc_ty _kc_co _checking (ty1:ty2:_) 
-    = do { _ <- kc_ty ty1
-         ; _ <- kc_ty ty2
-         ; return (ty1,ty2) }
-   kc_unsafe _ _ _ _ = panic "kc_unsafe"
-        
----------------------------------------------------
--- The csel* family
-
-csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (kcCsel_help fstOf3)
-csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (kcCsel_help sndOf3)
-cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (kcCsel_help thirdOf3) 
-
-kcCsel_help :: (forall a. (a,a,a) -> a) -> CoTyConKindChecker
-kcCsel_help select _kc_ty kc_co _checking (co : _)
-  = do { (ty1,ty2) <- kc_co co
-       ; case decompCsel_maybe ty1 ty2 of
-           Nothing  -> fail "decompCsel"
-           Just res -> return (select res) }
-kcCsel_help _ _ _ _ _ = panic "kcCsel_help"
-
-decompCsel_maybe :: Type -> Type -> Maybe ((Type,Type), (Type,Type), (Type,Type))
+------------
+decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type))
 --   If         co :: (s1~t1 => r1) ~ (s2~t2 => r2)
 -- Then   csel1 co ::            s1 ~ s2
 --        csel2 co ::           t1 ~ t2
 --        cselR co ::           r1 ~ r2
-decompCsel_maybe ty1 ty2
+decompCsel_maybe (ty1, ty2)
   | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1
   , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2
   = Just ((s1,s2), (t1,t2), (r1,r2))
-decompCsel_maybe _ _ = Nothing
-
-fstOf3   :: (a,b,c) -> a    
-sndOf3   :: (a,b,c) -> b    
-thirdOf3 :: (a,b,c) -> c    
-fstOf3      (a,_,_) =  a
-sndOf3      (_,b,_) =  b
-thirdOf3    (_,_,c) =  c
-
---------------------------------------
--- Their Names
-
-transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, 
-   rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName,
-   csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name
-
-transCoercionTyConName         = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon
-symCoercionTyConName           = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon
-leftCoercionTyConName          = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon
-rightCoercionTyConName         = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon
-instCoercionTyConName          = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon
-csel1CoercionTyConName  = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon
-csel2CoercionTyConName  = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon
-cselRCoercionTyConName  = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon
-unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
-
-mkCoConName :: FastString -> Unique -> TyCon -> Name
-mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
-                            key (ATyCon coCon) BuiltInSyntax
+decompCsel_maybe _ = Nothing
 \end{code}
 
 
@@ -693,233 +663,148 @@ mkEqPredCoI _   (ACo co1) ty2 coi2      = ACo $ PredTy $ EqPred co1 (fromCoI coi
 \end{code}
 
 %************************************************************************
-%*                                                                      *
-                 Optimising coercions                                                                  
-%*                                                                      *
+%*                                                                     *
+            The kind of a type, and of a coercion
+%*                                                                     *
 %************************************************************************
 
 \begin{code}
-optCoercion :: TvSubst -> Coercion -> NormalCo
--- ^ optCoercion applies a substitution to a coercion, 
---   *and* optimises it to reduce its size
-optCoercion env co = 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' :: TvSubst
-                       -> Bool        -- True <=> return (sym co)
-                       -> Coercion
-                       -> NormalCo     
-opt_co = opt_co'
--- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $
---                     co1 `seq` 
---                pprTrace "opt_co done }" (ppr co1) 
---               WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (s1,t1) 
---                                     $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )
---                co1
---  where
---    co1 = opt_co' sym co
---    same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2
---    (s,t) = coercionKind co
---    (s1,t1) | sym = (t,s)
---            | otherwise = (s,t)
---    (s2,t2) = coercionKind co1
-
-opt_co' env sym (AppTy ty1 ty2)          = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)
-opt_co' env sym (FunTy ty1 ty2)          = FunTy (opt_co env sym ty1) (opt_co env sym ty2)
-opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))
-opt_co' env sym (PredTy (IParam n ty))    = PredTy (IParam n (opt_co env sym ty))
-opt_co' _   _   co@(PredTy (EqPred {}))   = pprPanic "optCoercion" (ppr co)
-
-opt_co' env sym co@(TyVarTy tv)
-  | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty
-  | not (isCoVar tv)     = co   -- Identity; does not mention a CoVar
-  | ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..
-  | not sym              = co
-  | otherwise            = mkSymCoercion co
-  where
-    (ty1,ty2) = coVarKind tv
+typeKind :: Type -> Kind
+typeKind ty@(TyConApp tc tys) 
+  | isCoercionTyCon tc = typeKind (fst (coercionKind ty))
+  | otherwise          = foldr (\_ k -> kindFunResult k) (tyConKind tc) tys
+       -- During coercion optimisation we *do* match a type
+       -- against a coercion (see OptCoercion.matchesAxiomLhs)
+       -- So the use of typeKind in Unify.match_kind must work on coercions too
+       -- Hence the isCoercionTyCon case above
+
+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
+
+------------------
+predKind :: PredType -> Kind
+predKind (EqPred {}) = coSuperKind     -- A coercion kind!
+predKind (ClassP {}) = liftedTypeKind  -- Class and implicitPredicates are
+predKind (IParam {}) = liftedTypeKind  -- always represented by lifted types
+
+------------------
+-- | If it is the case that
+--
+-- > 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))
 
-opt_co' env sym (ForAllTy tv cor) 
-  | isCoVar tv = mkCoPredTy (opt_co env sym co1) (opt_co env sym co2) (opt_co env sym cor)
-  | otherwise  = case substTyVarBndr env tv of
-                   (env', tv') -> ForAllTy tv' (opt_co env' sym cor)
-  where
-    (co1,co2) = coVarKind tv
+  | 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 (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)
 
-opt_co' env sym (TyConApp tc cos)
-  | isCoercionTyCon tc
-  = foldl mkAppTy 
-         (opt_co_tc_app env sym tc (take arity cos))
-          (map (opt_co env sym) (drop arity cos))
   | otherwise
-  = TyConApp tc (map (opt_co env sym) cos)
-  where
-    arity = tyConArity tc
-
---------
-opt_co_tc_app :: TvSubst -> Bool -> TyCon -> [Coercion] -> NormalCo
--- Used for CoercionTyCons only
--- Arguments are *not* already simplified/substituted
-opt_co_tc_app env sym tc cos
-  | tc `hasKey` symCoercionTyConKey
-  = opt_co env (not sym) co1
-
-  | tc `hasKey` transCoercionTyConKey
-  = if sym then opt_trans opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
-           else opt_trans opt_co1 opt_co2
-
-  | tc `hasKey` leftCoercionTyConKey
-  , Just (opt_co1_left, _) <- splitAppTy_maybe opt_co1
-  = opt_co1_left       -- sym (left g) = left (sym g) 
-                       -- The opt_co has the sym pushed into it
-
-  | tc `hasKey` rightCoercionTyConKey
-  , Just (_, opt_co1_right) <- splitAppTy_maybe opt_co1
-  = opt_co1_right
-
-  | tc `hasKey` csel1CoercionTyConKey
-  , Just (s1,_,_) <- splitCoPredTy_maybe opt_co1
-  = s1
-
-  | tc `hasKey` csel2CoercionTyConKey
-  , Just (_,s2,_) <- splitCoPredTy_maybe opt_co1
-  = s2
-
-  | tc `hasKey` cselRCoercionTyConKey
-  , Just (_,_,r) <- splitCoPredTy_maybe opt_co1
-  = r
-
-  | tc `hasKey` instCoercionTyConKey   -- See if the first arg         
-                                       -- is already a forall
-  , Just (tv, co1_body) <- splitForAllTy_maybe co1
-  , let ty = substTy env co2
-  = opt_co (extendTvSubst env tv ty) sym co1_body
-
-  | tc `hasKey` instCoercionTyConKey   -- See if is *now* a forall
-  , Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1
-  , let ty = substTy env co2
-  = substTyWith [tv] [ty] opt_co1_body -- An inefficient one-variable substitution
-
-  | otherwise    -- 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) !!
-  = if sym then mkSymCoercion the_co 
-           else the_co
+--     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
-    (co1 : cos1) = cos
-    (co2 : _)    = cos1
-
-       -- These opt_cos have the sym pushed into them
-    opt_co1 = opt_co env sym co1
-    opt_co2 = opt_co env sym co2
-
-       -- However the_co does *not* have sym pushed into it
-    the_co = TyConApp tc (map (opt_co env False) cos)
-
--------------
-opt_trans :: NormalCo -> NormalCo -> NormalCo
-opt_trans co1 co2
-  | isIdNormCo co1 = co2
-  | otherwise      = opt_trans1 co1 co2
-
-opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
--- First arg is not the identity
-opt_trans1 co1 co2
-  | isIdNormCo co2 = co1
-  | otherwise      = opt_trans2 co1 co2
-
-opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
--- Neither arg is the identity
-opt_trans2 (TyConApp tc [co1a,co1b]) co2
-  | tc `hasKey` transCoercionTyConKey
-  = opt_trans1 co1a (opt_trans2 co1b co2)
-
-opt_trans2 co1 co2 
-  | Just co <- opt_trans_rule co1 co2
-  = co
-
-opt_trans2 co1 (TyConApp tc [co2a,co2b])
-  | tc `hasKey` transCoercionTyConKey
-  , Just co1_2a <- opt_trans_rule co1 co2a
-  = if isIdNormCo co1_2a
-    then co2b
-    else opt_trans2 co1_2a co2b
-
-opt_trans2 co1 co2
-  = mkTransCoercion co1 co2
-
-------
-opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
-opt_trans_rule (TyConApp tc [co1]) co2
-  | tc `hasKey` symCoercionTyConKey
-  , co1 `coreEqType` co2
-  , (_,ty2) <- coercionKind co2
-  = Just ty2
-
-opt_trans_rule co1 (TyConApp tc [co2])
-  | tc `hasKey` symCoercionTyConKey
-  , co1 `coreEqType` co2
-  , (ty1,_) <- coercionKind co1
-  = Just ty1
-
-opt_trans_rule (TyConApp tc1 [co1,ty1]) (TyConApp tc2 [co2,ty2])
-  | tc1 `hasKey` instCoercionTyConKey
-  , tc1 == tc2
-  , ty1 `coreEqType` ty2
-  = Just (mkInstCoercion (opt_trans2 co1 co2) ty1) 
-
-opt_trans_rule (TyConApp tc1 cos1) (TyConApp tc2 cos2)
-  | not (isCoercionTyCon tc1) || 
-    getUnique tc1 `elem` [ leftCoercionTyConKey, rightCoercionTyConKey
-                         , csel1CoercionTyConKey, csel2CoercionTyConKey
-                        , cselRCoercionTyConKey ]      --Yuk!
-  , tc1 == tc2                  -- Works for left,right, and csel* family
-                        -- BUT NOT equality axioms 
-                        -- E.g.        (g Int) `trans` (g Bool)
-                        --        /= g (Int . Bool)
-  = Just (TyConApp tc1 (zipWith opt_trans cos1 cos2))
-
-opt_trans_rule co1 co2
-  | Just (co1a, co1b) <- splitAppTy_maybe co1
-  , Just (co2a, co2b) <- splitAppTy_maybe co2
-  = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))
-
-  | Just (s1,t1,r1) <- splitCoPredTy_maybe co1
-  , Just (s2,t2,r2) <- splitCoPredTy_maybe co1
-  = Just (mkCoPredTy (opt_trans s1 s2)
-                     (opt_trans t1 t2)
-                     (opt_trans r1 r2))
-
-  | Just (tv1,r1) <- splitForAllTy_maybe co1
-  , Just (tv2,r2) <- splitForAllTy_maybe co2
-  , not (isCoVar tv1)               -- Both have same kind
-  , let r2' = substTyWith [tv2] [TyVarTy tv1] r2
-  = Just (ForAllTy tv1 (opt_trans2 r1 r2'))
-
-opt_trans_rule _ _ = Nothing
-
-  
--------------
-isIdNormCo :: NormalCo -> Bool
--- Cheap identity test: look for coercions with no coercion variables at all
--- So it'll return False for (sym g `trans` g)
-isIdNormCo ty = go ty
+    coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
+
+------------------
+-- | Apply 'coercionKind' to multiple 'Coercion's
+coercionKinds :: [Coercion] -> ([Type], [Type])
+coercionKinds tys = unzip $ 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
-    go (TyVarTy tv)           = not (isCoVar tv)
-    go (AppTy t1 t2)          = go t1 && go t2
-    go (FunTy t1 t2)          = go t1 && go t2
-    go (ForAllTy tv ty)        = go (tyVarKind tv) && go ty
-    go (TyConApp tc tys)       = not (isCoercionTyCon tc) && all go tys
-    go (PredTy (IParam _ ty))  = go ty
-    go (PredTy (ClassP _ tys)) = all go tys
-    go (PredTy (EqPred t1 t2)) = go t1 && go t2
-\end{code}  
+    (tys1, tys2) = coercionKinds cos
+coTyConAppKind desc cos = pprPanic "coTyConAppKind" (ppr desc $$ ppr cos)
+\end{code}
diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs
new file mode 100644 (file)
index 0000000..43de7d6
--- /dev/null
@@ -0,0 +1,403 @@
+%\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 PrelNames\r
+import Util\r
+import Outputable\r
+\end{code}\r
+\r
+%************************************************************************\r
+%*                                                                      *\r
+                 Optimising coercions                                                                  \r
+%*                                                                      *\r
+%************************************************************************\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
+-- opt_co sym co = 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
+--                co1\r
+--  where\r
+--    co1 = opt_co' sym co\r
+--    same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2\r
+--    (s,t) = coercionKind co\r
+--    (s1,t1) | sym = (t,s)\r
+--            | otherwise = (s,t)\r
+--    (s2,t2) = coercionKind co1\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
+  | isCoVar tv = mkCoPredTy (opt_co env sym co1) (opt_co env sym co2) (opt_co env sym cor)\r
+  | otherwise  = case substTyVarBndr env tv of\r
+                   (env', tv') -> ForAllTy tv' (opt_co env' sym cor)\r
+  where\r
+    (co1,co2) = coVarKind tv\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
+--------\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       -> TyConApp tc [opt_co2,opt_co1]\r
+        | otherwise -> TyConApp tc [opt_co1,opt_co2]\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 ty') sym co1_body\r
+\r
+                    -- See if is *now* a forall\r
+        | Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1\r
+        -> substTyWith [tv] [ty'] opt_co1_body -- An inefficient one-variable substitution\r
+\r
+        | otherwise\r
+        -> TyConApp tc [opt_co1, ty']\r
+        where\r
+          ty' = substTy env co2\r
+\r
+  where\r
+    (co1 : cos1) = cos\r
+    (co2 : _)    = cos1\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
+opt_trans_rule co1 co2\r
+  | Just (s1,t1,r1) <- splitCoPredTy_maybe co1\r
+  , Just (s2,t2,r2) <- etaCoPred_maybe co2\r
+  = Just (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (opt_trans r1 r2))\r
+\r
+  | Just (s2,t2,r2) <- splitCoPredTy_maybe co2\r
+  , Just (s1,t1,r1) <- etaCoPred_maybe co1\r
+  = Just (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (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
+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
+\end{code}  \r
index 958a0cb..0959699 100644 (file)
@@ -8,11 +8,12 @@ The @TyCon@ datatype
 \begin{code}
 module TyCon(
         -- * Main TyCon data types
-       TyCon, FieldLabel, CoTyConKindChecker,
+       TyCon, FieldLabel, 
 
        AlgTyConRhs(..), visibleDataCons, 
         TyConParent(..), 
        SynTyConRhs(..),
+        CoTyConDesc(..),
        AssocFamilyPermutation,
 
         -- ** Constructing TyCons
@@ -199,7 +200,7 @@ data TyCon
   | PrimTyCon {                        
        tyConUnique   :: Unique,
        tyConName     :: Name,
-       tc_kind     :: Kind,
+       tc_kind       :: Kind,
        tyConArity    :: Arity,                 -- SLPJ Oct06: I'm not sure what the significance
                                                --             of the arity of a primtycon is!
 
@@ -217,13 +218,13 @@ data TyCon
 
   -- | Type coercions, such as @(~)@, @sym@, @trans@, @left@ and @right@.
   -- INVARIANT: Coercion TyCons are always fully applied
-  --           But note that a CoercionTyCon can be over-saturated in a type.
+  --           But note that a CoTyCon can be *over*-saturated in a type.
   --           E.g.  (sym g1) Int  will be represented as (TyConApp sym [g1,Int])
-  | CoercionTyCon {    
+  | CoTyCon {  
        tyConUnique :: Unique,
         tyConName   :: Name,
        tyConArity  :: Arity,
-       coKindFun   :: CoTyConKindChecker
+       coTcDesc    :: CoTyConDesc
     }
 
   -- | Any types.  Like tuples, this is a potentially-infinite family of TyCons
@@ -250,23 +251,6 @@ data TyCon
         tyConName   :: Name
     }
 
-type CoTyConKindChecker = forall m. Monad m => CoTyConKindCheckerFun m
-
-type CoTyConKindCheckerFun m 
-  =    (Type -> m Kind)                -- Kind checker for types
-    -> (Type -> m (Type,Type)) -- and for coercions
-    -> Bool                    -- True => apply consistency checks
-    -> [Type]                  -- Exactly right number of args
-    -> m (Type, Type)          -- Kind of this application
-
-               -- ^ Function that when given a list of the type arguments to the 'TyCon'
-               -- constructs the types that the resulting coercion relates.
-               -- Returns Nothing if ill-kinded.
-               --
-               -- INVARIANT: 'coKindFun' is always applied to exactly 'tyConArity' args
-               -- E.g. for @trans (c1 :: ta=tb) (c2 :: tb=tc)@, the 'coKindFun' returns 
-               --      the kind as a pair of types: @(ta, tc)@
-
 -- | Names of the fields in an algebraic record type
 type FieldLabel = Name
 
@@ -324,7 +308,7 @@ data AlgTyConRhs
                        
                        -- See Note [Newtype eta]
       
-        nt_co :: Maybe TyCon   -- ^ A 'TyCon' (which is always a 'CoercionTyCon') that can have a 'Coercion' 
+        nt_co :: Maybe TyCon   -- ^ A 'TyCon' (which is always a 'CoTyCon') that can have a 'Coercion' 
                                 -- extracted from it to create the @newtype@ from the representation 'Type'.
                                 --
                                 -- This field is optional for non-recursive @newtype@s only.
@@ -377,7 +361,7 @@ data TyConParent
   --  of the current 'TyCon' (not the family one). INVARIANT: 
   --  the number of types matches the arity of the family 'TyCon'
   --
-  --  3) A 'CoercionTyCon' identifying the representation
+  --  3) A 'CoTyCon' identifying the representation
   --  type with the type instance family
   | FamilyTyCon
        TyCon
@@ -409,6 +393,20 @@ data SynTyConRhs
   | SynonymTyCon Type   -- ^ The synonym mentions head type variables. It acts as a
                        -- template for the expansion when the 'TyCon' is applied to some
                        -- types.
+
+--------------------
+data CoTyConDesc
+  = CoSym   | CoTrans
+  | CoLeft  | CoRight
+  | CoCsel1 | CoCsel2 | CoCselR
+  | CoInst
+
+  | CoAxiom    -- C tvs : F lhs-tys ~ rhs-ty
+      { co_ax_tvs :: [TyVar]
+      , co_ax_lhs :: Type
+      , co_ax_rhs :: Type }
+
+  | CoUnsafe 
 \end{code}
 
 Note [Newtype coercions]
@@ -420,7 +418,7 @@ newtype, to the newtype itself. For example,
    newtype T a = MkT (a -> a)
 
 the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t ->
-t.  This TyCon is a CoercionTyCon, so it does not have a kind on its
+t.  This TyCon is a CoTyCon, so it does not have a kind on its
 own; it basically has its own typing rule for the fully-applied
 version.  If the newtype T has k type variables then CoT has arity at
 most k.  In the case that the right hand side is a type application
@@ -438,7 +436,7 @@ and then when we used CoT at a particular type, s, we'd say
        CoT @ s
 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
 
-But in GHC we instead make CoT into a new piece of type syntax, CoercionTyCon,
+But in GHC we instead make CoT into a new piece of type syntax, CoTyCon,
 (like instCoercionTyCon, symCoercionTyCon etc), which must always
 be saturated, but which encodes as
        TyConApp CoT [s]
@@ -710,21 +708,14 @@ mkSynTyCon name kind tyvars rhs parent
 
 -- | Create a coercion 'TyCon'
 mkCoercionTyCon :: Name -> Arity 
-                -> CoTyConKindChecker
+                -> CoTyConDesc
                 -> TyCon
-mkCoercionTyCon name arity rule_fn
-  = CoercionTyCon {
+mkCoercionTyCon name arity desc
+  = CoTyCon {
         tyConName   = name,
         tyConUnique = nameUnique name,
         tyConArity  = arity,
-#ifdef DEBUG
-        coKindFun   = \ ty co fail args -> 
-                      ASSERT2( length args == arity, ppr name )
-                      rule_fn ty co fail args
-#else
-       coKindFun   = rule_fn
-#endif
-    }
+        coTcDesc    = desc }
 
 mkAnyTyCon :: Name -> Kind -> TyCon
 mkAnyTyCon name kind 
@@ -799,11 +790,6 @@ isNewTyCon :: TyCon -> Bool
 isNewTyCon (AlgTyCon {algTcRhs = NewTyCon {}}) = True
 isNewTyCon _                                   = False
 
-tyConHasKind :: TyCon -> Bool
-tyConHasKind (SuperKindTyCon {}) = False
-tyConHasKind (CoercionTyCon {})  = False
-tyConHasKind _                   = True
-
 -- | Take a 'TyCon' apart into the 'TyVar's it scopes over, the 'Type' it expands
 -- into, and (possibly) a coercion from the representation type to the @newtype@.
 -- Returns @Nothing@ if this is not possible.
@@ -852,9 +838,9 @@ isOpenSynTyCon tycon = isSynTyCon tycon && isOpenTyCon tycon
 isDecomposableTyCon :: TyCon -> Bool
 -- True iff we can deocmpose (T a b c) into ((T a b) c)
 -- Specifically NOT true of synonyms (open and otherwise) and coercions
-isDecomposableTyCon (SynTyCon      {}) = False
-isDecomposableTyCon (CoercionTyCon {}) = False
-isDecomposableTyCon _other             = True
+isDecomposableTyCon (SynTyCon {}) = False
+isDecomposableTyCon (CoTyCon {})  = False
+isDecomposableTyCon _other        = True
 
 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
 isGadtSyntaxTyCon :: TyCon -> Bool
@@ -972,15 +958,15 @@ isAnyTyCon _              = False
 -- | Attempt to pull a 'TyCon' apart into the arity and 'coKindFun' of
 -- a coercion 'TyCon'. Returns @Nothing@ if the 'TyCon' is not of the
 -- appropriate kind
-isCoercionTyCon_maybe :: Monad m => TyCon -> Maybe (Arity, CoTyConKindCheckerFun m)
-isCoercionTyCon_maybe (CoercionTyCon {tyConArity = ar, coKindFun = rule}) 
-  = Just (ar, rule)
+isCoercionTyCon_maybe :: TyCon -> Maybe (Arity, CoTyConDesc)
+isCoercionTyCon_maybe (CoTyCon {tyConArity = ar, coTcDesc = desc}) 
+  = Just (ar, desc)
 isCoercionTyCon_maybe _ = Nothing
 
 -- | Is this a 'TyCon' that represents a coercion?
 isCoercionTyCon :: TyCon -> Bool
-isCoercionTyCon (CoercionTyCon {}) = True
-isCoercionTyCon _                  = False
+isCoercionTyCon (CoTyCon {}) = True
+isCoercionTyCon _            = False
 
 -- | Identifies implicit tycons that, in particular, do not go into interface
 -- files (because they are implicitly reconstructed when the interface is
@@ -1000,7 +986,7 @@ isImplicitTyCon tycon | isTyConAssoc tycon           = True
                                                       isTupleTyCon tycon
 isImplicitTyCon _other                               = True
         -- catches: FunTyCon, PrimTyCon, 
-        -- CoercionTyCon, SuperKindTyCon
+        -- CoTyCon, SuperKindTyCon
 \end{code}
 
 
@@ -1064,7 +1050,12 @@ tyConKind (TupleTyCon { tc_kind = k }) = k
 tyConKind (SynTyCon   { tc_kind = k }) = k
 tyConKind (PrimTyCon  { tc_kind = k }) = k
 tyConKind (AnyTyCon   { tc_kind = k }) = k
-tyConKind tc                           = pprPanic "tyConKind" (ppr tc)
+tyConKind tc = pprPanic "tyConKind" (ppr tc)   -- SuperKindTyCon and CoTyCon
+
+tyConHasKind :: TyCon -> Bool
+tyConHasKind (SuperKindTyCon {}) = False
+tyConHasKind (CoTyCon {})        = False
+tyConHasKind _                   = True
 
 -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no constructors
 -- could be found
@@ -1243,6 +1234,18 @@ instance Ord TyCon where
 instance Uniquable TyCon where
     getUnique tc = tyConUnique tc
 
+instance Outputable CoTyConDesc where
+    ppr CoSym    = ptext (sLit "SYM")
+    ppr CoTrans  = ptext (sLit "TRANS")
+    ppr CoLeft   = ptext (sLit "LEFT")
+    ppr CoRight  = ptext (sLit "RIGHT")
+    ppr CoCsel1  = ptext (sLit "CSEL1")
+    ppr CoCsel2  = ptext (sLit "CSEL2")
+    ppr CoCselR  = ptext (sLit "CSELR")
+    ppr CoInst   = ptext (sLit "INST")
+    ppr CoUnsafe = ptext (sLit "UNSAFE")
+    ppr (CoAxiom {}) = ptext (sLit "AXIOM")
+
 instance Outputable TyCon where
     ppr tc  = ppr (getName tc) 
 
index 242e603..f894cd3 100644 (file)
@@ -47,7 +47,7 @@ module Type (
         tyFamInsts, predFamInsts,
 
         -- (Source types)
-        mkPredTy, mkPredTys, mkFamilyTyConApp,
+        mkPredTy, mkPredTys, mkFamilyTyConApp, isEqPred,
 
        -- ** Common type constructors
         funTyCon,
@@ -63,9 +63,6 @@ module Type (
        -- $kind_subtyping
         Kind, SimpleKind, KindVar,
         
-        -- ** Deconstructing Kinds 
-        kindFunResult, splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
-
         -- ** Common Kinds and SuperKinds
         liftedTypeKind, unliftedTypeKind, openTypeKind,
         argTypeKind, ubxTupleKind,
@@ -76,18 +73,9 @@ module Type (
         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
         argTypeKindTyCon, ubxTupleKindTyCon,
 
-        -- ** Predicates on Kinds
-        isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
-        isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
-        isCoSuperKind, isSuperKind, isCoercionKind, isEqPred,
-       mkArrowKind, mkArrowKinds,
-
-        isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
-        isSubKindCon,
-
        -- * Type free variables
        tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-       typeKind, expandTypeSynonyms,
+       expandTypeSynonyms,
 
        -- * Tidying type related things up for printing
        tidyType,      tidyTypes,
@@ -153,7 +141,6 @@ import VarSet
 
 import Name
 import Class
-import PrelNames
 import TyCon
 
 -- others
@@ -791,6 +778,10 @@ mkPredTy pred = PredTy pred
 mkPredTys :: ThetaType -> [Type]
 mkPredTys preds = map PredTy preds
 
+isEqPred :: PredType -> Bool
+isEqPred (EqPred _ _) = True
+isEqPred _            = False
+
 predTypeRep :: PredType -> Type
 -- ^ Convert a 'PredType' to its representation type. However, it unwraps 
 -- only the outermost level; for example, the result might be a newtype application
@@ -834,44 +825,10 @@ pprSourceTyCon tycon
 
 %************************************************************************
 %*                                                                     *
-\subsection{Kinds and free variables}
+            The free variables of a type
 %*                                                                     *
 %************************************************************************
 
----------------------------------------------------------------------
-               Finding the kind of a type
-               ~~~~~~~~~~~~~~~~~~~~~~~~~~
-\begin{code}
-typeKind :: Type -> Kind
-typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
-                                  -- We should be looking for the coercion kind,
-                                  -- not the type kind
-                               foldr (\_ k -> kindFunResult k) (tyConKind tycon) 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
-
-predKind :: PredType -> Kind
-predKind (EqPred {}) = coSuperKind     -- A coercion kind!
-predKind (ClassP {}) = liftedTypeKind  -- Class and implicitPredicates are
-predKind (IParam {}) = liftedTypeKind  -- always represented by lifted types
-\end{code}
-
-
----------------------------------------------------------------------
-               Free variables of a type
-               ~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
 tyVarsOfType :: Type -> TyVarSet
 -- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym
@@ -1587,20 +1544,20 @@ subst_ty :: TvSubst -> Type -> Type
 subst_ty subst ty
    = go ty
   where
-    go (TyVarTy tv)                = substTyVar subst tv
-    go (TyConApp tc tys)           = let args = map go tys
-                                     in  args `seqList` TyConApp tc args
+    go (TyVarTy tv)      = substTyVar subst tv
+    go (TyConApp tc tys) = let args = map go tys
+                           in  args `seqList` TyConApp tc args
 
-    go (PredTy p)                  = PredTy $! (substPred subst p)
+    go (PredTy p)        = PredTy $! (substPred subst p)
 
-    go (FunTy arg res)             = (FunTy $! (go arg)) $! (go res)
-    go (AppTy fun arg)             = mkAppTy (go fun) $! (go arg)
+    go (FunTy arg res)   = (FunTy $! (go arg)) $! (go res)
+    go (AppTy fun arg)   = mkAppTy (go fun) $! (go arg)
                 -- The mkAppTy smart constructor is important
                 -- we might be replacing (a Int), represented with App
                 -- by [Int], represented with TyConApp
-    go (ForAllTy tv ty)            = case substTyVarBndr subst tv of
-                                     (subst', tv') ->
-                                         ForAllTy tv' $! (subst_ty subst' ty)
+    go (ForAllTy tv ty)  = case substTyVarBndr subst tv of
+                              (subst', tv') ->
+                                 ForAllTy tv' $! (subst_ty subst' ty)
 
 substTyVar :: TvSubst -> TyVar  -> Type
 substTyVar subst@(TvSubst _ _) tv
@@ -1710,133 +1667,3 @@ When unifying two internal type variables, we collect their kind constraints by
 finding the GLB of the two.  Since the partial order is a tree, they only
 have a glb if one is a sub-kind of the other.  In that case, we bind the
 less-informative one to the more informative one.  Neat, eh?
-
-
-\begin{code}
-
-\end{code}
-
-%************************************************************************
-%*                                                                     *
-       Functions over Kinds            
-%*                                                                     *
-%************************************************************************
-
-\begin{code}
--- | Essentially 'funResultTy' on kinds
-kindFunResult :: Kind -> Kind
-kindFunResult k = funResultTy k
-
--- | Essentially 'splitFunTys' on kinds
-splitKindFunTys :: Kind -> ([Kind],Kind)
-splitKindFunTys k = splitFunTys k
-
-splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
-splitKindFunTy_maybe = splitFunTy_maybe
-
--- | Essentially 'splitFunTysN' on kinds
-splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
-splitKindFunTysN k = splitFunTysN k
-
--- | 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
-
-isSubOpenTypeKind :: Kind -> Bool
--- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
-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 (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 (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2')) 
-  = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
-isSubKind _             _                     = False
-
-eqKind :: Kind -> Kind -> Bool
-eqKind = tcEqType
-
-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
-  | 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
-
-isEqPred :: PredType -> Bool
-isEqPred (EqPred _ _) = True
-isEqPred _            = False
-\end{code}
index 7195e5b..a9586b6 100644 (file)
@@ -16,7 +16,7 @@ module Unify (
        Refinement, emptyRefinement, isEmptyRefinement, 
        matchRefine, refineType, refinePred, refineResType,
 
-        -- side-effect free unification
+        -- Side-effect free unification
         tcUnifyTys, BindFlag(..)
 
    ) where
index 16a1628..69b8c7e 100644 (file)
@@ -30,6 +30,9 @@ module Util (
 
         isIn, isn'tIn,
 
+        -- * Tuples
+        fstOf3, sndOf3, thirdOf3,
+
         -- * List operations controlled by another list
         takeList, dropList, splitAtList, split,
         dropTail,
@@ -181,6 +184,15 @@ nTimes 1 f = f
 nTimes n f = f . nTimes (n-1) f
 \end{code}
 
+\begin{code}
+fstOf3   :: (a,b,c) -> a    
+sndOf3   :: (a,b,c) -> b    
+thirdOf3 :: (a,b,c) -> c    
+fstOf3      (a,_,_) =  a
+sndOf3      (_,b,_) =  b
+thirdOf3    (_,_,c) =  c
+\end{code}
+
 %************************************************************************
 %*                                                                      *
 \subsection[Utils-lists]{General list processing}