mkForAllCastCo,

         mkFunResCastCo,

         mkFunCastCoNoFTF,

         applyForAllTy,

         decomposeFunCastCo,

 -- | Cast a type by an 'MCoercion'

 mkCastTyMCo :: Type -> MCoercion -> Type

 mkCastTyMCo ty MRefl    = ty

 mkFunResMCo :: Id -> CastCoercion -> CastCoercion

 mkFunResMCo _      ReflCastCo    = ReflCastCo

 mkGReflRightMCo r ty MRefl    = mkReflCo r ty

 mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co

 -- | Like 'mkCoherenceRightCo', but with an 'MCoercion'

 mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion

 mkCoherenceRightMCo _ _  MRefl    co2 = co2

         --      res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]

       = let arg_co  = mkSelCo SelForAll (mkSymCo co)

             res_co  = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)

             subst2' = extendTCvSubst subst2 b ty

         in

         go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys

 castCoercionKind1 g r t1 t2 h

   = case g of

       Refl {} -> assert (r == Nominal) $ -- Refl is always Nominal

       GRefl _ _ mco -> case mco of

                                (mkSymCo h `mkTransCo` kind_co `mkTransCo` h)

       _ -> castCoercionKind2 g r t1 t2 h h

          else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)

     go r ty@(LitTy {})     = assert (r == Nominal) $

                              mkNomReflCo ty

                                                         (substRightCo lc co)

     go r (CoercionTy co)   = mkProofIrrelCo r kco (substLeftCo lc co)

                                                   (substRightCo lc co)

       where kco = go Nominal (coercionType co)

   where

     go (Refl ty)              = ty

     go (GRefl _ ty MRefl)     = ty

     go (TyConAppCo _ tc cos)  = mkTyConApp tc (map go cos)

     go (AppCo co1 co2)        = mkAppTy (go co1) (go co2)

     go (CoVarCo cv)           = go_covar cv

               k2  = coercionRKind k_co

               tv2 = setTyVarKind tv1 (substTy subst k2)

               subst' = extendTvSubst (extendSubstInScope subst tv2) tv1 $

     go_forall_right subst (ForAllCo { fco_tcv = cv1, fco_visR = visR

                                     , fco_kind = k_mco, fco_body = co })

     go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2

                | Just ty2' <- coreView ty2 = go ty1 ty2'

             r = coercionRole co'

         in  mkCoherenceLeftCo r ty1 co co'

             r = coercionRole co'

         in  mkCoherenceRightCo r ty2 co co'

       where kind_co  = go (tyVarKind tv1) (tyVarKind tv2)

             in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co

             ty2'     = substTyWithInScope in_scope [tv2]

                          ty2

     go (ForAllTy (Bndr cv1 flag1) ty1) (ForAllTy (Bndr cv2 flag2) ty2)

 -- | Convert a 'CastCoercion' back into a 'Coercion', using a 'UnivCo' if we

 -- have discarded the original 'Coercion'.

 castCoToCo _      (CCoercion co)         = co

 castCoToCo lhs_ty (ZCoercion rhs_ty cos) = mkUnivCo ZCoercionProv (map CoVarCo (nonDetEltsUniqSet cos)) Representational lhs_ty rhs_ty

 castCoToCo lhs_ty ReflCastCo             = mkRepReflCo lhs_ty

 topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)

   -- used to look through newtypes to the right of

   -- function arrows, in 'GHC.Core.Type.getRuntimeArgTys'

                  (opt_trans is' r1 r2')

     where

       is' = is `extendInScopeSet` tv1

 -- Push transitivity inside forall

 -- forall over coercions.

                -- override the substitution for the original variable to the

                -- re-kinded one, suitably casted

                tv2    = tv1 `setTyVarKind` coercionLKind k_co'

                         `extendSubstInScope` tv2

           _ -> (subst1, tv1)

            ; redn <- withLC lc' $ normalise_type ty

            ; return $ mkForAllRedn vis tv' k_redn redn }

     go (TyVarTy tv)    = normalise_tyvar tv

       = do { redn <- go ty

            ; lc <- getLC

            ; let co' = substRightCo lc co

            ; return $ mkCastRedn2 Nominal ty co redn co'

              --       ^^^^^^^^^^^ uses castCoercionKind2

       = do { lintType body_ty

            ; lintForAllBody tcvs body_ty }

   = do { lintType ty

        ; ty_kind <- substTyM (typeKind ty)

        ; co_lk <- lintStarCoercion co

        ; ensureEqTys ty_kind co_lk (mkCastTyErr ty co ty_kind co_lk) }

   | isForAllTy_ty tyL

   = assertPpr (isForAllTy_ty tyR) (ppr co $$ ppr ty) $

   | otherwise

   = Nothing

 mkGReflRightRedn role ty co

   = mkReduction

       (mkGReflRightCo role ty co)

 {-# INLINE mkGReflRightRedn #-}

 -- | Create a 'Reduction' from a kind cast, in which

 -- Given @ty :: k1@, @mco :: k1 ~ k2@,

 -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@

 -- at the given 'Role'.

 mkGReflRightMRedn role ty mco

   = mkReduction

 {-# INLINE mkGReflRightMRedn #-}

 -- | Create a 'Reduction' from a kind cast, in which

 -- Given @ty :: k1@, @mco :: k1 ~ k2@,

 -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@

 -- at the given 'Role'.

 mkGReflLeftMRedn role ty mco

   = mkReduction

       ty

 {-# INLINE mkGReflLeftMRedn #-}

 mkCoherenceRightRedn r (Reduction co1 ty2) kco

   = mkReduction

       (mkCoherenceRightCo r ty2 kco co1)

 {-# INLINE mkCoherenceRightRedn #-}

 -- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'.

   -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)

   = mkReduction

       (castCoercionKind1 co r ty xi cast_co)

 {-# INLINE mkCastRedn1 #-}

 -- | Apply casts on both sides of a 'Reduction' (of the given 'Role').

 mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co'

   = mkReduction

       (castCoercionKind2 nco r ty nty cast_co cast_co')

 {-# INLINE mkCastRedn2 #-}

 -- | Apply one 'Reduction' to another.

 import GHC.Data.Pair

 import Data.Semigroup

 {-

 tyCoFVsOfType (AppTy fun arg)    f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc

 tyCoFVsOfType (FunTy _ w arg res)  f bound_vars acc = (tyCoFVsOfType w `unionFV` tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc

 tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfType ty)  f bound_vars acc

 tyCoFVsOfType (CoercionTy co)    f bound_vars acc = tyCoFVsOfCo co f bound_vars acc

 tyCoFVsBndr :: ForAllTyBinder -> FV -> FV

 almost_devoid_co_var_of_mco MRefl    _  = True

 almost_devoid_co_var_of_mco (MCo co) cv = almost_devoid_co_var_of_co co cv

 almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool

 almost_devoid_co_var_of_co (Refl {}) _ = True   -- covar is allowed in Refl and

 almost_devoid_co_var_of_co (GRefl {}) _ = True  -- GRefl, so we don't look into

   && (v == cv || almost_devoid_co_var_of_type ty cv)

 almost_devoid_co_var_of_type (CastTy ty co) cv

   = almost_devoid_co_var_of_type ty cv

 almost_devoid_co_var_of_type (CoercionTy co) cv

   = almost_devoid_co_var_of_co co cv

       = ((`delVarSet` tv) <$> go ty) `mappend`

         (invisible (tyCoVarsOfType $ varType tv))

     go (LitTy {}) = mempty

     go (CoercionTy co) = invisible $ tyCoVarsOfCo co

     invisible vs = Pair vs emptyVarSet

       where (invisibles, visibles) = partitionInvisibleTypes tc tys

     go (ForAllTy tvb ty)  = tyCoFVsBndr tvb $ go ty

     go LitTy{}            = emptyFV

     go (CoercionTy co)    = tyCoFVsOfCo co

 -- | Like 'invisibleVarsOfType', but for many types.

                                       go a `unionUniqSets` go b

                                       `unionUniqSets` go_tc (funTyFlagTyCon af)

      go (ForAllTy (Bndr tv _) ty)   = go ty `unionUniqSets` go (varType tv)

      go (CoercionTy co)             = go_co co

      go_co (Refl ty)               = go ty

      go_mco MRefl    = emptyUniqSet

      go_mco (MCo co) = go_co co

      go_cos cos   = foldr (unionUniqSets . go_co)  emptyUniqSet cos

      go_tc tc = unitUniqSet tc

                       -- Failing that, try to expand a synonym

     go cxt (CastTy ty co) =  do { ty' <- go cxt ty

                                 ; return (CastTy ty' co') }

     go cxt (CoercionTy co) = do { co' <- go_co cxt co

                                 ; return (CoercionTy co') }

     go_mco _   MRefl = return MRefl

     go_mco ctx (MCo co) = MCo <$> go_co ctx co

     ------------------

     go_co cxt (Refl ty)                 = do { ty' <- go cxt ty

                                              ; return (Refl ty') }

   | CastTy

         Type

                       -- INVARIANT: The cast is never reflexive \(EQ2)

                       -- INVARIANT: The Type is not a CastTy (use TransCo instead) \(EQ3)

                       -- INVARIANT: The Type is not a ForAllTy over a tyvar \(EQ4)

     go_ty env (TyVarTy tv)      = tyvar env tv

     go_ty env (AppTy t1 t2)     = go_ty env t1 `mappend` go_ty env t2

     go_ty _   (LitTy {})        = mempty

     go_ty env (CoercionTy co)   = go_co env co

     go_ty env (FunTy _ w arg res) = go_ty env w `mappend` go_ty env arg `mappend` go_ty env res

     go_ty env (TyConApp _ tys)  = go_tys env tys

     go_cos _   []     = mempty

     go_cos env (c:cs) = go_co env c `mappend` go_cos env cs

     go_co env (Refl ty)                = go_ty env ty

     go_co env (GRefl _ ty MRefl)       = go_ty env ty

     go_co env (GRefl _ ty (MCo co))    = go_ty env ty `mappend` go_co env co

 typeSize (FunTy _ _ t1 t2)          = typeSize t1 + typeSize t2

 typeSize (ForAllTy (Bndr tv _) t)   = typeSize (varType tv) + typeSize t

 typeSize (TyConApp _ ts)            = 1 + typesSize ts

 typeSize (CoercionTy co)            = coercionSize co

 typesSize :: [Type] -> Int

         !(subst',tv') = substVarBndrUnchecked subst tv

                         -- Unchecked because subst_ty is used from substTyUnchecked

     go (LitTy n)         = LitTy $! n

     go (CoercionTy co)   = CoercionTy $! (subst_co subst co)

 substTyVar :: Subst -> TyVar -> Type

 tidyType _   t@(TyConApp _ [])      = t -- Preserve sharing if possible

 tidyType env (TyConApp tycon tys)   = TyConApp tycon $! tidyTypes env tys

 tidyType env (AppTy fun arg)        = (AppTy $! (tidyType env fun)) $! (tidyType env arg)

 tidyType env (CoercionTy co)        = CoercionTy $! (tidyCo env co)

 tidyType env ty@(FunTy _ w arg res) = let { !w'   = tidyType env w

                                           ; !arg' = tidyType env arg

         getLevity, levityType_maybe,

         mkCastTy, mkCoercionTy, splitCastTy_maybe,

         ErrorMsgType, pprUserTypeErrorTy,

 import GHC.Types.Var

 import GHC.Types.Var.Env

 import GHC.Types.Var.Set

 import GHC.Core.TyCon

 import GHC.Builtin.Types.Prim

    , mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo

    , mkKindCo, mkSubCo, mkFunCo, funRole

    , decomposePiCos, coercionKind

    , topNormaliseNewType_maybe

    )

 import {-# SOURCE #-} GHC.Tc.Utils.TcType ( isConcreteTyVar )

     go subst (ForAllTy (Bndr tv vis) t)

       = let (subst', tv') = substVarBndrUsing go subst tv in

         ForAllTy (Bndr tv' vis) (go subst' t)

     go subst (CoercionTy co) = mkCoercionTy (go_co subst co)

     go_mco _     MRefl    = MRefl

     go_mco subst (MCo co) = MCo (go_co subst co)

     go_co subst (Refl ty)

       = mkNomReflCo (go subst ty)

     go_co subst (GRefl r ty mco)

     go_ty !env (TyVarTy tv)    = tyvar env tv

     go_ty !env (AppTy t1 t2)   = mkAppTy <$> go_ty env t1 <*> go_ty env t2

     go_ty !_   ty@(LitTy {})   = return ty

     go_ty !env (CoercionTy co) = CoercionTy <$> go_co env co

     go_ty !env ty@(FunTy _ w arg res)

     go_mco !_   MRefl    = return MRefl

     go_mco !env (MCo co) = MCo <$> (go_co env co)

     go_co :: env -> Coercion -> m Coercion

     go_co !env (Refl ty)                  = Refl <$> go_ty env ty

     go_co !env (GRefl r ty mco)           = mkGReflCo r <$> go_ty env ty <*> go_mco env mco

 -- | If the type is a tyvar, possibly under a cast, returns it, along

 -- with the coercion. Thus, the co is :: kind tv ~N kind ty

 getCastedTyVar_maybe ty = case coreFullView ty of

   CastTy (TyVarTy tv) co -> Just (tv, co)

   _                      -> Nothing

 -- | Applies a type to another, as in e.g. @k a@

 mkAppTy :: Type -> Type -> Type

   -- See Note [Respecting definitional equality], invariant (EQ1).

 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])

 mkAppTy ty1               ty2 = AppTy ty1 ty2

 mkAppTys :: Type -> [Type] -> Type

 mkAppTys ty1                []   = ty1

                                      -- Why do this? See (EQ1) of

                                      -- Note [Respecting definitional equality]

                                      -- in GHC.Core.TyCo.Rep

   where

     (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys

     (args_to_cast, leftovers) = splitAtList arg_cos arg_tys

 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)

 mkAppTys ty1                tys2 = foldl' AppTy ty1 tys2

 *                                                                      *

 ********************************************************************* -}

 splitCastTy_maybe ty

   | CastTy ty' co <- coreFullView ty = Just (ty', co)

   | otherwise                        = Nothing

 -- | Make a 'CastTy'. The Coercion must be nominal. Checks the

 -- Coercion for reflexivity, dropping it if it's reflexive.

 -- See @Note [Respecting definitional equality]@ in "GHC.Core.TyCo.Rep"

 -- NB: Do the slow check here. This is important to keep the splitXXX

 -- functions working properly. Otherwise, we may end up with something

 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)

 -- | Like 'mkCastTy', but avoids checking the coercion for reflexivity,

 -- as that can be expensive.

 mk_cast_ty orig_ty co = go orig_ty

   where

     go :: Type -> Type

     go (CastTy ty co1)

       -- (EQ3) from the Note

           -- call mkCastTy again for the reflexivity check

     go (ForAllTy (Bndr tv vis) inner_ty)

       -- (EQ4) from the Note

       -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep.

       | isTyVar tv

       = -- have to make sure that pushing the co in doesn't capture the bound var!

         if tv `elemVarSet` fvs

         then let empty_subst = mkEmptySubst (mkInScopeSet fvs)

 seqType (FunTy _ w t1 t2)           = seqType w `seq` seqType t1 `seq` seqType t2

 seqType (TyConApp tc tys)           = tc `seq` seqTypes tys

 seqType (ForAllTy (Bndr tv _) ty)   = seqType (varType tv) `seq` seqType ty

 seqType (CoercionTy co)             = seqCo co

 seqTypes :: [Type] -> ()

 typeKind (LitTy l)              = typeLiteralKind l

 typeKind (FunTy { ft_af = af }) = liftedTypeOrConstraintKind (funTyFlagResultTypeOrConstraint af)

 typeKind (TyVarTy tyvar)        = tyVarKind tyvar

 typeKind (CoercionTy co)        = coercionType co

 typeKind (AppTy fun arg)

 import GHC.Prelude

 import {-# SOURCE #-} GHC.Core.TyCon

 import GHC.Utils.Misc

 import GHC.Types.Var( FunTyFlag, TyVar )

 import GHC.Types.Basic( TypeOrConstraint )

 typeKind         :: HasDebugCallStack => Type -> Type

 isCoercionTy     :: Type -> Bool

 mkAppTy          :: Type -> Type -> Type

 mkTyConApp       :: TyCon -> [Type] -> Type

 getLevity        :: HasDebugCallStack => Type -> Type

 getTyVar_maybe   :: Type -> Maybe TyVar

                           -- False <=> Matching

 type InType      = Type       -- Before applying the RnEnv2

 unify_ty :: UMEnv

          -> InType -> InType  -- Types to be unified

                               -- OutCoercion: the RnEnv has already been applied

                               -- When matching, the coercion is in "target space",

                               --   not "template space"

   | Just ty2' <- coreView ty2 = unify_ty env ty1 ty2' kco

 unify_ty env (CastTy ty1 co1) ty2 kco

     -- See (KCU1) in Note [Kind coercions in Unify]

   = maybeApart MARCast  -- See (KCU2)

   | um_unif env