-- (c) The University of Glasgow 2006

{-# LANGUAGE CPP #-}

-- The default iteration limit is a bit too low for the definitions
-- in this module.
{-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}

module OptCoercion ( optCoercion, checkAxInstCo ) where

#include "HsVersions.h"

import GhcPrelude

import DynFlags
import TyCoRep
import Coercion
import Type hiding( substTyVarBndr, substTy )
import TcType       ( exactTyCoVarsOfType )
import TyCon
import CoAxiom
import VarSet
import VarEnv
import Outputable
import FamInstEnv ( flattenTys )
import Pair
import ListSetOps ( getNth )
import Util
import Unify
import InstEnv
import Control.Monad   ( zipWithM )

{-
%************************************************************************
%*                                                                      *
                 Optimising coercions
%*                                                                      *
%************************************************************************

Note [Optimising coercion optimisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Looking up a coercion's role or kind is linear in the size of the
coercion. Thus, doing this repeatedly during the recursive descent
of coercion optimisation is disastrous. We must be careful to avoid
doing this if at all possible.

Because it is generally easy to know a coercion's components' roles
from the role of the outer coercion, we pass down the known role of
the input in the algorithm below. We also keep functions opt_co2
and opt_co3 separate from opt_co4, so that the former two do Phantom
checks that opt_co4 can avoid. This is a big win because Phantom coercions
rarely appear within non-phantom coercions -- only in some TyConAppCos
and some AxiomInstCos. We handle these cases specially by calling
opt_co2.

Note [Optimising InstCo]
~~~~~~~~~~~~~~~~~~~~~~~~
(1) tv is a type variable
When we have (InstCo (ForAllCo tv h g) g2), we want to optimise.

Let's look at the typing rules.

h : k1 ~ k2
tv:k1 |- g : t1 ~ t2
-----------------------------
ForAllCo tv h g : (all tv:k1.t1) ~ (all tv:k2.t2[tv |-> tv |> sym h])

g1 : (all tv:k1.t1') ~ (all tv:k2.t2')
g2 : s1 ~ s2
--------------------
InstCo g1 g2 : t1'[tv |-> s1] ~ t2'[tv |-> s2]

We thus want some coercion proving this:

  (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym h])

If we substitute the *type* tv for the *coercion*
(g2 ; t2 ~ t2 |> sym h) in g, we'll get this result exactly.
This is bizarre,
though, because we're substituting a type variable with a coercion. However,
this operation already exists: it's called *lifting*, and defined in Coercion.
We just need to enhance the lifting operation to be able to deal with
an ambient substitution, which is why a LiftingContext stores a TCvSubst.

(2) cv is a coercion variable
Now consider we have (InstCo (ForAllCo cv h g) g2), we want to optimise.

h : (t1 ~r t2) ~N (t3 ~r t4)
cv : t1 ~r t2 |- g : t1' ~r2 t2'
n1 = nth r 2 (downgradeRole r N h) :: t1 ~r t3
n2 = nth r 3 (downgradeRole r N h) :: t2 ~r t4
------------------------------------------------
ForAllCo cv h g : (all cv:t1 ~r t2. t1') ~r2
                  (all cv:t3 ~r t4. t2'[cv |-> n1 ; cv ; sym n2])

g1 : (all cv:t1 ~r t2. t1') ~ (all cv: t3 ~r t4. t2')
g2 : h1 ~N h2
h1 : t1 ~r t2
h2 : t3 ~r t4
------------------------------------------------
InstCo g1 g2 : t1'[cv |-> h1] ~ t2'[cv |-> h2]

We thus want some coercion proving this:

  t1'[cv |-> h1] ~ t2'[cv |-> n1 ; h2; sym n2]

So we substitute the coercion variable c for the coercion
(h1 ~N (n1; h2; sym n2)) in g.
-}

optCoercion :: DynFlags -> TCvSubst -> Coercion -> NormalCo
-- ^ optCoercion applies a substitution to a coercion,
--   *and* optimises it to reduce its size
optCoercion :: DynFlags -> TCvSubst -> Coercion -> Coercion
optCoercion dflags :: DynFlags
dflags env :: TCvSubst
env co :: Coercion
co
  | DynFlags -> Bool
hasNoOptCoercion DynFlags
dflags = HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo TCvSubst
env Coercion
co
  | Bool
otherwise               = TCvSubst -> Coercion -> Coercion
optCoercion' TCvSubst
env Coercion
co

optCoercion' :: TCvSubst -> Coercion -> NormalCo
optCoercion' :: TCvSubst -> Coercion -> Coercion
optCoercion' env :: TCvSubst
env co :: Coercion
co
  | Bool
debugIsOn
  = let out_co :: Coercion
out_co = LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
lc Bool
False Coercion
co
        (Pair in_ty1 :: Type
in_ty1  in_ty2 :: Type
in_ty2,  in_role :: Role
in_role)  = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
        (Pair out_ty1 :: Type
out_ty1 out_ty2 :: Type
out_ty2, out_role :: Role
out_role) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
out_co
    in
    ASSERT2( substTy env in_ty1 `eqType` out_ty1 &&
             substTy env in_ty2 `eqType` out_ty2 &&
             in_role == out_role
           , text "optCoercion changed types!"
             $$ hang (text "in_co:") 2 (ppr co)
             $$ hang (text "in_ty1:") 2 (ppr in_ty1)
             $$ hang (text "in_ty2:") 2 (ppr in_ty2)
             $$ hang (text "out_co:") 2 (ppr out_co)
             $$ hang (text "out_ty1:") 2 (ppr out_ty1)
             $$ hang (text "out_ty2:") 2 (ppr out_ty2)
             $$ hang (text "subst:") 2 (ppr env) )
    Coercion
out_co

  | Bool
otherwise         = LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
lc Bool
False Coercion
co
  where
    lc :: LiftingContext
lc = TCvSubst -> LiftingContext
mkSubstLiftingContext TCvSubst
env

type NormalCo    = Coercion
  -- Invariants:
  --  * The substitution has been fully applied
  --  * For trans coercions (co1 `trans` co2)
  --       co1 is not a trans, and neither co1 nor co2 is identity

type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity

-- | Do we apply a @sym@ to the result?
type SymFlag = Bool

-- | Do we force the result to be representational?
type ReprFlag = Bool

-- | Optimize a coercion, making no assumptions. All coercions in
-- the lifting context are already optimized (and sym'd if nec'y)
opt_co1 :: LiftingContext
        -> SymFlag
        -> Coercion -> NormalCo
opt_co1 :: LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 env :: LiftingContext
env sym :: Bool
sym co :: Coercion
co = LiftingContext -> Bool -> Role -> Coercion -> Coercion
opt_co2 LiftingContext
env Bool
sym (Coercion -> Role
coercionRole Coercion
co) Coercion
co

-- See Note [Optimising coercion optimisation]
-- | Optimize a coercion, knowing the coercion's role. No other assumptions.
opt_co2 :: LiftingContext
        -> SymFlag
        -> Role   -- ^ The role of the input coercion
        -> Coercion -> NormalCo
opt_co2 :: LiftingContext -> Bool -> Role -> Coercion -> Coercion
opt_co2 env :: LiftingContext
env sym :: Bool
sym Phantom co :: Coercion
co = LiftingContext -> Bool -> Coercion -> Coercion
opt_phantom LiftingContext
env Bool
sym Coercion
co
opt_co2 env :: LiftingContext
env sym :: Bool
sym r :: Role
r       co :: Coercion
co = LiftingContext
-> Bool -> Maybe Role -> Role -> Coercion -> Coercion
opt_co3 LiftingContext
env Bool
sym Maybe Role
forall a. Maybe a
Nothing Role
r Coercion
co

-- See Note [Optimising coercion optimisation]
-- | Optimize a coercion, knowing the coercion's non-Phantom role.
opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
opt_co3 :: LiftingContext
-> Bool -> Maybe Role -> Role -> Coercion -> Coercion
opt_co3 env :: LiftingContext
env sym :: Bool
sym (Just Phantom)          _ co :: Coercion
co = LiftingContext -> Bool -> Coercion -> Coercion
opt_phantom LiftingContext
env Bool
sym Coercion
co
opt_co3 env :: LiftingContext
env sym :: Bool
sym (Just Representational) r :: Role
r co :: Coercion
co = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
True  Role
r Coercion
co
  -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore
opt_co3 env :: LiftingContext
env sym :: Bool
sym _                       r :: Role
r co :: Coercion
co = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
r Coercion
co

-- See Note [Optimising coercion optimisation]
-- | Optimize a non-phantom coercion.
opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo

opt_co4_wrap :: LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4
{-
opt_co4_wrap env sym rep r co
  = pprTrace "opt_co4_wrap {"
    ( vcat [ text "Sym:" <+> ppr sym
           , text "Rep:" <+> ppr rep
           , text "Role:" <+> ppr r
           , text "Co:" <+> ppr co ]) $
    ASSERT( r == coercionRole co )
    let result = opt_co4 env sym rep r co in
    pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
    result
-}

opt_co4 :: LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4 env :: LiftingContext
env _   rep :: Bool
rep r :: Role
r (Refl ty :: Type
ty)
  = ASSERT2( r == Nominal, text "Expected role:" <+> ppr r    $$
                           text "Found role:" <+> ppr Nominal $$
                           text "Type:" <+> ppr ty )
    HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env Type
ty

opt_co4 env :: LiftingContext
env _   rep :: Bool
rep r :: Role
r (GRefl _r :: Role
_r ty :: Type
ty MRefl)
  = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
                      text "Found role:" <+> ppr _r   $$
                      text "Type:" <+> ppr ty )
    HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env Type
ty

opt_co4 env :: LiftingContext
env sym :: Bool
sym  rep :: Bool
rep r :: Role
r (GRefl _r :: Role
_r ty :: Type
ty (MCo co :: Coercion
co))
  = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
                      text "Found role:" <+> ppr _r   $$
                      text "Type:" <+> ppr ty )
    if Coercion -> Bool
isGReflCo Coercion
co Bool -> Bool -> Bool
|| Coercion -> Bool
isGReflCo Coercion
co'
    then HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r' LiftingContext
env Type
ty
    else Bool -> Coercion -> Coercion
wrapSym Bool
sym (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r' Type
ty' Coercion
co' (HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r' LiftingContext
env Type
ty)
  where
    r' :: Role
r'  = Bool -> Role -> Role
chooseRole Bool
rep Role
r
    ty' :: Type
ty' = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (LiftingContext -> TCvSubst
lcSubstLeft LiftingContext
env) Type
ty
    co' :: Coercion
co' = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4 LiftingContext
env Bool
False Bool
False Role
Nominal Coercion
co

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (SymCo co :: Coercion
co)  = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env (Bool -> Bool
not Bool
sym) Bool
rep Role
r Coercion
co
  -- surprisingly, we don't have to do anything to the env here. This is
  -- because any "lifting" substitutions in the env are tied to ForAllCos,
  -- which treat their left and right sides differently. We don't want to
  -- exchange them.

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r g :: Coercion
g@(TyConAppCo _r :: Role
_r tc :: TyCon
tc cos :: [Coercion]
cos)
  = ASSERT( r == _r )
    case (Bool
rep, Role
r) of
      (True, Nominal) ->
        HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Representational TyCon
tc
                     ((Maybe Role -> Role -> Coercion -> Coercion)
-> [Maybe Role] -> [Role] -> [Coercion] -> [Coercion]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (LiftingContext
-> Bool -> Maybe Role -> Role -> Coercion -> Coercion
opt_co3 LiftingContext
env Bool
sym)
                               ((Role -> Maybe Role) -> [Role] -> [Maybe Role]
forall a b. (a -> b) -> [a] -> [b]
map Role -> Maybe Role
forall a. a -> Maybe a
Just (TyCon -> [Role]
tyConRolesRepresentational TyCon
tc))
                               (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal)
                               [Coercion]
cos)
      (False, Nominal) ->
        HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tc ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal) [Coercion]
cos)
      (_, Representational) ->
                      -- must use opt_co2 here, because some roles may be P
                      -- See Note [Optimising coercion optimisation]
        HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc ((Role -> Coercion -> Coercion)
-> [Role] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (LiftingContext -> Bool -> Role -> Coercion -> Coercion
opt_co2 LiftingContext
env Bool
sym)
                                   (TyCon -> [Role]
tyConRolesRepresentational TyCon
tc)  -- the current roles
                                   [Coercion]
cos)
      (_, Phantom) -> String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic "opt_co4 sees a phantom!" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
g)

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (AppCo co1 :: Coercion
co1 co2 :: Coercion
co2)
  = Coercion -> Coercion -> Coercion
mkAppCo (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r Coercion
co1)
            (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal Coercion
co2)

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (ForAllCo tv :: TyCoVar
tv k_co :: Coercion
k_co co :: Coercion
co)
  = case LiftingContext
-> Bool
-> TyCoVar
-> Coercion
-> (LiftingContext, TyCoVar, Coercion)
optForAllCoBndr LiftingContext
env Bool
sym TyCoVar
tv Coercion
k_co of
      (env' :: LiftingContext
env', tv' :: TyCoVar
tv', k_co' :: Coercion
k_co') -> TyCoVar -> Coercion -> Coercion -> Coercion
mkForAllCo TyCoVar
tv' Coercion
k_co' (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                            LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env' Bool
sym Bool
rep Role
r Coercion
co
     -- Use the "mk" functions to check for nested Refls

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (FunCo _r :: Role
_r co1 :: Coercion
co1 co2 :: Coercion
co2)
  = ASSERT( r == _r )
    if Bool
rep
    then Role -> Coercion -> Coercion -> Coercion
mkFunCo Role
Representational Coercion
co1' Coercion
co2'
    else Role -> Coercion -> Coercion -> Coercion
mkFunCo Role
r Coercion
co1' Coercion
co2'
  where
    co1' :: Coercion
co1' = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r Coercion
co1
    co2' :: Coercion
co2' = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r Coercion
co2

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (CoVarCo cv :: TyCoVar
cv)
  | Just co :: Coercion
co <- TCvSubst -> TyCoVar -> Maybe Coercion
lookupCoVar (LiftingContext -> TCvSubst
lcTCvSubst LiftingContext
env) TyCoVar
cv
  = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
env) Bool
sym Bool
rep Role
r Coercion
co

  | Type
ty1 Type -> Type -> Bool
`eqType` Type
ty2   -- See Note [Optimise CoVarCo to Refl]
  = Role -> Type -> Coercion
mkReflCo (Bool -> Role -> Role
chooseRole Bool
rep Role
r) Type
ty1

  | Bool
otherwise
  = ASSERT( isCoVar cv1 )
    Bool -> Role -> Coercion -> Coercion
wrapRole Bool
rep Role
r (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Bool -> Coercion -> Coercion
wrapSym Bool
sym (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    TyCoVar -> Coercion
CoVarCo TyCoVar
cv1

  where
    Pair ty1 :: Type
ty1 ty2 :: Type
ty2 = HasDebugCallStack => TyCoVar -> Pair Type
TyCoVar -> Pair Type
coVarTypes TyCoVar
cv1

    cv1 :: TyCoVar
cv1 = case InScopeSet -> TyCoVar -> Maybe TyCoVar
lookupInScope (LiftingContext -> InScopeSet
lcInScopeSet LiftingContext
env) TyCoVar
cv of
             Just cv1 :: TyCoVar
cv1 -> TyCoVar
cv1
             Nothing  -> WARN( True, text "opt_co: not in scope:"
                                     <+> ppr cv $$ ppr env)
                         TyCoVar
cv
          -- cv1 might have a substituted kind!

opt_co4 _ _ _ _ (HoleCo h :: CoercionHole
h)
  = String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic "opt_univ fell into a hole" (CoercionHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoercionHole
h)

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (AxiomInstCo con :: CoAxiom Branched
con ind :: Int
ind cos :: [Coercion]
cos)
    -- Do *not* push sym inside top-level axioms
    -- e.g. if g is a top-level axiom
    --   g a : f a ~ a
    -- then (sym (g ty)) /= g (sym ty) !!
  = ASSERT( r == coAxiomRole con )
    Bool -> Role -> Coercion -> Coercion
wrapRole Bool
rep (CoAxiom Branched -> Role
forall (br :: BranchFlag). CoAxiom br -> Role
coAxiomRole CoAxiom Branched
con) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    Bool -> Coercion -> Coercion
wrapSym Bool
sym (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                       -- some sub-cos might be P: use opt_co2
                       -- See Note [Optimising coercion optimisation]
    CoAxiom Branched -> Int -> [Coercion] -> Coercion
AxiomInstCo CoAxiom Branched
con Int
ind ((Role -> Coercion -> Coercion)
-> [Role] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (LiftingContext -> Bool -> Role -> Coercion -> Coercion
opt_co2 LiftingContext
env Bool
False)
                                 (CoAxBranch -> [Role]
coAxBranchRoles (CoAxiom Branched -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom Branched
con Int
ind))
                                 [Coercion]
cos)
      -- Note that the_co does *not* have sym pushed into it

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (UnivCo prov :: UnivCoProvenance
prov _r :: Role
_r t1 :: Type
t1 t2 :: Type
t2)
  = ASSERT( r == _r )
    LiftingContext
-> Bool -> UnivCoProvenance -> Role -> Type -> Type -> Coercion
opt_univ LiftingContext
env Bool
sym UnivCoProvenance
prov (Bool -> Role -> Role
chooseRole Bool
rep Role
r) Type
t1 Type
t2

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (TransCo co1 :: Coercion
co1 co2 :: Coercion
co2)
                      -- sym (g `o` h) = sym h `o` sym g
  | Bool
sym       = InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
in_scope Coercion
co2' Coercion
co1'
  | Bool
otherwise = InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
in_scope Coercion
co1' Coercion
co2'
  where
    co1' :: Coercion
co1' = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r Coercion
co1
    co2' :: Coercion
co2' = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r Coercion
co2
    in_scope :: InScopeSet
in_scope = LiftingContext -> InScopeSet
lcInScopeSet LiftingContext
env

opt_co4 env :: LiftingContext
env _sym :: Bool
_sym rep :: Bool
rep r :: Role
r (NthCo _r :: Role
_r n :: Int
n co :: Coercion
co)
  | Just (ty :: Type
ty, _) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  , Just (_tc :: TyCon
_tc, args :: [Type]
args) <- ASSERT( r == _r )
                        HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
  = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env ([Type]
args [Type] -> Int -> Type
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n)
  | Just (ty :: Type
ty, _) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  , Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0
  , Just (tv :: TyCoVar
tv, _) <- Type -> Maybe (TyCoVar, Type)
splitForAllTy_maybe Type
ty
      -- works for both tyvar and covar
  = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env (TyCoVar -> Type
varType TyCoVar
tv)

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (NthCo r1 :: Role
r1 n :: Int
n (TyConAppCo _ _ cos :: [Coercion]
cos))
  = ASSERT( r == r1 )
    LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r ([Coercion]
cos [Coercion] -> Int -> Coercion
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n)

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (NthCo _r :: Role
_r n :: Int
n (ForAllCo _ eta :: Coercion
eta _))
      -- works for both tyvar and covar
  = ASSERT( r == _r )
    ASSERT( n == 0 )
    LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
Nominal Coercion
eta

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (NthCo _r :: Role
_r n :: Int
n co :: Coercion
co)
  | TyConAppCo _ _ cos :: [Coercion]
cos <- Coercion
co'
  , let nth_co :: Coercion
nth_co = [Coercion]
cos [Coercion] -> Int -> Coercion
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n
  = if Bool
rep Bool -> Bool -> Bool
&& (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal)
      -- keep propagating the SubCo
    then LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
env) Bool
False Bool
True Role
Nominal Coercion
nth_co
    else Coercion
nth_co

  | ForAllCo _ eta :: Coercion
eta _ <- Coercion
co'
  = if Bool
rep
    then LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
env) Bool
False Bool
True Role
Nominal Coercion
eta
    else Coercion
eta

  | Bool
otherwise
  = Bool -> Role -> Coercion -> Coercion
wrapRole Bool
rep Role
r (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Int -> Coercion -> Coercion
NthCo Role
r Int
n Coercion
co'
  where
    co' :: Coercion
co' = LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
env Bool
sym Coercion
co

opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (LRCo lr :: LeftOrRight
lr co :: Coercion
co)
  | Just pr_co :: (Coercion, Coercion)
pr_co <- Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe Coercion
co
  = ASSERT( r == Nominal )
    LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
Nominal (LeftOrRight -> (Coercion, Coercion) -> Coercion
forall p. LeftOrRight -> (p, p) -> p
pick_lr LeftOrRight
lr (Coercion, Coercion)
pr_co)
  | Just pr_co :: (Coercion, Coercion)
pr_co <- Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe Coercion
co'
  = ASSERT( r == Nominal )
    if Bool
rep
    then LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
env) Bool
False Bool
True Role
Nominal (LeftOrRight -> (Coercion, Coercion) -> Coercion
forall p. LeftOrRight -> (p, p) -> p
pick_lr LeftOrRight
lr (Coercion, Coercion)
pr_co)
    else LeftOrRight -> (Coercion, Coercion) -> Coercion
forall p. LeftOrRight -> (p, p) -> p
pick_lr LeftOrRight
lr (Coercion, Coercion)
pr_co
  | Bool
otherwise
  = Bool -> Role -> Coercion -> Coercion
wrapRole Bool
rep Role
Nominal (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
lr Coercion
co'
  where
    co' :: Coercion
co' = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal Coercion
co

    pick_lr :: LeftOrRight -> (p, p) -> p
pick_lr CLeft  (l :: p
l, _) = p
l
    pick_lr CRight (_, r :: p
r) = p
r

-- See Note [Optimising InstCo]
opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (InstCo co1 :: Coercion
co1 arg :: Coercion
arg)
    -- forall over type...
  | Just (tv :: TyCoVar
tv, kind_co :: Coercion
kind_co, co_body :: Coercion
co_body) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co1
  = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> TyCoVar -> Coercion -> LiftingContext
extendLiftingContext LiftingContext
env TyCoVar
tv
                    (Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
Nominal Type
t2 (Coercion -> Coercion
mkSymCo Coercion
kind_co) Coercion
sym_arg))
                   -- mkSymCo kind_co :: k1 ~ k2
                   -- sym_arg :: (t1 :: k1) ~ (t2 :: k2)
                   -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1)
                 Bool
sym Bool
rep Role
r Coercion
co_body

    -- forall over coercion...
  | Just (cv :: TyCoVar
cv, kind_co :: Coercion
kind_co, co_body :: Coercion
co_body) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_co_maybe Coercion
co1
  , CoercionTy h1 :: Coercion
h1 <- Type
t1
  , CoercionTy h2 :: Coercion
h2 <- Type
t2
  = let new_co :: Coercion
new_co = TyCoVar -> Coercion -> Coercion -> Coercion -> Coercion
mk_new_co TyCoVar
cv (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal Coercion
kind_co) Coercion
h1 Coercion
h2
    in LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> TyCoVar -> Coercion -> LiftingContext
extendLiftingContext LiftingContext
env TyCoVar
cv Coercion
new_co) Bool
sym Bool
rep Role
r Coercion
co_body

    -- See if it is a forall after optimization
    -- If so, do an inefficient one-variable substitution, then re-optimize

    -- forall over type...
  | Just (tv' :: TyCoVar
tv', kind_co' :: Coercion
kind_co', co_body' :: Coercion
co_body') <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co1'
  = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> TyCoVar -> Coercion -> LiftingContext
extendLiftingContext (LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
env) TyCoVar
tv'
                    (Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
Nominal Type
t2' (Coercion -> Coercion
mkSymCo Coercion
kind_co') Coercion
arg'))
            Bool
False Bool
False Role
r' Coercion
co_body'

    -- forall over coercion...
  | Just (cv' :: TyCoVar
cv', kind_co' :: Coercion
kind_co', co_body' :: Coercion
co_body') <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_co_maybe Coercion
co1'
  , CoercionTy h1' :: Coercion
h1' <- Type
t1'
  , CoercionTy h2' :: Coercion
h2' <- Type
t2'
  = let new_co :: Coercion
new_co = TyCoVar -> Coercion -> Coercion -> Coercion -> Coercion
mk_new_co TyCoVar
cv' Coercion
kind_co' Coercion
h1' Coercion
h2'
    in LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> TyCoVar -> Coercion -> LiftingContext
extendLiftingContext (LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
env) TyCoVar
cv' Coercion
new_co)
                    Bool
False Bool
False Role
r' Coercion
co_body'

  | Bool
otherwise = Coercion -> Coercion -> Coercion
InstCo Coercion
co1' Coercion
arg'
  where
    co1' :: Coercion
co1'    = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r Coercion
co1
    r' :: Role
r'      = Bool -> Role -> Role
chooseRole Bool
rep Role
r
    arg' :: Coercion
arg'    = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal Coercion
arg
    sym_arg :: Coercion
sym_arg = Bool -> Coercion -> Coercion
wrapSym Bool
sym Coercion
arg'

    -- Performance note: don't be alarmed by the two calls to coercionKind
    -- here, as only one call to coercionKind is actually demanded per guard.
    -- t1/t2 are used when checking if co1 is a forall, and t1'/t2' are used
    -- when checking if co1' (i.e., co1 post-optimization) is a forall.
    --
    -- t1/t2 must come from sym_arg, not arg', since it's possible that arg'
    -- might have an extra Sym at the front (after being optimized) that co1
    -- lacks, so we need to use sym_arg to balance the number of Syms. (#15725)
    Pair t1 :: Type
t1  t2 :: Type
t2  = Coercion -> Pair Type
coercionKind Coercion
sym_arg
    Pair t1' :: Type
t1' t2' :: Type
t2' = Coercion -> Pair Type
coercionKind Coercion
arg'

    mk_new_co :: TyCoVar -> Coercion -> Coercion -> Coercion -> Coercion
mk_new_co cv :: TyCoVar
cv kind_co :: Coercion
kind_co h1 :: Coercion
h1 h2 :: Coercion
h2
      = let -- h1 :: (t1 ~ t2)
            -- h2 :: (t3 ~ t4)
            -- kind_co :: (t1 ~ t2) ~ (t3 ~ t4)
            -- n1 :: t1 ~ t3
            -- n2 :: t2 ~ t4
            -- new_co = (h1 :: t1 ~ t2) ~ ((n1;h2;sym n2) :: t1 ~ t2)
            r2 :: Role
r2  = TyCoVar -> Role
coVarRole TyCoVar
cv
            kind_co' :: Coercion
kind_co' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
r2 Role
Nominal Coercion
kind_co
            n1 :: Coercion
n1 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r2 2 Coercion
kind_co'
            n2 :: Coercion
n2 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r2 3 Coercion
kind_co'
         in Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal (Type -> Coercion
Refl (Coercion -> Type
coercionType Coercion
h1)) Coercion
h1
                           (Coercion
n1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
h2 Coercion -> Coercion -> Coercion
`mkTransCo` (Coercion -> Coercion
mkSymCo Coercion
n2))

opt_co4 env :: LiftingContext
env sym :: Bool
sym _rep :: Bool
_rep r :: Role
r (KindCo co :: Coercion
co)
  = ASSERT( r == Nominal )
    let kco' :: Coercion
kco' = Coercion -> Coercion
promoteCoercion Coercion
co in
    case Coercion
kco' of
      KindCo co' :: Coercion
co' -> Coercion -> Coercion
promoteCoercion (LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
env Bool
sym Coercion
co')
      _          -> LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal Coercion
kco'
  -- This might be able to be optimized more to do the promotion
  -- and substitution/optimization at the same time

opt_co4 env :: LiftingContext
env sym :: Bool
sym _ r :: Role
r (SubCo co :: Coercion
co)
  = ASSERT( r == Representational )
    LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
True Role
Nominal Coercion
co

-- This could perhaps be optimized more.
opt_co4 env :: LiftingContext
env sym :: Bool
sym rep :: Bool
rep r :: Role
r (AxiomRuleCo co :: CoAxiomRule
co cs :: [Coercion]
cs)
  = ASSERT( r == coaxrRole co )
    Bool -> Role -> Coercion -> Coercion
wrapRole Bool
rep Role
r (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    Bool -> Coercion -> Coercion
wrapSym Bool
sym (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo CoAxiomRule
co ((Role -> Coercion -> Coercion)
-> [Role] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (LiftingContext -> Bool -> Role -> Coercion -> Coercion
opt_co2 LiftingContext
env Bool
False) (CoAxiomRule -> [Role]
coaxrAsmpRoles CoAxiomRule
co) [Coercion]
cs)

{- Note [Optimise CoVarCo to Refl]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we have (c :: t~t) we can optimise it to Refl. That increases the
chances of floating the Refl upwards; e.g. Maybe c --> Refl (Maybe t)

We do so here in optCoercion, not in mkCoVarCo; see Note [mkCoVarCo]
in Coercion.
-}

-------------
-- | Optimize a phantom coercion. The input coercion may not necessarily
-- be a phantom, but the output sure will be.
opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
opt_phantom :: LiftingContext -> Bool -> Coercion -> Coercion
opt_phantom env :: LiftingContext
env sym :: Bool
sym co :: Coercion
co
  = LiftingContext
-> Bool -> UnivCoProvenance -> Role -> Type -> Type -> Coercion
opt_univ LiftingContext
env Bool
sym (Coercion -> UnivCoProvenance
PhantomProv (Coercion -> Coercion
mkKindCo Coercion
co)) Role
Phantom Type
ty1 Type
ty2
  where
    Pair ty1 :: Type
ty1 ty2 :: Type
ty2 = Coercion -> Pair Type
coercionKind Coercion
co

{- Note [Differing kinds]
   ~~~~~~~~~~~~~~~~~~~~~~
The two types may not have the same kind (although that would be very unusual).
But even if they have the same kind, and the same type constructor, the number
of arguments in a `CoTyConApp` can differ. Consider

  Any :: forall k. k

  Any * Int                      :: *
  Any (*->*) Maybe Int  :: *

Hence the need to compare argument lengths; see Trac #13658
 -}

opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
         -> Type -> Type -> Coercion
opt_univ :: LiftingContext
-> Bool -> UnivCoProvenance -> Role -> Type -> Type -> Coercion
opt_univ env :: LiftingContext
env sym :: Bool
sym (PhantomProv h :: Coercion
h) _r :: Role
_r ty1 :: Type
ty1 ty2 :: Type
ty2
  | Bool
sym       = Coercion -> Type -> Type -> Coercion
mkPhantomCo Coercion
h' Type
ty2' Type
ty1'
  | Bool
otherwise = Coercion -> Type -> Type -> Coercion
mkPhantomCo Coercion
h' Type
ty1' Type
ty2'
  where
    h' :: Coercion
h' = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4 LiftingContext
env Bool
sym Bool
False Role
Nominal Coercion
h
    ty1' :: Type
ty1' = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (LiftingContext -> TCvSubst
lcSubstLeft  LiftingContext
env) Type
ty1
    ty2' :: Type
ty2' = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (LiftingContext -> TCvSubst
lcSubstRight LiftingContext
env) Type
ty2

opt_univ env :: LiftingContext
env sym :: Bool
sym prov :: UnivCoProvenance
prov role :: Role
role oty1 :: Type
oty1 oty2 :: Type
oty2
  | Just (tc1 :: TyCon
tc1, tys1 :: [Type]
tys1) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
oty1
  , Just (tc2 :: TyCon
tc2, tys2 :: [Type]
tys2) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
oty2
  , TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
  , [Type] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [Type]
tys1 [Type]
tys2 -- see Note [Differing kinds]
      -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
      -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
  = let roles :: [Role]
roles    = Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc1
        arg_cos :: [Coercion]
arg_cos  = (Role -> Type -> Type -> Coercion)
-> [Role] -> [Type] -> [Type] -> [Coercion]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
prov') [Role]
roles [Type]
tys1 [Type]
tys2
        arg_cos' :: [Coercion]
arg_cos' = (Role -> Coercion -> Coercion)
-> [Role] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4 LiftingContext
env Bool
sym Bool
False) [Role]
roles [Coercion]
arg_cos
    in
    HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc1 [Coercion]
arg_cos'

  -- can't optimize the AppTy case because we can't build the kind coercions.

  | Just (tv1 :: TyCoVar
tv1, ty1 :: Type
ty1) <- Type -> Maybe (TyCoVar, Type)
splitForAllTy_ty_maybe Type
oty1
  , Just (tv2 :: TyCoVar
tv2, ty2 :: Type
ty2) <- Type -> Maybe (TyCoVar, Type)
splitForAllTy_ty_maybe Type
oty2
      -- NB: prov isn't interesting here either
  = let k1 :: Type
k1   = TyCoVar -> Type
tyVarKind TyCoVar
tv1
        k2 :: Type
k2   = TyCoVar -> Type
tyVarKind TyCoVar
tv2
        eta :: Coercion
eta  = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
prov' Role
Nominal Type
k1 Type
k2
          -- eta gets opt'ed soon, but not yet.
        ty2' :: Type
ty2' = HasCallStack => [TyCoVar] -> [Type] -> Type -> Type
[TyCoVar] -> [Type] -> Type -> Type
substTyWith [TyCoVar
tv2] [TyCoVar -> Type
TyVarTy TyCoVar
tv1 Type -> Coercion -> Type
`mkCastTy` Coercion
eta] Type
ty2

        (env' :: LiftingContext
env', tv1' :: TyCoVar
tv1', eta' :: Coercion
eta') = LiftingContext
-> Bool
-> TyCoVar
-> Coercion
-> (LiftingContext, TyCoVar, Coercion)
optForAllCoBndr LiftingContext
env Bool
sym TyCoVar
tv1 Coercion
eta
    in
    TyCoVar -> Coercion -> Coercion -> Coercion
mkForAllCo TyCoVar
tv1' Coercion
eta' (LiftingContext
-> Bool -> UnivCoProvenance -> Role -> Type -> Type -> Coercion
opt_univ LiftingContext
env' Bool
sym UnivCoProvenance
prov' Role
role Type
ty1 Type
ty2')

  | Just (cv1 :: TyCoVar
cv1, ty1 :: Type
ty1) <- Type -> Maybe (TyCoVar, Type)
splitForAllTy_co_maybe Type
oty1
  , Just (cv2 :: TyCoVar
cv2, ty2 :: Type
ty2) <- Type -> Maybe (TyCoVar, Type)
splitForAllTy_co_maybe Type
oty2
      -- NB: prov isn't interesting here either
  = let k1 :: Type
k1    = TyCoVar -> Type
varType TyCoVar
cv1
        k2 :: Type
k2    = TyCoVar -> Type
varType TyCoVar
cv2
        r' :: Role
r'    = TyCoVar -> Role
coVarRole TyCoVar
cv1
        eta :: Coercion
eta   = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
prov' Role
Nominal Type
k1 Type
k2
        eta_d :: Coercion
eta_d = Role -> Role -> Coercion -> Coercion
downgradeRole Role
r' Role
Nominal Coercion
eta
          -- eta gets opt'ed soon, but not yet.
        n_co :: Coercion
n_co  = (Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r' 2 Coercion
eta_d) Coercion -> Coercion -> Coercion
`mkTransCo`
                (TyCoVar -> Coercion
mkCoVarCo TyCoVar
cv1) Coercion -> Coercion -> Coercion
`mkTransCo`
                (HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r' 3 Coercion
eta_d)
        ty2' :: Type
ty2'  = [TyCoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars [TyCoVar
cv2] [Coercion
n_co] Type
ty2

        (env' :: LiftingContext
env', cv1' :: TyCoVar
cv1', eta' :: Coercion
eta') = LiftingContext
-> Bool
-> TyCoVar
-> Coercion
-> (LiftingContext, TyCoVar, Coercion)
optForAllCoBndr LiftingContext
env Bool
sym TyCoVar
cv1 Coercion
eta
    in
    TyCoVar -> Coercion -> Coercion -> Coercion
mkForAllCo TyCoVar
cv1' Coercion
eta' (LiftingContext
-> Bool -> UnivCoProvenance -> Role -> Type -> Type -> Coercion
opt_univ LiftingContext
env' Bool
sym UnivCoProvenance
prov' Role
role Type
ty1 Type
ty2')

  | Bool
otherwise
  = let ty1 :: Type
ty1 = TCvSubst -> Type -> Type
substTyUnchecked (LiftingContext -> TCvSubst
lcSubstLeft  LiftingContext
env) Type
oty1
        ty2 :: Type
ty2 = TCvSubst -> Type -> Type
substTyUnchecked (LiftingContext -> TCvSubst
lcSubstRight LiftingContext
env) Type
oty2
        (a :: Type
a, b :: Type
b) | Bool
sym       = (Type
ty2, Type
ty1)
               | Bool
otherwise = (Type
ty1, Type
ty2)
    in
    UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
prov' Role
role Type
a Type
b

  where
    prov' :: UnivCoProvenance
prov' = case UnivCoProvenance
prov of
      UnsafeCoerceProv   -> UnivCoProvenance
prov
      PhantomProv kco :: Coercion
kco    -> Coercion -> UnivCoProvenance
PhantomProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal Coercion
kco
      ProofIrrelProv kco :: Coercion
kco -> Coercion -> UnivCoProvenance
ProofIrrelProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal Coercion
kco
      PluginProv _       -> UnivCoProvenance
prov

-------------
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList :: InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList is :: InScopeSet
is = (Coercion -> Coercion -> Coercion)
-> [Coercion] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is)

opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
opt_trans :: InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans is :: InScopeSet
is co1 :: Coercion
co1 co2 :: Coercion
co2
  | Coercion -> Bool
isReflCo Coercion
co1 = Coercion
co2
    -- optimize when co1 is a Refl Co
  | Bool
otherwise    = InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans1 InScopeSet
is Coercion
co1 Coercion
co2

opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
-- First arg is not the identity
opt_trans1 :: InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans1 is :: InScopeSet
is co1 :: Coercion
co1 co2 :: Coercion
co2
  | Coercion -> Bool
isReflCo Coercion
co2 = Coercion
co1
    -- optimize when co2 is a Refl Co
  | Bool
otherwise    = InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans2 InScopeSet
is Coercion
co1 Coercion
co2

opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
-- Neither arg is the identity
opt_trans2 :: InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans2 is :: InScopeSet
is (TransCo co1a :: Coercion
co1a co1b :: Coercion
co1b) co2 :: Coercion
co2
    -- Don't know whether the sub-coercions are the identity
  = InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1a (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1b Coercion
co2)

opt_trans2 is :: InScopeSet
is co1 :: Coercion
co1 co2 :: Coercion
co2
  | Just co :: Coercion
co <- InScopeSet -> Coercion -> Coercion -> Maybe Coercion
opt_trans_rule InScopeSet
is Coercion
co1 Coercion
co2
  = Coercion
co

opt_trans2 is :: InScopeSet
is co1 :: Coercion
co1 (TransCo co2a :: Coercion
co2a co2b :: Coercion
co2b)
  | Just co1_2a :: Coercion
co1_2a <- InScopeSet -> Coercion -> Coercion -> Maybe Coercion
opt_trans_rule InScopeSet
is Coercion
co1 Coercion
co2a
  = if Coercion -> Bool
isReflCo Coercion
co1_2a
    then Coercion
co2b
    else InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans1 InScopeSet
is Coercion
co1_2a Coercion
co2b

opt_trans2 _ co1 :: Coercion
co1 co2 :: Coercion
co2
  = Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2

------
-- Optimize coercions with a top-level use of transitivity.
opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo

opt_trans_rule :: InScopeSet -> Coercion -> Coercion -> Maybe Coercion
opt_trans_rule is :: InScopeSet
is in_co1 :: Coercion
in_co1@(GRefl r1 :: Role
r1 t1 :: Type
t1 (MCo co1 :: Coercion
co1)) in_co2 :: Coercion
in_co2@(GRefl r2 :: Role
r2 _ (MCo co2 :: Coercion
co2))
  = ASSERT( r1 == r2 )
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "GRefl" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
r1 Type
t1 (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1 Coercion
co2)

-- Push transitivity through matching destructors
opt_trans_rule is :: InScopeSet
is in_co1 :: Coercion
in_co1@(NthCo r1 :: Role
r1 d1 :: Int
d1 co1 :: Coercion
co1) in_co2 :: Coercion
in_co2@(NthCo r2 :: Role
r2 d2 :: Int
d2 co2 :: Coercion
co2)
  | Int
d1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
d2
  , Coercion -> Role
coercionRole Coercion
co1 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Coercion -> Role
coercionRole Coercion
co2
  , Coercion
co1 Coercion -> Coercion -> Bool
`compatible_co` Coercion
co2
  = ASSERT( r1 == r2 )
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "PushNth" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r1 Int
d1 (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1 Coercion
co2)

opt_trans_rule is :: InScopeSet
is in_co1 :: Coercion
in_co1@(LRCo d1 :: LeftOrRight
d1 co1 :: Coercion
co1) in_co2 :: Coercion
in_co2@(LRCo d2 :: LeftOrRight
d2 co2 :: Coercion
co2)
  | LeftOrRight
d1 LeftOrRight -> LeftOrRight -> Bool
forall a. Eq a => a -> a -> Bool
== LeftOrRight
d2
  , Coercion
co1 Coercion -> Coercion -> Bool
`compatible_co` Coercion
co2
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "PushLR" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    LeftOrRight -> Coercion -> Coercion
mkLRCo LeftOrRight
d1 (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1 Coercion
co2)

-- Push transitivity inside instantiation
opt_trans_rule is :: InScopeSet
is in_co1 :: Coercion
in_co1@(InstCo co1 :: Coercion
co1 ty1 :: Coercion
ty1) in_co2 :: Coercion
in_co2@(InstCo co2 :: Coercion
co2 ty2 :: Coercion
ty2)
  | Coercion
ty1 Coercion -> Coercion -> Bool
`eqCoercion` Coercion
ty2
  , Coercion
co1 Coercion -> Coercion -> Bool
`compatible_co` Coercion
co2
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "TrPushInst" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    Coercion -> Coercion -> Coercion
mkInstCo (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1 Coercion
co2) Coercion
ty1

opt_trans_rule is :: InScopeSet
is in_co1 :: Coercion
in_co1@(UnivCo p1 :: UnivCoProvenance
p1 r1 :: Role
r1 tyl1 :: Type
tyl1 _tyr1 :: Type
_tyr1)
                  in_co2 :: Coercion
in_co2@(UnivCo p2 :: UnivCoProvenance
p2 r2 :: Role
r2 _tyl2 :: Type
_tyl2 tyr2 :: Type
tyr2)
  | Just prov' :: UnivCoProvenance
prov' <- UnivCoProvenance -> UnivCoProvenance -> Maybe UnivCoProvenance
opt_trans_prov UnivCoProvenance
p1 UnivCoProvenance
p2
  = ASSERT( r1 == r2 )
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "UnivCo" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
prov' Role
r1 Type
tyl1 Type
tyr2
  where
    -- if the provenances are different, opt'ing will be very confusing
    opt_trans_prov :: UnivCoProvenance -> UnivCoProvenance -> Maybe UnivCoProvenance
opt_trans_prov UnsafeCoerceProv      UnsafeCoerceProv      = UnivCoProvenance -> Maybe UnivCoProvenance
forall a. a -> Maybe a
Just UnivCoProvenance
UnsafeCoerceProv
    opt_trans_prov (PhantomProv kco1 :: Coercion
kco1)    (PhantomProv kco2 :: Coercion
kco2)
      = UnivCoProvenance -> Maybe UnivCoProvenance
forall a. a -> Maybe a
Just (UnivCoProvenance -> Maybe UnivCoProvenance)
-> UnivCoProvenance -> Maybe UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ Coercion -> UnivCoProvenance
PhantomProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
kco1 Coercion
kco2
    opt_trans_prov (ProofIrrelProv kco1 :: Coercion
kco1) (ProofIrrelProv kco2 :: Coercion
kco2)
      = UnivCoProvenance -> Maybe UnivCoProvenance
forall a. a -> Maybe a
Just (UnivCoProvenance -> Maybe UnivCoProvenance)
-> UnivCoProvenance -> Maybe UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ Coercion -> UnivCoProvenance
ProofIrrelProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
kco1 Coercion
kco2
    opt_trans_prov (PluginProv str1 :: String
str1)     (PluginProv str2 :: String
str2)     | String
str1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
str2 = UnivCoProvenance -> Maybe UnivCoProvenance
forall a. a -> Maybe a
Just UnivCoProvenance
p1
    opt_trans_prov _ _ = Maybe UnivCoProvenance
forall a. Maybe a
Nothing

-- Push transitivity down through matching top-level constructors.
opt_trans_rule is :: InScopeSet
is in_co1 :: Coercion
in_co1@(TyConAppCo r1 :: Role
r1 tc1 :: TyCon
tc1 cos1 :: [Coercion]
cos1) in_co2 :: Coercion
in_co2@(TyConAppCo r2 :: Role
r2 tc2 :: TyCon
tc2 cos2 :: [Coercion]
cos2)
  | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
  = ASSERT( r1 == r2 )
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "PushTyConApp" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r1 TyCon
tc1 (InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 [Coercion]
cos2)

opt_trans_rule is :: InScopeSet
is in_co1 :: Coercion
in_co1@(FunCo r1 :: Role
r1 co1a :: Coercion
co1a co1b :: Coercion
co1b) in_co2 :: Coercion
in_co2@(FunCo r2 :: Role
r2 co2a :: Coercion
co2a co2b :: Coercion
co2b)
  = ASSERT( r1 == r2 )   -- Just like the TyConAppCo/TyConAppCo case
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "PushFun" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    Role -> Coercion -> Coercion -> Coercion
mkFunCo Role
r1 (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1a Coercion
co2a) (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1b Coercion
co2b)

opt_trans_rule is :: InScopeSet
is in_co1 :: Coercion
in_co1@(AppCo co1a :: Coercion
co1a co1b :: Coercion
co1b) in_co2 :: Coercion
in_co2@(AppCo co2a :: Coercion
co2a co2b :: Coercion
co2b)
  -- Must call opt_trans_rule_app; see Note [EtaAppCo]
  = InScopeSet
-> Coercion
-> Coercion
-> Coercion
-> [Coercion]
-> Coercion
-> [Coercion]
-> Maybe Coercion
opt_trans_rule_app InScopeSet
is Coercion
in_co1 Coercion
in_co2 Coercion
co1a [Coercion
co1b] Coercion
co2a [Coercion
co2b]

-- Eta rules
opt_trans_rule is :: InScopeSet
is co1 :: Coercion
co1@(TyConAppCo r :: Role
r tc :: TyCon
tc cos1 :: [Coercion]
cos1) co2 :: Coercion
co2
  | Just cos2 :: [Coercion]
cos2 <- TyCon -> Coercion -> Maybe [Coercion]
etaTyConAppCo_maybe TyCon
tc Coercion
co2
  = ASSERT( cos1 `equalLength` cos2 )
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "EtaCompL" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc (InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 [Coercion]
cos2)

opt_trans_rule is :: InScopeSet
is co1 :: Coercion
co1 co2 :: Coercion
co2@(TyConAppCo r :: Role
r tc :: TyCon
tc cos2 :: [Coercion]
cos2)
  | Just cos1 :: [Coercion]
cos1 <- TyCon -> Coercion -> Maybe [Coercion]
etaTyConAppCo_maybe TyCon
tc Coercion
co1
  = ASSERT( cos1 `equalLength` cos2 )
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "EtaCompR" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc (InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 [Coercion]
cos2)

opt_trans_rule is :: InScopeSet
is co1 :: Coercion
co1@(AppCo co1a :: Coercion
co1a co1b :: Coercion
co1b) co2 :: Coercion
co2
  | Just (co2a :: Coercion
co2a,co2b :: Coercion
co2b) <- Coercion -> Maybe (Coercion, Coercion)
etaAppCo_maybe Coercion
co2
  = InScopeSet
-> Coercion
-> Coercion
-> Coercion
-> [Coercion]
-> Coercion
-> [Coercion]
-> Maybe Coercion
opt_trans_rule_app InScopeSet
is Coercion
co1 Coercion
co2 Coercion
co1a [Coercion
co1b] Coercion
co2a [Coercion
co2b]

opt_trans_rule is :: InScopeSet
is co1 :: Coercion
co1 co2 :: Coercion
co2@(AppCo co2a :: Coercion
co2a co2b :: Coercion
co2b)
  | Just (co1a :: Coercion
co1a,co1b :: Coercion
co1b) <- Coercion -> Maybe (Coercion, Coercion)
etaAppCo_maybe Coercion
co1
  = InScopeSet
-> Coercion
-> Coercion
-> Coercion
-> [Coercion]
-> Coercion
-> [Coercion]
-> Maybe Coercion
opt_trans_rule_app InScopeSet
is Coercion
co1 Coercion
co2 Coercion
co1a [Coercion
co1b] Coercion
co2a [Coercion
co2b]

-- Push transitivity inside forall
-- forall over types.
opt_trans_rule is :: InScopeSet
is co1 :: Coercion
co1 co2 :: Coercion
co2
  | Just (tv1 :: TyCoVar
tv1, eta1 :: Coercion
eta1, r1 :: Coercion
r1) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co1
  , Just (tv2 :: TyCoVar
tv2, eta2 :: Coercion
eta2, r2 :: Coercion
r2) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
etaForAllCo_ty_maybe Coercion
co2
  = TyCoVar
-> Coercion
-> Coercion
-> TyCoVar
-> Coercion
-> Coercion
-> Maybe Coercion
push_trans TyCoVar
tv1 Coercion
eta1 Coercion
r1 TyCoVar
tv2 Coercion
eta2 Coercion
r2

  | Just (tv2 :: TyCoVar
tv2, eta2 :: Coercion
eta2, r2 :: Coercion
r2) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co2
  , Just (tv1 :: TyCoVar
tv1, eta1 :: Coercion
eta1, r1 :: Coercion
r1) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
etaForAllCo_ty_maybe Coercion
co1
  = TyCoVar
-> Coercion
-> Coercion
-> TyCoVar
-> Coercion
-> Coercion
-> Maybe Coercion
push_trans TyCoVar
tv1 Coercion
eta1 Coercion
r1 TyCoVar
tv2 Coercion
eta2 Coercion
r2

  where
  push_trans :: TyCoVar
-> Coercion
-> Coercion
-> TyCoVar
-> Coercion
-> Coercion
-> Maybe Coercion
push_trans tv1 :: TyCoVar
tv1 eta1 :: Coercion
eta1 r1 :: Coercion
r1 tv2 :: TyCoVar
tv2 eta2 :: Coercion
eta2 r2 :: Coercion
r2
    -- Given:
    --   co1 = /\ tv1 : eta1. r1
    --   co2 = /\ tv2 : eta2. r2
    -- Wanted:
    --   /\tv1 : (eta1;eta2).  (r1; r2[tv2 |-> tv1 |> eta1])
    = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "EtaAllTy_ty" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
      TyCoVar -> Coercion -> Coercion -> Coercion
mkForAllCo TyCoVar
tv1 (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
eta1 Coercion
eta2) (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is' Coercion
r1 Coercion
r2')
    where
      is' :: InScopeSet
is' = InScopeSet
is InScopeSet -> TyCoVar -> InScopeSet
`extendInScopeSet` TyCoVar
tv1
      r2' :: Coercion
r2' = [TyCoVar] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked [TyCoVar
tv2] [Type -> Coercion -> Type
mkCastTy (TyCoVar -> Type
TyVarTy TyCoVar
tv1) Coercion
eta1] Coercion
r2

-- Push transitivity inside forall
-- forall over coercions.
opt_trans_rule is :: InScopeSet
is co1 :: Coercion
co1 co2 :: Coercion
co2
  | Just (cv1 :: TyCoVar
cv1, eta1 :: Coercion
eta1, r1 :: Coercion
r1) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_co_maybe Coercion
co1
  , Just (cv2 :: TyCoVar
cv2, eta2 :: Coercion
eta2, r2 :: Coercion
r2) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
etaForAllCo_co_maybe Coercion
co2
  = TyCoVar
-> Coercion
-> Coercion
-> TyCoVar
-> Coercion
-> Coercion
-> Maybe Coercion
push_trans TyCoVar
cv1 Coercion
eta1 Coercion
r1 TyCoVar
cv2 Coercion
eta2 Coercion
r2

  | Just (cv2 :: TyCoVar
cv2, eta2 :: Coercion
eta2, r2 :: Coercion
r2) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_co_maybe Coercion
co2
  , Just (cv1 :: TyCoVar
cv1, eta1 :: Coercion
eta1, r1 :: Coercion
r1) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
etaForAllCo_co_maybe Coercion
co1
  = TyCoVar
-> Coercion
-> Coercion
-> TyCoVar
-> Coercion
-> Coercion
-> Maybe Coercion
push_trans TyCoVar
cv1 Coercion
eta1 Coercion
r1 TyCoVar
cv2 Coercion
eta2 Coercion
r2

  where
  push_trans :: TyCoVar
-> Coercion
-> Coercion
-> TyCoVar
-> Coercion
-> Coercion
-> Maybe Coercion
push_trans cv1 :: TyCoVar
cv1 eta1 :: Coercion
eta1 r1 :: Coercion
r1 cv2 :: TyCoVar
cv2 eta2 :: Coercion
eta2 r2 :: Coercion
r2
    -- Given:
    --   co1 = /\ cv1 : eta1. r1
    --   co2 = /\ cv2 : eta2. r2
    -- Wanted:
    --   n1 = nth 2 eta1
    --   n2 = nth 3 eta1
    --   nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2])
    = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "EtaAllTy_co" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
      TyCoVar -> Coercion -> Coercion -> Coercion
mkForAllCo TyCoVar
cv1 (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
eta1 Coercion
eta2) (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is' Coercion
r1 Coercion
r2')
    where
      is' :: InScopeSet
is'  = InScopeSet
is InScopeSet -> TyCoVar -> InScopeSet
`extendInScopeSet` TyCoVar
cv1
      role :: Role
role = TyCoVar -> Role
coVarRole TyCoVar
cv1
      eta1' :: Coercion
eta1' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
Nominal Coercion
eta1
      n1 :: Coercion
n1   = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
role 2 Coercion
eta1'
      n2 :: Coercion
n2   = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
role 3 Coercion
eta1'
      r2' :: Coercion
r2'  = HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo ([TyCoVar] -> [Coercion] -> TCvSubst
HasDebugCallStack => [TyCoVar] -> [Coercion] -> TCvSubst
zipCvSubst [TyCoVar
cv2] [(Coercion -> Coercion
mkSymCo Coercion
n1) Coercion -> Coercion -> Coercion
`mkTransCo`
                                        (TyCoVar -> Coercion
mkCoVarCo TyCoVar
cv1) Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
n2])
                    Coercion
r2

-- Push transitivity inside axioms
opt_trans_rule is :: InScopeSet
is co1 :: Coercion
co1 co2 :: Coercion
co2

  -- See Note [Why call checkAxInstCo during optimisation]
  -- TrPushSymAxR
  | Just (sym :: Bool
sym, con :: CoAxiom Branched
con, ind :: Int
ind, cos1 :: [Coercion]
cos1) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co1_is_axiom_maybe
  , Bool
True <- Bool
sym
  , Just cos2 :: [Coercion]
cos2 <- Bool -> CoAxiom Branched -> Int -> Coercion -> Maybe [Coercion]
forall (br :: BranchFlag).
Bool -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
matchAxiom Bool
sym CoAxiom Branched
con Int
ind Coercion
co2
  , let newAxInst :: Coercion
newAxInst = CoAxiom Branched -> Int -> [Coercion] -> Coercion
AxiomInstCo CoAxiom Branched
con Int
ind (InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
mkSymCo [Coercion]
cos2) [Coercion]
cos1)
  , Maybe CoAxBranch
Nothing <- Coercion -> Maybe CoAxBranch
checkAxInstCo Coercion
newAxInst
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "TrPushSymAxR" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Coercion -> Coercion
SymCo Coercion
newAxInst

  -- TrPushAxR
  | Just (sym :: Bool
sym, con :: CoAxiom Branched
con, ind :: Int
ind, cos1 :: [Coercion]
cos1) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co1_is_axiom_maybe
  , Bool
False <- Bool
sym
  , Just cos2 :: [Coercion]
cos2 <- Bool -> CoAxiom Branched -> Int -> Coercion -> Maybe [Coercion]
forall (br :: BranchFlag).
Bool -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
matchAxiom Bool
sym CoAxiom Branched
con Int
ind Coercion
co2
  , let newAxInst :: Coercion
newAxInst = CoAxiom Branched -> Int -> [Coercion] -> Coercion
AxiomInstCo CoAxiom Branched
con Int
ind (InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 [Coercion]
cos2)
  , Maybe CoAxBranch
Nothing <- Coercion -> Maybe CoAxBranch
checkAxInstCo Coercion
newAxInst
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "TrPushAxR" Coercion
co1 Coercion
co2 Coercion
newAxInst

  -- TrPushSymAxL
  | Just (sym :: Bool
sym, con :: CoAxiom Branched
con, ind :: Int
ind, cos2 :: [Coercion]
cos2) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co2_is_axiom_maybe
  , Bool
True <- Bool
sym
  , Just cos1 :: [Coercion]
cos1 <- Bool -> CoAxiom Branched -> Int -> Coercion -> Maybe [Coercion]
forall (br :: BranchFlag).
Bool -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
matchAxiom (Bool -> Bool
not Bool
sym) CoAxiom Branched
con Int
ind Coercion
co1
  , let newAxInst :: Coercion
newAxInst = CoAxiom Branched -> Int -> [Coercion] -> Coercion
AxiomInstCo CoAxiom Branched
con Int
ind (InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos2 ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
mkSymCo [Coercion]
cos1))
  , Maybe CoAxBranch
Nothing <- Coercion -> Maybe CoAxBranch
checkAxInstCo Coercion
newAxInst
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "TrPushSymAxL" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Coercion -> Coercion
SymCo Coercion
newAxInst

  -- TrPushAxL
  | Just (sym :: Bool
sym, con :: CoAxiom Branched
con, ind :: Int
ind, cos2 :: [Coercion]
cos2) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co2_is_axiom_maybe
  , Bool
False <- Bool
sym
  , Just cos1 :: [Coercion]
cos1 <- Bool -> CoAxiom Branched -> Int -> Coercion -> Maybe [Coercion]
forall (br :: BranchFlag).
Bool -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
matchAxiom (Bool -> Bool
not Bool
sym) CoAxiom Branched
con Int
ind Coercion
co1
  , let newAxInst :: Coercion
newAxInst = CoAxiom Branched -> Int -> [Coercion] -> Coercion
AxiomInstCo CoAxiom Branched
con Int
ind (InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 [Coercion]
cos2)
  , Maybe CoAxBranch
Nothing <- Coercion -> Maybe CoAxBranch
checkAxInstCo Coercion
newAxInst
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "TrPushAxL" Coercion
co1 Coercion
co2 Coercion
newAxInst

  -- TrPushAxSym/TrPushSymAx
  | Just (sym1 :: Bool
sym1, con1 :: CoAxiom Branched
con1, ind1 :: Int
ind1, cos1 :: [Coercion]
cos1) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co1_is_axiom_maybe
  , Just (sym2 :: Bool
sym2, con2 :: CoAxiom Branched
con2, ind2 :: Int
ind2, cos2 :: [Coercion]
cos2) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co2_is_axiom_maybe
  , CoAxiom Branched
con1 CoAxiom Branched -> CoAxiom Branched -> Bool
forall a. Eq a => a -> a -> Bool
== CoAxiom Branched
con2
  , Int
ind1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ind2
  , Bool
sym1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Bool
not Bool
sym2
  , let branch :: CoAxBranch
branch = CoAxiom Branched -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom Branched
con1 Int
ind1
        qtvs :: [TyCoVar]
qtvs = CoAxBranch -> [TyCoVar]
coAxBranchTyVars CoAxBranch
branch [TyCoVar] -> [TyCoVar] -> [TyCoVar]
forall a. [a] -> [a] -> [a]
++ CoAxBranch -> [TyCoVar]
coAxBranchCoVars CoAxBranch
branch
        lhs :: Type
lhs  = CoAxiom Branched -> Int -> Type
forall (br :: BranchFlag). CoAxiom br -> Int -> Type
coAxNthLHS CoAxiom Branched
con1 Int
ind1
        rhs :: Type
rhs  = CoAxBranch -> Type
coAxBranchRHS CoAxBranch
branch
        pivot_tvs :: TyCoVarSet
pivot_tvs = Type -> TyCoVarSet
exactTyCoVarsOfType (if Bool
sym2 then Type
rhs else Type
lhs)
  , (TyCoVar -> Bool) -> [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TyCoVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
pivot_tvs) [TyCoVar]
qtvs
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "TrPushAxSym" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    if Bool
sym2
       -- TrPushAxSym
    then Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith Role
role [TyCoVar]
qtvs (InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
mkSymCo [Coercion]
cos2)) Type
lhs
       -- TrPushSymAx
    else Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith Role
role [TyCoVar]
qtvs (InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is ((Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
mkSymCo [Coercion]
cos1) [Coercion]
cos2) Type
rhs
  where
    co1_is_axiom_maybe :: Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co1_is_axiom_maybe = Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
isAxiom_maybe Coercion
co1
    co2_is_axiom_maybe :: Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co2_is_axiom_maybe = Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
isAxiom_maybe Coercion
co2
    role :: Role
role = Coercion -> Role
coercionRole Coercion
co1 -- should be the same as coercionRole co2!

opt_trans_rule _ co1 :: Coercion
co1 co2 :: Coercion
co2        -- Identity rule
  | (Pair ty1 :: Type
ty1 _, r :: Role
r) <- Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co1
  , Pair _ ty2 :: Type
ty2 <- Coercion -> Pair Type
coercionKind Coercion
co2
  , Type
ty1 Type -> Type -> Bool
`eqType` Type
ty2
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule "RedTypeDirRefl" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    Role -> Type -> Coercion
mkReflCo Role
r Type
ty2

opt_trans_rule _ _ _ = Maybe Coercion
forall a. Maybe a
Nothing

-- See Note [EtaAppCo]
opt_trans_rule_app :: InScopeSet
                   -> Coercion   -- original left-hand coercion (printing only)
                   -> Coercion   -- original right-hand coercion (printing only)
                   -> Coercion   -- left-hand coercion "function"
                   -> [Coercion] -- left-hand coercion "args"
                   -> Coercion   -- right-hand coercion "function"
                   -> [Coercion] -- right-hand coercion "args"
                   -> Maybe Coercion
opt_trans_rule_app :: InScopeSet
-> Coercion
-> Coercion
-> Coercion
-> [Coercion]
-> Coercion
-> [Coercion]
-> Maybe Coercion
opt_trans_rule_app is :: InScopeSet
is orig_co1 :: Coercion
orig_co1 orig_co2 :: Coercion
orig_co2 co1a :: Coercion
co1a co1bs :: [Coercion]
co1bs co2a :: Coercion
co2a co2bs :: [Coercion]
co2bs
  | AppCo co1aa :: Coercion
co1aa co1ab :: Coercion
co1ab <- Coercion
co1a
  , Just (co2aa :: Coercion
co2aa, co2ab :: Coercion
co2ab) <- Coercion -> Maybe (Coercion, Coercion)
etaAppCo_maybe Coercion
co2a
  = InScopeSet
-> Coercion
-> Coercion
-> Coercion
-> [Coercion]
-> Coercion
-> [Coercion]
-> Maybe Coercion
opt_trans_rule_app InScopeSet
is Coercion
orig_co1 Coercion
orig_co2 Coercion
co1aa (Coercion
co1abCoercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
co1bs) Coercion
co2aa (Coercion
co2abCoercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
co2bs)

  | AppCo co2aa :: Coercion
co2aa co2ab :: Coercion
co2ab <- Coercion
co2a
  , Just (co1aa :: Coercion
co1aa, co1ab :: Coercion
co1ab) <- Coercion -> Maybe (Coercion, Coercion)
etaAppCo_maybe Coercion
co1a
  = InScopeSet
-> Coercion
-> Coercion
-> Coercion
-> [Coercion]
-> Coercion
-> [Coercion]
-> Maybe Coercion
opt_trans_rule_app InScopeSet
is Coercion
orig_co1 Coercion
orig_co2 Coercion
co1aa (Coercion
co1abCoercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
co1bs) Coercion
co2aa (Coercion
co2abCoercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
co2bs)

  | Bool
otherwise
  = ASSERT( co1bs `equalLength` co2bs )
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule ("EtaApps:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Coercion] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Coercion]
co1bs)) Coercion
orig_co1 Coercion
orig_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    let Pair _ rt1a :: Type
rt1a = Coercion -> Pair Type
coercionKind Coercion
co1a
        (Pair lt2a :: Type
lt2a _, rt2a :: Role
rt2a) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co2a

        Pair _ rt1bs :: [Type]
rt1bs = (Coercion -> Pair Type) -> [Coercion] -> Pair [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Coercion -> Pair Type
coercionKind [Coercion]
co1bs
        Pair lt2bs :: [Type]
lt2bs _ = (Coercion -> Pair Type) -> [Coercion] -> Pair [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Coercion -> Pair Type
coercionKind [Coercion]
co2bs
        rt2bs :: [Role]
rt2bs = (Coercion -> Role) -> [Coercion] -> [Role]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Role
coercionRole [Coercion]
co2bs

        kcoa :: Coercion
kcoa = Coercion -> Coercion
mkKindCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Coercion
buildCoercion Type
lt2a Type
rt1a
        kcobs :: [Coercion]
kcobs = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
mkKindCo ([Coercion] -> [Coercion]) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Coercion) -> [Type] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Type -> Coercion
buildCoercion [Type]
lt2bs [Type]
rt1bs

        co2a' :: Coercion
co2a'   = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
rt2a Type
lt2a Coercion
kcoa Coercion
co2a
        co2bs' :: [Coercion]
co2bs'  = (Role -> Type -> Coercion -> Coercion)
-> [Role] -> [Type] -> [Coercion] -> [Coercion]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Role -> Type -> Coercion -> Coercion
mkGReflLeftCo [Role]
rt2bs [Type]
lt2bs [Coercion]
kcobs
        co2bs'' :: [Coercion]
co2bs'' = (Coercion -> Coercion -> Coercion)
-> [Coercion] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Coercion -> Coercion -> Coercion
mkTransCo [Coercion]
co2bs' [Coercion]
co2bs
    in
    Coercion -> [Coercion] -> Coercion
mkAppCos (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1a Coercion
co2a')
             ((Coercion -> Coercion -> Coercion)
-> [Coercion] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is) [Coercion]
co1bs [Coercion]
co2bs'')

fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule _rule :: String
_rule _co1 :: Coercion
_co1 _co2 :: Coercion
_co2 res :: Coercion
res
  = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
res

{-
Note [Conflict checking with AxiomInstCo]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following type family and axiom:

type family Equal (a :: k) (b :: k) :: Bool
type instance where
  Equal a a = True
  Equal a b = False
--
Equal :: forall k::*. k -> k -> Bool
axEqual :: { forall k::*. forall a::k. Equal k a a ~ True
           ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False }

We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is
0-based, so this is the second branch of the axiom.) The problem is that, on
the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~
False) and that all is OK. But, all is not OK: we want to use the first branch
of the axiom in this case, not the second. The problem is that the parameters
of the first branch can unify with the supplied coercions, thus meaning that
the first branch should be taken. See also Note [Apartness] in
types/FamInstEnv.hs.

Note [Why call checkAxInstCo during optimisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It is possible that otherwise-good-looking optimisations meet with disaster
in the presence of axioms with multiple equations. Consider

type family Equal (a :: *) (b :: *) :: Bool where
  Equal a a = True
  Equal a b = False
type family Id (a :: *) :: * where
  Id a = a

axEq :: { [a::*].       Equal a a ~ True
        ; [a::*, b::*]. Equal a b ~ False }
axId :: [a::*]. Id a ~ a

co1 = Equal (axId[0] Int) (axId[0] Bool)
  :: Equal (Id Int) (Id Bool) ~  Equal Int Bool
co2 = axEq[1] <Int> <Bool>
  :: Equal Int Bool ~ False

We wish to optimise (co1 ; co2). We end up in rule TrPushAxL, noting that
co2 is an axiom and that matchAxiom succeeds when looking at co1. But, what
happens when we push the coercions inside? We get

co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
  :: Equal (Id Int) (Id Bool) ~ False

which is bogus! This is because the type system isn't smart enough to know
that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
families. At the time of writing, I (Richard Eisenberg) couldn't think of
a way of detecting this any more efficient than just building the optimised
coercion and checking.

Note [EtaAppCo]
~~~~~~~~~~~~~~~
Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd
like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that
the resultant coercions might not be well kinded. Here is an example (things
labeled with x don't matter in this example):

  k1 :: Type
  k2 :: Type

  a :: k1 -> Type
  b :: k1

  h :: k1 ~ k2

  co1a :: x1 ~ (a |> (h -> <Type>)
  co1b :: x2 ~ (b |> h)

  co2a :: a ~ x3
  co2b :: b ~ x4

First, convince yourself of the following:

  co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h)
  co2a co2b :: a b   ~ x3 x4

  (a |> (h -> <Type>)) (b |> h) `eqType` a b

That last fact is due to Note [Non-trivial definitional equality] in TyCoRep,
where we ignore coercions in types as long as two types' kinds are the same.
In our case, we meet this last condition, because

  (a |> (h -> <Type>)) (b |> h) :: Type
    and
  a b :: Type

So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the
suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the
kinds don't match up.

The solution here is to twiddle the kinds in the output coercions. First, we
need to find coercions

  ak :: kind(a |> (h -> <Type>)) ~ kind(a)
  bk :: kind(b |> h)             ~ kind(b)

This can be done with mkKindCo and buildCoercion. The latter assumes two
types are identical modulo casts and builds a coercion between them.

Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
output coercions. These are well-kinded.

Also, note that all of this is done after accumulated any nested AppCo
parameters. This step is to avoid quadratic behavior in calling coercionKind.

The problem described here was first found in dependent/should_compile/dynamic-paper.

-}

-- | Check to make sure that an AxInstCo is internally consistent.
-- Returns the conflicting branch, if it exists
-- See Note [Conflict checking with AxiomInstCo]
checkAxInstCo :: Coercion -> Maybe CoAxBranch
-- defined here to avoid dependencies in Coercion
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism] in CoreLint
checkAxInstCo :: Coercion -> Maybe CoAxBranch
checkAxInstCo (AxiomInstCo ax :: CoAxiom Branched
ax ind :: Int
ind cos :: [Coercion]
cos)
  = let branch :: CoAxBranch
branch       = CoAxiom Branched -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom Branched
ax Int
ind
        tvs :: [TyCoVar]
tvs          = CoAxBranch -> [TyCoVar]
coAxBranchTyVars CoAxBranch
branch
        cvs :: [TyCoVar]
cvs          = CoAxBranch -> [TyCoVar]
coAxBranchCoVars CoAxBranch
branch
        incomps :: [CoAxBranch]
incomps      = CoAxBranch -> [CoAxBranch]
coAxBranchIncomps CoAxBranch
branch
        (tys :: [Type]
tys, cotys :: [Type]
cotys) = [TyCoVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [TyCoVar]
tvs ((Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Pair Type -> Type
forall a. Pair a -> a
pFst (Pair Type -> Type) -> (Coercion -> Pair Type) -> Coercion -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> Pair Type
coercionKind) [Coercion]
cos)
        co_args :: [Coercion]
co_args      = (Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
stripCoercionTy [Type]
cotys
        subst :: TCvSubst
subst        = [TyCoVar] -> [Type] -> TCvSubst
HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst
zipTvSubst [TyCoVar]
tvs [Type]
tys TCvSubst -> TCvSubst -> TCvSubst
`composeTCvSubst`
                       [TyCoVar] -> [Coercion] -> TCvSubst
HasDebugCallStack => [TyCoVar] -> [Coercion] -> TCvSubst
zipCvSubst [TyCoVar]
cvs [Coercion]
co_args
        target :: [Type]
target   = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst (CoAxBranch -> [Type]
coAxBranchLHS CoAxBranch
branch)
        in_scope :: InScopeSet
in_scope = TyCoVarSet -> InScopeSet
mkInScopeSet (TyCoVarSet -> InScopeSet) -> TyCoVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
                   [TyCoVarSet] -> TyCoVarSet
unionVarSets ((CoAxBranch -> TyCoVarSet) -> [CoAxBranch] -> [TyCoVarSet]
forall a b. (a -> b) -> [a] -> [b]
map ([Type] -> TyCoVarSet
tyCoVarsOfTypes ([Type] -> TyCoVarSet)
-> (CoAxBranch -> [Type]) -> CoAxBranch -> TyCoVarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxBranch -> [Type]
coAxBranchLHS) [CoAxBranch]
incomps)
        flattened_target :: [Type]
flattened_target = InScopeSet -> [Type] -> [Type]
flattenTys InScopeSet
in_scope [Type]
target in
    [Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict [Type]
flattened_target [CoAxBranch]
incomps
  where
    check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
    check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict _    [] = Maybe CoAxBranch
forall a. Maybe a
Nothing
    check_no_conflict flat :: [Type]
flat (b :: CoAxBranch
b@CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs_incomp } : rest :: [CoAxBranch]
rest)
         -- See Note [Apartness] in FamInstEnv
      | UnifyResultM TCvSubst
SurelyApart <- (TyCoVar -> BindFlag) -> [Type] -> [Type] -> UnifyResultM TCvSubst
tcUnifyTysFG TyCoVar -> BindFlag
instanceBindFun [Type]
flat [Type]
lhs_incomp
      = [Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict [Type]
flat [CoAxBranch]
rest
      | Bool
otherwise
      = CoAxBranch -> Maybe CoAxBranch
forall a. a -> Maybe a
Just CoAxBranch
b
checkAxInstCo _ = Maybe CoAxBranch
forall a. Maybe a
Nothing


-----------
wrapSym :: SymFlag -> Coercion -> Coercion
wrapSym :: Bool -> Coercion -> Coercion
wrapSym sym :: Bool
sym co :: Coercion
co | Bool
sym       = Coercion -> Coercion
mkSymCo Coercion
co
               | Bool
otherwise = Coercion
co

-- | Conditionally set a role to be representational
wrapRole :: ReprFlag
         -> Role         -- ^ current role
         -> Coercion -> Coercion
wrapRole :: Bool -> Role -> Coercion -> Coercion
wrapRole False _       = Coercion -> Coercion
forall a. a -> a
id
wrapRole True  current :: Role
current = Role -> Role -> Coercion -> Coercion
downgradeRole Role
Representational Role
current

-- | If we require a representational role, return that. Otherwise,
-- return the "default" role provided.
chooseRole :: ReprFlag
           -> Role    -- ^ "default" role
           -> Role
chooseRole :: Bool -> Role -> Role
chooseRole True _ = Role
Representational
chooseRole _    r :: Role
r = Role
r

-----------
isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
isAxiom_maybe (SymCo co :: Coercion
co)
  | Just (sym :: Bool
sym, con :: CoAxiom Branched
con, ind :: Int
ind, cos :: [Coercion]
cos) <- Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
isAxiom_maybe Coercion
co
  = (Bool, CoAxiom Branched, Int, [Coercion])
-> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
forall a. a -> Maybe a
Just (Bool -> Bool
not Bool
sym, CoAxiom Branched
con, Int
ind, [Coercion]
cos)
isAxiom_maybe (AxiomInstCo con :: CoAxiom Branched
con ind :: Int
ind cos :: [Coercion]
cos)
  = (Bool, CoAxiom Branched, Int, [Coercion])
-> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
forall a. a -> Maybe a
Just (Bool
False, CoAxiom Branched
con, Int
ind, [Coercion]
cos)
isAxiom_maybe _ = Maybe (Bool, CoAxiom Branched, Int, [Coercion])
forall a. Maybe a
Nothing

matchAxiom :: Bool -- True = match LHS, False = match RHS
           -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
matchAxiom :: Bool -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
matchAxiom sym :: Bool
sym ax :: CoAxiom br
ax@(CoAxiom { co_ax_tc :: forall (br :: BranchFlag). CoAxiom br -> TyCon
co_ax_tc = TyCon
tc }) ind :: Int
ind co :: Coercion
co
  | CoAxBranch { cab_tvs :: CoAxBranch -> [TyCoVar]
cab_tvs = [TyCoVar]
qtvs
               , cab_cvs :: CoAxBranch -> [TyCoVar]
cab_cvs = []   -- can't infer these, so fail if there are any
               , cab_roles :: CoAxBranch -> [Role]
cab_roles = [Role]
roles
               , cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs
               , cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs } <- CoAxiom br -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Int
ind
  , Just subst :: LiftingContext
subst <- TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
liftCoMatch ([TyCoVar] -> TyCoVarSet
mkVarSet [TyCoVar]
qtvs)
                              (if Bool
sym then (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
lhs) else Type
rhs)
                              Coercion
co
  , (TyCoVar -> Bool) -> [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TyCoVar -> LiftingContext -> Bool
`isMappedByLC` LiftingContext
subst) [TyCoVar]
qtvs
  = (Role -> TyCoVar -> Maybe Coercion)
-> [Role] -> [TyCoVar] -> Maybe [Coercion]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (LiftingContext -> Role -> TyCoVar -> Maybe Coercion
liftCoSubstTyVar LiftingContext
subst) [Role]
roles [TyCoVar]
qtvs

  | Bool
otherwise
  = Maybe [Coercion]
forall a. Maybe a
Nothing

-------------
compatible_co :: Coercion -> Coercion -> Bool
-- Check whether (co1 . co2) will be well-kinded
compatible_co :: Coercion -> Coercion -> Bool
compatible_co co1 :: Coercion
co1 co2 :: Coercion
co2
  = Type
x1 Type -> Type -> Bool
`eqType` Type
x2
  where
    Pair _ x1 :: Type
x1 = Coercion -> Pair Type
coercionKind Coercion
co1
    Pair x2 :: Type
x2 _ = Coercion -> Pair Type
coercionKind Coercion
co2

-------------
{-
etaForAllCo
~~~~~~~~~~~~~~~~~
(1) etaForAllCo_ty_maybe
Suppose we have

  g : all a1:k1.t1  ~  all a2:k2.t2

but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:

  g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g))

Call the kind coercion h1 and the body coercion h2. We can see that

  h2 : t1 ~ t2[a2 |-> (a1 |> h1)]

According to the typing rule for ForAllCo, we get that

  g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1])

or

  g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> a1])

as desired.

(2) etaForAllCo_co_maybe
Suppose we have

  g : all c1:(s1~s2). t1 ~ all c2:(s3~s4). t2

Similarly, we do this

  g' = all c1:h1. h2
     : all c1:(s1~s2). t1 ~ all c1:(s3~s4). t2[c2 |-> (sym eta1;c1;eta2)]
                                              [c1 |-> eta1;c1;sym eta2]

Here,

  h1   = mkNthCo Nominal 0 g :: (s1~s2)~(s3~s4)
  eta1 = mkNthCo r 2 h1      :: (s1 ~ s3)
  eta2 = mkNthCo r 3 h1      :: (s2 ~ s4)
  h2   = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
-}
etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
-- Try to make the coercion be of form (forall tv:kind_co. co)
etaForAllCo_ty_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
etaForAllCo_ty_maybe co :: Coercion
co
  | Just (tv :: TyCoVar
tv, kind_co :: Coercion
kind_co, r :: Coercion
r) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co
  = (TyCoVar, Coercion, Coercion)
-> Maybe (TyCoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just (TyCoVar
tv, Coercion
kind_co, Coercion
r)

  | Pair ty1 :: Type
ty1 ty2 :: Type
ty2  <- Coercion -> Pair Type
coercionKind Coercion
co
  , Just (tv1 :: TyCoVar
tv1, _) <- Type -> Maybe (TyCoVar, Type)
splitForAllTy_ty_maybe Type
ty1
  , Type -> Bool
isForAllTy_ty Type
ty2
  , let kind_co :: Coercion
kind_co = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal 0 Coercion
co
  = (TyCoVar, Coercion, Coercion)
-> Maybe (TyCoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just ( TyCoVar
tv1, Coercion
kind_co
         , Coercion -> Coercion -> Coercion
mkInstCo Coercion
co (Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
Nominal (TyCoVar -> Type
TyVarTy TyCoVar
tv1) Coercion
kind_co))

  | Bool
otherwise
  = Maybe (TyCoVar, Coercion, Coercion)
forall a. Maybe a
Nothing

etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
-- Try to make the coercion be of form (forall cv:kind_co. co)
etaForAllCo_co_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
etaForAllCo_co_maybe co :: Coercion
co
  | Just (cv :: TyCoVar
cv, kind_co :: Coercion
kind_co, r :: Coercion
r) <- Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_co_maybe Coercion
co
  = (TyCoVar, Coercion, Coercion)
-> Maybe (TyCoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just (TyCoVar
cv, Coercion
kind_co, Coercion
r)

  | Pair ty1 :: Type
ty1 ty2 :: Type
ty2  <- Coercion -> Pair Type
coercionKind Coercion
co
  , Just (cv1 :: TyCoVar
cv1, _) <- Type -> Maybe (TyCoVar, Type)
splitForAllTy_co_maybe Type
ty1
  , Type -> Bool
isForAllTy_co Type
ty2
  = let kind_co :: Coercion
kind_co  = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal 0 Coercion
co
        r :: Role
r        = TyCoVar -> Role
coVarRole TyCoVar
cv1
        l_co :: Coercion
l_co     = TyCoVar -> Coercion
mkCoVarCo TyCoVar
cv1
        kind_co' :: Coercion
kind_co' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
r Role
Nominal Coercion
kind_co
        r_co :: Coercion
r_co     = (Coercion -> Coercion
mkSymCo (HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r 2 Coercion
kind_co')) Coercion -> Coercion -> Coercion
`mkTransCo`
                   Coercion
l_co Coercion -> Coercion -> Coercion
`mkTransCo`
                   (HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r 3 Coercion
kind_co')
    in (TyCoVar, Coercion, Coercion)
-> Maybe (TyCoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just ( TyCoVar
cv1, Coercion
kind_co
            , Coercion -> Coercion -> Coercion
mkInstCo Coercion
co (Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal Coercion
kind_co Coercion
l_co Coercion
r_co))

  | Bool
otherwise
  = Maybe (TyCoVar, Coercion, Coercion)
forall a. Maybe a
Nothing

etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
-- If possible, split a coercion
--   g :: t1a t1b ~ t2a t2b
-- into a pair of coercions (left g, right g)
etaAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
etaAppCo_maybe co :: Coercion
co
  | Just (co1 :: Coercion
co1,co2 :: Coercion
co2) <- Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe Coercion
co
  = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just (Coercion
co1,Coercion
co2)
  | (Pair ty1 :: Type
ty1 ty2 :: Type
ty2, Nominal) <- Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
  , Just (_,t1 :: Type
t1) <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ty1
  , Just (_,t2 :: Type
t2) <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ty2
  , let isco1 :: Bool
isco1 = Type -> Bool
isCoercionTy Type
t1
  , let isco2 :: Bool
isco2 = Type -> Bool
isCoercionTy Type
t2
  , Bool
isco1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
isco2
  = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just (LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
CLeft Coercion
co, LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
CRight Coercion
co)
  | Bool
otherwise
  = Maybe (Coercion, Coercion)
forall a. Maybe a
Nothing

etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
-- If possible, split a coercion
--       g :: T s1 .. sn ~ T t1 .. tn
-- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
etaTyConAppCo_maybe tc :: TyCon
tc (TyConAppCo _ tc2 :: TyCon
tc2 cos2 :: [Coercion]
cos2)
  = ASSERT( tc == tc2 ) Just cos2

etaTyConAppCo_maybe tc :: TyCon
tc co :: Coercion
co
  | TyCon -> Bool
mightBeUnsaturatedTyCon TyCon
tc
  , (Pair ty1 :: Type
ty1 ty2 :: Type
ty2, r :: Role
r) <- Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
  , Just (tc1 :: TyCon
tc1, tys1 :: [Type]
tys1)  <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
  , Just (tc2 :: TyCon
tc2, tys2 :: [Type]
tys2)  <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty2
  , TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
  , TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc Role
r  -- See Note [NthCo and newtypes] in TyCoRep
  , let n :: Int
n = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys1
  , [Type]
tys2 [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` Int
n      -- This can fail in an erroneous progam
                           -- E.g. T a ~# T a b
                           -- Trac #14607
  = ASSERT( tc == tc1 )
    [Coercion] -> Maybe [Coercion]
forall a. a -> Maybe a
Just (Int -> Coercion -> [Role] -> [Coercion]
decomposeCo Int
n Coercion
co (Role -> TyCon -> [Role]
tyConRolesX Role
r TyCon
tc1))
    -- NB: n might be <> tyConArity tc
    -- e.g.   data family T a :: * -> *
    --        g :: T a b ~ T c d

  | Bool
otherwise
  = Maybe [Coercion]
forall a. Maybe a
Nothing

{-
Note [Eta for AppCo]
~~~~~~~~~~~~~~~~~~~~
Suppose we have
   g :: s1 t1 ~ s2 t2

Then we can't necessarily make
   left  g :: s1 ~ s2
   right g :: t1 ~ t2
because it's possible that
   s1 :: * -> *         t1 :: *
   s2 :: (*->*) -> *    t2 :: * -> *
and in that case (left g) does not have the same
kind on either side.

It's enough to check that
  kind t1 = kind t2
because if g is well-kinded then
  kind (s1 t2) = kind (s2 t2)
and these two imply
  kind s1 = kind s2

-}

optForAllCoBndr :: LiftingContext -> Bool
                -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
optForAllCoBndr :: LiftingContext
-> Bool
-> TyCoVar
-> Coercion
-> (LiftingContext, TyCoVar, Coercion)
optForAllCoBndr env :: LiftingContext
env sym :: Bool
sym
  = Bool
-> (Coercion -> Coercion)
-> LiftingContext
-> TyCoVar
-> Coercion
-> (LiftingContext, TyCoVar, Coercion)
substForAllCoBndrUsingLC Bool
sym (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal) LiftingContext
env