Tidy up coercions, and implement csel1, csel2, cselR

In preparation for implementing the PushC rule for coercion-swizzling
in the Simplifier, I had to inmplement the three new decomposition
operators for coercions, which I've called csel1, csel2, and cselR.

     co :: ((s1~t1) => r1) ~ ((s2~t2) => r2)
     ---------------------------------------
              csel1 co :: s1~s2

and similarly csel2, cselR.

On the way I fixed the coercionKind function for types of form
          (s1~t2) => r2
which currently are expressed as a forall type.  

And I refactored quite a bit to help myself understand what is
going on.

8 files changed, 272 insertions, 131 deletions

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index 5156bbcf40..2cbe7449af 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -37,6 +37,7 @@ import DynFlags
 import Outputable
 import FastString
 import Util
+import Control.Monad
 import Data.Maybe
 \end{code}
 
@@ -99,11 +100,22 @@ lintCoreBindings dflags _whoDunnit _binds
   = return ()
 
 lintCoreBindings dflags whoDunnit binds
-  = case (initL (lint_binds binds)) of
-      Nothing       -> showPass dflags ("Core Linted result of " ++ whoDunnit)
-      Just bad_news -> printDump (display bad_news)	>>
-		       ghcExit dflags 1
+  | isEmptyBag errs
+  = do { showPass dflags ("Core Linted result of " ++ whoDunnit)
+       ; unless (isEmptyBag warns) $ printDump $
+         (banner "warnings" $$ displayMessageBag warns)
+       ; return () }
+
+  | otherwise
+  = do { printDump (vcat [ banner "errors", displayMessageBag errs
+			 , ptext (sLit "*** Offending Program ***")
+			 , pprCoreBindings binds
+			 , ptext (sLit "*** End of Offense ***") ])
+
+       ; ghcExit dflags 1 }
   where
+    (warns, errs) = initL (lint_binds binds)
+
 	-- Put all the top-level binders in scope at the start
 	-- This is because transformation rules can bring something
 	-- into use 'unexpectedly'
@@ -114,13 +126,12 @@ lintCoreBindings dflags whoDunnit binds
     lint_bind (Rec prs)		= mapM_ (lintSingleBinding TopLevel Recursive) prs
     lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
 
-    display bad_news
-      = vcat [  text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
-		bad_news,
-		ptext (sLit "*** Offending Program ***"),
-		pprCoreBindings binds,
-		ptext (sLit "*** End of Offense ***")
-	]
+    banner string = ptext (sLit "*** Core Lint")      <+> text string 
+                    <+> ptext (sLit ": in result of") <+> text whoDunnit 
+                    <+> ptext (sLit "***")
+
+displayMessageBag :: Bag Message -> SDoc
+displayMessageBag msgs = vcat (punctuate blankLine (bagToList msgs))
 \end{code}
 
 %************************************************************************
@@ -139,9 +150,12 @@ lintUnfolding :: SrcLoc
 	      -> Maybe Message	-- Nothing => OK
 
 lintUnfolding locn vars expr
-  = initL (addLoc (ImportedUnfolding locn) $
-	   addInScopeVars vars	           $
-	   lintCoreExpr expr)
+  | isEmptyBag errs = Nothing
+  | otherwise       = Just (displayMessageBag errs)
+  where
+    (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
+                            addInScopeVars vars	           $
+                            lintCoreExpr expr)
 \end{code}
 
 %************************************************************************
@@ -172,6 +186,9 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
         -- Check whether binder's specialisations contain any out-of-scope variables
        ; mapM_ (checkBndrIdInScope binder) bndr_vars 
 
+       ; when (isLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
+              (addWarnL (ptext (sLit "INLINE binder is loop breaker:") <+> ppr binder))
+
       -- Check whether arity and demand type are consistent (only if demand analysis
       -- already happened)
        ; checkL (case maybeDmdTy of
@@ -351,7 +368,7 @@ lintCoreArg fun_ty arg =
         Just (arg,res) -> 
           do { checkTys arg arg_ty err1
              ; return res }
-        _ -> addErrL err2 }
+        _ -> failWithL err2 }
 \end{code}
 
 \begin{code}
@@ -359,7 +376,7 @@ lintCoreArg fun_ty arg =
 lintTyApp :: OutType -> OutType -> LintM OutType
 lintTyApp ty arg_ty 
   = case splitForAllTy_maybe ty of
-      Nothing -> addErrL (mkTyAppMsg ty arg_ty)
+      Nothing -> failWithL (mkTyAppMsg ty arg_ty)
 
       Just (tyvar,body)
         -> do	{ checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
@@ -372,12 +389,15 @@ checkKinds tyvar arg_ty
 	-- tyvar; notably this is used so that we can give
 	-- 	error :: forall a:*. String -> a
 	-- and then apply it to both boxed and unboxed types.
-  = checkL (arg_kind `isSubKind` tyvar_kind)
-	   (mkKindErrMsg tyvar arg_ty)
+  | isCoVar tyvar = unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
+                           (addErrL (mkCoAppErrMsg tyvar arg_ty))
+  | otherwise     = unless (arg_kind `isSubKind` tyvar_kind)
+                           (addErrL (mkKindErrMsg tyvar arg_ty))
   where
     tyvar_kind = tyVarKind tyvar
-    arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
-	     | otherwise     = typeKind arg_ty
+    arg_kind   = typeKind arg_ty
+    (s1,t1) = coVarKind tyvar
+    (s2,t2) = coercionKind arg_ty
 
 checkDeadIdOcc :: Id -> LintM ()
 -- Occurrences of an Id should never be dead....
@@ -561,8 +581,10 @@ newtype LintM a =
             TvSubst ->               -- Current type substitution; we also use this
 				     -- to keep track of all the variables in scope,
 				     -- both Ids and TyVars
-	    Bag Message ->           -- Error messages so far
-	    (Maybe a, Bag Message) } -- Result and error messages (if any)
+	    WarnsAndErrs ->           -- Error and warning messages so far
+	    (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
+
+type WarnsAndErrs = (Bag Message, Bag Message)
 
 {-	Note [Type substitution]
 	~~~~~~~~~~~~~~~~~~~~~~~~
@@ -581,7 +603,7 @@ Here we substitute 'ty' for 'a' in 'body', on the fly.
 
 instance Monad LintM where
   return x = LintM (\ _   _     errs -> (Just x, errs))
-  fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
+  fail err = failWithL (text err)
   m >>= k  = LintM (\ loc subst errs -> 
                        let (res, errs') = unLintM m loc subst errs in
                          case res of
@@ -601,25 +623,33 @@ data LintLocInfo
 
                  
 \begin{code}
-initL :: LintM a -> Maybe Message {- errors -}
+initL :: LintM a -> WarnsAndErrs    -- Errors and warnings
 initL m
-  = case unLintM m [] emptyTvSubst emptyBag of
-      (_, errs) | isEmptyBag errs -> Nothing
-		| otherwise	  -> Just (vcat (punctuate blankLine (bagToList errs)))
+  = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
+      (_, errs) -> errs
 \end{code}
 
 \begin{code}
 checkL :: Bool -> Message -> LintM ()
 checkL True  _   = return ()
-checkL False msg = addErrL msg
+checkL False msg = failWithL msg
+
+failWithL :: Message -> LintM a
+failWithL msg = LintM $ \ loc subst (warns,errs) ->
+                (Nothing, (warns, addMsg subst errs msg loc))
 
-addErrL :: Message -> LintM a
-addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
+addErrL :: Message -> LintM ()
+addErrL msg = LintM $ \ loc subst (warns,errs) -> 
+              (Just (), (warns, addMsg subst errs msg loc))
 
-addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
-addErr subst errs_so_far msg locs
+addWarnL :: Message -> LintM ()
+addWarnL msg = LintM $ \ loc subst (warns,errs) -> 
+              (Just (), (addMsg subst warns msg loc, errs))
+
+addMsg :: TvSubst ->  Bag Message -> Message -> [LintLocInfo] -> Bag Message
+addMsg subst msgs msg locs
   = ASSERT( notNull locs )
-    errs_so_far `snocBag` mk_msg msg
+    msgs `snocBag` mk_msg msg
   where
    (loc, cxt1) = dumpLoc (head locs)
    cxts        = [snd (dumpLoc loc) | loc <- locs]   
@@ -644,7 +674,7 @@ addInScopeVars vars m
   | null dups
   = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
   | otherwise
-  = addErrL (dupVars dups)
+  = failWithL (dupVars dups)
   where
     (_, dups) = removeDups compare vars 
 
@@ -672,7 +702,7 @@ lookupIdInScope id
   = do	{ subst <- getTvSubst
 	; case lookupInScope (getTvInScope subst) id of
 		Just v  -> return v
-		Nothing -> do { _ <- addErrL out_of_scope
+		Nothing -> do { addErrL out_of_scope
 			      ; return id } }
   where
     out_of_scope = ppr id <+> ptext (sLit "is out of scope")
@@ -837,6 +867,14 @@ mkKindErrMsg tyvar arg_ty
 	  hang (ptext (sLit "Arg type:"))   
 	         4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 
+mkCoAppErrMsg :: TyVar -> Type -> Message
+mkCoAppErrMsg tyvar arg_ty
+  = vcat [ptext (sLit "Kinds don't match in coercion application:"),
+	  hang (ptext (sLit "Coercion variable:"))
+		 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
+	  hang (ptext (sLit "Arg coercion:"))   
+	         4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
+
 mkTyAppMsg :: Type -> Type -> Message
 mkTyAppMsg ty arg_ty
   = vcat [text "Illegal type application:",
diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs
index 5dff2c81f7..23eec4917b 100644
--- a/compiler/coreSyn/CoreUtils.lhs
+++ b/compiler/coreSyn/CoreUtils.lhs
@@ -210,7 +210,7 @@ mkCoerce co expr
 --    if to_ty `coreEqType` from_ty
 --    then expr
 --    else 
-        ASSERT2(from_ty `coreEqType` (exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ ppr (coercionKindPredTy co))
+        ASSERT2(from_ty `coreEqType` (exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ pprEqPred (coercionKind co))
          (Cast expr co)
 \end{code}
 
diff --git a/compiler/coreSyn/PprCore.lhs b/compiler/coreSyn/PprCore.lhs
index 3bdb79c331..56c6572a5e 100644
--- a/compiler/coreSyn/PprCore.lhs
+++ b/compiler/coreSyn/PprCore.lhs
@@ -123,7 +123,7 @@ ppr_expr add_par (Cast expr co)
   where
     pprCo co | opt_SuppressCoercions = ptext (sLit "...")
              | otherwise = parens
-                         $ sep [ppr co, dcolon <+> ppr (coercionKindPredTy co)]
+                         $ sep [ppr co, dcolon <+> pprEqPred (coercionKind co)]
 	 
 
 ppr_expr add_par expr@(Lam _ _)
@@ -407,18 +407,20 @@ instance Outputable Unfolding where
       		     , uf_expandable=exp, uf_guidance=g, uf_arity=arity}) 
 	= ptext (sLit "Unf") <> braces (pp_info $$ pp_rhs)
     where
-      pp_info = hsep [ ptext (sLit "TopLvl=") <> ppr top 
-                     , ptext (sLit "Arity=") <> int arity
-                     , ptext (sLit "Value=") <> ppr hnf
-                     , ptext (sLit "ConLike=") <> ppr conlike
-                     , ptext (sLit "Cheap=") <> ppr cheap
-                     , ptext (sLit "Expandable=") <> ppr exp
-                     , ppr g ]
+      pp_info = fsep $ punctuate comma 
+                [ ptext (sLit "TopLvl=")     <> ppr top 
+                , ptext (sLit "Arity=")      <> int arity
+                , ptext (sLit "Value=")      <> ppr hnf
+                , ptext (sLit "ConLike=")    <> ppr conlike
+                , ptext (sLit "Cheap=")      <> ppr cheap
+                , ptext (sLit "Expandable=") <> ppr exp
+                , ptext (sLit "Guidance=")   <> ppr g ]
+      pp_tmpl = ptext (sLit "Tmpl=") <+> ppr rhs
       pp_rhs = case g of
       	      	  UnfoldNever         -> usually_empty
 		  UnfoldIfGoodArgs {} -> usually_empty
-                  _other              -> ppr rhs
-      usually_empty = ifPprDebug (ppr rhs)
+                  _other              -> pp_tmpl
+      usually_empty = ifPprDebug pp_tmpl
             -- In this case show 'rhs' only in debug mode
 \end{code}
 
diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs
index 842f98de86..b5c48fee02 100644
--- a/compiler/prelude/PrelNames.lhs
+++ b/compiler/prelude/PrelNames.lhs
@@ -1026,7 +1026,8 @@ argTypeKindTyConKey                     = mkPreludeTyConUnique 91
 
 -- Coercion constructors
 symCoercionTyConKey, transCoercionTyConKey, leftCoercionTyConKey,
-    rightCoercionTyConKey, instCoercionTyConKey, unsafeCoercionTyConKey
+    rightCoercionTyConKey, instCoercionTyConKey, unsafeCoercionTyConKey,
+    csel1CoercionTyConKey, csel2CoercionTyConKey, cselRCoercionTyConKey
     :: Unique
 symCoercionTyConKey                     = mkPreludeTyConUnique 93
 transCoercionTyConKey                   = mkPreludeTyConUnique 94
@@ -1034,10 +1035,13 @@ leftCoercionTyConKey                    = mkPreludeTyConUnique 95
 rightCoercionTyConKey                   = mkPreludeTyConUnique 96
 instCoercionTyConKey                    = mkPreludeTyConUnique 97
 unsafeCoercionTyConKey                  = mkPreludeTyConUnique 98
+csel1CoercionTyConKey                   = mkPreludeTyConUnique 99
+csel2CoercionTyConKey                   = mkPreludeTyConUnique 100
+cselRCoercionTyConKey                   = mkPreludeTyConUnique 101
 
 unknownTyConKey, unknown1TyConKey, unknown2TyConKey, unknown3TyConKey,
     opaqueTyConKey :: Unique
-unknownTyConKey				= mkPreludeTyConUnique 99
+unknownTyConKey				= mkPreludeTyConUnique 129
 unknown1TyConKey			= mkPreludeTyConUnique 130
 unknown2TyConKey			= mkPreludeTyConUnique 131
 unknown3TyConKey			= mkPreludeTyConUnique 132
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index bec90db772..83a5af341c 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -1,4 +1,4 @@
-%
+T%
 % (c) The University of Glasgow 2006
 %
 
@@ -21,8 +21,8 @@ module Coercion (
         -- * Main data type
         Coercion,
  
-        mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
-        coercionKind, coercionKinds, coercionKindPredTy, isIdentityCoercion,
+        mkCoKind, mkReflCoKind, coVarKind,
+        coercionKind, coercionKinds, isIdentityCoercion,
 
 	-- ** Equality predicates
 	isEqPred, mkEqPred, getEqPredTys, isEqPredTy,  
@@ -34,12 +34,14 @@ module Coercion (
 	mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
         mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
+        mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, 
 
         splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
 
         unsafeCoercionTyCon, symCoercionTyCon,
         transCoercionTyCon, leftCoercionTyCon, 
         rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
+        csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon, 
 
         -- ** Optimisation
 	optCoercion,
@@ -98,6 +100,24 @@ decomposeCo n co
 -------------------------------------------------------
 -- and some coercion kind stuff
 
+coVarKind :: CoVar -> (Type,Type) 
+-- c :: t1 ~ t2
+coVarKind cv = splitCoVarKind (tyVarKind cv)
+
+-- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
+-- Panics if the argument is not a valid 'CoercionKind'
+splitCoVarKind :: Kind -> (Type, Type)
+splitCoVarKind co | Just co' <- kindView co = splitCoVarKind co'
+splitCoVarKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
+
+-- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion'
+mkCoKind :: Type -> Type -> CoercionKind
+mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
+
+-- | (mkCoPredTy s t r) produces the type:   (s~t) => r
+mkCoPredTy :: Type -> Type -> Type -> Type
+mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r
+
 -- | Tests whether a type is just a type equality predicate
 isEqPredTy :: Type -> Bool
 isEqPredTy (PredTy pred) = isEqPred pred
@@ -113,34 +133,17 @@ getEqPredTys :: PredType -> (Type,Type)
 getEqPredTys (EqPred ty1 ty2) = (ty1, ty2)
 getEqPredTys other	      = pprPanic "getEqPredTys" (ppr other)
 
--- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion'
-mkCoKind :: Type -> Type -> CoercionKind
-mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2)
-
 -- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself
 mkReflCoKind :: Type -> CoercionKind
 mkReflCoKind ty = mkCoKind ty ty
 
--- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'.
--- Panics if the argument is not a valid 'CoercionKind'
-splitCoercionKind :: CoercionKind -> (Type, Type)
-splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co'
-splitCoercionKind (PredTy (EqPred ty1 ty2))    = (ty1, ty2)
-
--- | Take a 'CoercionKind' apart into the two types it relates, if possible. See also 'splitCoercionKind'
-splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
-splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co'
-splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
-splitCoercionKind_maybe _ = Nothing
-
 -- | 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)@.
--- See also 'coercionKindPredTy'
 coercionKind :: Coercion -> (Type, Type)
-coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
+coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
                             | otherwise = (ty, ty)
 coercionKind (AppTy ty1 ty2) 
   = let (t1, t2) = coercionKind ty1
@@ -161,13 +164,40 @@ coercionKind (FunTy ty1 ty2)
   = let (t1, t2) = coercionKind ty1
         (s1, s2) = coercionKind ty2 in
     (mkFunTy t1 s1, mkFunTy t2 s2)
-coercionKind (ForAllTy tv ty) 
+
+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)) 
-  = let k1 = coercionKindPredTy c1
+  = 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))
@@ -175,11 +205,6 @@ coercionKind (PredTy (IParam name ty))
   = let (ty1, ty2) = coercionKind ty in
     (PredTy (IParam name ty1), PredTy (IParam name ty2))
 
--- | Recover the 'CoercionKind' corresponding to a particular 'Coerceion'. See also 'coercionKind'
--- and 'mkCoKind'
-coercionKindPredTy :: Coercion -> CoercionKind
-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
@@ -189,11 +214,17 @@ isIdentityCoercion :: Coercion -> Bool
 isIdentityCoercion co  
   = case coercionKind co of
        (t1,t2) -> t1 `coreEqType` t2
+\end{code}
 
--------------------------------------
--- Coercion kind and type mk's
--- (make saturated TyConApp CoercionTyCon{...} args)
+%************************************************************************
+%*									*
+            Building coercions
+%*									*
+%************************************************************************
 
+Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args)
+
+\begin{code}
 -- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to
 -- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function
 -- if possible
@@ -323,6 +354,12 @@ mkRightCoercions n co
        = acc
 
 
+mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
+mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
+mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
+mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co]
+
+-------------------------------
 mkInstCoercion :: Coercion -> Type -> Coercion
 -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
 -- the resulting beta-reduction, otherwise it creates a suspended instantiation.
@@ -432,24 +469,34 @@ mkFamInstCoercion name tvs family instTys rep_tycon
     rule args = (substTyWith tvs args $		     -- with sigma = [tys/tvs],
 		   TyConApp family instTys,	     --       sigma (F ts)
 		 TyConApp rep_tycon args)	     --   ~ R tys
+\end{code}
 
---------------------------------------
--- Coercion Type Constructors...
-
--- Example.  The coercion ((sym c) (sym d) (sym e))
--- will be represented by (TyConApp sym [c, sym d, sym e])
--- If sym c :: p1=q1
---    sym d :: p2=q2
---    sym e :: p3=q3
--- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
-
--- | Coercion type constructors: avoid using these directly and instead use the @mk*Coercion@ and @split*Coercion@ family
--- of functions if possible.
-symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon
+
+%************************************************************************
+%*									*
+            Coercion Type Constructors
+%*									*
+%************************************************************************
+
+Example.  The coercion ((sym c) (sym d) (sym e))
+will be represented by (TyConApp sym [c, sym d, sym e])
+If sym c :: p1=q1
+   sym d :: p2=q2
+   sym e :: p3=q3
+then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
+
+\begin{code}
+-- | Coercion type constructors: avoid using these directly and instead use 
+-- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
+--
 -- Each coercion TyCon is built with the special CoercionTyCon record and
 -- carries its own kinding rule.  Such CoercionTyCons must be fully applied
 -- by any TyConApp in which they are applied, however they may also be over
 -- applied (see example above) and the kinding function must deal with this.
+symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, 
+  rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon,
+  csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon
+
 symCoercionTyCon = 
   mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf
   where
@@ -462,43 +509,42 @@ transCoercionTyCon =
   where
     composeCoercionKindsOf (co1:co2:rest)
       = ASSERT( null rest )
-        WARN( not (r1 `coreEqType` a2), 
+        WARN( not (r1 `coreEqType` a2),
               text "Strange! Type mismatch in trans coercion, probably a bug"
               $$
-              ppr r1 <+> text "=/=" <+> ppr a2)
+	      _err_stuff )
         (a1, r2)
       where
         (a1, r1) = coercionKind co1
         (a2, r2) = coercionKind co2 
 
-leftCoercionTyCon =
-  mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
-  where
-    leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
-      where
-        (ty1,ty2) = fst (splitCoercionKindOf co)
+        _err_stuff = vcat [ text "co1:" <+> ppr co1
+                          , text "co1 kind left:"  <+> ppr a1
+                          , text "co1 kind right:" <+> ppr r1
+                          , text "co2:" <+> ppr co2
+                          , text "co2 kind left:"  <+> ppr a2
+                          , text "co2 kind right:" <+> ppr r2 ]
 
-rightCoercionTyCon =
-  mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
-  where
-    rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
-      where
-        (ty1,ty2) = snd (splitCoercionKindOf co)
+---------------------------------------------------
+leftCoercionTyCon  = mkCoercionTyCon leftCoercionTyConName  1 (fst . decompLR)
+rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (snd . decompLR)
 
-splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
+decompLR :: [Type] -> ((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))
-splitCoercionKindOf co
-  | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
+decompLR (co : rest)
+  | (ty1, ty2) <- coercionKind co
   , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
   , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2
-  = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
-splitCoercionKindOf co 
-  = pprPanic "Coercion.splitCoercionKindOf" 
-             (ppr co $$ ppr (coercionKindPredTy co))
+  = ASSERT( null rest) 
+    ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
+decompLR cos 
+  = pprPanic "Coercion.decompLR" 
+             (ppr cos $$ vcat (map (pprEqPred .coercionKind) cos))
 
+---------------------------------------------------
 instCoercionTyCon 
   =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind
   where
@@ -510,29 +556,71 @@ instCoercionTyCon
 				     (instantiateCo t1 ty, instantiateCo t2 ty)
       where (t1, t2) = coercionKind co1
 
+---------------------------------------------------
 unsafeCoercionTyCon 
   = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
   where
    unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) 
         
+---------------------------------------------------
+-- The csel* family
+--   If         co :: (s1~t1 => r1) ~ (s2~t2 => r2)
+-- Then   csel1 co :: s1 ~ s2
+--        csel2 co :: t1 ~ t2
+--        cselR co :: r1 ~ r2
+
+csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (fstOf3   . decompCsel)
+csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (sndOf3   . decompCsel)
+cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (thirdOf3 . decompCsel)
+
+decompCsel :: [Coercion] -> ((Type,Type), (Type,Type), (Type,Type))
+decompCsel (co : rest)
+  | (ty1,ty2) <- coercionKind co
+  , Just (cv1, r1) <- splitForAllTy_maybe ty1
+  , Just (cv2, r2) <- splitForAllTy_maybe ty2
+  , (s1,t1) <- ASSERT( isCoVar cv1) coVarKind cv1
+  , (s2,t2) <- ASSERT( isCoVar cv1) coVarKind cv2
+  = ASSERT( null rest )
+    ((s1,s2), (t1,t2), (r1,r2))
+decompCsel other = pprPanic "decompCsel" (ppr other)
+
+fstOf3   :: (a,b,c) -> a    
+sndOf3   :: (a,b,c) -> b    
+thirdOf3 :: (a,b,c) -> c    
+fstOf3      (a,_,_) =  a
+sndOf3      (_,b,_) =  b
+thirdOf3    (_,_,c) =  c
+
 --------------------------------------
--- ...and their names
+-- 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
-
-transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: 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
-unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
+\end{code}
 
 
+%************************************************************************
+%*									*
+            Newtypes
+%*									*
+%************************************************************************
 
+\begin{code}
 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
 -- ^ If @co :: T ts ~ rep_ty@ then:
 --
@@ -574,6 +662,12 @@ coreEqCoercion = coreEqType
 \end{code}
 
 
+%************************************************************************
+%*									*
+            CoercionI and its constructors
+%*									*
+%************************************************************************
+
 --------------------------------------
 -- CoercionI smart constructors
 --	lifted smart constructors of ordinary coercions
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index 590819443c..8dfe475349 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -132,7 +132,7 @@ module Type (
 
 	-- * Pretty-printing
 	pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
-	pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind,
+	pprPred, pprEqPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind,
 	
 	pprSourceTyCon
     ) where
@@ -446,8 +446,8 @@ splitAppTys ty = split ty ty []
 \begin{code}
 mkFunTy :: Type -> Type -> Type
 -- ^ Creates a function type from the given argument and result type
-mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildCoVar (PredTy (EqPred ty1 ty2))) res
-mkFunTy arg res = FunTy arg res
+mkFunTy arg@(PredTy (EqPred {})) res = ForAllTy (mkWildCoVar arg) res
+mkFunTy arg                      res = FunTy    arg               res
 
 mkFunTys :: [Type] -> Type -> Type
 mkFunTys tys ty = foldr mkFunTy ty tys
diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs
index c1670f67bd..a5176ce0ed 100644
--- a/compiler/types/TypeRep.lhs
+++ b/compiler/types/TypeRep.lhs
@@ -20,7 +20,7 @@ module TypeRep (
 	-- Pretty-printing
 	pprType, pprParendType, pprTypeApp,
 	pprTyThing, pprTyThingCategory, 
-	pprPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
+	pprPred, pprEqPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
 
 	-- Kinds
 	liftedTypeKind, unliftedTypeKind, openTypeKind,
@@ -428,9 +428,12 @@ pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
 pprPred :: PredType -> SDoc
 pprPred (ClassP cls tys) = pprClassPred cls tys
 pprPred (IParam ip ty)   = ppr ip <> dcolon <> pprType ty
-pprPred (EqPred ty1 ty2) = sep [ ppr_type FunPrec ty1
-                               , nest 2 (ptext (sLit "~"))
-                               , ppr_type FunPrec ty2]
+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]
 			       -- Precedence looks like (->) so that we get
 			       --    Maybe a ~ Bool
 			       --    (a->a) ~ Bool
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 07c927ca80..7195e5b2f5 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -206,7 +206,7 @@ match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
 -- Match the kind of the template tyvar with the kind of Type
 -- Note [Matching kinds]
 match_kind menv subst tv ty
-  | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
+  | isCoVar tv = do { let (ty1,ty2) = coVarKind tv
 			  (ty3,ty4) = coercionKind ty
 		    ; subst1 <- match menv subst ty1 ty3
 		    ; match menv subst1 ty2 ty4 }