{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
module GHC.Core.FamInstEnv (
FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
pprFamInst, pprFamInsts,
mkImportedFamInst,
FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
unionFamInstEnv, extendFamInstEnv, extendFamInstEnvList,
famInstEnvElts, famInstEnvSize, familyInstances, familyNameInstances,
mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
mkNewTypeCoAxiom,
FamInstMatch(..),
lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
isDominatedBy, apartnessCheck, compatibleBranches,
InjectivityCheckResult(..),
lookupFamInstEnvInjectivityConflicts, injectiveBranches,
topNormaliseType, topNormaliseType_maybe,
normaliseType, normaliseTcApp,
topReduceTyFamApp_maybe, reduceTyFamApp_maybe
) where
import GHC.Prelude
import GHC.Core.Unify
import GHC.Core.Type as Type
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom
import GHC.Core.Reduction
import GHC.Core.RoughMap
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.Name
import GHC.Data.Maybe
import GHC.Types.Var
import GHC.Types.SrcLoc
import Control.Monad
import Data.List( mapAccumL )
import Data.Array( Array, assocs )
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Data.Bag
data FamInst
= FamInst { FamInst -> CoAxiom Unbranched
fi_axiom :: CoAxiom Unbranched
, FamInst -> FamFlavor
fi_flavor :: FamFlavor
, FamInst -> Name
fi_fam :: Name
, FamInst -> [RoughMatchTc]
fi_tcs :: [RoughMatchTc]
, FamInst -> [TyVar]
fi_tvs :: [TyVar]
, FamInst -> [TyVar]
fi_cvs :: [CoVar]
, FamInst -> [Type]
fi_tys :: [Type]
, FamInst -> Type
fi_rhs :: Type
}
data FamFlavor
= SynFamilyInst
| DataFamilyInst TyCon
famInstAxiom :: FamInst -> CoAxiom Unbranched
famInstAxiom :: FamInst -> CoAxiom Unbranched
famInstAxiom = FamInst -> CoAxiom Unbranched
fi_axiom
famInstSplitLHS :: FamInst -> (TyCon, [Type])
famInstSplitLHS :: FamInst -> (TyCon, [Type])
famInstSplitLHS (FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
axiom, fi_tys :: FamInst -> [Type]
fi_tys = [Type]
lhs })
= (CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Unbranched
axiom, [Type]
lhs)
famInstRHS :: FamInst -> Type
famInstRHS :: FamInst -> Type
famInstRHS = FamInst -> Type
fi_rhs
famInstTyCon :: FamInst -> TyCon
famInstTyCon :: FamInst -> TyCon
famInstTyCon = CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon (CoAxiom Unbranched -> TyCon)
-> (FamInst -> CoAxiom Unbranched) -> FamInst -> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> CoAxiom Unbranched
famInstAxiom
famInstsRepTyCons :: [FamInst] -> [TyCon]
famInstsRepTyCons :: [FamInst] -> [TyCon]
famInstsRepTyCons [FamInst]
fis = [TyCon
tc | FamInst { fi_flavor :: FamInst -> FamFlavor
fi_flavor = DataFamilyInst TyCon
tc } <- [FamInst]
fis]
famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
famInstRepTyCon_maybe FamInst
fi
= case FamInst -> FamFlavor
fi_flavor FamInst
fi of
DataFamilyInst TyCon
tycon -> TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
tycon
FamFlavor
SynFamilyInst -> Maybe TyCon
forall a. Maybe a
Nothing
dataFamInstRepTyCon :: FamInst -> TyCon
dataFamInstRepTyCon :: FamInst -> TyCon
dataFamInstRepTyCon FamInst
fi
= case FamInst -> FamFlavor
fi_flavor FamInst
fi of
DataFamilyInst TyCon
tycon -> TyCon
tycon
FamFlavor
SynFamilyInst -> String -> SDoc -> TyCon
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"dataFamInstRepTyCon" (FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr FamInst
fi)
instance NamedThing FamInst where
getName :: FamInst -> Name
getName = CoAxiom Unbranched -> Name
forall (br :: BranchFlag). CoAxiom br -> Name
coAxiomName (CoAxiom Unbranched -> Name)
-> (FamInst -> CoAxiom Unbranched) -> FamInst -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> CoAxiom Unbranched
fi_axiom
instance Outputable FamInst where
ppr :: FamInst -> SDoc
ppr = FamInst -> SDoc
pprFamInst
pprFamInst :: FamInst -> SDoc
pprFamInst :: FamInst -> SDoc
pprFamInst (FamInst { fi_flavor :: FamInst -> FamFlavor
fi_flavor = FamFlavor
flavor, fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
ax
, fi_tvs :: FamInst -> [TyVar]
fi_tvs = [TyVar]
tvs, fi_tys :: FamInst -> [Type]
fi_tys = [Type]
tys, fi_rhs :: FamInst -> Type
fi_rhs = Type
rhs })
= SDoc -> BranchIndex -> SDoc -> SDoc
hang (SDoc
ppr_tc_sort SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"instance"
SDoc -> SDoc -> SDoc
<+> TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser (CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Unbranched
ax) (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
ax))
BranchIndex
2 (SDoc -> SDoc
whenPprDebug SDoc
debug_stuff)
where
ppr_tc_sort :: SDoc
ppr_tc_sort = case FamFlavor
flavor of
FamFlavor
SynFamilyInst -> String -> SDoc
text String
"type"
DataFamilyInst TyCon
tycon
| TyCon -> Bool
isDataTyCon TyCon
tycon -> String -> SDoc
text String
"data"
| TyCon -> Bool
isNewTyCon TyCon
tycon -> String -> SDoc
text String
"newtype"
| TyCon -> Bool
isAbstractTyCon TyCon
tycon -> String -> SDoc
text String
"data"
| Bool
otherwise -> String -> SDoc
text String
"WEIRD" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tycon
debug_stuff :: SDoc
debug_stuff = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Coercion axiom:" SDoc -> SDoc -> SDoc
<+> CoAxiom Unbranched -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoAxiom Unbranched
ax
, String -> SDoc
text String
"Tvs:" SDoc -> SDoc -> SDoc
<+> [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs
, String -> SDoc
text String
"LHS:" SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
, String -> SDoc
text String
"RHS:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs ]
pprFamInsts :: [FamInst] -> SDoc
pprFamInsts :: [FamInst] -> SDoc
pprFamInsts [FamInst]
finsts = [SDoc] -> SDoc
vcat ((FamInst -> SDoc) -> [FamInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map FamInst -> SDoc
pprFamInst [FamInst]
finsts)
mkImportedFamInst :: Name
-> [RoughMatchTc]
-> CoAxiom Unbranched
-> FamInst
mkImportedFamInst :: Name -> [RoughMatchTc] -> CoAxiom Unbranched -> FamInst
mkImportedFamInst Name
fam [RoughMatchTc]
mb_tcs CoAxiom Unbranched
axiom
= FamInst {
fi_fam :: Name
fi_fam = Name
fam,
fi_tcs :: [RoughMatchTc]
fi_tcs = [RoughMatchTc]
mb_tcs,
fi_tvs :: [TyVar]
fi_tvs = [TyVar]
tvs,
fi_cvs :: [TyVar]
fi_cvs = [TyVar]
cvs,
fi_tys :: [Type]
fi_tys = [Type]
tys,
fi_rhs :: Type
fi_rhs = Type
rhs,
fi_axiom :: CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
axiom,
fi_flavor :: FamFlavor
fi_flavor = FamFlavor
flavor }
where
~(CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
tys
, cab_tvs :: CoAxBranch -> [TyVar]
cab_tvs = [TyVar]
tvs
, cab_cvs :: CoAxBranch -> [TyVar]
cab_cvs = [TyVar]
cvs
, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs }) = CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
axiom
flavor :: FamFlavor
flavor = case (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
rhs of
Just (TyCon
tc, [Type]
_)
| Just CoAxiom Unbranched
ax' <- TyCon -> Maybe (CoAxiom Unbranched)
tyConFamilyCoercion_maybe TyCon
tc
, CoAxiom Unbranched
ax' CoAxiom Unbranched -> CoAxiom Unbranched -> Bool
forall a. Eq a => a -> a -> Bool
== CoAxiom Unbranched
axiom
-> TyCon -> FamFlavor
DataFamilyInst TyCon
tc
Maybe (TyCon, [Type])
_ -> FamFlavor
SynFamilyInst
type FamInstEnvs = (FamInstEnv, FamInstEnv)
data FamInstEnv
= FamIE !Int
!(RoughMap FamInst)
instance Outputable FamInstEnv where
ppr :: FamInstEnv -> SDoc
ppr (FamIE BranchIndex
_ RoughMap FamInst
fs) = String -> SDoc
text String
"FamIE" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((FamInst -> SDoc) -> [FamInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([FamInst] -> [SDoc]) -> [FamInst] -> [SDoc]
forall a b. (a -> b) -> a -> b
$ RoughMap FamInst -> [FamInst]
forall a. RoughMap a -> [a]
elemsRM RoughMap FamInst
fs)
famInstEnvSize :: FamInstEnv -> Int
famInstEnvSize :: FamInstEnv -> BranchIndex
famInstEnvSize (FamIE BranchIndex
sz RoughMap FamInst
_) = BranchIndex
sz
emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
emptyFamInstEnvs = (FamInstEnv
emptyFamInstEnv, FamInstEnv
emptyFamInstEnv)
emptyFamInstEnv :: FamInstEnv
emptyFamInstEnv :: FamInstEnv
emptyFamInstEnv = BranchIndex -> RoughMap FamInst -> FamInstEnv
FamIE BranchIndex
0 RoughMap FamInst
forall a. RoughMap a
emptyRM
famInstEnvElts :: FamInstEnv -> [FamInst]
famInstEnvElts :: FamInstEnv -> [FamInst]
famInstEnvElts (FamIE BranchIndex
_ RoughMap FamInst
rm) = RoughMap FamInst -> [FamInst]
forall a. RoughMap a -> [a]
elemsRM RoughMap FamInst
rm
familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
familyInstances (FamInstEnv, FamInstEnv)
envs TyCon
tc
= (FamInstEnv, FamInstEnv) -> Name -> [FamInst]
familyNameInstances (FamInstEnv, FamInstEnv)
envs (TyCon -> Name
tyConName TyCon
tc)
familyNameInstances :: (FamInstEnv, FamInstEnv) -> Name -> [FamInst]
familyNameInstances :: (FamInstEnv, FamInstEnv) -> Name -> [FamInst]
familyNameInstances (FamInstEnv
pkg_fie, FamInstEnv
home_fie) Name
fam
= FamInstEnv -> [FamInst]
get FamInstEnv
home_fie [FamInst] -> [FamInst] -> [FamInst]
forall a. [a] -> [a] -> [a]
++ FamInstEnv -> [FamInst]
get FamInstEnv
pkg_fie
where
get :: FamInstEnv -> [FamInst]
get :: FamInstEnv -> [FamInst]
get (FamIE BranchIndex
_ RoughMap FamInst
env) = [RoughMatchLookupTc] -> RoughMap FamInst -> [FamInst]
forall a. [RoughMatchLookupTc] -> RoughMap a -> [a]
lookupRM [Name -> RoughMatchLookupTc
RML_KnownTc Name
fam] RoughMap FamInst
env
unionFamInstEnv :: FamInstEnv -> FamInstEnv -> FamInstEnv
unionFamInstEnv :: FamInstEnv -> FamInstEnv -> FamInstEnv
unionFamInstEnv (FamIE BranchIndex
sa RoughMap FamInst
a) (FamIE BranchIndex
sb RoughMap FamInst
b) = BranchIndex -> RoughMap FamInst -> FamInstEnv
FamIE (BranchIndex
sa BranchIndex -> BranchIndex -> BranchIndex
forall a. Num a => a -> a -> a
+ BranchIndex
sb) (RoughMap FamInst
a RoughMap FamInst -> RoughMap FamInst -> RoughMap FamInst
forall a. RoughMap a -> RoughMap a -> RoughMap a
`unionRM` RoughMap FamInst
b)
extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
extendFamInstEnvList FamInstEnv
inst_env [FamInst]
fis = (FamInstEnv -> FamInst -> FamInstEnv)
-> FamInstEnv -> [FamInst] -> FamInstEnv
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnv FamInstEnv
inst_env [FamInst]
fis
extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnv (FamIE BranchIndex
s RoughMap FamInst
inst_env)
ins_item :: FamInst
ins_item@(FamInst {fi_fam :: FamInst -> Name
fi_fam = Name
cls_nm})
= BranchIndex -> RoughMap FamInst -> FamInstEnv
FamIE (BranchIndex
sBranchIndex -> BranchIndex -> BranchIndex
forall a. Num a => a -> a -> a
+BranchIndex
1) (RoughMap FamInst -> FamInstEnv) -> RoughMap FamInst -> FamInstEnv
forall a b. (a -> b) -> a -> b
$ [RoughMatchTc] -> FamInst -> RoughMap FamInst -> RoughMap FamInst
forall a. [RoughMatchTc] -> a -> RoughMap a -> RoughMap a
insertRM [RoughMatchTc]
rough_tmpl FamInst
ins_item RoughMap FamInst
inst_env
where
rough_tmpl :: [RoughMatchTc]
rough_tmpl = Name -> RoughMatchTc
RM_KnownTc Name
cls_nm RoughMatchTc -> [RoughMatchTc] -> [RoughMatchTc]
forall a. a -> [a] -> [a]
: FamInst -> [RoughMatchTc]
fi_tcs FamInst
ins_item
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
compatibleBranches (CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs1, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs1 })
(CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs2, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs2 })
= case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
alwaysBindFun [Type]
commonlhs1 [Type]
commonlhs2 of
UnifyResult
SurelyApart -> Bool
True
MaybeApart {} -> Bool
False
Unifiable TCvSubst
subst -> TCvSubst -> Type -> Type
Type.substTyAddInScope TCvSubst
subst Type
rhs1 Type -> Type -> Bool
`eqType`
TCvSubst -> Type -> Type
Type.substTyAddInScope TCvSubst
subst Type
rhs2
where
([Type]
commonlhs1, [Type]
commonlhs2) = [Type] -> [Type] -> ([Type], [Type])
forall a b. [a] -> [b] -> ([a], [b])
zipAndUnzip [Type]
lhs1 [Type]
lhs2
data InjectivityCheckResult
= InjectivityAccepted
| InjectivityUnified CoAxBranch CoAxBranch
injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch
-> InjectivityCheckResult
injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult
injectiveBranches [Bool]
injectivity
ax1 :: CoAxBranch
ax1@(CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs1, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs1 })
ax2 :: CoAxBranch
ax2@(CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs2, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs2 })
= let getInjArgs :: [Type] -> [Type]
getInjArgs = [Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList [Bool]
injectivity
in case Bool -> Type -> Type -> Maybe TCvSubst
tcUnifyTyWithTFs Bool
True Type
rhs1 Type
rhs2 of
Maybe TCvSubst
Nothing -> InjectivityCheckResult
InjectivityAccepted
Just TCvSubst
subst ->
let lhs1Subst :: [Type]
lhs1Subst = (() :: Constraint) => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst ([Type] -> [Type]
getInjArgs [Type]
lhs1)
lhs2Subst :: [Type]
lhs2Subst = (() :: Constraint) => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst ([Type] -> [Type]
getInjArgs [Type]
lhs2)
in if [Type] -> [Type] -> Bool
eqTypes [Type]
lhs1Subst [Type]
lhs2Subst
then InjectivityCheckResult
InjectivityAccepted
else CoAxBranch -> CoAxBranch -> InjectivityCheckResult
InjectivityUnified ( CoAxBranch
ax1 { cab_lhs :: [Type]
cab_lhs = (() :: Constraint) => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst [Type]
lhs1
, cab_rhs :: Type
cab_rhs = (() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
Type.substTy TCvSubst
subst Type
rhs1 })
( CoAxBranch
ax2 { cab_lhs :: [Type]
cab_lhs = (() :: Constraint) => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
Type.substTys TCvSubst
subst [Type]
lhs2
, cab_rhs :: Type
cab_rhs = (() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
Type.substTy TCvSubst
subst Type
rhs2 })
computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
computeAxiomIncomps [CoAxBranch]
branches
= ([CoAxBranch], [CoAxBranch]) -> [CoAxBranch]
forall a b. (a, b) -> b
snd (([CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch))
-> [CoAxBranch] -> [CoAxBranch] -> ([CoAxBranch], [CoAxBranch])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
go [] [CoAxBranch]
branches)
where
go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
go [CoAxBranch]
prev_brs CoAxBranch
cur_br
= (CoAxBranch
new_br CoAxBranch -> [CoAxBranch] -> [CoAxBranch]
forall a. a -> [a] -> [a]
: [CoAxBranch]
prev_brs, CoAxBranch
new_br)
where
new_br :: CoAxBranch
new_br = CoAxBranch
cur_br { cab_incomps :: [CoAxBranch]
cab_incomps = [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
mk_incomps [CoAxBranch]
prev_brs CoAxBranch
cur_br }
mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
mk_incomps [CoAxBranch]
prev_brs CoAxBranch
cur_br
= (CoAxBranch -> Bool) -> [CoAxBranch] -> [CoAxBranch]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (CoAxBranch -> Bool) -> CoAxBranch -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxBranch -> CoAxBranch -> Bool
compatibleBranches CoAxBranch
cur_br) [CoAxBranch]
prev_brs
mkCoAxBranch :: [TyVar]
-> [TyVar]
-> [CoVar]
-> [Type]
-> Type
-> [Role]
-> SrcSpan
-> CoAxBranch
mkCoAxBranch :: [TyVar]
-> [TyVar]
-> [TyVar]
-> [Type]
-> Type
-> [Role]
-> SrcSpan
-> CoAxBranch
mkCoAxBranch [TyVar]
tvs [TyVar]
eta_tvs [TyVar]
cvs [Type]
lhs Type
rhs [Role]
roles SrcSpan
loc
= CoAxBranch { cab_tvs :: [TyVar]
cab_tvs = [TyVar]
tvs'
, cab_eta_tvs :: [TyVar]
cab_eta_tvs = [TyVar]
eta_tvs'
, cab_cvs :: [TyVar]
cab_cvs = [TyVar]
cvs'
, cab_lhs :: [Type]
cab_lhs = TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
lhs
, cab_roles :: [Role]
cab_roles = [Role]
roles
, cab_rhs :: Type
cab_rhs = TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
rhs
, cab_loc :: SrcSpan
cab_loc = SrcSpan
loc
, cab_incomps :: [CoAxBranch]
cab_incomps = [CoAxBranch]
placeHolderIncomps }
where
(TidyEnv
env1, [TyVar]
tvs') = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyVarBndrs TidyEnv
init_tidy_env [TyVar]
tvs
(TidyEnv
env2, [TyVar]
eta_tvs') = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyVarBndrs TidyEnv
env1 [TyVar]
eta_tvs
(TidyEnv
env, [TyVar]
cvs') = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyVarBndrs TidyEnv
env2 [TyVar]
cvs
init_occ_env :: TidyOccEnv
init_occ_env = [OccName] -> TidyOccEnv
initTidyOccEnv [String -> OccName
mkTyVarOcc String
"_"]
init_tidy_env :: TidyEnv
init_tidy_env = TidyOccEnv -> TidyEnv
mkEmptyTidyEnv TidyOccEnv
init_occ_env
mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
mkBranchedCoAxiom Name
ax_name TyCon
fam_tc [CoAxBranch]
branches
= CoAxiom { co_ax_unique :: Unique
co_ax_unique = Name -> Unique
nameUnique Name
ax_name
, co_ax_name :: Name
co_ax_name = Name
ax_name
, co_ax_tc :: TyCon
co_ax_tc = TyCon
fam_tc
, co_ax_role :: Role
co_ax_role = Role
Nominal
, co_ax_implicit :: Bool
co_ax_implicit = Bool
False
, co_ax_branches :: Branches Branched
co_ax_branches = [CoAxBranch] -> Branches Branched
manyBranches ([CoAxBranch] -> [CoAxBranch]
computeAxiomIncomps [CoAxBranch]
branches) }
mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
mkUnbranchedCoAxiom Name
ax_name TyCon
fam_tc CoAxBranch
branch
= CoAxiom { co_ax_unique :: Unique
co_ax_unique = Name -> Unique
nameUnique Name
ax_name
, co_ax_name :: Name
co_ax_name = Name
ax_name
, co_ax_tc :: TyCon
co_ax_tc = TyCon
fam_tc
, co_ax_role :: Role
co_ax_role = Role
Nominal
, co_ax_implicit :: Bool
co_ax_implicit = Bool
False
, co_ax_branches :: Branches Unbranched
co_ax_branches = CoAxBranch -> Branches Unbranched
unbranched (CoAxBranch
branch { cab_incomps :: [CoAxBranch]
cab_incomps = [] }) }
mkSingleCoAxiom :: Role -> Name
-> [TyVar] -> [TyVar] -> [CoVar]
-> TyCon -> [Type] -> Type
-> CoAxiom Unbranched
mkSingleCoAxiom :: Role
-> Name
-> [TyVar]
-> [TyVar]
-> [TyVar]
-> TyCon
-> [Type]
-> Type
-> CoAxiom Unbranched
mkSingleCoAxiom Role
role Name
ax_name [TyVar]
tvs [TyVar]
eta_tvs [TyVar]
cvs TyCon
fam_tc [Type]
lhs_tys Type
rhs_ty
= CoAxiom { co_ax_unique :: Unique
co_ax_unique = Name -> Unique
nameUnique Name
ax_name
, co_ax_name :: Name
co_ax_name = Name
ax_name
, co_ax_tc :: TyCon
co_ax_tc = TyCon
fam_tc
, co_ax_role :: Role
co_ax_role = Role
role
, co_ax_implicit :: Bool
co_ax_implicit = Bool
False
, co_ax_branches :: Branches Unbranched
co_ax_branches = CoAxBranch -> Branches Unbranched
unbranched (CoAxBranch
branch { cab_incomps :: [CoAxBranch]
cab_incomps = [] }) }
where
branch :: CoAxBranch
branch = [TyVar]
-> [TyVar]
-> [TyVar]
-> [Type]
-> Type
-> [Role]
-> SrcSpan
-> CoAxBranch
mkCoAxBranch [TyVar]
tvs [TyVar]
eta_tvs [TyVar]
cvs [Type]
lhs_tys Type
rhs_ty
((TyVar -> Role) -> [TyVar] -> [Role]
forall a b. (a -> b) -> [a] -> [b]
map (Role -> TyVar -> Role
forall a b. a -> b -> a
const Role
Nominal) [TyVar]
tvs)
(Name -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Name
ax_name)
mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
mkNewTypeCoAxiom Name
name TyCon
tycon [TyVar]
tvs [Role]
roles Type
rhs_ty
= CoAxiom { co_ax_unique :: Unique
co_ax_unique = Name -> Unique
nameUnique Name
name
, co_ax_name :: Name
co_ax_name = Name
name
, co_ax_implicit :: Bool
co_ax_implicit = Bool
True
, co_ax_role :: Role
co_ax_role = Role
Representational
, co_ax_tc :: TyCon
co_ax_tc = TyCon
tycon
, co_ax_branches :: Branches Unbranched
co_ax_branches = CoAxBranch -> Branches Unbranched
unbranched (CoAxBranch
branch { cab_incomps :: [CoAxBranch]
cab_incomps = [] }) }
where
branch :: CoAxBranch
branch = [TyVar]
-> [TyVar]
-> [TyVar]
-> [Type]
-> Type
-> [Role]
-> SrcSpan
-> CoAxBranch
mkCoAxBranch [TyVar]
tvs [] [] ([TyVar] -> [Type]
mkTyVarTys [TyVar]
tvs) Type
rhs_ty
[Role]
roles (Name -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Name
name)
data FamInstMatch = FamInstMatch { FamInstMatch -> FamInst
fim_instance :: FamInst
, FamInstMatch -> [Type]
fim_tys :: [Type]
, FamInstMatch -> [Coercion]
fim_cos :: [Coercion]
}
instance Outputable FamInstMatch where
ppr :: FamInstMatch -> SDoc
ppr (FamInstMatch { fim_instance :: FamInstMatch -> FamInst
fim_instance = FamInst
inst
, fim_tys :: FamInstMatch -> [Type]
fim_tys = [Type]
tys
, fim_cos :: FamInstMatch -> [Coercion]
fim_cos = [Coercion]
cos })
= String -> SDoc
text String
"match with" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr FamInst
inst) SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
<+> [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
cos
lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
lookupFamInstEnvByTyCon :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
lookupFamInstEnvByTyCon (FamInstEnv
pkg_ie, FamInstEnv
home_ie) TyCon
fam_tc
= FamInstEnv -> [FamInst]
get FamInstEnv
pkg_ie [FamInst] -> [FamInst] -> [FamInst]
forall a. [a] -> [a] -> [a]
++ FamInstEnv -> [FamInst]
get FamInstEnv
home_ie
where
get :: FamInstEnv -> [FamInst]
get (FamIE BranchIndex
_ RoughMap FamInst
rm) = [RoughMatchLookupTc] -> RoughMap FamInst -> [FamInst]
forall a. [RoughMatchLookupTc] -> RoughMap a -> [a]
lookupRM [Name -> RoughMatchLookupTc
RML_KnownTc (TyCon -> Name
tyConName TyCon
fam_tc)] RoughMap FamInst
rm
lookupFamInstEnv
:: FamInstEnvs
-> TyCon -> [Type]
-> [FamInstMatch]
lookupFamInstEnv :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch]
lookupFamInstEnv
= FamInstLookupMode FamInstMatch
-> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch]
forall a.
FamInstLookupMode a
-> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [a]
lookup_fam_inst_env FamInstLookupMode FamInstMatch
WantMatches
lookupFamInstEnvConflicts
:: FamInstEnvs
-> FamInst
-> [FamInst]
lookupFamInstEnvConflicts :: (FamInstEnv, FamInstEnv) -> FamInst -> [FamInst]
lookupFamInstEnvConflicts (FamInstEnv, FamInstEnv)
envs FamInst
fam_inst
= FamInstLookupMode FamInst
-> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInst]
forall a.
FamInstLookupMode a
-> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [a]
lookup_fam_inst_env (FamInst -> FamInstLookupMode FamInst
WantConflicts FamInst
fam_inst) (FamInstEnv, FamInstEnv)
envs TyCon
fam [Type]
tys
where
(TyCon
fam, [Type]
tys) = FamInst -> (TyCon, [Type])
famInstSplitLHS FamInst
fam_inst
lookupFamInstEnvInjectivityConflicts
:: [Bool]
-> FamInstEnvs
-> FamInst
-> [CoAxBranch]
lookupFamInstEnvInjectivityConflicts :: [Bool] -> (FamInstEnv, FamInstEnv) -> FamInst -> [CoAxBranch]
lookupFamInstEnvInjectivityConflicts [Bool]
injList (FamInstEnv, FamInstEnv)
fam_inst_envs
fam_inst :: FamInst
fam_inst@(FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
new_axiom })
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon -> Bool
isOpenFamilyTyCon TyCon
fam
= []
| Bool
otherwise
= (FamInst -> CoAxBranch) -> [FamInst] -> [CoAxBranch]
forall a b. (a -> b) -> [a] -> [b]
map (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch (CoAxiom Unbranched -> CoAxBranch)
-> (FamInst -> CoAxiom Unbranched) -> FamInst -> CoAxBranch
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> CoAxiom Unbranched
fi_axiom) ([FamInst] -> [CoAxBranch]) -> [FamInst] -> [CoAxBranch]
forall a b. (a -> b) -> a -> b
$
(FamInst -> Bool) -> [FamInst] -> [FamInst]
forall a. (a -> Bool) -> [a] -> [a]
filter FamInst -> Bool
isInjConflict ([FamInst] -> [FamInst]) -> [FamInst] -> [FamInst]
forall a b. (a -> b) -> a -> b
$
(FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
familyInstances (FamInstEnv, FamInstEnv)
fam_inst_envs TyCon
fam
where
fam :: TyCon
fam = FamInst -> TyCon
famInstTyCon FamInst
fam_inst
new_branch :: CoAxBranch
new_branch = CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
new_axiom
isInjConflict :: FamInst -> Bool
isInjConflict (FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
old_axiom })
| InjectivityCheckResult
InjectivityAccepted <-
[Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult
injectiveBranches [Bool]
injList (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
old_axiom) CoAxBranch
new_branch
= Bool
False
| Bool
otherwise = Bool
True
data FamInstLookupMode a where
WantConflicts :: FamInst -> FamInstLookupMode FamInst
WantMatches :: FamInstLookupMode FamInstMatch
lookup_fam_inst_env'
:: forall a . FamInstLookupMode a
-> FamInstEnv
-> TyCon -> [Type]
-> [a]
lookup_fam_inst_env' :: forall a.
FamInstLookupMode a -> FamInstEnv -> TyCon -> [Type] -> [a]
lookup_fam_inst_env' FamInstLookupMode a
lookup_mode (FamIE BranchIndex
_ RoughMap FamInst
ie) TyCon
fam [Type]
match_tys
| TyCon -> Bool
isOpenFamilyTyCon TyCon
fam
, let xs :: [FamInst]
xs = (Bag FamInst, [FamInst]) -> [FamInst]
rm_fun ([RoughMatchLookupTc]
-> RoughMap FamInst -> (Bag FamInst, [FamInst])
forall a. [RoughMatchLookupTc] -> RoughMap a -> (Bag a, [a])
lookupRM' [RoughMatchLookupTc]
rough_tmpl RoughMap FamInst
ie)
, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [FamInst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FamInst]
xs
= (FamInst -> Maybe a) -> [FamInst] -> [a]
forall (f :: * -> *) a b.
Foldable f =>
(a -> Maybe b) -> f a -> [b]
mapMaybe' FamInst -> Maybe a
check_fun [FamInst]
xs
| Bool
otherwise = []
where
rough_tmpl :: [RoughMatchLookupTc]
rough_tmpl :: [RoughMatchLookupTc]
rough_tmpl = Name -> RoughMatchLookupTc
RML_KnownTc (TyCon -> Name
tyConName TyCon
fam) RoughMatchLookupTc -> [RoughMatchLookupTc] -> [RoughMatchLookupTc]
forall a. a -> [a] -> [a]
: (Type -> RoughMatchLookupTc) -> [Type] -> [RoughMatchLookupTc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> RoughMatchLookupTc
typeToRoughMatchLookupTc [Type]
match_tys
rm_fun :: (Bag FamInst, [FamInst]) -> [FamInst]
((Bag FamInst, [FamInst]) -> [FamInst]
rm_fun, FamInst -> Maybe a
check_fun) = case FamInstLookupMode a
lookup_mode of
WantConflicts FamInst
fam_inst -> ((Bag FamInst, [FamInst]) -> [FamInst]
forall a b. (a, b) -> b
snd, FamInst -> FamInst -> Maybe FamInst
unify_fun FamInst
fam_inst)
FamInstLookupMode a
WantMatches -> (Bag FamInst -> [FamInst]
forall a. Bag a -> [a]
bagToList (Bag FamInst -> [FamInst])
-> ((Bag FamInst, [FamInst]) -> Bag FamInst)
-> (Bag FamInst, [FamInst])
-> [FamInst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bag FamInst, [FamInst]) -> Bag FamInst
forall a b. (a, b) -> a
fst, FamInst -> Maybe a
FamInst -> Maybe FamInstMatch
match_fun)
unify_fun :: FamInst -> FamInst -> Maybe FamInst
unify_fun FamInst
orig_fam_inst item :: FamInst
item@(FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
old_axiom, fi_tys :: FamInst -> [Type]
fi_tys = [Type]
tpl_tys, fi_tvs :: FamInst -> [TyVar]
fi_tvs = [TyVar]
tpl_tvs })
= Bool -> SDoc -> Maybe FamInst -> Maybe FamInst
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
tys TyCoVarSet -> TyCoVarSet -> Bool
`disjointVarSet` [TyVar] -> TyCoVarSet
mkVarSet [TyVar]
tpl_tvs)
((TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys) SDoc -> SDoc -> SDoc
$$
([TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tpl_tvs SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tpl_tys)) (Maybe FamInst -> Maybe FamInst) -> Maybe FamInst -> Maybe FamInst
forall a b. (a -> b) -> a -> b
$
if CoAxBranch -> CoAxBranch -> Bool
compatibleBranches (CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch CoAxiom Unbranched
old_axiom) CoAxBranch
new_branch
then Maybe FamInst
forall a. Maybe a
Nothing
else FamInst -> Maybe FamInst
forall a. a -> Maybe a
Just FamInst
item
where
new_branch :: CoAxBranch
new_branch = CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch (FamInst -> CoAxiom Unbranched
famInstAxiom FamInst
orig_fam_inst)
(TyCon
fam, [Type]
tys) = FamInst -> (TyCon, [Type])
famInstSplitLHS FamInst
orig_fam_inst
match_fun :: FamInst -> Maybe FamInstMatch
match_fun item :: FamInst
item@(FamInst { fi_tvs :: FamInst -> [TyVar]
fi_tvs = [TyVar]
tpl_tvs, fi_cvs :: FamInst -> [TyVar]
fi_cvs = [TyVar]
tpl_cvs
, fi_tys :: FamInst -> [Type]
fi_tys = [Type]
tpl_tys }) = do
TCvSubst
subst <- [Type] -> [Type] -> Maybe TCvSubst
tcMatchTys [Type]
tpl_tys [Type]
match_tys1
FamInstMatch -> Maybe FamInstMatch
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (FamInstMatch { fim_instance :: FamInst
fim_instance = FamInst
item
, fim_tys :: [Type]
fim_tys = TCvSubst -> [TyVar] -> [Type]
substTyVars TCvSubst
subst [TyVar]
tpl_tvs [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
`chkAppend` [Type]
match_tys2
, fim_cos :: [Coercion]
fim_cos = Bool -> [Coercion] -> [Coercion]
forall a. HasCallStack => Bool -> a -> a
assert ((TyVar -> Bool) -> [TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe Coercion -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Coercion -> Bool)
-> (TyVar -> Maybe Coercion) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCvSubst -> TyVar -> Maybe Coercion
lookupCoVar TCvSubst
subst) [TyVar]
tpl_cvs) ([Coercion] -> [Coercion]) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> a -> b
$
TCvSubst -> [TyVar] -> [Coercion]
substCoVars TCvSubst
subst [TyVar]
tpl_cvs
})
where
([Type]
match_tys1, [Type]
match_tys2) = [Type] -> ([Type], [Type])
split_tys [Type]
tpl_tys
split_tys :: [Type] -> ([Type], [Type])
split_tys [Type]
tpl_tys
| TyCon -> Bool
isTypeFamilyTyCon TyCon
fam
= ([Type], [Type])
pre_rough_split_tys
| Bool
otherwise
= let ([Type]
match_tys1, [Type]
match_tys2) = [Type] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [Type]
tpl_tys [Type]
match_tys
in ([Type]
match_tys1, [Type]
match_tys2)
([Type]
pre_match_tys1, [Type]
pre_match_tys2) = BranchIndex -> [Type] -> ([Type], [Type])
forall a. BranchIndex -> [a] -> ([a], [a])
splitAt (TyCon -> BranchIndex
tyConArity TyCon
fam) [Type]
match_tys
pre_rough_split_tys :: ([Type], [Type])
pre_rough_split_tys
= ([Type]
pre_match_tys1, [Type]
pre_match_tys2)
lookup_fam_inst_env
:: FamInstLookupMode a
-> FamInstEnvs
-> TyCon -> [Type]
-> [a]
lookup_fam_inst_env :: forall a.
FamInstLookupMode a
-> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [a]
lookup_fam_inst_env FamInstLookupMode a
match_fun (FamInstEnv
pkg_ie, FamInstEnv
home_ie) TyCon
fam [Type]
tys
= FamInstLookupMode a -> FamInstEnv -> TyCon -> [Type] -> [a]
forall a.
FamInstLookupMode a -> FamInstEnv -> TyCon -> [Type] -> [a]
lookup_fam_inst_env' FamInstLookupMode a
match_fun FamInstEnv
home_ie TyCon
fam [Type]
tys
[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ FamInstLookupMode a -> FamInstEnv -> TyCon -> [Type] -> [a]
forall a.
FamInstLookupMode a -> FamInstEnv -> TyCon -> [Type] -> [a]
lookup_fam_inst_env' FamInstLookupMode a
match_fun FamInstEnv
pkg_ie TyCon
fam [Type]
tys
isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
isDominatedBy CoAxBranch
branch [CoAxBranch]
branches
= [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (CoAxBranch -> Bool) -> [CoAxBranch] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map CoAxBranch -> Bool
match [CoAxBranch]
branches
where
lhs :: [Type]
lhs = CoAxBranch -> [Type]
coAxBranchLHS CoAxBranch
branch
match :: CoAxBranch -> Bool
match (CoAxBranch { cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
tys })
= Maybe TCvSubst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TCvSubst -> Bool) -> Maybe TCvSubst -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> [Type] -> Maybe TCvSubst
tcMatchTys [Type]
tys [Type]
lhs
reduceTyFamApp_maybe :: FamInstEnvs
-> Role
-> TyCon -> [Type]
-> Maybe Reduction
reduceTyFamApp_maybe :: (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe Reduction
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
envs Role
role TyCon
tc [Type]
tys
| Role
Phantom <- Role
role
= Maybe Reduction
forall a. Maybe a
Nothing
| case Role
role of
Role
Representational -> TyCon -> Bool
isOpenFamilyTyCon TyCon
tc
Role
_ -> TyCon -> Bool
isOpenTypeFamilyTyCon TyCon
tc
, FamInstMatch { fim_instance :: FamInstMatch -> FamInst
fim_instance = FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
ax }
, fim_tys :: FamInstMatch -> [Type]
fim_tys = [Type]
inst_tys
, fim_cos :: FamInstMatch -> [Coercion]
fim_cos = [Coercion]
inst_cos } : [FamInstMatch]
_ <- (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch]
lookupFamInstEnv (FamInstEnv, FamInstEnv)
envs TyCon
tc [Type]
tys
= let co :: Coercion
co = Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
role CoAxiom Unbranched
ax [Type]
inst_tys [Coercion]
inst_cos
in Reduction -> Maybe Reduction
forall a. a -> Maybe a
Just (Reduction -> Maybe Reduction) -> Reduction -> Maybe Reduction
forall a b. (a -> b) -> a -> b
$ Coercion -> Reduction
coercionRedn Coercion
co
| Just CoAxiom Branched
ax <- TyCon -> Maybe (CoAxiom Branched)
isClosedSynFamilyTyConWithAxiom_maybe TyCon
tc
, Just (BranchIndex
ind, [Type]
inst_tys, [Coercion]
inst_cos) <- CoAxiom Branched
-> [Type] -> Maybe (BranchIndex, [Type], [Coercion])
chooseBranch CoAxiom Branched
ax [Type]
tys
= let co :: Coercion
co = Role
-> CoAxiom Branched
-> BranchIndex
-> [Type]
-> [Coercion]
-> Coercion
forall (br :: BranchFlag).
Role
-> CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Coercion
mkAxInstCo Role
role CoAxiom Branched
ax BranchIndex
ind [Type]
inst_tys [Coercion]
inst_cos
in Reduction -> Maybe Reduction
forall a. a -> Maybe a
Just (Reduction -> Maybe Reduction) -> Reduction -> Maybe Reduction
forall a b. (a -> b) -> a -> b
$ Coercion -> Reduction
coercionRedn Coercion
co
| Just BuiltInSynFamily
ax <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
tc
, Just (CoAxiomRule
coax,[Type]
ts,Type
ty) <- BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam BuiltInSynFamily
ax [Type]
tys
, Role
role Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== CoAxiomRule -> Role
coaxrRole CoAxiomRule
coax
= let co :: Coercion
co = CoAxiomRule -> [Coercion] -> Coercion
mkAxiomRuleCo CoAxiomRule
coax ((Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo (CoAxiomRule -> [Role]
coaxrAsmpRoles CoAxiomRule
coax) [Type]
ts)
in Reduction -> Maybe Reduction
forall a. a -> Maybe a
Just (Reduction -> Maybe Reduction) -> Reduction -> Maybe Reduction
forall a b. (a -> b) -> a -> b
$ Coercion -> Type -> Reduction
mkReduction Coercion
co Type
ty
| Bool
otherwise
= Maybe Reduction
forall a. Maybe a
Nothing
chooseBranch :: CoAxiom Branched -> [Type]
-> Maybe (BranchIndex, [Type], [Coercion])
chooseBranch :: CoAxiom Branched
-> [Type] -> Maybe (BranchIndex, [Type], [Coercion])
chooseBranch CoAxiom Branched
axiom [Type]
tys
= do { let num_pats :: BranchIndex
num_pats = CoAxiom Branched -> BranchIndex
forall (br :: BranchFlag). CoAxiom br -> BranchIndex
coAxiomNumPats CoAxiom Branched
axiom
([Type]
target_tys, [Type]
extra_tys) = BranchIndex -> [Type] -> ([Type], [Type])
forall a. BranchIndex -> [a] -> ([a], [a])
splitAt BranchIndex
num_pats [Type]
tys
branches :: Branches Branched
branches = CoAxiom Branched -> Branches Branched
forall (br :: BranchFlag). CoAxiom br -> Branches br
coAxiomBranches CoAxiom Branched
axiom
; (BranchIndex
ind, [Type]
inst_tys, [Coercion]
inst_cos)
<- Array BranchIndex CoAxBranch
-> [Type] -> Maybe (BranchIndex, [Type], [Coercion])
findBranch (Branches Branched -> Array BranchIndex CoAxBranch
forall (br :: BranchFlag).
Branches br -> Array BranchIndex CoAxBranch
unMkBranches Branches Branched
branches) [Type]
target_tys
; (BranchIndex, [Type], [Coercion])
-> Maybe (BranchIndex, [Type], [Coercion])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ( BranchIndex
ind, [Type]
inst_tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
`chkAppend` [Type]
extra_tys, [Coercion]
inst_cos ) }
findBranch :: Array BranchIndex CoAxBranch
-> [Type]
-> Maybe (BranchIndex, [Type], [Coercion])
findBranch :: Array BranchIndex CoAxBranch
-> [Type] -> Maybe (BranchIndex, [Type], [Coercion])
findBranch Array BranchIndex CoAxBranch
branches [Type]
target_tys
= ((BranchIndex, CoAxBranch)
-> Maybe (BranchIndex, [Type], [Coercion])
-> Maybe (BranchIndex, [Type], [Coercion]))
-> Maybe (BranchIndex, [Type], [Coercion])
-> [(BranchIndex, CoAxBranch)]
-> Maybe (BranchIndex, [Type], [Coercion])
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (BranchIndex, CoAxBranch)
-> Maybe (BranchIndex, [Type], [Coercion])
-> Maybe (BranchIndex, [Type], [Coercion])
go Maybe (BranchIndex, [Type], [Coercion])
forall a. Maybe a
Nothing (Array BranchIndex CoAxBranch -> [(BranchIndex, CoAxBranch)]
forall i e. Ix i => Array i e -> [(i, e)]
assocs Array BranchIndex CoAxBranch
branches)
where
go :: (BranchIndex, CoAxBranch)
-> Maybe (BranchIndex, [Type], [Coercion])
-> Maybe (BranchIndex, [Type], [Coercion])
go :: (BranchIndex, CoAxBranch)
-> Maybe (BranchIndex, [Type], [Coercion])
-> Maybe (BranchIndex, [Type], [Coercion])
go (BranchIndex
index, CoAxBranch
branch) Maybe (BranchIndex, [Type], [Coercion])
other
= let (CoAxBranch { cab_tvs :: CoAxBranch -> [TyVar]
cab_tvs = [TyVar]
tpl_tvs, cab_cvs :: CoAxBranch -> [TyVar]
cab_cvs = [TyVar]
tpl_cvs
, cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
tpl_lhs
, cab_incomps :: CoAxBranch -> [CoAxBranch]
cab_incomps = [CoAxBranch]
incomps }) = CoAxBranch
branch
in_scope :: InScopeSet
in_scope = TyCoVarSet -> InScopeSet
mkInScopeSet ([TyCoVarSet] -> TyCoVarSet
unionVarSets ([TyCoVarSet] -> TyCoVarSet) -> [TyCoVarSet] -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
(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_tys
in case [Type] -> [Type] -> Maybe TCvSubst
tcMatchTys [Type]
tpl_lhs [Type]
target_tys of
Just TCvSubst
subst
| [Type] -> CoAxBranch -> Bool
apartnessCheck [Type]
flattened_target CoAxBranch
branch
->
Bool
-> Maybe (BranchIndex, [Type], [Coercion])
-> Maybe (BranchIndex, [Type], [Coercion])
forall a. HasCallStack => Bool -> a -> a
assert ((TyVar -> Bool) -> [TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe Coercion -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Coercion -> Bool)
-> (TyVar -> Maybe Coercion) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCvSubst -> TyVar -> Maybe Coercion
lookupCoVar TCvSubst
subst) [TyVar]
tpl_cvs) (Maybe (BranchIndex, [Type], [Coercion])
-> Maybe (BranchIndex, [Type], [Coercion]))
-> Maybe (BranchIndex, [Type], [Coercion])
-> Maybe (BranchIndex, [Type], [Coercion])
forall a b. (a -> b) -> a -> b
$
(BranchIndex, [Type], [Coercion])
-> Maybe (BranchIndex, [Type], [Coercion])
forall a. a -> Maybe a
Just (BranchIndex
index, TCvSubst -> [TyVar] -> [Type]
substTyVars TCvSubst
subst [TyVar]
tpl_tvs, TCvSubst -> [TyVar] -> [Coercion]
substCoVars TCvSubst
subst [TyVar]
tpl_cvs)
Maybe TCvSubst
_ -> Maybe (BranchIndex, [Type], [Coercion])
other
apartnessCheck :: [Type]
-> CoAxBranch
-> Bool
apartnessCheck :: [Type] -> CoAxBranch -> Bool
apartnessCheck [Type]
flattened_target (CoAxBranch { cab_incomps :: CoAxBranch -> [CoAxBranch]
cab_incomps = [CoAxBranch]
incomps })
= (CoAxBranch -> Bool) -> [CoAxBranch] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (UnifyResult -> Bool
forall {a}. UnifyResultM a -> Bool
isSurelyApart
(UnifyResult -> Bool)
-> (CoAxBranch -> UnifyResult) -> CoAxBranch -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
alwaysBindFun [Type]
flattened_target
([Type] -> UnifyResult)
-> (CoAxBranch -> [Type]) -> CoAxBranch -> UnifyResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxBranch -> [Type]
coAxBranchLHS) [CoAxBranch]
incomps
where
isSurelyApart :: UnifyResultM a -> Bool
isSurelyApart UnifyResultM a
SurelyApart = Bool
True
isSurelyApart UnifyResultM a
_ = Bool
False
topNormaliseType :: FamInstEnvs -> Type -> Type
topNormaliseType :: (FamInstEnv, FamInstEnv) -> Type -> Type
topNormaliseType (FamInstEnv, FamInstEnv)
env Type
ty
= case (FamInstEnv, FamInstEnv) -> Type -> Maybe Reduction
topNormaliseType_maybe (FamInstEnv, FamInstEnv)
env Type
ty of
Just Reduction
redn -> Reduction -> Type
reductionReducedType Reduction
redn
Maybe Reduction
Nothing -> Type
ty
topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction
topNormaliseType_maybe :: (FamInstEnv, FamInstEnv) -> Type -> Maybe Reduction
topNormaliseType_maybe (FamInstEnv, FamInstEnv)
env Type
ty
= do { ((Coercion
co, MCoercionN
mkind_co), Type
nty) <- NormaliseStepper (Coercion, MCoercionN)
-> ((Coercion, MCoercionN)
-> (Coercion, MCoercionN) -> (Coercion, MCoercionN))
-> Type
-> Maybe ((Coercion, MCoercionN), Type)
forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX NormaliseStepper (Coercion, MCoercionN)
stepper (Coercion, MCoercionN)
-> (Coercion, MCoercionN) -> (Coercion, MCoercionN)
combine Type
ty
; let hredn :: HetReduction
hredn = Reduction -> MCoercionN -> HetReduction
mkHetReduction (Coercion -> Type -> Reduction
mkReduction Coercion
co Type
nty) MCoercionN
mkind_co
; Reduction -> Maybe Reduction
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> Maybe Reduction) -> Reduction -> Maybe Reduction
forall a b. (a -> b) -> a -> b
$ Role -> HetReduction -> Reduction
homogeniseHetRedn Role
Representational HetReduction
hredn }
where
stepper :: NormaliseStepper (Coercion, MCoercionN)
stepper = NormaliseStepper (Coercion, MCoercionN)
unwrapNewTypeStepper' NormaliseStepper (Coercion, MCoercionN)
-> NormaliseStepper (Coercion, MCoercionN)
-> NormaliseStepper (Coercion, MCoercionN)
forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
`composeSteppers` NormaliseStepper (Coercion, MCoercionN)
tyFamStepper
combine :: (Coercion, MCoercionN)
-> (Coercion, MCoercionN) -> (Coercion, MCoercionN)
combine (Coercion
c1, MCoercionN
mc1) (Coercion
c2, MCoercionN
mc2) = (Coercion
c1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
c2, MCoercionN
mc1 MCoercionN -> MCoercionN -> MCoercionN
`mkTransMCo` MCoercionN
mc2)
unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN)
unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN)
unwrapNewTypeStepper' RecTcChecker
rec_nts TyCon
tc [Type]
tys
= (Coercion -> (Coercion, MCoercionN))
-> NormaliseStepResult Coercion
-> NormaliseStepResult (Coercion, MCoercionN)
forall ev1 ev2.
(ev1 -> ev2) -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
mapStepResult (, MCoercionN
MRefl) (NormaliseStepResult Coercion
-> NormaliseStepResult (Coercion, MCoercionN))
-> NormaliseStepResult Coercion
-> NormaliseStepResult (Coercion, MCoercionN)
forall a b. (a -> b) -> a -> b
$ NormaliseStepper Coercion
unwrapNewTypeStepper RecTcChecker
rec_nts TyCon
tc [Type]
tys
tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
tyFamStepper RecTcChecker
rec_nts TyCon
tc [Type]
tys
= case (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> Maybe HetReduction
topReduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
env TyCon
tc [Type]
tys of
Just (HetReduction (Reduction Coercion
co Type
rhs) MCoercionN
res_co)
-> RecTcChecker
-> Type
-> (Coercion, MCoercionN)
-> NormaliseStepResult (Coercion, MCoercionN)
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts Type
rhs (Coercion
co, MCoercionN
res_co)
Maybe HetReduction
_ -> NormaliseStepResult (Coercion, MCoercionN)
forall ev. NormaliseStepResult ev
NS_Done
normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> Reduction
normaliseTcApp :: (FamInstEnv, FamInstEnv) -> Role -> TyCon -> [Type] -> Reduction
normaliseTcApp (FamInstEnv, FamInstEnv)
env Role
role TyCon
tc [Type]
tys
= (FamInstEnv, FamInstEnv)
-> Role -> TyCoVarSet -> NormM Reduction -> Reduction
forall a.
(FamInstEnv, FamInstEnv) -> Role -> TyCoVarSet -> NormM a -> a
initNormM (FamInstEnv, FamInstEnv)
env Role
role ([Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
tys) (NormM Reduction -> Reduction) -> NormM Reduction -> Reduction
forall a b. (a -> b) -> a -> b
$
TyCon -> [Type] -> NormM Reduction
normalise_tc_app TyCon
tc [Type]
tys
normalise_tc_app :: TyCon -> [Type] -> NormM Reduction
normalise_tc_app :: TyCon -> [Type] -> NormM Reduction
normalise_tc_app TyCon
tc [Type]
tys
| Just ([(TyVar, Type)]
tenv, Type
rhs, [Type]
tys') <- TyCon -> [Type] -> Maybe ([(TyVar, Type)], Type, [Type])
forall tyco.
TyCon -> [tyco] -> Maybe ([(TyVar, tyco)], Type, [tyco])
expandSynTyCon_maybe TyCon
tc [Type]
tys
, Bool -> Bool
not (TyCon -> Bool
isFamFreeTyCon TyCon
tc)
=
Type -> NormM Reduction
normalise_type (Type -> [Type] -> Type
mkAppTys ((() :: Constraint) => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy ([(TyVar, Type)] -> TCvSubst
mkTvSubstPrs [(TyVar, Type)]
tenv) Type
rhs) [Type]
tys')
| TyCon -> Bool
isFamilyTyCon TyCon
tc
=
do { (FamInstEnv, FamInstEnv)
env <- NormM (FamInstEnv, FamInstEnv)
getEnv
; Role
role <- NormM Role
getRole
; ArgsReductions redns :: Reductions
redns@(Reductions [Coercion]
args_cos [Type]
ntys) MCoercionN
res_co <- TyCon -> [Type] -> NormM ArgsReductions
normalise_tc_args TyCon
tc [Type]
tys
; case (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe Reduction
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
env Role
role TyCon
tc [Type]
ntys of
Just Reduction
redn1
-> do { Reduction
redn2 <- Reduction -> NormM Reduction
normalise_reduction Reduction
redn1
; let redn3 :: Reduction
redn3 = (() :: Constraint) => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc [Coercion]
args_cos Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn2
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Reduction -> MCoercionN -> Reduction
assemble_result Role
role Reduction
redn3 MCoercionN
res_co }
Maybe Reduction
_ ->
Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$
Role -> Reduction -> MCoercionN -> Reduction
assemble_result Role
role (Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
role TyCon
tc Reductions
redns) MCoercionN
res_co }
| Bool
otherwise
=
do { ArgsReductions Reductions
redns MCoercionN
res_co <- TyCon -> [Type] -> NormM ArgsReductions
normalise_tc_args TyCon
tc [Type]
tys
; Role
role <- NormM Role
getRole
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$
Role -> Reduction -> MCoercionN -> Reduction
assemble_result Role
role (Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
role TyCon
tc Reductions
redns) MCoercionN
res_co }
where
assemble_result :: Role
-> Reduction
-> MCoercionN
-> Reduction
assemble_result :: Role -> Reduction -> MCoercionN -> Reduction
assemble_result Role
r Reduction
redn MCoercionN
kind_co
= Role -> Reduction -> MCoercionN -> Reduction
mkCoherenceRightMRedn Role
r Reduction
redn (MCoercionN -> MCoercionN
mkSymMCo MCoercionN
kind_co)
topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type]
-> Maybe HetReduction
topReduceTyFamApp_maybe :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> Maybe HetReduction
topReduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
envs TyCon
fam_tc [Type]
arg_tys
| TyCon -> Bool
isFamilyTyCon TyCon
fam_tc
, Just Reduction
redn <- (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe Reduction
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
envs Role
role TyCon
fam_tc [Type]
ntys
= HetReduction -> Maybe HetReduction
forall a. a -> Maybe a
Just (HetReduction -> Maybe HetReduction)
-> HetReduction -> Maybe HetReduction
forall a b. (a -> b) -> a -> b
$
Reduction -> MCoercionN -> HetReduction
mkHetReduction
((() :: Constraint) => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
fam_tc [Coercion]
args_cos Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn)
MCoercionN
res_co
| Bool
otherwise
= Maybe HetReduction
forall a. Maybe a
Nothing
where
role :: Role
role = Role
Representational
ArgsReductions (Reductions [Coercion]
args_cos [Type]
ntys) MCoercionN
res_co
= (FamInstEnv, FamInstEnv)
-> Role -> TyCoVarSet -> NormM ArgsReductions -> ArgsReductions
forall a.
(FamInstEnv, FamInstEnv) -> Role -> TyCoVarSet -> NormM a -> a
initNormM (FamInstEnv, FamInstEnv)
envs Role
role ([Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
arg_tys)
(NormM ArgsReductions -> ArgsReductions)
-> NormM ArgsReductions -> ArgsReductions
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> NormM ArgsReductions
normalise_tc_args TyCon
fam_tc [Type]
arg_tys
normalise_tc_args :: TyCon -> [Type] -> NormM ArgsReductions
normalise_tc_args :: TyCon -> [Type] -> NormM ArgsReductions
normalise_tc_args TyCon
tc [Type]
tys
= do { Role
role <- NormM Role
getRole
; Type -> [Role] -> [Type] -> NormM ArgsReductions
normalise_args (TyCon -> Type
tyConKind TyCon
tc) (Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc) [Type]
tys }
normaliseType :: FamInstEnvs
-> Role
-> Type -> Reduction
normaliseType :: (FamInstEnv, FamInstEnv) -> Role -> Type -> Reduction
normaliseType (FamInstEnv, FamInstEnv)
env Role
role Type
ty
= (FamInstEnv, FamInstEnv)
-> Role -> TyCoVarSet -> NormM Reduction -> Reduction
forall a.
(FamInstEnv, FamInstEnv) -> Role -> TyCoVarSet -> NormM a -> a
initNormM (FamInstEnv, FamInstEnv)
env Role
role (Type -> TyCoVarSet
tyCoVarsOfType Type
ty) (NormM Reduction -> Reduction) -> NormM Reduction -> Reduction
forall a b. (a -> b) -> a -> b
$ Type -> NormM Reduction
normalise_type Type
ty
normalise_type :: Type -> NormM Reduction
normalise_type :: Type -> NormM Reduction
normalise_type Type
ty
= Type -> NormM Reduction
go Type
ty
where
go :: Type -> NormM Reduction
go :: Type -> NormM Reduction
go (TyConApp TyCon
tc [Type]
tys) = TyCon -> [Type] -> NormM Reduction
normalise_tc_app TyCon
tc [Type]
tys
go ty :: Type
ty@(LitTy {})
= do { Role
r <- NormM Role
getRole
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
r Type
ty }
go (AppTy Type
ty1 Type
ty2) = Type -> [Type] -> NormM Reduction
go_app_tys Type
ty1 [Type
ty2]
go (FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
vis, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
= do { Reduction
arg_redn <- Type -> NormM Reduction
go Type
ty1
; Reduction
res_redn <- Type -> NormM Reduction
go Type
ty2
; Reduction
w_redn <- Role -> NormM Reduction -> NormM Reduction
forall a. Role -> NormM a -> NormM a
withRole Role
Nominal (NormM Reduction -> NormM Reduction)
-> NormM Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ Type -> NormM Reduction
go Type
w
; Role
r <- NormM Role
getRole
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ Role
-> AnonArgFlag -> Reduction -> Reduction -> Reduction -> Reduction
mkFunRedn Role
r AnonArgFlag
vis Reduction
w_redn Reduction
arg_redn Reduction
res_redn }
go (ForAllTy (Bndr TyVar
tcvar ArgFlag
vis) Type
ty)
= do { (LiftingContext
lc', TyVar
tv', Reduction
k_redn) <- TyVar -> NormM (LiftingContext, TyVar, Reduction)
normalise_var_bndr TyVar
tcvar
; Reduction
redn <- LiftingContext -> NormM Reduction -> NormM Reduction
forall a. LiftingContext -> NormM a -> NormM a
withLC LiftingContext
lc' (NormM Reduction -> NormM Reduction)
-> NormM Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ Type -> NormM Reduction
normalise_type Type
ty
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ ArgFlag -> TyVar -> Reduction -> Reduction -> Reduction
mkForAllRedn ArgFlag
vis TyVar
tv' Reduction
k_redn Reduction
redn }
go (TyVarTy TyVar
tv) = TyVar -> NormM Reduction
normalise_tyvar TyVar
tv
go (CastTy Type
ty Coercion
co)
= do { Reduction
redn <- Type -> NormM Reduction
go Type
ty
; LiftingContext
lc <- NormM LiftingContext
getLC
; let co' :: Coercion
co' = LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Coercion -> Reduction -> Coercion -> Reduction
mkCastRedn2 Role
Nominal Type
ty Coercion
co Reduction
redn Coercion
co'
}
go (CoercionTy Coercion
co)
= do { LiftingContext
lc <- NormM LiftingContext
getLC
; Role
r <- NormM Role
getRole
; let kco :: Coercion
kco = (() :: Constraint) => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc (Coercion -> Type
coercionType Coercion
co)
co' :: Coercion
co' = LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Coercion -> Coercion -> Coercion -> Reduction
mkProofIrrelRedn Role
r Coercion
kco Coercion
co Coercion
co' }
go_app_tys :: Type
-> [Type]
-> NormM Reduction
go_app_tys :: Type -> [Type] -> NormM Reduction
go_app_tys (AppTy Type
ty1 Type
ty2) [Type]
tys = Type -> [Type] -> NormM Reduction
go_app_tys Type
ty1 (Type
ty2 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
tys)
go_app_tys Type
fun_ty [Type]
arg_tys
= do { fun_redn :: Reduction
fun_redn@(Reduction Coercion
fun_co Type
nfun) <- Type -> NormM Reduction
go Type
fun_ty
; case HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
nfun of
Just (TyCon
tc, [Type]
xis) ->
do { Reduction
redn <- Type -> NormM Reduction
go (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type]
xis [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
arg_tys))
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$
Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
fun_co ((Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
mkNomReflCo [Type]
arg_tys) Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn }
Maybe (TyCon, [Type])
Nothing ->
do { ArgsReductions Reductions
redns MCoercionN
res_co
<- Type -> [Role] -> [Type] -> NormM ArgsReductions
normalise_args ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
nfun)
(Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal)
[Type]
arg_tys
; Role
role <- NormM Role
getRole
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$
Role -> Reduction -> MCoercionN -> Reduction
mkCoherenceRightMRedn Role
role
(Reduction -> Reductions -> Reduction
mkAppRedns Reduction
fun_redn Reductions
redns)
(MCoercionN -> MCoercionN
mkSymMCo MCoercionN
res_co) } }
normalise_args :: Kind
-> [Role]
-> [Type]
-> NormM ArgsReductions
normalise_args :: Type -> [Role] -> [Type] -> NormM ArgsReductions
normalise_args Type
fun_ki [Role]
roles [Type]
args
= do { [Reduction]
normed_args <- (Role -> Type -> NormM Reduction)
-> [Role] -> [Type] -> NormM [Reduction]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Role -> Type -> NormM Reduction
normalise1 [Role]
roles [Type]
args
; ArgsReductions -> NormM ArgsReductions
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgsReductions -> NormM ArgsReductions)
-> ArgsReductions -> NormM ArgsReductions
forall a b. (a -> b) -> a -> b
$ [TyCoBinder]
-> Type -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
(() :: Constraint) =>
[TyCoBinder]
-> Type -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
simplifyArgsWorker [TyCoBinder]
ki_binders Type
inner_ki TyCoVarSet
fvs [Role]
roles [Reduction]
normed_args }
where
([TyCoBinder]
ki_binders, Type
inner_ki) = Type -> ([TyCoBinder], Type)
splitPiTys Type
fun_ki
fvs :: TyCoVarSet
fvs = [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
args
normalise1 :: Role -> Type -> NormM Reduction
normalise1 Role
role Type
ty
= Role -> NormM Reduction -> NormM Reduction
forall a. Role -> NormM a -> NormM a
withRole Role
role (NormM Reduction -> NormM Reduction)
-> NormM Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ Type -> NormM Reduction
normalise_type Type
ty
normalise_tyvar :: TyVar -> NormM Reduction
normalise_tyvar :: TyVar -> NormM Reduction
normalise_tyvar TyVar
tv
= Bool -> NormM Reduction -> NormM Reduction
forall a. HasCallStack => Bool -> a -> a
assert (TyVar -> Bool
isTyVar TyVar
tv) (NormM Reduction -> NormM Reduction)
-> NormM Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$
do { LiftingContext
lc <- NormM LiftingContext
getLC
; Role
r <- NormM Role
getRole
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ case LiftingContext -> Role -> TyVar -> Maybe Coercion
liftCoSubstTyVar LiftingContext
lc Role
r TyVar
tv of
Just Coercion
co -> Coercion -> Reduction
coercionRedn Coercion
co
Maybe Coercion
Nothing -> Role -> Type -> Reduction
mkReflRedn Role
r (TyVar -> Type
mkTyVarTy TyVar
tv) }
normalise_reduction :: Reduction -> NormM Reduction
normalise_reduction :: Reduction -> NormM Reduction
normalise_reduction (Reduction Coercion
co Type
ty)
= do { Reduction
redn' <- Type -> NormM Reduction
normalise_type Type
ty
; Reduction -> NormM Reduction
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> NormM Reduction) -> Reduction -> NormM Reduction
forall a b. (a -> b) -> a -> b
$ Coercion
co Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn' }
normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Reduction)
normalise_var_bndr :: TyVar -> NormM (LiftingContext, TyVar, Reduction)
normalise_var_bndr TyVar
tcvar
= do { LiftingContext
lc1 <- NormM LiftingContext
getLC
; (FamInstEnv, FamInstEnv)
env <- NormM (FamInstEnv, FamInstEnv)
getEnv
; let callback :: LiftingContext -> Type -> Reduction
callback LiftingContext
lc Type
ki = NormM Reduction
-> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> Reduction
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM (Type -> NormM Reduction
normalise_type Type
ki) (FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
Nominal
; (LiftingContext, TyVar, Reduction)
-> NormM (LiftingContext, TyVar, Reduction)
forall a. a -> NormM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((LiftingContext, TyVar, Reduction)
-> NormM (LiftingContext, TyVar, Reduction))
-> (LiftingContext, TyVar, Reduction)
-> NormM (LiftingContext, TyVar, Reduction)
forall a b. (a -> b) -> a -> b
$ (Reduction -> Coercion)
-> (LiftingContext -> Type -> Reduction)
-> LiftingContext
-> TyVar
-> (LiftingContext, TyVar, Reduction)
forall r.
(r -> Coercion)
-> (LiftingContext -> Type -> r)
-> LiftingContext
-> TyVar
-> (LiftingContext, TyVar, r)
liftCoSubstVarBndrUsing Reduction -> Coercion
reductionCoercion LiftingContext -> Type -> Reduction
callback LiftingContext
lc1 TyVar
tcvar }
newtype NormM a = NormM { forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM ::
FamInstEnvs -> LiftingContext -> Role -> a }
deriving ((forall a b. (a -> b) -> NormM a -> NormM b)
-> (forall a b. a -> NormM b -> NormM a) -> Functor NormM
forall a b. a -> NormM b -> NormM a
forall a b. (a -> b) -> NormM a -> NormM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> NormM a -> NormM b
fmap :: forall a b. (a -> b) -> NormM a -> NormM b
$c<$ :: forall a b. a -> NormM b -> NormM a
<$ :: forall a b. a -> NormM b -> NormM a
Functor)
initNormM :: FamInstEnvs -> Role
-> TyCoVarSet
-> NormM a -> a
initNormM :: forall a.
(FamInstEnv, FamInstEnv) -> Role -> TyCoVarSet -> NormM a -> a
initNormM (FamInstEnv, FamInstEnv)
env Role
role TyCoVarSet
vars (NormM (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
thing_inside)
= (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
thing_inside (FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
role
where
in_scope :: InScopeSet
in_scope = TyCoVarSet -> InScopeSet
mkInScopeSet TyCoVarSet
vars
lc :: LiftingContext
lc = InScopeSet -> LiftingContext
emptyLiftingContext InScopeSet
in_scope
getRole :: NormM Role
getRole :: NormM Role
getRole = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> Role)
-> NormM Role
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (\ (FamInstEnv, FamInstEnv)
_ LiftingContext
_ Role
r -> Role
r)
getLC :: NormM LiftingContext
getLC :: NormM LiftingContext
getLC = ((FamInstEnv, FamInstEnv)
-> LiftingContext -> Role -> LiftingContext)
-> NormM LiftingContext
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (\ (FamInstEnv, FamInstEnv)
_ LiftingContext
lc Role
_ -> LiftingContext
lc)
getEnv :: NormM FamInstEnvs
getEnv :: NormM (FamInstEnv, FamInstEnv)
getEnv = ((FamInstEnv, FamInstEnv)
-> LiftingContext -> Role -> (FamInstEnv, FamInstEnv))
-> NormM (FamInstEnv, FamInstEnv)
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (\ (FamInstEnv, FamInstEnv)
env LiftingContext
_ Role
_ -> (FamInstEnv, FamInstEnv)
env)
withRole :: Role -> NormM a -> NormM a
withRole :: forall a. Role -> NormM a -> NormM a
withRole Role
r NormM a
thing = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a)
-> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a b. (a -> b) -> a -> b
$ \ (FamInstEnv, FamInstEnv)
envs LiftingContext
lc Role
_old_r -> NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM NormM a
thing (FamInstEnv, FamInstEnv)
envs LiftingContext
lc Role
r
withLC :: LiftingContext -> NormM a -> NormM a
withLC :: forall a. LiftingContext -> NormM a -> NormM a
withLC LiftingContext
lc NormM a
thing = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a)
-> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a b. (a -> b) -> a -> b
$ \ (FamInstEnv, FamInstEnv)
envs LiftingContext
_old_lc Role
r -> NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM NormM a
thing (FamInstEnv, FamInstEnv)
envs LiftingContext
lc Role
r
instance Monad NormM where
NormM a
ma >>= :: forall a b. NormM a -> (a -> NormM b) -> NormM b
>>= a -> NormM b
fmb = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b)
-> NormM b
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b)
-> NormM b)
-> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b)
-> NormM b
forall a b. (a -> b) -> a -> b
$ \(FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
r ->
let a :: a
a = NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM NormM a
ma (FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
r in
NormM b -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b
forall a.
NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a
runNormM (a -> NormM b
fmb a
a) (FamInstEnv, FamInstEnv)
env LiftingContext
lc Role
r
instance Applicative NormM where
pure :: forall a. a -> NormM a
pure a
x = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a.
((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a)
-> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a)
-> NormM a
forall a b. (a -> b) -> a -> b
$ \ (FamInstEnv, FamInstEnv)
_ LiftingContext
_ Role
_ -> a
x
<*> :: forall a b. NormM (a -> b) -> NormM a -> NormM b
(<*>) = NormM (a -> b) -> NormM a -> NormM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap