+---------------------------------------------------
+-- 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
+