{-# LANGUAGE CPP #-}
module GHC.Core.Coercion.Opt
( optCoercion
, checkAxInstCo
, OptCoercionOpts (..)
)
where
#include "HsVersions.h"
import GHC.Prelude
import GHC.Driver.Ppr
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Subst
import GHC.Core.Coercion
import GHC.Core.Type as Type hiding( substTyVarBndr, substTy )
import GHC.Tc.Utils.TcType ( exactTyCoVarsOfType )
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Data.Pair
import GHC.Data.List.SetOps ( getNth )
import GHC.Core.Unify
import Control.Monad ( zipWithM )
import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Panic
newtype OptCoercionOpts = OptCoercionOpts
{ OptCoercionOpts -> Bool
optCoercionEnabled :: Bool
}
optCoercion :: OptCoercionOpts -> TCvSubst -> Coercion -> NormalCo
optCoercion :: OptCoercionOpts -> TCvSubst -> Coercion -> Coercion
optCoercion OptCoercionOpts
opts TCvSubst
env Coercion
co
| OptCoercionOpts -> Bool
optCoercionEnabled OptCoercionOpts
opts = TCvSubst -> Coercion -> Coercion
optCoercion' TCvSubst
env Coercion
co
| Bool
otherwise = HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo TCvSubst
env Coercion
co
optCoercion' :: TCvSubst -> Coercion -> NormalCo
optCoercion' :: TCvSubst -> Coercion -> Coercion
optCoercion' TCvSubst
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
ASSERT2( substTyUnchecked env in_ty1 `eqType` out_ty1 &&
substTyUnchecked env in_ty2 `eqType` out_ty2 &&
in_role == out_role
, text "optCoercion changed types!"
$$ hang (text "in_co:") 2 (ppr co)
$$ hang (text "in_ty1:") 2 (ppr in_ty1)
$$ hang (text "in_ty2:") 2 (ppr in_ty2)
$$ hang (text "out_co:") 2 (ppr out_co)
$$ hang (text "out_ty1:") 2 (ppr out_ty1)
$$ hang (text "out_ty2:") 2 (ppr out_ty2)
$$ hang (text "subst:") 2 (ppr env) )
Coercion
out_co
| Bool
otherwise = LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
lc Bool
False Coercion
co
where
lc :: LiftingContext
lc = TCvSubst -> LiftingContext
mkSubstLiftingContext TCvSubst
env
type NormalCo = Coercion
type NormalNonIdCo = NormalCo
type SymFlag = Bool
type ReprFlag = Bool
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
opt_co2 :: LiftingContext
-> SymFlag
-> Role
-> 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
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
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
opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
opt_co4_wrap :: LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4
opt_co4 :: LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4 LiftingContext
env Bool
_ Bool
rep Role
r (Refl Type
ty)
= ASSERT2( r == Nominal, text "Expected role:" <+> ppr r $$
text "Found role:" <+> ppr Nominal $$
text "Type:" <+> ppr ty )
HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env Type
ty
opt_co4 LiftingContext
env Bool
_ Bool
rep Role
r (GRefl Role
_r Type
ty MCoercion
MRefl)
= ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
text "Found role:" <+> ppr _r $$
text "Type:" <+> ppr ty )
HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env Type
ty
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (GRefl Role
_r Type
ty (MCo Coercion
co))
= ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
text "Found role:" <+> ppr _r $$
text "Type:" <+> ppr ty )
if Coercion -> Bool
isGReflCo Coercion
co Bool -> Bool -> Bool
|| Coercion -> Bool
isGReflCo Coercion
co'
then HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r' LiftingContext
env Type
ty
else Bool -> Coercion -> Coercion
wrapSym Bool
sym (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r' Type
ty' Coercion
co' (HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r' LiftingContext
env Type
ty)
where
r' :: Role
r' = Bool -> Role -> Role
chooseRole Bool
rep Role
r
ty' :: Type
ty' = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (LiftingContext -> TCvSubst
lcSubstLeft LiftingContext
env) Type
ty
co' :: Coercion
co' = LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4 LiftingContext
env Bool
False Bool
False Role
Nominal Coercion
co
opt_co4 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
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r g :: Coercion
g@(TyConAppCo Role
_r TyCon
tc [Coercion]
cos)
= ASSERT( r == _r )
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]
tyConRolesRepresentational 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) ->
HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc ((Role -> Coercion -> Coercion)
-> [Role] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (LiftingContext -> Bool -> Role -> Coercion -> Coercion
opt_co2 LiftingContext
env Bool
sym)
(TyCon -> [Role]
tyConRolesRepresentational TyCon
tc)
[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
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (FunCo Role
_r Coercion
cow Coercion
co1 Coercion
co2)
= ASSERT( r == _r )
if Bool
rep
then Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
Representational Coercion
cow' Coercion
co1' Coercion
co2'
else Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r 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
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (CoVarCo CoVar
cv)
| Just Coercion
co <- TCvSubst -> CoVar -> Maybe Coercion
lookupCoVar (LiftingContext -> TCvSubst
lcTCvSubst 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
= Role -> Type -> Coercion
mkReflCo (Bool -> Role -> Role
chooseRole Bool
rep Role
r) Type
ty1
| Bool
otherwise
= ASSERT( isCoVar cv1 )
Bool -> Role -> Coercion -> Coercion
wrapRole Bool
rep Role
r (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Bool -> Coercion -> Coercion
wrapSym Bool
sym (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
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 -> WARN( True, text "opt_co: not in scope:"
<+> ppr cv $$ ppr env)
CoVar
cv
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)
= ASSERT( r == coAxiomRole con )
Bool -> Role -> Coercion -> Coercion
wrapRole Bool
rep (CoAxiom Branched -> Role
forall (br :: BranchFlag). CoAxiom br -> Role
coAxiomRole CoAxiom Branched
con) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
Bool -> Coercion -> Coercion
wrapSym Bool
sym (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
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)
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (UnivCo UnivCoProvenance
prov Role
_r Type
t1 Type
t2)
= ASSERT( r == _r )
LiftingContext
-> Bool -> UnivCoProvenance -> Role -> Type -> Type -> Coercion
opt_univ LiftingContext
env Bool
sym UnivCoProvenance
prov (Bool -> Role -> Role
chooseRole Bool
rep Role
r) Type
t1 Type
t2
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (TransCo Coercion
co1 Coercion
co2)
| 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 (NthCo Role
_r Int
n Coercion
co)
| Just (Type
ty, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
, Just (TyCon
_tc, [Type]
args) <- ASSERT( r == _r )
HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
= HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env ([Type]
args [Type] -> Int -> Type
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n)
| Just (Type
ty, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
, Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
, Just (CoVar
tv, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
ty
= HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst (Bool -> Role -> Role
chooseRole Bool
rep Role
r) LiftingContext
env (CoVar -> Type
varType CoVar
tv)
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (NthCo Role
r1 Int
n (TyConAppCo Role
_ TyCon
_ [Coercion]
cos))
= ASSERT( r == r1 )
LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r ([Coercion]
cos [Coercion] -> Int -> Coercion
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n)
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (NthCo Role
r1 Int
n (FunCo Role
_r2 Coercion
w Coercion
co1 Coercion
co2))
= ASSERT( r == r1 )
LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
r (Int -> Coercion -> Coercion -> Coercion -> Coercion
mkNthCoFunCo Int
n Coercion
w Coercion
co1 Coercion
co2)
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (NthCo Role
_r Int
n (ForAllCo CoVar
_ Coercion
eta Coercion
_))
= ASSERT( r == _r )
ASSERT( n == 0 )
LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
Nominal Coercion
eta
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (NthCo Role
_r Int
n Coercion
co)
| Just Coercion
nth_co <- case Coercion
co' of
TyConAppCo Role
_ TyCon
_ [Coercion]
cos -> 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
_ Coercion
w Coercion
co1 Coercion
co2 -> Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Int -> Coercion -> Coercion -> Coercion -> Coercion
mkNthCoFunCo Int
n Coercion
w Coercion
co1 Coercion
co2)
ForAllCo CoVar
_ Coercion
eta Coercion
_ -> Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
eta
Coercion
_ -> 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)
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
$ Role -> Int -> Coercion -> Coercion
NthCo Role
r Int
n Coercion
co'
where
co' :: Coercion
co' = LiftingContext -> Bool -> Coercion -> Coercion
opt_co1 LiftingContext
env Bool
sym Coercion
co
opt_co4 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
= ASSERT( r == Nominal )
LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
rep Role
Nominal (LeftOrRight -> (Coercion, Coercion) -> Coercion
forall {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'
= ASSERT( r == Nominal )
if Bool
rep
then LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap (LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
env) Bool
False Bool
True Role
Nominal (LeftOrRight -> (Coercion, Coercion) -> Coercion
forall {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
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (InstCo Coercion
co1 Coercion
arg)
| 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))
Bool
sym Bool
rep Role
r Coercion
co_body
| 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
| 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'
| 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'
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
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 => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r2 Int
2 Coercion
kind_co'
n2 :: Coercion
n2 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r2 Int
3 Coercion
kind_co'
in Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal (Type -> Coercion
Refl (Coercion -> Type
coercionType Coercion
h1)) Coercion
h1
(Coercion
n1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
h2 Coercion -> Coercion -> Coercion
`mkTransCo` (Coercion -> Coercion
mkSymCo Coercion
n2))
opt_co4 LiftingContext
env Bool
sym Bool
_rep Role
r (KindCo Coercion
co)
= ASSERT( r == Nominal )
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'
opt_co4 LiftingContext
env Bool
sym Bool
_ Role
r (SubCo Coercion
co)
= ASSERT( r == Representational )
LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4_wrap LiftingContext
env Bool
sym Bool
True Role
Nominal Coercion
co
opt_co4 LiftingContext
env Bool
sym Bool
rep Role
r (AxiomRuleCo CoAxiomRule
co [Coercion]
cs)
= ASSERT( r == coaxrRole co )
Bool -> Role -> Coercion -> Coercion
wrapRole Bool
rep Role
r (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
Bool -> Coercion -> Coercion
wrapSym Bool
sym (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo CoAxiomRule
co ((Role -> Coercion -> Coercion)
-> [Role] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (LiftingContext -> Bool -> Role -> Coercion -> Coercion
opt_co2 LiftingContext
env Bool
False) (CoAxiomRule -> [Role]
coaxrAsmpRoles CoAxiomRule
co) [Coercion]
cs)
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
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' = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (LiftingContext -> TCvSubst
lcSubstLeft LiftingContext
env) Type
ty1
ty2' :: Type
ty2' = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (LiftingContext -> TCvSubst
lcSubstRight LiftingContext
env) Type
ty2
opt_univ 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
, [Type] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [Type]
tys1 [Type]
tys2
= let roles :: [Role]
roles = Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc1
arg_cos :: [Coercion]
arg_cos = (Role -> Type -> Type -> Coercion)
-> [Role] -> [Type] -> [Type] -> [Coercion]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
prov') [Role]
roles [Type]
tys1 [Type]
tys2
arg_cos' :: [Coercion]
arg_cos' = (Role -> Coercion -> Coercion)
-> [Role] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (LiftingContext -> Bool -> Bool -> Role -> Coercion -> Coercion
opt_co4 LiftingContext
env Bool
sym Bool
False) [Role]
roles [Coercion]
arg_cos
in
HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc1 [Coercion]
arg_cos'
| 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
= 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
ty2' :: Type
ty2' = HasCallStack => [CoVar] -> [Type] -> Type -> Type
[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
= 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
n_co :: Coercion
n_co = (Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r' Int
2 Coercion
eta_d) Coercion -> Coercion -> Coercion
`mkTransCo`
(CoVar -> Coercion
mkCoVarCo CoVar
cv1) Coercion -> Coercion -> Coercion
`mkTransCo`
(HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r' Int
3 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 = TCvSubst -> Type -> Type
substTyUnchecked (LiftingContext -> TCvSubst
lcSubstLeft LiftingContext
env) Type
oty1
ty2 :: Type
ty2 = TCvSubst -> Type -> Type
substTyUnchecked (LiftingContext -> TCvSubst
lcSubstRight LiftingContext
env) Type
oty2
(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
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
UnivCoProvenance
CorePrepProv -> 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. String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"opt_transList" (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is)
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
| Bool
otherwise = InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans1 InScopeSet
is Coercion
co1 Coercion
co2
opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
opt_trans1 :: InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans1 InScopeSet
is Coercion
co1 Coercion
co2
| Coercion -> Bool
isReflCo Coercion
co2 = Coercion
co1
| Bool
otherwise = InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans2 InScopeSet
is Coercion
co1 Coercion
co2
opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
opt_trans2 :: InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans2 InScopeSet
is (TransCo Coercion
co1a Coercion
co1b) Coercion
co2
= 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
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))
= ASSERT( r1 == r2 )
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)
opt_trans_rule InScopeSet
is in_co1 :: Coercion
in_co1@(NthCo Role
r1 Int
d1 Coercion
co1) in_co2 :: Coercion
in_co2@(NthCo Role
r2 Int
d2 Coercion
co2)
| Int
d1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
d2
, Coercion -> Role
coercionRole Coercion
co1 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Coercion -> Role
coercionRole Coercion
co2
, Coercion
co1 Coercion -> Coercion -> Bool
`compatible_co` Coercion
co2
= ASSERT( r1 == r2 )
String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"PushNth" Coercion
in_co1 Coercion
in_co2 (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$
HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r1 Int
d1 (InScopeSet -> Coercion -> Coercion -> Coercion
opt_trans InScopeSet
is Coercion
co1 Coercion
co2)
opt_trans_rule 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)
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
= ASSERT( r1 == r2 )
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
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
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
= ASSERT( r1 == r2 )
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 Coercion
w1 Coercion
co1a Coercion
co1b) in_co2 :: Coercion
in_co2@(FunCo Role
r2 Coercion
w2 Coercion
co2a Coercion
co2b)
= ASSERT( r1 == r2)
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 -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r1 (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)
= 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]
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]
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
= 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
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
= 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 => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
role Int
2 Coercion
eta1'
n2 :: Coercion
n2 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
role Int
3 Coercion
eta1'
r2' :: Coercion
r2' = HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo ([CoVar] -> [Coercion] -> TCvSubst
HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst
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
opt_trans_rule InScopeSet
is Coercion
co1 Coercion
co2
| Just (Bool
sym, CoAxiom Branched
con, Int
ind, [Coercion]
cos1) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co1_is_axiom_maybe
, 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)
, Maybe CoAxBranch
Nothing <- Coercion -> Maybe CoAxBranch
checkAxInstCo Coercion
newAxInst
= 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
| Just (Bool
sym, CoAxiom Branched
con, Int
ind, [Coercion]
cos1) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co1_is_axiom_maybe
, 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)
, Maybe CoAxBranch
Nothing <- Coercion -> Maybe CoAxBranch
checkAxInstCo Coercion
newAxInst
= String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"TrPushAxR" Coercion
co1 Coercion
co2 Coercion
newAxInst
| Just (Bool
sym, CoAxiom Branched
con, Int
ind, [Coercion]
cos2) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co2_is_axiom_maybe
, 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))
, Maybe CoAxBranch
Nothing <- Coercion -> Maybe CoAxBranch
checkAxInstCo Coercion
newAxInst
= 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
| Just (Bool
sym, CoAxiom Branched
con, Int
ind, [Coercion]
cos2) <- Maybe (Bool, CoAxiom Branched, Int, [Coercion])
co2_is_axiom_maybe
, 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)
, Maybe CoAxBranch
Nothing <- Coercion -> Maybe CoAxBranch
checkAxInstCo Coercion
newAxInst
= String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule String
"TrPushAxL" Coercion
co1 Coercion
co2 Coercion
newAxInst
| 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 :: TyCoVarSet
pivot_tvs = Type -> TyCoVarSet
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 -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
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
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
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
opt_trans_rule InScopeSet
_ Coercion
co1 Coercion
co2
| 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
opt_trans_rule_app :: InScopeSet
-> Coercion
-> Coercion
-> Coercion
-> [Coercion]
-> Coercion
-> [Coercion]
-> 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
= ASSERT( co1bs `equalLength` co2bs )
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 (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
checkAxInstCo :: Coercion -> Maybe CoAxBranch
checkAxInstCo :: Coercion -> Maybe CoAxBranch
checkAxInstCo (AxiomInstCo CoAxiom Branched
ax Int
ind [Coercion]
cos)
= let branch :: CoAxBranch
branch = CoAxiom Branched -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom Branched
ax Int
ind
tvs :: [CoVar]
tvs = CoAxBranch -> [CoVar]
coAxBranchTyVars CoAxBranch
branch
cvs :: [CoVar]
cvs = CoAxBranch -> [CoVar]
coAxBranchCoVars CoAxBranch
branch
incomps :: [CoAxBranch]
incomps = CoAxBranch -> [CoAxBranch]
coAxBranchIncomps CoAxBranch
branch
([Type]
tys, [Type]
cotys) = [CoVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs ((Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
coercionLKind [Coercion]
cos)
co_args :: [Coercion]
co_args = (Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
stripCoercionTy [Type]
cotys
subst :: TCvSubst
subst = [CoVar] -> [Type] -> TCvSubst
HasDebugCallStack => [CoVar] -> [Type] -> TCvSubst
zipTvSubst [CoVar]
tvs [Type]
tys TCvSubst -> TCvSubst -> TCvSubst
`composeTCvSubst`
[CoVar] -> [Coercion] -> TCvSubst
HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst
zipCvSubst [CoVar]
cvs [Coercion]
co_args
target :: [Type]
target = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst (CoAxBranch -> [Type]
coAxBranchLHS CoAxBranch
branch)
in_scope :: InScopeSet
in_scope = TyCoVarSet -> InScopeSet
mkInScopeSet (TyCoVarSet -> InScopeSet) -> TyCoVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
[TyCoVarSet] -> TyCoVarSet
unionVarSets ((CoAxBranch -> TyCoVarSet) -> [CoAxBranch] -> [TyCoVarSet]
forall a b. (a -> b) -> [a] -> [b]
map ([Type] -> TyCoVarSet
tyCoVarsOfTypes ([Type] -> TyCoVarSet)
-> (CoAxBranch -> [Type]) -> CoAxBranch -> TyCoVarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxBranch -> [Type]
coAxBranchLHS) [CoAxBranch]
incomps)
flattened_target :: [Type]
flattened_target = InScopeSet -> [Type] -> [Type]
flattenTys InScopeSet
in_scope [Type]
target in
[Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict [Type]
flattened_target [CoAxBranch]
incomps
where
check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict [Type]
_ [] = Maybe CoAxBranch
forall a. Maybe a
Nothing
check_no_conflict [Type]
flat (b :: CoAxBranch
b@CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs_incomp } : [CoAxBranch]
rest)
| UnifyResultM TCvSubst
SurelyApart <- BindFun -> [Type] -> [Type] -> UnifyResultM TCvSubst
tcUnifyTysFG BindFun
alwaysBindFun [Type]
flat [Type]
lhs_incomp
= [Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict [Type]
flat [CoAxBranch]
rest
| Bool
otherwise
= CoAxBranch -> Maybe CoAxBranch
forall a. a -> Maybe a
Just CoAxBranch
b
checkAxInstCo Coercion
_ = Maybe CoAxBranch
forall a. Maybe a
Nothing
wrapSym :: SymFlag -> Coercion -> Coercion
wrapSym :: Bool -> Coercion -> Coercion
wrapSym Bool
sym Coercion
co | Bool
sym = Coercion -> Coercion
mkSymCo Coercion
co
| Bool
otherwise = Coercion
co
wrapRole :: ReprFlag
-> 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
chooseRole :: ReprFlag
-> 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
-> 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 = []
, 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 <- TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
liftCoMatch ([CoVar] -> TyCoVarSet
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
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_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
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 => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal Int
0 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)
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 => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal Int
0 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 => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
2 Coercion
kind_co')) Coercion -> Coercion -> Coercion
`mkTransCo`
Coercion
l_co Coercion -> Coercion -> Coercion
`mkTransCo`
(HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
3 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)
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]
etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
etaTyConAppCo_maybe TyCon
tc (TyConAppCo Role
_ TyCon
tc2 [Coercion]
cos2)
= ASSERT( tc == tc2 ) Just cos2
etaTyConAppCo_maybe TyCon
tc Coercion
co
| Bool -> Bool
not (TyCon -> Bool
mustBeSaturated 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
, let n :: Int
n = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys1
, [Type]
tys2 [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` Int
n
= ASSERT( tc == tc1 )
[Coercion] -> Maybe [Coercion]
forall a. a -> Maybe a
Just (Int -> Coercion -> [Role] -> [Coercion]
decomposeCo Int
n Coercion
co (Role -> TyCon -> [Role]
tyConRolesX Role
r TyCon
tc1))
| Bool
otherwise
= Maybe [Coercion]
forall a. Maybe a
Nothing
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