+ | Just (ty', coi) <- instNewTyCon_maybe tc tys
+ = case coi of
+ ACo co -> Just (ty', co)
+ IdCo -> panic "splitNewTypeRepCo_maybe"
+ -- This case handled by coreView
+splitNewTypeRepCo_maybe _
+ = Nothing
+
+-- | Determines syntactic equality of coercions
+coreEqCoercion :: Coercion -> Coercion -> Bool
+coreEqCoercion = coreEqType
+
+coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
+coreEqCoercion2 = coreEqType2
+\end{code}
+
+
+%************************************************************************
+%* *
+ CoercionI and its constructors
+%* *
+%************************************************************************
+
+--------------------------------------
+-- CoercionI smart constructors
+-- lifted smart constructors of ordinary coercions
+
+\begin{code}
+-- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it
+-- can represent either one of:
+--
+-- 1. A proper 'Coercion'
+--
+-- 2. The identity coercion
+data CoercionI = IdCo | ACo Coercion
+
+instance Outputable CoercionI where
+ ppr IdCo = ptext (sLit "IdCo")
+ ppr (ACo co) = ppr co
+
+isIdentityCoI :: CoercionI -> Bool
+isIdentityCoI IdCo = True
+isIdentityCoI _ = False
+
+-- | Tests whether all the given 'CoercionI's represent the identity coercion
+allIdCoIs :: [CoercionI] -> Bool
+allIdCoIs = all isIdentityCoI
+
+-- | For each 'CoercionI' in the input list, return either the 'Coercion' it
+-- contains or the corresponding 'Type' from the other list
+zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
+zipCoArgs cois tys = zipWith fromCoI cois tys
+
+-- | Return either the 'Coercion' contained within the 'CoercionI' or the given
+-- 'Type' if the 'CoercionI' is the identity 'Coercion'
+fromCoI :: CoercionI -> Type -> Type
+fromCoI IdCo ty = ty -- Identity coercion represented
+fromCoI (ACo co) _ = co -- by the type itself
+
+-- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion'
+mkSymCoI :: CoercionI -> CoercionI
+mkSymCoI IdCo = IdCo
+mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
+ -- the smart constructor
+ -- is too smart with tyvars
+
+-- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion'
+mkTransCoI :: CoercionI -> CoercionI -> CoercionI
+mkTransCoI IdCo aco = aco
+mkTransCoI aco IdCo = aco
+mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
+
+-- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
+mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
+mkTyConAppCoI tyCon tys cois
+ | allIdCoIs cois = IdCo
+ | otherwise = ACo (TyConApp tyCon (zipCoArgs cois tys))
+
+-- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion'
+mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkAppTyCoI _ IdCo _ IdCo = IdCo
+mkAppTyCoI ty1 coi1 ty2 coi2 =
+ ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
+
+
+mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkFunTyCoI _ IdCo _ IdCo = IdCo
+mkFunTyCoI ty1 coi1 ty2 coi2 =
+ ACo $ mkFunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
+
+-- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion'
+mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
+mkForAllTyCoI _ IdCo = IdCo
+mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
+
+-- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion,
+-- panic
+fromACo :: CoercionI -> Coercion
+fromACo (ACo co) = co
+fromACo (IdCo {}) = panic "fromACo"
+
+-- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies:
+--
+-- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
+mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
+mkClassPPredCoI cls tys cois
+ | allIdCoIs cois = IdCo
+ | otherwise = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
+
+-- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
+mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
+mkIParamPredCoI _ IdCo = IdCo
+mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
+
+-- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
+mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkEqPredCoI _ IdCo _ IdCo = IdCo
+mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
+mkEqPredCoI _ (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
+\end{code}
+
+%************************************************************************
+%* *
+ The kind of a type, and of a coercion
+%* *
+%************************************************************************
+
+\begin{code}
+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))
+
+ | 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)