{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
module GHC.Core.FamInstEnv (
FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
pprFamInst, pprFamInsts, orphNamesOfFamInst,
mkImportedFamInst, mkLocalFamInst,
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( IsOrphan, chooseOrphanAnchor )
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.Core.FVs( orphNamesOfAxiomLHS )
import GHC.Builtin.Types.Literals( tryMatchFam )
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.Name
import GHC.Types.Var
import GHC.Types.SrcLoc
import GHC.Types.Name.Set
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Data.FastString
import GHC.Data.Maybe
import GHC.Data.Bag
import GHC.Data.List.Infinite (Infinite (..))
import qualified GHC.Data.List.Infinite as Inf
import Control.Monad
import Data.List( mapAccumL )
import Data.Array( Array, assocs )
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
, FamInst -> IsOrphan
fi_orphan :: IsOrphan
}
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)
orphNamesOfFamInst :: FamInst -> NameSet
orphNamesOfFamInst :: FamInst -> NameSet
orphNamesOfFamInst (FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
ax }) = CoAxiom Unbranched -> NameSet
forall (br :: BranchFlag). CoAxiom br -> NameSet
orphNamesOfAxiomLHS CoAxiom Unbranched
ax
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)
mkLocalFamInst :: FamFlavor -> CoAxiom Unbranched
-> [TyVar] -> [CoVar] -> [Type] -> Type
-> FamInst
mkLocalFamInst :: FamFlavor
-> CoAxiom Unbranched
-> [TyVar]
-> [TyVar]
-> [Type]
-> Type
-> FamInst
mkLocalFamInst FamFlavor
flavor CoAxiom Unbranched
axiom [TyVar]
tvs [TyVar]
cvs [Type]
lhs Type
rhs
= FamInst { fi_fam :: Name
fi_fam = Name
fam_tc_name
, fi_flavor :: FamFlavor
fi_flavor = FamFlavor
flavor
, fi_tcs :: [RoughMatchTc]
fi_tcs = [Type] -> [RoughMatchTc]
roughMatchTcs [Type]
lhs
, fi_tvs :: [TyVar]
fi_tvs = [TyVar]
tvs
, fi_cvs :: [TyVar]
fi_cvs = [TyVar]
cvs
, fi_tys :: [Type]
fi_tys = [Type]
lhs
, fi_rhs :: Type
fi_rhs = Type
rhs
, fi_axiom :: CoAxiom Unbranched
fi_axiom = CoAxiom Unbranched
axiom
, fi_orphan :: IsOrphan
fi_orphan = NameSet -> IsOrphan
chooseOrphanAnchor NameSet
orph_names }
where
mod :: Module
mod = Bool -> Module -> Module
forall a. HasCallStack => Bool -> a -> a
assert (Name -> Bool
isExternalName (CoAxiom Unbranched -> Name
forall (br :: BranchFlag). CoAxiom br -> Name
coAxiomName CoAxiom Unbranched
axiom)) (Module -> Module) -> Module -> Module
forall a b. (a -> b) -> a -> b
$
HasDebugCallStack => Name -> Module
Name -> Module
nameModule (CoAxiom Unbranched -> Name
forall (br :: BranchFlag). CoAxiom br -> Name
coAxiomName CoAxiom Unbranched
axiom)
is_local :: Name -> Bool
is_local Name
name = Module -> Name -> Bool
nameIsLocalOrFrom Module
mod Name
name
orph_names :: NameSet
orph_names = (Name -> Bool) -> NameSet -> NameSet
filterNameSet Name -> Bool
is_local (NameSet -> NameSet) -> NameSet -> NameSet
forall a b. (a -> b) -> a -> b
$
CoAxiom Unbranched -> NameSet
forall (br :: BranchFlag). CoAxiom br -> NameSet
orphNamesOfAxiomLHS CoAxiom Unbranched
axiom NameSet -> Name -> NameSet
`extendNameSet` Name
fam_tc_name
fam_tc_name :: Name
fam_tc_name = TyCon -> Name
tyConName (CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Unbranched
axiom)
mkImportedFamInst :: Name
-> [RoughMatchTc]
-> CoAxiom Unbranched
-> IsOrphan
-> FamInst
mkImportedFamInst :: Name -> [RoughMatchTc] -> CoAxiom Unbranched -> IsOrphan -> FamInst
mkImportedFamInst Name
fam [RoughMatchTc]
mb_tcs CoAxiom Unbranched
axiom IsOrphan
orphan
= 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,
fi_orphan :: IsOrphan
fi_orphan = IsOrphan
orphan }
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 HasDebugCallStack => 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 -> HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
Type.substTyAddInScope Subst
subst Type
rhs1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType`
HasDebugCallStack => Subst -> Type -> Type
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 = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
Type.substTys Subst
subst ([Type] -> [Type]
getInjArgs [Type]
lhs1)
lhs2Subst :: [Type]
lhs2Subst = HasDebugCallStack => 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 <- [Type] -> [Type] -> Maybe Subst
tcMatchTys [Type]
tpl_tys [Type]
match_tys1
return (FamInstMatch { fim_instance = item
, fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2
, fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $
substCoVars subst 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 -> CoAxiomRule -> [Type] -> [Coercion] -> Coercion
mkAxInstCo Role
role (CoAxiom Branched -> BranchIndex -> CoAxiomRule
BranchedAxiom 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
builtin_fam <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
tc
, Just (CoAxiomRule
rewrite,[Type]
ts,Type
ty) <- BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type)
tryMatchFam BuiltInSynFamily
builtin_fam [Type]
tys
= let co :: Coercion
co = CoAxiomRule -> [Coercion] -> Coercion
mkAxiomCo CoAxiomRule
rewrite ((Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
mkNomReflCo [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
; (ind, inst_tys, 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
; return ( ind, inst_tys `chkAppend` extra_tys, 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 { ((co, mkind_co), 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 = Reduction -> MCoercionN -> HetReduction
mkHetReduction (Coercion -> Type -> Reduction
mkReduction Coercion
co Type
nty) MCoercionN
mkind_co
; return $ homogeniseHetRedn Representational 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 HasDebugCallStack => Coercion -> Coercion -> Coercion
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
(HasDebugCallStack => 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 (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy ([(TyVar, Type)] -> Subst
mkTvSubstPrs [(TyVar, Type)]
tenv) Type
rhs) [Type]
tys')
| TyCon -> Bool
isFamilyTyCon TyCon
tc
=
do { env <- NormM (FamInstEnv, FamInstEnv)
getEnv
; role <- getRole
; ArgsReductions redns@(Reductions args_cos ntys) res_co <- normalise_tc_args tc tys
; case reduceTyFamApp_maybe env role tc ntys of
Just Reduction
redn1
-> do { redn2 <- Reduction -> NormM Reduction
normalise_reduction Reduction
redn1
; let redn3 = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc [Coercion]
args_cos Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn2
; return $ assemble_result role redn3 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 redns res_co <- TyCon -> [Type] -> NormM ArgsReductions
normalise_tc_args TyCon
tc [Type]
tys
; role <- getRole
; return $
assemble_result role (mkTyConAppRedn role tc redns) 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 <- NormM Role
getRole
; normalise_args (tyConKind tc) (tyConRolesX role tc) 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 { r <- NormM Role
getRole
; return $ mkReflRedn r 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 { arg_redn <- Type -> NormM Reduction
go Type
ty1
; res_redn <- go ty2
; w_redn <- withRole Nominal $ go w
; r <- getRole
; return $ mkFunRedn r vis w_redn arg_redn res_redn }
go (ForAllTy (Bndr TyVar
tcvar ForAllTyFlag
vis) Type
ty)
= do { (lc', tv', k_redn) <- TyVar -> NormM (LiftingContext, TyVar, Reduction)
normalise_var_bndr TyVar
tcvar
; redn <- withLC lc' $ normalise_type ty
; return $ mkForAllRedn vis tv' k_redn redn }
go (TyVarTy TyVar
tv) = TyVar -> NormM Reduction
normalise_tyvar TyVar
tv
go (CastTy Type
ty Coercion
co)
= do { redn <- Type -> NormM Reduction
go Type
ty
; lc <- getLC
; let co' = LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co
; return $ mkCastRedn2 Nominal ty co redn co'
}
go (CoercionTy Coercion
co)
= do { lc <- NormM LiftingContext
getLC
; r <- getRole
; let kco = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc (Coercion -> Type
coercionType Coercion
co)
co' = LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co
; return $ mkProofIrrelRedn r kco co 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_co nfun) <- Type -> NormM Reduction
go Type
fun_ty
; case tcSplitTyConApp_maybe nfun of
Just (TyCon
tc, [Type]
xis) ->
do { redn <- Type -> NormM Reduction
go (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type]
xis [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
arg_tys))
; return $
mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTransRedn` redn }
Maybe (TyCon, [Type])
Nothing ->
do { ArgsReductions redns res_co
<- Type -> Infinite Role -> [Type] -> NormM ArgsReductions
normalise_args (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
nfun)
(Role -> Infinite Role
forall a. a -> Infinite a
Inf.repeat Role
Nominal)
[Type]
arg_tys
; role <- getRole
; return $
mkCoherenceRightMRedn role
(mkAppRedns fun_redn redns)
(mkSymMCo 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 { 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
; return $ simplifyArgsWorker ki_binders inner_ki fvs roles 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 { lc <- NormM LiftingContext
getLC
; r <- getRole
; return $ case liftCoSubstTyVar lc r 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 { redn' <- Type -> NormM Reduction
normalise_type Type
ty
; return $ co `mkTransRedn` redn' }
normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Reduction)
normalise_var_bndr :: TyVar -> NormM (LiftingContext, TyVar, Reduction)
normalise_var_bndr TyVar
tcvar
= do { lc1 <- NormM LiftingContext
getLC
; env <- getEnv
; let 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
; return $ liftCoSubstVarBndrUsing reductionCoercion callback lc1 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