{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
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.TyCo.Compare( eqType, eqTypes )
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.FastString
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
import GHC.Data.List.Infinite (Infinite (..))
import qualified GHC.Data.List.Infinite as Inf
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
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"instance"
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> 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
forall doc. IsOutput doc => doc -> doc
whenPprDebug SDoc
debug_stuff)
where
ppr_tc_sort :: SDoc
ppr_tc_sort = case FamFlavor
flavor of
FamFlavor
SynFamilyInst -> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"type"
DataFamilyInst TyCon
tycon
| TyCon -> Bool
isDataTyCon TyCon
tycon -> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"data"
| TyCon -> Bool
isNewTyCon TyCon
tycon -> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"newtype"
| TyCon -> Bool
isAbstractTyCon TyCon
tycon -> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"data"
| Bool
otherwise -> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"WEIRD" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tycon
debug_stuff :: SDoc
debug_stuff = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Coercion axiom:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoAxiom Unbranched -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoAxiom Unbranched
ax
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Tvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"LHS:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"RHS:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs ]
pprFamInsts :: [FamInst] -> SDoc
pprFamInsts :: [FamInst] -> SDoc
pprFamInsts [FamInst]
finsts = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
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
forall doc. IsLine doc => String -> doc
text String
"FamIE" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
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 Subst
subst -> Subst -> Type -> Type
Type.substTyAddInScope Subst
subst Type
rhs1 Type -> Type -> Bool
`eqType`
Subst -> Type -> Type
Type.substTyAddInScope Subst
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_tvs :: CoAxBranch -> [TyVar]
cab_tvs = [TyVar]
tvs1, cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs1, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs1 })
ax2 :: CoAxBranch
ax2@(CoAxBranch { cab_tvs :: CoAxBranch -> [TyVar]
cab_tvs = [TyVar]
tvs2, 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_scope :: InScopeSet
in_scope = [TyVar] -> InScopeSet
mkInScopeSetList ([TyVar]
tvs1 [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
tvs2)
in case Bool -> InScopeSet -> Type -> Type -> Maybe Subst
tcUnifyTyWithTFs Bool
True InScopeSet
in_scope Type
rhs1 Type
rhs2 of
Maybe Subst
Nothing -> InjectivityCheckResult
InjectivityAccepted
Just Subst
subst
| [Type] -> [Type] -> Bool
eqTypes [Type]
lhs1Subst [Type]
lhs2Subst
-> InjectivityCheckResult
InjectivityAccepted
| Bool
otherwise
-> CoAxBranch -> CoAxBranch -> InjectivityCheckResult
InjectivityUnified ( CoAxBranch
ax1 { cab_lhs = Type.substTys subst lhs1
, cab_rhs = Type.substTy subst rhs1 })
( CoAxBranch
ax2 { cab_lhs = Type.substTys subst lhs2
, cab_rhs = Type.substTy subst rhs2 })
where
lhs1Subst :: [Type]
lhs1Subst = (() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
Type.substTys Subst
subst ([Type] -> [Type]
getInjArgs [Type]
lhs1)
lhs2Subst :: [Type]
lhs2Subst = (() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
Type.substTys Subst
subst ([Type] -> [Type]
getInjArgs [Type]
lhs2)
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 = mk_incomps prev_brs 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 [FastString -> OccName
mkTyVarOccFS (String -> FastString
fsLit 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 = [] }) }
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 = [] }) }
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 = [] }) }
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
forall doc. IsLine doc => String -> doc
text String
"match with" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (FamInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr FamInst
inst) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [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
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
([TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tpl_tvs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [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
Subst
subst <- [Type] -> [Type] -> Maybe Subst
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 = Subst -> [TyVar] -> [Type]
substTyVars Subst
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
. Subst -> TyVar -> Maybe Coercion
lookupCoVar Subst
subst) [TyVar]
tpl_cvs) ([Coercion] -> [Coercion]) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> a -> b
$
Subst -> [TyVar] -> [Coercion]
substCoVars Subst
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 Subst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Subst -> Bool) -> Maybe Subst -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> [Type] -> Maybe Subst
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 Subst
tcMatchTys [Type]
tpl_lhs [Type]
target_tys of
Just Subst
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
. Subst -> TyVar -> Maybe Coercion
lookupCoVar Subst
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, Subst -> [TyVar] -> [Type]
substTyVars Subst
subst [TyVar]
tpl_tvs, Subst -> [TyVar] -> [Coercion]
substCoVars Subst
subst [TyVar]
tpl_cvs)
Maybe Subst
_ -> 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
= (, MCoercionN
MRefl) (Coercion -> (Coercion, MCoercionN))
-> NormaliseStepResult Coercion
-> NormaliseStepResult (Coercion, MCoercionN)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
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
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
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
| ExpandsSyn [(TyVar, Type)]
tenv Type
rhs [Type]
tys' <- TyCon -> [Type] -> ExpandSynResult Type
forall tyco. TyCon -> [tyco] -> ExpandSynResult 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) => Subst -> Type -> Type
Subst -> Type -> Type
substTy ([(TyVar, Type)] -> Subst
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)
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 -> Infinite Role -> [Type] -> NormM ArgsReductions
normalise_args (TyCon -> Type
tyConKind TyCon
tc) (Role -> TyCon -> Infinite Role
tyConRolesX Role
role TyCon
tc) [Type]
tys }
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 -> FunTyFlag
ft_af = FunTyFlag
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
-> FunTyFlag -> Reduction -> Reduction -> Reduction -> Reduction
mkFunRedn Role
r FunTyFlag
vis Reduction
w_redn Reduction
arg_redn Reduction
res_redn }
go (ForAllTy (Bndr TyVar
tcvar ForAllTyFlag
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
$ ForAllTyFlag -> TyVar -> Reduction -> Reduction -> Reduction
mkForAllRedn ForAllTyFlag
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 -> Infinite Role -> [Type] -> NormM ArgsReductions
normalise_args ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
nfun)
(Role -> Infinite Role
forall a. a -> Infinite a
Inf.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
-> Infinite Role
-> [Type]
-> NormM ArgsReductions
normalise_args :: Type -> Infinite Role -> [Type] -> NormM ArgsReductions
normalise_args Type
fun_ki Infinite 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 (Infinite Role -> [Role]
forall a. Infinite a -> [a]
Inf.toList Infinite 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
$ [PiTyBinder]
-> Type
-> TyCoVarSet
-> Infinite Role
-> [Reduction]
-> ArgsReductions
(() :: Constraint) =>
[PiTyBinder]
-> Type
-> TyCoVarSet
-> Infinite Role
-> [Reduction]
-> ArgsReductions
simplifyArgsWorker [PiTyBinder]
ki_binders Type
inner_ki TyCoVarSet
fvs Infinite Role
roles [Reduction]
normed_args }
where
([PiTyBinder]
ki_binders, Type
inner_ki) = Type -> ([PiTyBinder], 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