-- (c) The University of Glasgow 2006

{-# LANGUAGE CPP #-}

module GHC.Core.Coercion.Opt
   ( optCoercion
   , OptCoercionOpts (..)
   )
where

import GHC.Prelude

import GHC.Tc.Utils.TcType   ( exactTyCoVarsOfType )

import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.Compare( eqType )
import GHC.Core.Coercion
import GHC.Core.Type as Type hiding( substTyVarBndr, substTy )
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import GHC.Core.Unify

import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.Unique.Set

import GHC.Data.Pair
import GHC.Data.List.SetOps ( getNth )

import GHC.Utils.Outputable
import GHC.Utils.Constants (debugIsOn)
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain

import Control.Monad   ( zipWithM )

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

This module does coercion optimisation.  See the paper

   Evidence normalization in Systtem FV (RTA'13)
   https://simon.peytonjones.org/evidence-normalization/

The paper is also in the GHC repo, in docs/opt-coercion.

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 GHC.Core.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.
-}

-- | Coercion optimisation options
newtype OptCoercionOpts = OptCoercionOpts
   { OptCoercionOpts -> Bool
optCoercionEnabled :: Bool  -- ^ Enable coercion optimisation (reduce its size)
   }

optCoercion :: OptCoercionOpts -> Subst -> Coercion -> NormalCo
-- ^ optCoercion applies a substitution to a coercion,
--   *and* optimises it to reduce its size
optCoercion :: OptCoercionOpts -> Subst -> Coercion -> Coercion
optCoercion OptCoercionOpts
opts Subst
env Coercion
co
  | OptCoercionOpts -> Bool
optCoercionEnabled OptCoercionOpts
opts
  = Subst -> Coercion -> Coercion
optCoercion' Subst
env Coercion
co
{-
  = pprTrace "optCoercion {" (text "Co:" <+> ppr co) $
    let result = optCoercion' env co in
    pprTrace "optCoercion }" (vcat [ text "Co:" <+> ppr co
                                   , text "Optco:" <+> ppr result ]) $
    result
-}

  | Bool
otherwise
  = HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo Subst
env Coercion
co


optCoercion' :: Subst -> Coercion -> NormalCo
optCoercion' :: Subst -> Coercion -> Coercion
optCoercion' Subst
env Coercion
co
  | Bool
debugIsOn
  = let out_co :: Coercion
out_co = LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
lc Bool
False Coercion
co
        (Pair Type
in_ty1  Type
in_ty2,  Role
in_role)  = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
        (Pair Type
out_ty1 Type
out_ty2, Role
out_role) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
out_co
    in
    Bool -> SDoc -> Coercion -> Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Subst -> Type -> Type
substTyUnchecked Subst
env Type
in_ty1 Type -> Type -> Bool
`eqType` Type
out_ty1 Bool -> Bool -> Bool
&&
               Subst -> Type -> Type
substTyUnchecked Subst
env Type
in_ty2 Type -> Type -> Bool
`eqType` Type
out_ty2 Bool -> Bool -> Bool
&&
               Role
in_role Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
out_role)
              (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"optCoercion changed types!")
                  Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in_co:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in_ty1:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
in_ty1
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in_ty2:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
in_ty2
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"out_co:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
out_co
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"out_ty1:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
out_ty1
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"out_ty2:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
out_ty2
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in_role:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
in_role
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"out_role:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
out_role
                          , [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ (CoVar -> SDoc) -> [CoVar] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map CoVar -> SDoc
ppr_one ([CoVar] -> [SDoc]) -> [CoVar] -> [SDoc]
forall a b. (a -> b) -> a -> b
$ UniqSet CoVar -> [CoVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet (UniqSet CoVar -> [CoVar]) -> UniqSet CoVar -> [CoVar]
forall a b. (a -> b) -> a -> b
$ Coercion -> UniqSet CoVar
coVarsOfCo Coercion
co
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"subst:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Subst -> SDoc
forall a. Outputable a => a -> SDoc
ppr Subst
env ]))
               Coercion
out_co

  | Bool
otherwise         = LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
lc Bool
False Coercion
co
  where
    lc :: LiftingContext
lc = Subst -> LiftingContext
mkSubstLiftingContext Subst
env
    ppr_one :: CoVar -> SDoc
ppr_one CoVar
cv = CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
cv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CoVar -> Type
coVarKind CoVar
cv)


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 LiftingContext
env Bool
sym 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 LiftingContext
env Bool
sym Role
Phantom Coercion
co = LiftingContext -> Bool -> Coercion -> Coercion
opt_phantom LiftingContext
env Bool
sym Coercion
co
opt_co2 LiftingContext
env Bool
sym Role
r       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 LiftingContext
env Bool
sym (Just Role
Phantom)          Role
_ Coercion
co = LiftingContext -> Bool -> Coercion -> Coercion
opt_phantom LiftingContext
env Bool
sym Coercion
co
opt_co3 LiftingContext
env Bool
sym (Just Role
Representational) Role
r 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 LiftingContext
env Bool
sym Maybe Role
_                       Role
r 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
-- Precondition: In every call (opt_co4 lc sym rep role co)
--               we should have role = coercionRole co
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 LiftingContext
env Bool
_   Bool
rep Role
r (Refl Type
ty)
  = Bool -> SDoc -> Coercion -> Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal)
              (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Expected role:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r    SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Found role:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
Nominal SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env Type
ty

opt_co4 LiftingContext
env Bool
_   Bool
rep Role
r (GRefl Role
_r Type
ty MCoercion
MRefl)
  = Bool -> SDoc -> Coercion -> Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
_r)
              (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Expected role:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Found role:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
_r   SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env Type
ty

opt_co4 LiftingContext
env Bool
sym  Bool
rep Role
r (GRefl Role
_r Type
ty (MCo Coercion
co))
  = Bool -> SDoc -> Coercion -> Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
_r)
              (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Expected role:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Found role:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
_r   SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    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' = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (LiftingContext -> Subst
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 LiftingContext
env Bool
sym Bool
rep Role
r (SymCo 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 LiftingContext
env Bool
sym Bool
rep Role
r g :: Coercion
g@(TyConAppCo Role
_r TyCon
tc [Coercion]
cos)
  = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
_r) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    case (Bool
rep, Role
r) of
      (Bool
True, Role
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]
tyConRoleListRepresentational TyCon
tc))
                               (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal)
                               [Coercion]
cos)
      (Bool
False, Role
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)
      (Bool
_, Role
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]
tyConRoleListRepresentational TyCon
tc)  -- the current roles
                                   [Coercion]
cos)
      (Bool
_, Role
Phantom) -> String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"opt_co4 sees a phantom!" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
g)

opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (AppCo Coercion
co1 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 LiftingContext
env Bool
sym Bool
rep Role
r (ForAllCo CoVar
tv Coercion
k_co Coercion
co)
  = case LiftingContext
-> Bool -> CoVar -> Coercion -> (LiftingContext, CoVar, Coercion)
optForAllCoBndr LiftingContext
env Bool
sym CoVar
tv Coercion
k_co of
      (LiftingContext
env', CoVar
tv', Coercion
k_co') -> CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
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 LiftingContext
env Bool
sym Bool
rep Role
r (FunCo Role
_r FunTyFlag
afl FunTyFlag
afr Coercion
cow Coercion
co1 Coercion
co2)
  = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
_r) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    Role
-> FunTyFlag
-> FunTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkFunCo2 Role
r' FunTyFlag
afl' FunTyFlag
afr' Coercion
cow' 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
    cow' :: Coercion
cow' = LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
env Bool
sym Coercion
cow
    !r' :: Role
r' | Bool
rep       = Role
Representational
        | Bool
otherwise = Role
r
    !(FunTyFlag
afl', FunTyFlag
afr') | Bool
sym       = (FunTyFlag
afr,FunTyFlag
afl)
                  | Bool
otherwise = (FunTyFlag
afl,FunTyFlag
afr)

opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (CoVarCo CoVar
cv)
  | Just Coercion
co <- Subst -> CoVar -> Maybe Coercion
lookupCoVar (LiftingContext -> Subst
lcSubst LiftingContext
env) CoVar
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
  = Bool
-> (Bool -> Role -> Coercion -> Coercion)
-> Bool
-> Role
-> Coercion
-> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (CoVar -> Bool
isCoVar CoVar
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
$
    CoVar -> Coercion
CoVarCo CoVar
cv1

  where
    Pair Type
ty1 Type
ty2 = HasDebugCallStack => CoVar -> Pair Type
CoVar -> Pair Type
coVarTypes CoVar
cv1

    cv1 :: CoVar
cv1 = case InScopeSet -> CoVar -> Maybe CoVar
lookupInScope (LiftingContext -> InScopeSet
lcInScopeSet LiftingContext
env) CoVar
cv of
             Just CoVar
cv1 -> CoVar
cv1
             Maybe CoVar
Nothing  -> Bool -> String -> SDoc -> CoVar -> CoVar
forall a. HasCallStack => Bool -> String -> SDoc -> a -> a
warnPprTrace Bool
True
                          String
"opt_co: not in scope"
                          (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
cv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ LiftingContext -> SDoc
forall a. Outputable a => a -> SDoc
ppr LiftingContext
env)
                          CoVar
cv
          -- cv1 might have a substituted kind!

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

opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (AxiomInstCo CoAxiom Branched
con Int
ind [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) !!
  = Bool
-> (Bool -> Role -> Coercion -> Coercion)
-> Bool
-> Role
-> Coercion
-> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== CoAxiom Branched -> Role
forall (br :: BranchFlag). CoAxiom br -> Role
coAxiomRole CoAxiom Branched
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 LiftingContext
env Bool
sym Bool
rep Role
r (UnivCo UnivCoProvenance
prov Role
_r Type
t1 Type
t2)
  = Bool
-> (LiftingContext
    -> Bool -> UnivCoProvenance -> Role -> Type -> Type -> Coercion)
-> LiftingContext
-> Bool
-> UnivCoProvenance
-> Role
-> Type
-> Type
-> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
_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 LiftingContext
env Bool
sym Bool
rep Role
r (TransCo Coercion
co1 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 LiftingContext
env Bool
_sym Bool
rep Role
r (SelCo CoSel
n Coercion
co)
  | Just (Type
ty, Role
_co_role) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
  = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env (HasDebugCallStack => CoSel -> Type -> Type
CoSel -> Type -> Type
getNthFromType CoSel
n Type
ty)
    -- NB: it is /not/ true that r = _co_role
    --     Rather, r = coercionRole (SelCo n co)

opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (SelCo (SelTyCon Int
n Role
r1) (TyConAppCo Role
_ TyCon
_ [Coercion]
cos))
  = Bool
-> (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion)
-> LiftingContext
-> Bool
-> Bool
-> Role
-> Coercion
-> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
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)

-- see the definition of GHC.Builtin.Types.Prim.funTyCon
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (SelCo (SelFun FunSel
fs) (FunCo Role
_r2 FunTyFlag
_afl FunTyFlag
_afr Coercion
w Coercion
co1 Coercion
co2))
  = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r (FunSel -> Coercion -> Coercion -> Coercion -> Coercion
forall a. FunSel -> a -> a -> a -> a
getNthFun FunSel
fs Coercion
w Coercion
co1 Coercion
co2)

opt_co4 LiftingContext
env Bool
sym Bool
rep Role
_ (SelCo CoSel
SelForAll (ForAllCo CoVar
_ Coercion
eta Coercion
_))
      -- works for both tyvar and covar
  = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
Nominal Coercion
eta

opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (SelCo CoSel
n Coercion
co)
  | Just Coercion
nth_co <- case (Coercion
co', CoSel
n) of
      (TyConAppCo Role
_ TyCon
_ [Coercion]
cos, SelTyCon Int
n Role
_) -> Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just ([Coercion]
cos [Coercion] -> Int -> Coercion
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n)
      (FunCo Role
_ FunTyFlag
_ FunTyFlag
_ Coercion
w Coercion
co1 Coercion
co2, SelFun FunSel
fs) -> Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (FunSel -> Coercion -> Coercion -> Coercion -> Coercion
forall a. FunSel -> a -> a -> a -> a
getNthFun FunSel
fs Coercion
w Coercion
co1 Coercion
co2)
      (ForAllCo CoVar
_ Coercion
eta Coercion
_, CoSel
SelForAll)      -> Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
eta
      (Coercion, CoSel)
_                  -> Maybe Coercion
forall a. Maybe a
Nothing
  = 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

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

opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (LRCo LeftOrRight
lr Coercion
co)
  | Just (Coercion, Coercion)
pr_co <- Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe Coercion
co
  = Bool
-> (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion)
-> LiftingContext
-> Bool
-> Bool
-> Role
-> Coercion
-> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal )
    LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
Nominal (LeftOrRight -> (Coercion, Coercion) -> Coercion
forall {a}. LeftOrRight -> (a, a) -> a
pick_lr LeftOrRight
lr (Coercion, Coercion)
pr_co)
  | Just (Coercion, Coercion)
pr_co <- Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe Coercion
co'
  = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    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 {a}. LeftOrRight -> (a, a) -> a
pick_lr LeftOrRight
lr (Coercion, Coercion)
pr_co)
    else LeftOrRight -> (Coercion, Coercion) -> Coercion
forall {a}. LeftOrRight -> (a, a) -> a
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 -> (a, a) -> a
pick_lr LeftOrRight
CLeft  (a
l, a
_) = a
l
    pick_lr LeftOrRight
CRight (a
_, a
r) = a
r

-- See Note [Optimising InstCo]
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (InstCo Coercion
co1 Coercion
arg)
    -- forall over type...
  | Just (CoVar
tv, Coercion
kind_co, Coercion
co_body) <- Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co1
  = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContext LiftingContext
env CoVar
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 (CoVar
cv, Coercion
kind_co, Coercion
co_body) <- Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_co_maybe Coercion
co1
  , CoercionTy Coercion
h1 <- Type
t1
  , CoercionTy Coercion
h2 <- Type
t2
  = let new_co :: Coercion
new_co = CoVar -> Coercion -> Coercion -> Coercion -> Coercion
mk_new_co CoVar
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 -> CoVar -> Coercion -> LiftingContext
extendLiftingContext LiftingContext
env CoVar
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 (CoVar
tv', Coercion
kind_co', Coercion
co_body') <- Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co1'
  = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContext (LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
env) CoVar
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 (CoVar
cv', Coercion
kind_co', Coercion
co_body') <- Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_co_maybe Coercion
co1'
  , CoercionTy Coercion
h1' <- Type
t1'
  , CoercionTy Coercion
h2' <- Type
t2'
  = let new_co :: Coercion
new_co = CoVar -> Coercion -> Coercion -> Coercion -> Coercion
mk_new_co CoVar
cv' Coercion
kind_co' Coercion
h1' Coercion
h2'
    in LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContext (LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
env) CoVar
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 Type
t1  Type
t2  = Coercion -> Pair Type
coercionKind Coercion
sym_arg
    Pair Type
t1' Type
t2' = Coercion -> Pair Type
coercionKind Coercion
arg'

    mk_new_co :: CoVar -> Coercion -> Coercion -> Coercion -> Coercion
mk_new_co CoVar
cv Coercion
kind_co Coercion
h1 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  = CoVar -> Role
coVarRole CoVar
cv
            kind_co' :: Coercion
kind_co' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
r2 Role
Nominal Coercion
kind_co
            n1 :: Coercion
n1 = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Int -> Role -> CoSel
SelTyCon Int
2 Role
r2) Coercion
kind_co'
            n2 :: Coercion
n2 = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Int -> Role -> CoSel
SelTyCon Int
3 Role
r2) 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 LiftingContext
env Bool
sym Bool
_rep Role
r (KindCo Coercion
co)
  = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    let kco' :: Coercion
kco' = Coercion -> Coercion
promoteCoercion Coercion
co in
    case Coercion
kco' of
      KindCo Coercion
co' -> Coercion -> Coercion
promoteCoercion (LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
env Bool
sym Coercion
co')
      Coercion
_          -> 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 LiftingContext
env Bool
sym Bool
_ Role
r (SubCo Coercion
co)
  = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Representational) (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
True Role
Nominal Coercion
co

-- This could perhaps be optimized more.
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (AxiomRuleCo CoAxiomRule
co [Coercion]
cs)
  = Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== CoAxiomRule -> Role
coaxrRole CoAxiomRule
co) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
    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 GHC.Core.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 LiftingContext
env Bool
sym 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 Type
ty1 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 #13658

Note [opt_univ needs injectivity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If opt_univ sees a coercion between `T a1 a2` and `T b1 b2` it will optimize it
by producing a TyConAppCo for T, and pushing the UnivCo into the arguments.  But
this works only if T is injective. Otherwise we can have something like

  type family F x where
    F Int  = Int
    F Bool = Int

where `UnivCo :: F Int ~ F Bool` is reasonable (it is effectively just an
alternative representation for a couple of uses of AxiomInstCos) but we do not
want to produce `F (UnivCo :: Int ~ Bool)` where the inner coercion is clearly
inconsistent.  Hence the opt_univ case for TyConApps checks isInjectiveTyCon.
See #19509.

 -}

opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
         -> Type -> Type -> Coercion
opt_univ :: LiftingContext
-> Bool -> UnivCoProvenance -> Role -> Type -> Type -> Coercion
opt_univ LiftingContext
env Bool
sym (PhantomProv Coercion
h) Role
_r Type
ty1 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' = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (LiftingContext -> Subst
lcSubstLeft  LiftingContext
env) Type
ty1
    ty2' :: Type
ty2' = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (LiftingContext -> Subst
lcSubstRight LiftingContext
env) Type
ty2

opt_univ LiftingContext
env Bool
sym UnivCoProvenance
prov Role
role Type
oty1 Type
oty2
  | Just (TyCon
tc1, [Type]
tys1) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
oty1
  , Just (TyCon
tc2, [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
  , TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc1 Role
role  -- see Note [opt_univ needs injectivity]
  , [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]
tyConRoleListX 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 (CoVar
tv1, Type
ty1) <- Type -> Maybe (CoVar, Type)
splitForAllTyVar_maybe Type
oty1
  , Just (CoVar
tv2, Type
ty2) <- Type -> Maybe (CoVar, Type)
splitForAllTyVar_maybe Type
oty2
      -- NB: prov isn't interesting here either
  = let k1 :: Type
k1   = CoVar -> Type
tyVarKind CoVar
tv1
        k2 :: Type
k2   = CoVar -> Type
tyVarKind CoVar
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' = [CoVar] -> [Type] -> Type -> Type
HasDebugCallStack => [CoVar] -> [Type] -> Type -> Type
substTyWith [CoVar
tv2] [CoVar -> Type
TyVarTy CoVar
tv1 Type -> Coercion -> Type
`mkCastTy` Coercion
eta] Type
ty2

        (LiftingContext
env', CoVar
tv1', Coercion
eta') = LiftingContext
-> Bool -> CoVar -> Coercion -> (LiftingContext, CoVar, Coercion)
optForAllCoBndr LiftingContext
env Bool
sym CoVar
tv1 Coercion
eta
    in
    CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
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 (CoVar
cv1, Type
ty1) <- Type -> Maybe (CoVar, Type)
splitForAllCoVar_maybe Type
oty1
  , Just (CoVar
cv2, Type
ty2) <- Type -> Maybe (CoVar, Type)
splitForAllCoVar_maybe Type
oty2
      -- NB: prov isn't interesting here either
  = let k1 :: Type
k1    = CoVar -> Type
varType CoVar
cv1
        k2 :: Type
k2    = CoVar -> Type
varType CoVar
cv2
        r' :: Role
r'    = CoVar -> Role
coVarRole CoVar
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 => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Int -> Role -> CoSel
SelTyCon Int
2 Role
r') Coercion
eta_d) Coercion -> Coercion -> Coercion
`mkTransCo`
                (CoVar -> Coercion
mkCoVarCo CoVar
cv1) Coercion -> Coercion -> Coercion
`mkTransCo`
                (HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Int -> Role -> CoSel
SelTyCon Int
3 Role
r') Coercion
eta_d)
        ty2' :: Type
ty2'  = [CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars [CoVar
cv2] [Coercion
n_co] Type
ty2

        (LiftingContext
env', CoVar
cv1', Coercion
eta') = LiftingContext
-> Bool -> CoVar -> Coercion -> (LiftingContext, CoVar, Coercion)
optForAllCoBndr LiftingContext
env Bool
sym CoVar
cv1 Coercion
eta
    in
    CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
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 = Subst -> Type -> Type
substTyUnchecked (LiftingContext -> Subst
lcSubstLeft  LiftingContext
env) Type
oty1
        ty2 :: Type
ty2 = Subst -> Type -> Type
substTyUnchecked (LiftingContext -> Subst
lcSubstRight LiftingContext
env) Type
oty2
        (Type
a, 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
#if __GLASGOW_HASKELL__ < 901
-- This alt is redundant with the first match of the FunDef
      PhantomProv kco    -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
#endif
      ProofIrrelProv 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 String
_       -> UnivCoProvenance
prov
      CorePrepProv Bool
_     -> UnivCoProvenance
prov

-------------
opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList :: HasDebugCallStack =>
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is = String
-> (Coercion -> Coercion -> Coercion)
-> [Coercion]
-> [Coercion]
-> [Coercion]
forall a b c.
HasDebugCallStack =>
String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"opt_transList" (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is)
  -- The input lists must have identical length.

opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
opt_trans :: InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1 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 InScopeSet
is Coercion
co1 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 InScopeSet
is (TransCo Coercion
co1a Coercion
co1b) 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 InScopeSet
is Coercion
co1 Coercion
co2
  | Just Coercion
co <- InScopeSet -> Coercion -> Coercion -> Maybe Coercion
opt_trans_rule InScopeSet
is Coercion
co1 Coercion
co2
  = Coercion
co

opt_trans2 InScopeSet
is Coercion
co1 (TransCo Coercion
co2a Coercion
co2b)
  | Just 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 InScopeSet
_ Coercion
co1 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 InScopeSet
is in_co1 :: Coercion
in_co1@(GRefl Role
r1 Type
t1 (MCo Coercion
co1)) in_co2 :: Coercion
in_co2@(GRefl Role
r2 Type
_ (MCo Coercion
co2))
  = Bool -> Maybe Coercion -> Maybe Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r1 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
r2) (Maybe Coercion -> Maybe Coercion)
-> Maybe Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"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 InScopeSet
is in_co1 :: Coercion
in_co1@(SelCo CoSel
d1 Coercion
co1) in_co2 :: Coercion
in_co2@(SelCo CoSel
d2 Coercion
co2)
  | CoSel
d1 CoSel -> CoSel -> Bool
forall a. Eq a => a -> a -> Bool
== CoSel
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
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"PushNth" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo CoSel
d1 (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1 Coercion
co2)

opt_trans_rule InScopeSet
is in_co1 :: Coercion
in_co1@(LRCo LeftOrRight
d1 Coercion
co1) in_co2 :: Coercion
in_co2@(LRCo LeftOrRight
d2 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 String
"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 InScopeSet
is in_co1 :: Coercion
in_co1@(InstCo Coercion
co1 Coercion
ty1) in_co2 :: Coercion
in_co2@(InstCo Coercion
co2 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 String
"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 InScopeSet
is in_co1 :: Coercion
in_co1@(UnivCo UnivCoProvenance
p1 Role
r1 Type
tyl1 Type
_tyr1)
                  in_co2 :: Coercion
in_co2@(UnivCo UnivCoProvenance
p2 Role
r2 Type
_tyl2 Type
tyr2)
  | Just UnivCoProvenance
prov' <- UnivCoProvenance -> UnivCoProvenance -> Maybe UnivCoProvenance
opt_trans_prov UnivCoProvenance
p1 UnivCoProvenance
p2
  = Bool -> Maybe Coercion -> Maybe Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r1 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
r2) (Maybe Coercion -> Maybe Coercion)
-> Maybe Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"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 (PhantomProv Coercion
kco1)    (PhantomProv 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 Coercion
kco1) (ProofIrrelProv 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 String
str1)     (PluginProv 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 UnivCoProvenance
_ UnivCoProvenance
_ = Maybe UnivCoProvenance
forall a. Maybe a
Nothing

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

opt_trans_rule InScopeSet
is in_co1 :: Coercion
in_co1@(FunCo Role
r1 FunTyFlag
afl1 FunTyFlag
afr1 Coercion
w1 Coercion
co1a Coercion
co1b)
                  in_co2 :: Coercion
in_co2@(FunCo Role
r2 FunTyFlag
afl2 FunTyFlag
afr2 Coercion
w2 Coercion
co2a Coercion
co2b)
  = Bool -> Maybe Coercion -> Maybe Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Role
r1 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
r2)     (Maybe Coercion -> Maybe Coercion)
-> Maybe Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$     -- Just like the TyConAppCo/TyConAppCo case
    Bool -> Maybe Coercion -> Maybe Coercion
forall a. HasCallStack => Bool -> a -> a
assert (FunTyFlag
afr1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
afl2) (Maybe Coercion -> Maybe Coercion)
-> Maybe Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"PushFun" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    Role
-> FunTyFlag
-> FunTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkFunCo2 Role
r1 FunTyFlag
afl1 FunTyFlag
afr2 (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
w1 Coercion
w2)
                          (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 InScopeSet
is in_co1 :: Coercion
in_co1@(AppCo Coercion
co1a Coercion
co1b) in_co2 :: Coercion
in_co2@(AppCo Coercion
co2a 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 InScopeSet
is co1 :: Coercion
co1@(TyConAppCo Role
r TyCon
tc [Coercion]
cos1) Coercion
co2
  | Just [Coercion]
cos2 <- TyCon -> Coercion -> Maybe [Coercion]
etaTyConAppCo_maybe TyCon
tc Coercion
co2
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"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 (HasDebugCallStack =>
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 [Coercion]
cos2)

opt_trans_rule InScopeSet
is Coercion
co1 co2 :: Coercion
co2@(TyConAppCo Role
r TyCon
tc [Coercion]
cos2)
  | Just [Coercion]
cos1 <- TyCon -> Coercion -> Maybe [Coercion]
etaTyConAppCo_maybe TyCon
tc Coercion
co1
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"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 (HasDebugCallStack =>
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 [Coercion]
cos2)

opt_trans_rule InScopeSet
is co1 :: Coercion
co1@(AppCo Coercion
co1a Coercion
co1b) Coercion
co2
  | Just (Coercion
co2a,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 InScopeSet
is Coercion
co1 co2 :: Coercion
co2@(AppCo Coercion
co2a Coercion
co2b)
  | Just (Coercion
co1a,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 InScopeSet
is Coercion
co1 Coercion
co2
  | Just (CoVar
tv1, Coercion
eta1, Coercion
r1) <- Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co1
  , Just (CoVar
tv2, Coercion
eta2, Coercion
r2) <- Coercion -> Maybe (CoVar, Coercion, Coercion)
etaForAllCo_ty_maybe Coercion
co2
  = CoVar
-> Coercion
-> Coercion
-> CoVar
-> Coercion
-> Coercion
-> Maybe Coercion
push_trans CoVar
tv1 Coercion
eta1 Coercion
r1 CoVar
tv2 Coercion
eta2 Coercion
r2

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

  where
  push_trans :: CoVar
-> Coercion
-> Coercion
-> CoVar
-> Coercion
-> Coercion
-> Maybe Coercion
push_trans CoVar
tv1 Coercion
eta1 Coercion
r1 CoVar
tv2 Coercion
eta2 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 String
"EtaAllTy_ty" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
      CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
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 -> CoVar -> InScopeSet
`extendInScopeSet` CoVar
tv1
      r2' :: Coercion
r2' = [CoVar] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked [CoVar
tv2] [Type -> Coercion -> Type
mkCastTy (CoVar -> Type
TyVarTy CoVar
tv1) Coercion
eta1] Coercion
r2

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

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

  where
  push_trans :: CoVar
-> Coercion
-> Coercion
-> CoVar
-> Coercion
-> Coercion
-> Maybe Coercion
push_trans CoVar
cv1 Coercion
eta1 Coercion
r1 CoVar
cv2 Coercion
eta2 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 String
"EtaAllTy_co" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
      CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
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 -> CoVar -> InScopeSet
`extendInScopeSet` CoVar
cv1
      role :: Role
role = CoVar -> Role
coVarRole CoVar
cv1
      eta1' :: Coercion
eta1' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
Nominal Coercion
eta1
      n1 :: Coercion
n1   = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Int -> Role -> CoSel
SelTyCon Int
2 Role
role) Coercion
eta1'
      n2 :: Coercion
n2   = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Int -> Role -> CoSel
SelTyCon Int
3 Role
role) Coercion
eta1'
      r2' :: Coercion
r2'  = HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo ([CoVar] -> [Coercion] -> Subst
HasDebugCallStack => [CoVar] -> [Coercion] -> Subst
zipCvSubst [CoVar
cv2] [(Coercion -> Coercion
mkSymCo Coercion
n1) Coercion -> Coercion -> Coercion
`mkTransCo`
                                        (CoVar -> Coercion
mkCoVarCo CoVar
cv1) Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
n2])
                    Coercion
r2

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

  -- See Note [Push transitivity inside axioms] and
  -- Note [Push transitivity inside newtype axioms only]
  -- TrPushSymAxR
  | Just (Bool
sym, CoAxiom Branched
con, Int
ind, [Coercion]
cos1) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co1_is_axiom_maybe
  , TyCon -> Bool
isNewTyCon (CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
con)
  , Bool
True <- Bool
sym
  , Just [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 (HasDebugCallStack =>
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
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)
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"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 (Bool
sym, CoAxiom Branched
con, Int
ind, [Coercion]
cos1) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co1_is_axiom_maybe
  , TyCon -> Bool
isNewTyCon (CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
con)
  , Bool
False <- Bool
sym
  , Just [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 (HasDebugCallStack =>
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 [Coercion]
cos2)
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"TrPushAxR" Coercion
co1 Coercion
co2 Coercion
newAxInst

  -- TrPushSymAxL
  | Just (Bool
sym, CoAxiom Branched
con, Int
ind, [Coercion]
cos2) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co2_is_axiom_maybe
  , TyCon -> Bool
isNewTyCon (CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
con)
  , Bool
True <- Bool
sym
  , Just [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 (HasDebugCallStack =>
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
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))
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"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 (Bool
sym, CoAxiom Branched
con, Int
ind, [Coercion]
cos2) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co2_is_axiom_maybe
  , TyCon -> Bool
isNewTyCon (CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
con)
  , Bool
False <- Bool
sym
  , Just [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 (HasDebugCallStack =>
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
opt_transList InScopeSet
is [Coercion]
cos1 [Coercion]
cos2)
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"TrPushAxL" Coercion
co1 Coercion
co2 Coercion
newAxInst

  -- TrPushAxSym/TrPushSymAx
  | Just (Bool
sym1, CoAxiom Branched
con1, Int
ind1, [Coercion]
cos1) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co1_is_axiom_maybe
  , Just (Bool
sym2, CoAxiom Branched
con2, Int
ind2, [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 :: [CoVar]
qtvs = CoAxBranch -> [CoVar]
coAxBranchTyVars CoAxBranch
branch [CoVar] -> [CoVar] -> [CoVar]
forall a. [a] -> [a] -> [a]
++ CoAxBranch -> [CoVar]
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 :: UniqSet CoVar
pivot_tvs = Type -> UniqSet CoVar
exactTyCoVarsOfType (if Bool
sym2 then Type
rhs else Type
lhs)
  , (CoVar -> Bool) -> [CoVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (CoVar -> UniqSet CoVar -> Bool
`elemVarSet` UniqSet CoVar
pivot_tvs) [CoVar]
qtvs
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"TrPushAxSym" Coercion
co1 Coercion
co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    if Bool
sym2
       -- TrPushAxSym
    then Role -> [CoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith Role
role [CoVar]
qtvs (HasDebugCallStack =>
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
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 -> [CoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith Role
role [CoVar]
qtvs (HasDebugCallStack =>
InScopeSet -> [Coercion] -> [Coercion] -> [Coercion]
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 InScopeSet
_ Coercion
co1 Coercion
co2        -- Identity rule
  | let ty1 :: Type
ty1 = Coercion -> Type
coercionLKind Coercion
co1
        r :: Role
r   = Coercion -> Role
coercionRole Coercion
co1
        ty2 :: Type
ty2 = Coercion -> Type
coercionRKind Coercion
co2
  , Type
ty1 Type -> Type -> Bool
`eqType` Type
ty2
  = String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"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 InScopeSet
_ Coercion
_ Coercion
_ = 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 InScopeSet
is Coercion
orig_co1 Coercion
orig_co2 Coercion
co1a [Coercion]
co1bs Coercion
co2a [Coercion]
co2bs
  | AppCo Coercion
co1aa Coercion
co1ab <- Coercion
co1a
  , Just (Coercion
co2aa, 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 Coercion
co2aa Coercion
co2ab <- Coercion
co2a
  , Just (Coercion
co1aa, 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
  = Bool -> Maybe Coercion -> Maybe Coercion
forall a. HasCallStack => Bool -> a -> a
assert ([Coercion]
co1bs [Coercion] -> [Coercion] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Coercion]
co2bs) (Maybe Coercion -> Maybe Coercion)
-> Maybe Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
    String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule (String
"EtaApps:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Coercion] -> Int
forall a. [a] -> 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 rt1a :: Type
rt1a = Coercion -> Type
coercionRKind Coercion
co1a

        lt2a :: Type
lt2a = Coercion -> Type
coercionLKind Coercion
co2a
        rt2a :: Role
rt2a = Coercion -> Role
coercionRole  Coercion
co2a

        rt1bs :: [Type]
rt1bs = (Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
coercionRKind [Coercion]
co1bs
        lt2bs :: [Type]
lt2bs = (Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
coercionLKind [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 String
_rule Coercion
_co1 Coercion
_co2 Coercion
res
  = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
res

{-
Note [Push transitivity inside axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
opt_trans_rule tries to push transitivity inside axioms to deal with cases like
the following:

    newtype N a = MkN a

    axN :: N a ~R# a

    covar :: a ~R# b
    co1 = axN <a> :: N a ~R# a
    co2 = axN <b> :: N b ~R# b

    co :: a ~R# b
    co = sym co1 ; N covar ; co2

When we are optimising co, we want to notice that the two axiom instantiations
cancel out. This is implemented by rules such as TrPushSymAxR, which transforms
    sym (axN <a>) ; N covar
into
    sym (axN covar)
so that TrPushSymAx can subsequently transform
    sym (axN covar) ; axN <b>
into
    covar
which is much more compact. In some perf test cases this kind of pattern can be
generated repeatedly during simplification, so it is very important we squash it
to stop coercions growing exponentially.  For more details see the paper:

    Evidence normalisation in System FC
    Dimitrios Vytiniotis and Simon Peyton Jones
    RTA'13, 2013
    https://www.microsoft.com/en-us/research/publication/evidence-normalization-system-fc-2/


Note [Push transitivity inside newtype axioms only]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The optimization described in Note [Push transitivity inside axioms] is possible
for both newtype and type family axioms.  However, for type family axioms it is
relatively common to have transitive sequences of axioms instantiations, for
example:

    data Nat = Zero | Suc Nat

    type family Index (n :: Nat) (xs :: [Type]) :: Type where
      Index Zero    (x : xs) = x
      Index (Suc n) (x : xs) = Index n xs

    axIndex :: { forall x::Type. forall xs::[Type]. Index Zero (x : xs) ~ x
               ; forall n::Nat. forall x::Type. forall xs::[Type]. Index (Suc n) (x : xs) ~ Index n xs }

    co :: Index (Suc (Suc Zero)) [a, b, c] ~ c
    co = axIndex[1] <Suc Zero> <a> <[b, c]>
       ; axIndex[1] <Zero> <b> <[c]>
       ; axIndex[0] <c> <[]>

Not only are there no cancellation opportunities here, but calling matchAxiom
repeatedly down the transitive chain is very expensive.  Hence we do not attempt
to push transitivity inside type family axioms.  See #8095, !9210 and related tickets.

This is implemented by opt_trans_rule checking that the axiom is for a newtype
constructor (i.e. not a type family).  Adding these guards substantially
improved performance (reduced bytes allocated by more than 10%) for the tests
CoOpt_Singletons, LargeRecord, T12227, T12545, T13386, T15703, T5030, T8095.

A side benefit is that we do not risk accidentally creating an ill-typed
coercion; see Note [Why call checkAxInstCo during optimisation].

There may exist programs that previously relied on pushing transitivity inside
type family axioms to avoid creating huge coercions, which will regress in
compile time performance as a result of this change.  We do not currently know
of any examples, but if any come to light we may need to reconsider this
behaviour.


Note [Why call checkAxInstCo during optimisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
NB: The following is no longer relevant, because we no longer push transitivity
into type family axioms (Note [Push transitivity inside newtype axioms only]).
It is retained for reference in case we change this behaviour in the future.

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 GHC.Core.TyCo.Rep,
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.

-}

-----------
wrapSym :: SymFlag -> Coercion -> Coercion
wrapSym :: Bool -> Coercion -> Coercion
wrapSym Bool
sym 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 Bool
False Role
_       = Coercion -> Coercion
forall a. a -> a
id
wrapRole Bool
True  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 Bool
True Role
_ = Role
Representational
chooseRole Bool
_    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 Coercion
co)
  | Just (Bool
sym, CoAxiom Branched
con, Int
ind, [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 CoAxiom Branched
con Int
ind [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 Coercion
_ = 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 :: forall (br :: BranchFlag).
Bool -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
matchAxiom Bool
sym ax :: CoAxiom br
ax@(CoAxiom { co_ax_tc :: forall (br :: BranchFlag). CoAxiom br -> TyCon
co_ax_tc = TyCon
tc }) Int
ind Coercion
co
  | CoAxBranch { cab_tvs :: CoAxBranch -> [CoVar]
cab_tvs = [CoVar]
qtvs
               , cab_cvs :: CoAxBranch -> [CoVar]
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 LiftingContext
subst <- UniqSet CoVar -> Type -> Coercion -> Maybe LiftingContext
liftCoMatch ([CoVar] -> UniqSet CoVar
mkVarSet [CoVar]
qtvs)
                              (if Bool
sym then (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
lhs) else Type
rhs)
                              Coercion
co
  , (CoVar -> Bool) -> [CoVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (CoVar -> LiftingContext -> Bool
`isMappedByLC` LiftingContext
subst) [CoVar]
qtvs
  = (Role -> CoVar -> Maybe Coercion)
-> [Role] -> [CoVar] -> Maybe [Coercion]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (LiftingContext -> Role -> CoVar -> Maybe Coercion
liftCoSubstTyVar LiftingContext
subst) [Role]
roles [CoVar]
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 Coercion
co1 Coercion
co2
  = Type
x1 Type -> Type -> Bool
`eqType` Type
x2
  where
    x1 :: Type
x1 = Coercion -> Type
coercionRKind Coercion
co1
    x2 :: Type
x2 = Coercion -> Type
coercionLKind 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   = mkSelCo Nominal 0 g       :: (s1~s2)~(s3~s4)
  eta1 = mkSelCo (SelTyCon 2 r) h1 :: (s1 ~ s3)
  eta2 = mkSelCo (SelTyCon 3 r) 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 (CoVar, Coercion, Coercion)
etaForAllCo_ty_maybe Coercion
co
  | Just (CoVar
tv, Coercion
kind_co, Coercion
r) <- Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_ty_maybe Coercion
co
  = (CoVar, Coercion, Coercion) -> Maybe (CoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just (CoVar
tv, Coercion
kind_co, Coercion
r)

  | Pair Type
ty1 Type
ty2  <- Coercion -> Pair Type
coercionKind Coercion
co
  , Just (CoVar
tv1, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTyVar_maybe Type
ty1
  , Type -> Bool
isForAllTy_ty Type
ty2
  , let kind_co :: Coercion
kind_co = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo CoSel
SelForAll Coercion
co
  = (CoVar, Coercion, Coercion) -> Maybe (CoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just ( CoVar
tv1, Coercion
kind_co
         , Coercion -> Coercion -> Coercion
mkInstCo Coercion
co (Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
Nominal (CoVar -> Type
TyVarTy CoVar
tv1) Coercion
kind_co))

  | Bool
otherwise
  = Maybe (CoVar, 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 (CoVar, Coercion, Coercion)
etaForAllCo_co_maybe Coercion
co
  | Just (CoVar
cv, Coercion
kind_co, Coercion
r) <- Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_co_maybe Coercion
co
  = (CoVar, Coercion, Coercion) -> Maybe (CoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just (CoVar
cv, Coercion
kind_co, Coercion
r)

  | Pair Type
ty1 Type
ty2  <- Coercion -> Pair Type
coercionKind Coercion
co
  , Just (CoVar
cv1, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllCoVar_maybe Type
ty1
  , Type -> Bool
isForAllTy_co Type
ty2
  = let kind_co :: Coercion
kind_co  = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo CoSel
SelForAll Coercion
co
        r :: Role
r        = CoVar -> Role
coVarRole CoVar
cv1
        l_co :: Coercion
l_co     = CoVar -> Coercion
mkCoVarCo CoVar
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 => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Int -> Role -> CoSel
SelTyCon Int
2 Role
r) Coercion
kind_co')
                   Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
l_co
                   Coercion -> Coercion -> Coercion
`mkTransCo` HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo (Int -> Role -> CoSel
SelTyCon Int
3 Role
r) Coercion
kind_co'
    in (CoVar, Coercion, Coercion) -> Maybe (CoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just ( CoVar
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 (CoVar, 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 Coercion
co
  | Just (Coercion
co1,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 Type
ty1 Type
ty2, Role
Nominal) <- Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
  , Just (Type
_,Type
t1) <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ty1
  , Just (Type
_,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 [ SelCo (SelTyCon 0)     g :: s1~t1
--      , ...
--      , SelCo (SelTyCon (n-1)) g :: sn~tn ]
etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
etaTyConAppCo_maybe TyCon
tc (TyConAppCo Role
_ TyCon
tc2 [Coercion]
cos2)
  = Bool -> Maybe [Coercion] -> Maybe [Coercion]
forall a. HasCallStack => Bool -> a -> a
assert (TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2) (Maybe [Coercion] -> Maybe [Coercion])
-> Maybe [Coercion] -> Maybe [Coercion]
forall a b. (a -> b) -> a -> b
$ [Coercion] -> Maybe [Coercion]
forall a. a -> Maybe a
Just [Coercion]
cos2

etaTyConAppCo_maybe TyCon
tc Coercion
co
  | Bool -> Bool
not (TyCon -> Bool
tyConMustBeSaturated TyCon
tc)
  , (Pair Type
ty1 Type
ty2, Role
r) <- Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
  , Just (TyCon
tc1, [Type]
tys1)  <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
  , Just (TyCon
tc2, [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 [SelCo and newtypes] in GHC.Core.TyCo.Rep
  , let n :: Int
n = [Type] -> Int
forall a. [a] -> 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 program
                           -- E.g. T a ~# T a b
                           -- #14607
  = Bool -> Maybe [Coercion] -> Maybe [Coercion]
forall a. HasCallStack => Bool -> a -> a
assert (TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc1) (Maybe [Coercion] -> Maybe [Coercion])
-> Maybe [Coercion] -> Maybe [Coercion]
forall a b. (a -> b) -> a -> b
$
    [Coercion] -> Maybe [Coercion]
forall a. a -> Maybe a
Just (Int -> Coercion -> Infinite Role -> [Coercion]
decomposeCo Int
n Coercion
co (Role -> TyCon -> Infinite 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 -> CoVar -> Coercion -> (LiftingContext, CoVar, Coercion)
optForAllCoBndr LiftingContext
env Bool
sym
  = Bool
-> (Coercion -> Coercion)
-> LiftingContext
-> CoVar
-> Coercion
-> (LiftingContext, CoVar, Coercion)
substForAllCoBndrUsingLC Bool
sym (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
False Role
Nominal) LiftingContext
env