+typeKind :: Type -> Kind
+typeKind ty@(TyConApp tc tys)
+ | isCoercionTyCon tc = typeKind (fst (coercionKind ty))
+ | otherwise = kindAppResult (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))
+
+ | 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 (ClassP cl args))
+ = let (lArgs, rArgs) = coercionKinds args in
+ (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
+coercionKind (PredTy (IParam name ty))
+ = let (ty1, ty2) = coercionKind ty in
+ (PredTy (IParam name ty1), PredTy (IParam name ty2))
+coercionKind (PredTy (EqPred c1 c2))
+ = pprTrace "coercionKind" (pprEqPred (c1,c2)) $
+ -- These should not show up in coercions at all
+ -- becuase they are in the form of for-alls
+ let k1 = coercionKindPredTy c1
+ k2 = coercionKindPredTy c2 in
+ (k1,k2)
+ where
+ coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2
+
+------------------
+-- | 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)