seqCastCoercion :: CastCoercion -> ()

 seqCastCoercion (CCoercion co) = seqCo co

 seqCastCoercion (ZCoercion ty cos) = seqType ty `seq` seqVarSet cos

 seqCo :: Coercion -> ()

 seqCo (Refl ty)             = seqType ty

 castCoercionLKind :: HasDebugCallStack => Type -> CastCoercion -> Type

 castCoercionLKind _ (CCoercion co) = coercionLKind co

 castCoercionLKind lhs_ty (ZCoercion _ _) = lhs_ty

 -- | Compute the right type of a 'CastCoercion', like 'coercionRKind'.

 -- | Equality test on 'CastCoercion', where the LHS type is the same for both

 -- coercions, so we merely need to compare the RHS types.

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

 -- have discarded the original 'Coercion'.

 castCoToCo :: Type -> CastCoercion -> CoercionR

 castCoToCo _      (CCoercion co)         = co

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

 -- | Compose two 'CastCoercion's transitively, like 'mkTransCo'.  If either is

 -- zapped the whole result will be zapped.

 mkTransCastCo :: HasDebugCallStack => CastCoercion -> CastCoercion -> CastCoercion

 mkTransCastCo cco (CCoercion co)     = mkTransCastCoCo cco co

 mkTransCastCo cco (ZCoercion ty cos) = ZCoercion ty (shallowCoVarsOfCastCo cco `unionVarSet` cos)

 -- | Transitively compose a 'CastCoercion' followed by a 'Coercion'.

 mkTransCastCoCo :: HasDebugCallStack => CastCoercion -> Coercion -> CastCoercion

 mkTransCastCoCo (CCoercion co1)   co2 = CCoercion (mkTransCo co1 co2)

 mkTransCastCoCo (ZCoercion _ cos) co2 = ZCoercion (coercionRKind co2) (shallowCoVarsOfCo co2 `unionVarSet` cos)

 -- | Transitively compose a 'Coercion' followed by a 'CastCoercion'.

 mkTransCoCastCo :: HasDebugCallStack => Coercion -> CastCoercion -> CastCoercion

 mkTransCoCastCo co1 (CCoercion co2)    = CCoercion (mkTransCo co1 co2)

 mkTransCoCastCo co1 (ZCoercion ty cos) = ZCoercion ty (shallowCoVarsOfCo co1 `unionVarSet` cos)

 -- | Slowly checks if the coercion is reflexive. Don't call this in a loop,

 -- as it walks over the entire coercion.

 isReflexiveCastCo :: Type -> CastCoercion -> Bool

 isReflexiveCastCo _      (CCoercion co) = isReflexiveCo co

 isReflexiveCastCo lhs_ty (ZCoercion rhs_ty _) = lhs_ty `eqType` rhs_ty

 cast_co_fvs :: CastCoercion -> FV

 cast_co_fvs (CCoercion co)     fv_cand in_scope acc = (tyCoFVsOfCo co) fv_cand in_scope acc

 cast_co_fvs (ZCoercion ty cos) fv_cand in_scope acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCoVarSet cos) fv_cand in_scope acc

 ---------

 rhs_fvs :: (Id, CoreExpr) -> FV

 import GHC.Data.TrieMap

 import GHC.Core.Map.Type

 import GHC.Core

 import GHC.Core.Type

 import GHC.Types.Tickish

 import GHC.Types.Var

     go (Type t1)    (Type t2)        = eqDeBruijnType (D env1 t1) (D env2 t2)

     -- See Note [Alpha-equality for Coercion arguments]

     go (Coercion {}) (Coercion {}) = True

     go (App f1 a1)   (App f2 a2)   = go f1 f2 && go a1 a2

     go (Tick n1 e1) (Tick n2 e2)

       =  eqDeBruijnTickish (D env1 n1) (D env2 n2)

     go (Lit l)              = cm_lit  >.> lookupTM l

     go (Type t)             = cm_type >.> lkG (D env t)

     go (Coercion c)         = cm_co   >.> lkG (D env c)

     go (Tick tickish e)     = cm_tick >.> lkG (D env e) >=> lkTickish tickish

     go (App e1 e2)          = cm_app  >.> lkG (D env e2) >=> lkG (D env e1)

     go (Lam v e)            = cm_lam  >.> lkG (D (extendCME env v) e)

                                                  |> xtG (D env c) f }

 xtE (D _   (Lit l))              f m = m { cm_lit  = cm_lit m  |> alterTM l f }

 xtE (D env (Cast e c))           f m = m { cm_cast = cm_cast m |> xtG (D env e)

 xtE (D env (Tick t e))           f m = m { cm_tick = cm_tick m |> xtG (D env e)

                                                  |>> xtTickish t f }

 xtE (D env (App e1 e2))          f m = m { cm_app = cm_app m |> xtG (D env e2)

     {-# INLINE fmap #-}

 instance TrieMap CastCoercionMap where

    emptyTM                     = CastCoercionMap emptyTM

    lookupTM k   (CastCoercionMap m) = lookupTM (deBruijnize k) m

    alterTM k f  (CastCoercionMap m) = CastCoercionMap (alterTM (deBruijnize k) f m)

     {-# INLINE fmap #-}

 instance TrieMap CastCoercionMapX where

   emptyTM = CastCoercionMapX emptyTM

   lookupTM = lkX

   alterTM  = xtX

   filterTM f (CastCoercionMapX core_tm) = CastCoercionMapX (filterTM f core_tm)

   mapMaybeTM f (CastCoercionMapX core_tm) = CastCoercionMapX (mapMaybeTM f core_tm)

 {-

     go :: [Var] -> CoreExpr -> ([Var], CoreExpr)

     -- The accumulator is in reverse order

     go bs (Lam b e)   = go (b:bs) e

     go bs e           = (reverse bs, e)

     -- We are in a cast; peel off casts until we hit a lambda.

     -- (go_c bs e c) is same as (go bs e (e |> c))

     go_c bs (Lam b e)    co  = go_lam bs b e co

     -- We are in a lambda under a cast; peel off lambdas and build a

     -- new coercion for the body.

     -- (go_lam bs b e c) is same as (go_c bs (\b.e) c)

       | isTyVar b

       , let Pair tyL tyR = coercionKind co

       , assert (isForAllTy_ty tyL) $

         isForAllTy_ty tyR

       , isReflCo (mkSelCo SelForAll co)  -- See Note [collectBindersPushingCo]

       | isCoVar b

       , let Pair tyL tyR = coercionKind co

         isForAllTy_co tyR

       , isReflCo (mkSelCo SelForAll co)  -- See Note [collectBindersPushingCo]

       , let cov = mkCoVarCo b

       | isId b

       , let Pair tyL tyR = coercionKind co

       , (co_mult, co_arg, co_res) <- decomposeFunCo co

       , isReflCo co_mult -- See Note [collectBindersPushingCo]

       , isReflCo co_arg  -- See Note [collectBindersPushingCo]

 {- Note [collectBindersPushingCo]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   where

     (cpr_ty, e') = cprAnal env e

     cpr_ty'

 cprAnal' env (Tick t e)

   = (cpr_ty, Tick t e')

 castCoercionDmdEnv :: CastCoercion -> DmdEnv

 castCoercionDmdEnv (CCoercion co)    = coercionDmdEnv co

 castCoercionDmdEnv (ZCoercion _ cos) = coVarSetDmdEnv cos

 coercionsDmdEnv :: [Coercion] -> DmdEnv

 coercionsDmdEnv cos

           else

                 return (interesting, Cast arg' co, strict_args) }

   where

   -- Check for a constructor application

   -- NB: this *precedes* the Var case, so that we catch nullary constrs

 pprOptCastCoercion :: CastCoercion -> SDoc

 pprOptCastCoercion (CCoercion co) = pprOptCo co

 pprOptCastCoercion (ZCoercion ty cos) = pprOptZappedCo ty cos

 pprOptZappedCo :: Type -> CoVarSet -> SDoc

 pprOptZappedCo ty cos = sdocOption sdocSuppressCoercions $ \case

 tyCoVarsOfCastCo :: CastCoercion -> TyCoVarSet

 tyCoVarsOfCastCo (CCoercion co)     = coVarsOfCo co

 tyCoVarsOfCastCo (ZCoercion ty cos) = tyCoVarsOfType ty `unionVarSet` cos

 tyCoVarsOfType :: Type -> TyCoVarSet

 -- The "deep" TyCoVars of the the type

 shallowCoVarsOfCastCo :: CastCoercion -> CoVarSet

 shallowCoVarsOfCastCo (CCoercion co) = shallowCoVarsOfCo co

 shallowCoVarsOfCastCo (ZCoercion ty cos) = shallowCoVarsOfType ty `unionVarSet` cos

 {- *********************************************************************

 coVarsOfCastCo :: CastCoercion -> CoVarSet

 coVarsOfCastCo (CCoercion co) = coVarsOfCo co

 coVarsOfCastCo (ZCoercion ty cos) = coVarsOfType ty `unionVarSet` cos -- TODO cos doesn't include deep, this isn't enough?

 -- See Note [Finding free coercion variables]

 coVarsOfType  :: Type       -> CoVarSet

 tyCoFVsOfCastCoercion :: CastCoercion -> FV

 tyCoFVsOfCastCoercion (CCoercion co) = tyCoFVsOfCo co

 tyCoFVsOfCastCoercion (ZCoercion ty cos) = tyCoFVsOfType ty `unionFV` tyCoFVsOfCoVarSet cos

 tyCoFVsOfCoVarSet :: CoVarSet -> FV

 tyCoFVsOfCoVarSet = nonDetStrictFoldVarSet (unionFV . tyCoFVsOfCoVar) emptyFV -- TODO better way? Nondeterminism?

 tidyToIfaceCastCoSty :: CastCoercion -> PprStyle -> IfaceCastCoercion

 tidyToIfaceCastCoSty (CCoercion co)     sty = IfaceCCoercion (tidyToIfaceCoSty co sty)

 tidyToIfaceCastCoSty (ZCoercion ty cos) sty = IfaceZCoercion (tidyToIfaceType ty) (map (flip tidyToIfaceCoSty sty . CoVarCo) (nonDetEltsUniqSet cos)) -- TODO

 tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion

 tidyToIfaceCoSty co sty

 data CastCoercion

   = CCoercion CoercionR        -- Not zapped; the Coercion has Representational role

   | ZCoercion Type CoVarSet    -- Zapped; stores only the RHS type and free CoVars

   deriving Data.Data

 -- | A 'Coercion' is concrete evidence of the equality/convertibility

 castCoercionSize :: CastCoercion -> Int

 castCoercionSize (CCoercion co) = coercionSize co

 castCoercionSize (ZCoercion ty cos) = typeSize ty + sizeVarSet cos

 coercionSize :: Coercion -> Int

 coercionSize (Refl ty)             = typeSize ty

 substCastCo :: HasDebugCallStack => Subst -> CastCoercion -> CastCoercion

 substCastCo subst (CCoercion co)     = CCoercion (substCo subst co)

 substCastCo subst (ZCoercion ty cos) = ZCoercion (substTy subst ty) (substCoVarSet subst cos)

 substCoVarSet :: HasDebugCallStack => Subst -> CoVarSet -> CoVarSet

 substCoVarSet subst = nonDetStrictFoldVarSet (unionVarSet . shallowCoVarsOfCo . substCoVar subst) emptyVarSet -- TODO better impl; determinism?

 tidyCos env = strictMap (tidyCo env)

 tidyCastCo :: TidyEnv -> CastCoercion -> CastCoercion

 tidyCastCo env (ZCoercion ty cos) = ZCoercion (tidyType env ty) (mapVarSet (tidyTyCoVarOcc env) cos)

   , Type ty <- rhs           = substTyWithUnchecked [tv] [ty] (exprType body)

   | otherwise                = exprType body

 exprType (Case _ _ ty _)     = ty

 exprType (Tick _ e)          = exprType e

 exprType (Lam binder expr)   = mkLamType binder (exprType expr)

 exprType e@(App _ _)

 mkCastCo :: HasDebugCallStack => CoreExpr -> CastCoercion -> CoreExpr

 mkCastCo expr (CCoercion co)     = mkCast expr co

 mkCastCo expr (ZCoercion ty cos) = mkCastZ expr ty cos

 -- | Wrap the given expression in the coercion safely, dropping

 -- identity coercions and coalescing nested coercions

 -- | A cheap equality test which bales out fast!

 --      If it returns @True@ the arguments are definitely equal,

 --      otherwise, they may or may not be equal.

 cheapEqExpr = cheapEqExpr' (const False)

 -- | Cheap expression equality test, can ignore ticks by type.

 {-# INLINE cheapEqExpr' #-}

 cheapEqExpr' ignoreTick e1 e2

   = go e1 e2

     go (Type t1)  (Type t2)        = t1 `eqType` t2

     go (Coercion c1) (Coercion c2) = c1 `eqCoercion` c2

     go (App f1 a1) (App f2 a2)     = f1 `go` f2 && a1 `go` a2

     go (Tick t1 e1) e2 | ignoreTick t1 = go e1 e2

     go e1 (Tick t2 e2) | ignoreTick t2 = go e1 e2

 diffExpr _   env (Coercion co1) (Coercion co2)

                                        | eqCoercionX env co1 co2        = []

 diffExpr top env (Cast e1 co1)  (Cast e2 co2)

 diffExpr top env (Tick n1 e1)   e2

   | not (tickishIsCode n1)                 = diffExpr top env e1 e2

 diffExpr top env e1             (Tick n2 e2)

 toIfaceCastCoercion :: CastCoercion -> IfaceCastCoercion

 toIfaceCastCoercion (CCoercion co) = IfaceCCoercion (toIfaceCoercion co)

 toIfaceCastCoercion (ZCoercion ty cos) = IfaceZCoercion (toIfaceType ty) (map (toIfaceCoercion . CoVarCo) (nonDetEltsUniqSet cos)) -- TODO determinism

 toIfaceCoercion :: Coercion -> IfaceCoercion

 toIfaceCoercion = toIfaceCoercionX emptyVarSet

 rnIfaceMCo (IfaceMCo co) = IfaceMCo <$> rnIfaceCo co

 rnIfaceCastCo :: Rename IfaceCastCoercion

 rnIfaceCastCo (IfaceZCoercion ty cos) = IfaceZCoercion <$> rnIfaceType ty <*> mapM rnIfaceCo cos

 rnIfaceCo :: Rename IfaceCoercion

 rnIfaceCo (IfaceReflCo ty)              = IfaceReflCo <$> rnIfaceType ty

 freeNamesIfMCoercion (IfaceMCo co) = freeNamesIfCoercion co

 freeNamesIfCastCoercion :: IfaceCastCoercion -> NameSet

 freeNamesIfCastCoercion (IfaceZCoercion ty cos) = freeNamesIfType ty &&& fnList freeNamesIfCoercion cos

 freeNamesIfCoercion :: IfaceCoercion -> NameSet

 freeNamesIfCoercion (IfaceReflCo t) = freeNamesIfType t

 data IfaceCastCoercion

   = IfaceCCoercion IfaceCoercion

   | IfaceZCoercion IfaceType [IfaceCoercion]

   deriving (Eq, Ord)

 data IfaceCoercion

 pprIfaceCastCoercion :: IfaceCastCoercion -> SDoc

 pprIfaceCastCoercion (IfaceCCoercion co) = pprIfaceCoercion co

 pprIfaceCastCoercion (IfaceZCoercion ty cos) = text "Zap" <+> pprParendIfaceType ty <+> ppr cos

 pprParendIfaceCastCoercion :: IfaceCastCoercion -> SDoc

 pprParendIfaceCastCoercion (IfaceCCoercion co) = pprParendIfaceCoercion co

 pprParendIfaceCastCoercion (IfaceZCoercion ty cos) = parens (pprIfaceCastCoercion (IfaceZCoercion ty cos))

 pprIfaceCoercion, pprParendIfaceCoercion :: IfaceCoercion -> SDoc

 pprIfaceCoercion = ppr_co topPrec

           putByte bh 2

           put_ bh a

           put_ bh b

   get bh = do

     tag <- getByte bh

          2 -> do a <- get bh

                  b <- get bh

                  return $ IfaceZCoercion a b

          _ -> panic ("get IfaceCastCoercion " ++ show tag)

   rnf = \case

     IfaceCCoercion f1 -> rnf f1

     IfaceZCoercion f1 f2 -> rnf f1 `seq` rnf f2

 instance NFData IfaceCoercion where

   rnf = \case

 tcIfaceCastCoercion :: IfaceCastCoercion -> IfL CastCoercion

 tcIfaceCastCoercion (IfaceCCoercion co)     = CCoercion <$> tcIfaceCo co

 tcIfaceCastCoercion (IfaceZCoercion ty cos) = ZCoercion <$> tcIfaceType ty <*> (shallowCoVarsOfCos <$> mapM tcIfaceCo cos)

 tcIfaceCo :: IfaceCoercion -> IfL Coercion

 tcIfaceCo = go

       CCoercion co     -> not (anyFreeVarsOfCo (== v) co)

       ZCoercion ty cvs -> not (anyFreeVarsOfType (== v) ty)

                        && not (v `elemVarSet` cvs)

     not_in_submult :: TyVar -> SubMultCo -> Bool

     not_in_submult v = \case

 zonkCastCo :: CastCoercion -> ZonkTcM CastCoercion

 zonkCastCo (CCoercion co) = CCoercion <$> zonkCoToCo co

 zonkCastCo (ZCoercion ty cos) = ZCoercion <$> zonkTcTypeToTypeX ty <*> zonkCoVarSet cos

 zonkCoVarSet :: CoVarSet -> ZonkTcM CoVarSet

 zonkCoVarSet = fmap shallowCoVarsOfCos . mapM zonkCoVarOcc . nonDetEltsUniqSet

        }

 zonkEvTerm ev@(EvCastExpr _ (ZCoercion{}) _)

   = pprPanic "zonkEvTerm: ZCoercion" (ppr ev)

 zonkEvTerm (EvTypeable ty ev)

   = EvTypeable <$> zonkTcTypeToTypeX ty <*> zonkEvTypeable ev

 zonkEvTerm (EvFun { et_tvs = tvs, et_given = evs