mkProofIrrelCo,

         downgradeRole,

         mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,

         castCoercionKind, castCoercionKind1, castCoercionKind2,

         -- ** Decomposition

         tyConRoleListX, tyConRoleListRepresentational, funRole,

         pickLR,

         mkCoherenceRightMCo,

         mkFunResMCo, mkPiMCos,

         isReflMCo, checkReflexiveMCo,

         -- ** Substitution

         CvSubstEnv, emptyCvSubstEnv,

         lookupCoVar,

         substCoVarBndr,

         extendTvSubstAndInScope, getCvSubstEnv,

 coToMCo co | isReflCo co = MRefl

            | otherwise   = MCo co

 checkReflexiveMCo :: MCoercion -> MCoercion

 checkReflexiveMCo MRefl                       = MRefl

 checkReflexiveMCo (MCo co) | isReflexiveCo co = MRefl

                            | otherwise        = MCo co

 -- | Make a generalized reflexive coercion

 mkGReflCo :: Role -> Type -> MCoercionN -> Coercion

 mkGReflCo r ty mco

   | otherwise

   = -- I'd like to have this assert, but sadly it's not true during type

     -- inference because the types are not fully zonked

 splitFunCo_maybe (FunCo { fco_arg = arg, fco_res = res }) = Just (arg, res)

 splitFunCo_maybe _ = Nothing

 splitForAllCo_maybe (ForAllCo { fco_tcv = tv, fco_visL = vL, fco_visR = vR

 splitForAllCo_maybe co

   | Just (ty, r)        <- isReflCo_maybe co

   , Just (Bndr tcv vis, body_ty) <- splitForAllForAllTyBinder_maybe ty

 splitForAllCo_maybe _ = Nothing

 -- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder

 splitForAllCo_ty_maybe co

   | Just stuff@(tv, _, _, _, _) <- splitForAllCo_maybe co

   , isTyVar tv

 splitForAllCo_ty_maybe _ = Nothing

 -- | Like 'splitForAllCo_maybe', but only returns Just for covar binder

 splitForAllCo_co_maybe co

   | Just stuff@(cv, _, _, _, _) <- splitForAllCo_maybe co

   , isCoVar cv

   | otherwise

   = Nothing

 -- Guaranteed to work very quickly.

 -- | Tests if this coercion is obviously reflexive. Guaranteed to work

 -- very quickly. Sometimes a coercion can be reflexive, but not obviously

 -- so. c.f. 'isReflexiveCo'

 isReflCo :: Coercion -> Bool

 isReflCo (Refl{}) = True

 isReflCo _ = False

 -- | Returns the type coerced if this coercion is reflexive. Guaranteed

 -- to work very quickly. Sometimes a coercion can be reflexive, but not

 -- obviously so. c.f. 'isReflexiveCo_maybe'

 isReflCo_maybe :: Coercion -> Maybe (Type, Role)

 isReflCo_maybe (Refl ty) = Just (ty, Nominal)

 isReflCo_maybe _ = Nothing

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

 isReflexiveCo :: Coercion -> Bool

 isReflexiveCo = isJust . isReflexiveCo_maybe

 -- | Extracts the coerced type from a reflexive coercion. This potentially

 -- walks over the entire coercion, so avoid doing this in a loop.

 isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)

 isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal)

 isReflexiveCo_maybe co

   | ty1 `eqType` ty2

   = Just (ty1, r)

   = Nothing

   where (Pair ty1 ty2, r) = coercionKindRole co

 {-

 %************************************************************************

 -- | Make a Coercion from a tycovar, a kind coercion, and a body coercion.

 mkForAllCo v visL visR kind_co co

   | Just (ty, r) <- isReflCo_maybe co

   , visL `eqForAllVis` visR

   = mkReflCo r (mkTyCoForAllTy v visL ty)

 mkForAllVisCos :: HasDebugCallStack => [ForAllTyBinder] -> Coercion -> Coercion

 mkForAllVisCos bndrs orig_co = foldr go orig_co bndrs

   where

 -- | Make a Coercion quantified over a type/coercion variable;

 -- the variable has the same kind and visibility in both sides of the coercion

   | otherwise

   = foldr go orig_co vs

   where

 -- | Like 'mkForAllCo', but there is no need to check that the inner coercion isn't Refl;

 --   the caller has done that. (For example, it is guaranteed in 'mkHomoForAllCos'.)

 -- The kind of the tycovar should be the left-hand kind of the kind coercion.

 mkForAllCo_NoRefl tcv visL visR kind_co co

   = assertGoodForAllCo tcv visL visR kind_co co $

     ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR

              , fco_kind = kind_co, fco_body = co }

 assertGoodForAllCo :: HasDebugCallStack

 -- Check ForAllCo invariants; see Note [ForAllCo] in GHC.Core.TyCo.Rep

 assertGoodForAllCo tcv visL visR kind_co co

   | isTyVar tcv

   | otherwise

         -- The kind of the tycovar should be the left-hand kind of the kind coercion.

   . assertPpr (almostDevoidCoVarOfCo tcv co) doc

         -- See (FC6) in Note [ForAllCo] in GHC.Core.TyCo.Rep

         -- See (FC7) in Note [ForAllCo] in GHC.Core.TyCo.Rep

   where

     tcv_type      = varType tcv

     doc = vcat [ text "Var:" <+> ppr tcv <+> dcolon <+> ppr tcv_type

                , text "Vis:" <+> ppr visL <+> ppr visR

                , text "body_co" <+> ppr co ]

 mkNakedForAllCo :: TyVar    -- Never a CoVar

   = mkReflCo r (mkForAllTy (Bndr tv visL) ty)

   | otherwise

   = ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR

 mkCoVarCo :: CoVar -> Coercion

 mkSymCo (SymCo co)         = co

 mkSymCo (SubCo (SymCo co)) = SubCo co

 mkSymCo co@(ForAllCo { fco_kind = kco, fco_body = body_co })

 mkSymCo co                 = SymCo co

 -- | mkTransCo creates a new 'Coercion' by composing the two

     go cs co

   where

       -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)

       -- then (nth SelForAll co :: k1 ~N k2)

       -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)

 mkInstCo co_fun co_arg

   | Just (tcv, _, _, kind_co, body_co) <- splitForAllCo_maybe co_fun

   , Just (arg, _) <- isReflCo_maybe co_arg

   = assertPpr (isReflexiveCo kind_co) (ppr co_fun $$ ppr co_arg) $

        -- If the arg is Refl, then kind_co must be reflexive too

 mkInstCo co arg = InstCo co arg

 -- | Given @ty :: k1@, @co :: k1 ~ k2@,

 -- produces @co' :: ty ~r (ty |> co)@

 mkGReflRightCo r ty co

 -- | Given @r@, @ty :: k1@, and @co :: k1 ~N k2@,

 -- produces @co' :: (ty |> co) ~r ty@

 mkGReflLeftCo r ty co

 -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~r ty'@,

 -- produces @co' :: (ty |> co) ~r ty'

 -- It is not only a utility function, but it saves allocation when co

 -- is a GRefl coercion.

 mkCoherenceLeftCo r ty co co2

 -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~r ty@,

 -- produces @co' :: ty' ~r (ty |> co)

 -- It is not only a utility function, but it saves allocation when co

 -- is a GRefl coercion.

 mkCoherenceRightCo r ty co co2

 -- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.

 mkKindCo :: Coercion -> Coercion

       Nothing  -> pprPanic "downgradeRole" (ppr co)

 -- | Make a "coercion between coercions".

 -- if the two coercion prove the same fact, I just don't care what

 -- the individual coercions are.

 {-

 %************************************************************************

     go r (TyConApp tc tys)  = mkTyConAppCo r tc (zipWith go (tyConRoleListX r tc) tys)

     go r (FunTy af w t1 t2) = mkFunCo r af (go Nominal w) (go r t1) (go r t2)

     go r t@(ForAllTy (Bndr v vis) ty)

            -- Lifting a ForAllTy over a coercion variable could fail as ForAllCo

            -- imposes an extra restriction on where a covar can appear. See

            -- (FC6) of Note [ForAllCo] in GHC.Tc.TyCo.Rep

             -- We specifically check for this and panic because we know that

            -- there's a hole in the type system here (see (FC6), and we'd rather

            -- panic than fall into it.

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

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

                              mkNomReflCo ty

 liftCoSubstVarBndr lc tv

   = liftCoSubstVarBndrUsing id callback lc tv

   where

     callback lc' ty' = ty_co_subst lc' Nominal ty'

 -- the callback must produce a nominal coercion

 seqCo (AxiomCo _ cs)        = seqCos cs

 seqCo (ForAllCo tv visL visR k co)

   = seqType (varType tv) `seq` rnf visL `seq` rnf visR `seq`

 seqCo (FunCo r af1 af2 w co1 co2)

   = r `seq` af1 `seq` af2 `seq` seqCo w `seq` seqCo co1 `seq` seqCo co2

 seqCo (UnivCo { uco_prov = p, uco_role = r

                     , fco_kind = k_co, fco_body = co1 })

       = case which of

           CLeft  -> mkTyCoForAllTy tv1 visL (go co1)

                  -> mkTyCoForAllTy tv1 visR (go co1)

                  | otherwise

                  -> go_forall_right empty_subst co

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

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

       -- See Note [Nested ForAllCos]

       | isTyVar tv1

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

       | isCoVar cv1

     go_forall_right subst other_co

       -- when other_co is not a ForAllCo

     go (ForAllTy (Bndr tv1 flag1) ty1) (ForAllTy (Bndr tv2 flag2) ty2)

       | isTyVar tv1

       = assert (isTyVar tv2) $

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

             in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co

             ty2'     = substTyWithInScope in_scope [tv2]

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

       = assert (isCoVar cv1 && isCoVar cv2) $

       where s1 = varType cv1

             s2 = varType cv2

             kind_co = go s1 s2

             eta2 = mkSelCo (SelTyCon 3 r) kind_co'

             subst = mkEmptySubst $ mkInScopeSet $

             ty2'  = substTy (extendCvSubst subst cv2 $ mkSymCo eta1 `mkTransCo`

                                                        mkCoVarCo cv1 `mkTransCo`

                                                        eta2)

 mkReflCo :: Role -> Type -> Coercion

 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion

 mkAppCo :: Coercion -> Coercion -> Coercion

 mkFunCo      :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion

 mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion

 mkFunCo2     :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion

 funRole :: Role -> FunSel -> Role

 isReflCo :: Coercion -> Bool

 isReflexiveCo :: Coercion -> Bool

 decomposePiCos :: HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)

   = optCoercion' env co

 {-

     let result = optCoercion' env co in

     pprTrace "optCoercion }"

        (vcat [ text "Co:"    <+> ppr (coercionSize co)

              , text "Optco:" <+> ppWhen (isReflCo result) (text "(refl)")

     result

 -}

               (text "Expected role:" <+> ppr r $$

                text "Found role:" <+> ppr _r   $$

                text "Type:" <+> ppr ty) $

     then wrapSym sym ty_co

     else wrapSym sym $ mk_coherence_right_co r' (coercionRKind ty_co) kco' ty_co

             -- ty :: k1

 -- Push transitivity inside forall

 -- forall over types.

 opt_trans_rule is co1 co2

   where

     -- Given:

     -- Wanted:

     = fireTransRule "EtaAllTy_ty" co1 co2 $

     where

       is' = is `extendInScopeSet` tv1

 -- Push transitivity inside forall

 -- forall over coercions.

 opt_trans_rule is co1 co2

   where

     -- Given:

     -- Wanted:

     = fireTransRule "EtaAllTy_co" co1 co2 $

     where

       is'  = is `extendInScopeSet` cv1

       role = coVarRole cv1