{-# LANGUAGE ScopedTypeVariables, PatternSynonyms, MultiWayIf #-}
{-# LANGUAGE DeriveFunctor #-}
module GHC.Core.Unify (
tcMatchTy, tcMatchTyKi,
tcMatchTys, tcMatchTyKis,
tcMatchTyX, tcMatchTysX, tcMatchTyKisX,
tcMatchTyX_BM, ruleMatchTyKiX,
tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
tcUnifyTysFG, tcUnifyTyWithTFs,
BindFun, BindFlag(..), matchBindFun, alwaysBindFun,
UnifyResult, UnifyResultM(..), MaybeApartReason(..),
typesCantMatch, typesAreApart,
liftCoMatch,
flattenTys, flattenTysX,
) where
import GHC.Prelude
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Name( Name, mkSysTvName, mkSystemVarName )
import GHC.Core.Type hiding ( getTvSubstEnv )
import GHC.Core.Coercion hiding ( getCvSubstEnv )
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Compare ( eqType, tcEqType )
import GHC.Core.TyCo.FVs ( tyCoVarsOfCoList, tyCoFVsOfTypes )
import GHC.Core.TyCo.Subst ( mkTvSubst, emptyIdSubstEnv )
import GHC.Core.Map.Type
import GHC.Utils.FV( FV, fvVarList )
import GHC.Utils.Misc
import GHC.Data.Pair
import GHC.Utils.Outputable
import GHC.Types.Unique
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set
import GHC.Exts( oneShot )
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Data.FastString
import Data.List ( mapAccumL )
import Control.Monad
import qualified Data.Semigroup as S
type BindFun = TyCoVar -> Type -> BindFlag
tcMatchTy :: Type -> Type -> Maybe Subst
tcMatchTy :: Type -> Type -> Maybe Subst
tcMatchTy Type
ty1 Type
ty2 = [Type] -> [Type] -> Maybe Subst
tcMatchTys [Type
ty1] [Type
ty2]
tcMatchTyX_BM :: BindFun -> Subst
-> Type -> Type -> Maybe Subst
tcMatchTyX_BM :: BindFun -> Subst -> Type -> Type -> Maybe Subst
tcMatchTyX_BM BindFun
bind_me Subst
subst Type
ty1 Type
ty2
= BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
bind_me Bool
False Subst
subst [Type
ty1] [Type
ty2]
tcMatchTyKi :: Type -> Type -> Maybe Subst
tcMatchTyKi :: Type -> Type -> Maybe Subst
tcMatchTyKi Type
ty1 Type
ty2
= BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
tc_match_tys BindFun
alwaysBindFun Bool
True [Type
ty1] [Type
ty2]
tcMatchTyX :: Subst
-> Type
-> Type
-> Maybe Subst
tcMatchTyX :: Subst -> Type -> Type -> Maybe Subst
tcMatchTyX Subst
subst Type
ty1 Type
ty2
= BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
alwaysBindFun Bool
False Subst
subst [Type
ty1] [Type
ty2]
tcMatchTys :: [Type]
-> [Type]
-> Maybe Subst
tcMatchTys :: [Type] -> [Type] -> Maybe Subst
tcMatchTys [Type]
tys1 [Type]
tys2
= BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
tc_match_tys BindFun
alwaysBindFun Bool
False [Type]
tys1 [Type]
tys2
tcMatchTyKis :: [Type]
-> [Type]
-> Maybe Subst
tcMatchTyKis :: [Type] -> [Type] -> Maybe Subst
tcMatchTyKis [Type]
tys1 [Type]
tys2
= BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
tc_match_tys BindFun
alwaysBindFun Bool
True [Type]
tys1 [Type]
tys2
tcMatchTysX :: Subst
-> [Type]
-> [Type]
-> Maybe Subst
tcMatchTysX :: Subst -> [Type] -> [Type] -> Maybe Subst
tcMatchTysX Subst
subst [Type]
tys1 [Type]
tys2
= BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
alwaysBindFun Bool
False Subst
subst [Type]
tys1 [Type]
tys2
tcMatchTyKisX :: Subst
-> [Type]
-> [Type]
-> Maybe Subst
tcMatchTyKisX :: Subst -> [Type] -> [Type] -> Maybe Subst
tcMatchTyKisX Subst
subst [Type]
tys1 [Type]
tys2
= BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
alwaysBindFun Bool
True Subst
subst [Type]
tys1 [Type]
tys2
tc_match_tys :: BindFun
-> Bool
-> [Type]
-> [Type]
-> Maybe Subst
tc_match_tys :: BindFun -> Bool -> [Type] -> [Type] -> Maybe Subst
tc_match_tys BindFun
bind_me Bool
match_kis [Type]
tys1 [Type]
tys2
= BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
bind_me Bool
match_kis (InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope) [Type]
tys1 [Type]
tys2
where
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
tyCoVarsOfTypes [Type]
tys1 VarSet -> VarSet -> VarSet
`unionVarSet` [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys2)
tc_match_tys_x :: BindFun
-> Bool
-> Subst
-> [Type]
-> [Type]
-> Maybe Subst
tc_match_tys_x :: BindFun -> Bool -> Subst -> [Type] -> [Type] -> Maybe Subst
tc_match_tys_x BindFun
bind_me Bool
match_kis (Subst InScopeSet
in_scope IdSubstEnv
id_env TvSubstEnv
tv_env CvSubstEnv
cv_env) [Type]
tys1 [Type]
tys2
= case BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys BindFun
bind_me
Bool
False
Bool
False
Bool
match_kis
(InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope) TvSubstEnv
tv_env CvSubstEnv
cv_env [Type]
tys1 [Type]
tys2 of
Unifiable (TvSubstEnv
tv_env', CvSubstEnv
cv_env')
-> Subst -> Maybe Subst
forall a. a -> Maybe a
Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
id_env TvSubstEnv
tv_env' CvSubstEnv
cv_env'
UnifyResultM (TvSubstEnv, CvSubstEnv)
_ -> Maybe Subst
forall a. Maybe a
Nothing
ruleMatchTyKiX
:: TyCoVarSet
-> RnEnv2
-> TvSubstEnv
-> Type
-> Type
-> Maybe TvSubstEnv
ruleMatchTyKiX :: VarSet -> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv
ruleMatchTyKiX VarSet
tmpl_tvs RnEnv2
rn_env TvSubstEnv
tenv Type
tmpl Type
target
= case BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys (VarSet -> BindFun
matchBindFun VarSet
tmpl_tvs) Bool
False Bool
False
Bool
True
RnEnv2
rn_env TvSubstEnv
tenv CvSubstEnv
emptyCvSubstEnv [Type
tmpl] [Type
target] of
Unifiable (TvSubstEnv
tenv', CvSubstEnv
_) -> TvSubstEnv -> Maybe TvSubstEnv
forall a. a -> Maybe a
Just TvSubstEnv
tenv'
UnifyResultM (TvSubstEnv, CvSubstEnv)
_ -> Maybe TvSubstEnv
forall a. Maybe a
Nothing
matchBindFun :: TyCoVarSet -> BindFun
matchBindFun :: VarSet -> BindFun
matchBindFun VarSet
tvs OutTyVar
tv Type
_ty
| OutTyVar
tv OutTyVar -> VarSet -> Bool
`elemVarSet` VarSet
tvs = BindFlag
BindMe
| Bool
otherwise = BindFlag
Apart
alwaysBindFun :: BindFun
alwaysBindFun :: BindFun
alwaysBindFun OutTyVar
_tv Type
_ty = BindFlag
BindMe
typesCantMatch :: [(Type,Type)] -> Bool
typesCantMatch :: [(Type, Type)] -> Bool
typesCantMatch [(Type, Type)]
prs = ((Type, Type) -> Bool) -> [(Type, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Type -> Type -> Bool) -> (Type, Type) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Type -> Type -> Bool
typesAreApart) [(Type, Type)]
prs
typesAreApart :: Type -> Type -> Bool
typesAreApart :: Type -> Type -> Bool
typesAreApart Type
t1 Type
t2 = case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
alwaysBindFun [Type
t1] [Type
t2] of
UnifyResult
SurelyApart -> Bool
True
UnifyResult
_ -> Bool
False
tcUnifyTy :: Type -> Type
-> Maybe Subst
tcUnifyTy :: Type -> Type -> Maybe Subst
tcUnifyTy Type
t1 Type
t2 = BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTys BindFun
alwaysBindFun [Type
t1] [Type
t2]
tcUnifyTyKi :: Type -> Type -> Maybe Subst
tcUnifyTyKi :: Type -> Type -> Maybe Subst
tcUnifyTyKi Type
t1 Type
t2 = BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTyKis BindFun
alwaysBindFun [Type
t1] [Type
t2]
tcUnifyTyWithTFs :: Bool
-> InScopeSet
-> Type -> Type
-> Maybe Subst
tcUnifyTyWithTFs :: Bool -> InScopeSet -> Type -> Type -> Maybe Subst
tcUnifyTyWithTFs Bool
twoWay InScopeSet
in_scope Type
t1 Type
t2
= case BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys BindFun
alwaysBindFun Bool
twoWay Bool
True Bool
False
RnEnv2
rn_env TvSubstEnv
emptyTvSubstEnv CvSubstEnv
emptyCvSubstEnv
[Type
t1] [Type
t2] of
Unifiable (TvSubstEnv
tv_subst, CvSubstEnv
_cv_subst) -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ TvSubstEnv -> Subst
maybe_fix TvSubstEnv
tv_subst
MaybeApart MaybeApartReason
_reason (TvSubstEnv
tv_subst, CvSubstEnv
_cv_subst) -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ TvSubstEnv -> Subst
maybe_fix TvSubstEnv
tv_subst
UnifyResultM (TvSubstEnv, CvSubstEnv)
SurelyApart -> Maybe Subst
forall a. Maybe a
Nothing
where
rn_env :: RnEnv2
rn_env = InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope
maybe_fix :: TvSubstEnv -> Subst
maybe_fix | Bool
twoWay = InScopeSet -> TvSubstEnv -> Subst
niFixSubst InScopeSet
in_scope
| Bool
otherwise = InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
in_scope
tcUnifyTys :: BindFun
-> [Type] -> [Type]
-> Maybe Subst
tcUnifyTys :: BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTys BindFun
bind_fn [Type]
tys1 [Type]
tys2
= case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
bind_fn [Type]
tys1 [Type]
tys2 of
Unifiable Subst
result -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
result
UnifyResult
_ -> Maybe Subst
forall a. Maybe a
Nothing
tcUnifyTyKis :: BindFun
-> [Type] -> [Type]
-> Maybe Subst
tcUnifyTyKis :: BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTyKis BindFun
bind_fn [Type]
tys1 [Type]
tys2
= case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTyKisFG BindFun
bind_fn [Type]
tys1 [Type]
tys2 of
Unifiable Subst
result -> Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
result
UnifyResult
_ -> Maybe Subst
forall a. Maybe a
Nothing
type UnifyResult = UnifyResultM Subst
data UnifyResultM a = Unifiable a
| MaybeApart MaybeApartReason
a
| SurelyApart
deriving (forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM b)
-> (forall a b. a -> UnifyResultM b -> UnifyResultM a)
-> Functor UnifyResultM
forall a b. a -> UnifyResultM b -> UnifyResultM a
forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM 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) -> UnifyResultM a -> UnifyResultM b
fmap :: forall a b. (a -> b) -> UnifyResultM a -> UnifyResultM b
$c<$ :: forall a b. a -> UnifyResultM b -> UnifyResultM a
<$ :: forall a b. a -> UnifyResultM b -> UnifyResultM a
Functor
data MaybeApartReason
= MARTypeFamily
| MARInfinite
| MARTypeVsConstraint
instance Outputable MaybeApartReason where
ppr :: MaybeApartReason -> SDoc
ppr MaybeApartReason
MARTypeFamily = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MARTypeFamily"
ppr MaybeApartReason
MARInfinite = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MARInfinite"
ppr MaybeApartReason
MARTypeVsConstraint = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MARTypeVsConstraint"
instance Semigroup MaybeApartReason where
MaybeApartReason
MARTypeFamily <> :: MaybeApartReason -> MaybeApartReason -> MaybeApartReason
<> MaybeApartReason
r = MaybeApartReason
r
MaybeApartReason
MARInfinite <> MaybeApartReason
_ = MaybeApartReason
MARInfinite
MaybeApartReason
MARTypeVsConstraint <> MaybeApartReason
r = MaybeApartReason
r
instance Applicative UnifyResultM where
pure :: forall a. a -> UnifyResultM a
pure = a -> UnifyResultM a
forall a. a -> UnifyResultM a
Unifiable
<*> :: forall a b.
UnifyResultM (a -> b) -> UnifyResultM a -> UnifyResultM b
(<*>) = UnifyResultM (a -> b) -> UnifyResultM a -> UnifyResultM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad UnifyResultM where
UnifyResultM a
SurelyApart >>= :: forall a b.
UnifyResultM a -> (a -> UnifyResultM b) -> UnifyResultM b
>>= a -> UnifyResultM b
_ = UnifyResultM b
forall a. UnifyResultM a
SurelyApart
MaybeApart MaybeApartReason
r1 a
x >>= a -> UnifyResultM b
f = case a -> UnifyResultM b
f a
x of
Unifiable b
y -> MaybeApartReason -> b -> UnifyResultM b
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart MaybeApartReason
r1 b
y
MaybeApart MaybeApartReason
r2 b
y -> MaybeApartReason -> b -> UnifyResultM b
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart (MaybeApartReason
r1 MaybeApartReason -> MaybeApartReason -> MaybeApartReason
forall a. Semigroup a => a -> a -> a
S.<> MaybeApartReason
r2) b
y
UnifyResultM b
SurelyApart -> UnifyResultM b
forall a. UnifyResultM a
SurelyApart
Unifiable a
x >>= a -> UnifyResultM b
f = a -> UnifyResultM b
f a
x
tcUnifyTysFG :: BindFun
-> [Type] -> [Type]
-> UnifyResult
tcUnifyTysFG :: BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
bind_fn [Type]
tys1 [Type]
tys2
= Bool -> BindFun -> [Type] -> [Type] -> UnifyResult
tc_unify_tys_fg Bool
False BindFun
bind_fn [Type]
tys1 [Type]
tys2
tcUnifyTyKisFG :: BindFun
-> [Type] -> [Type]
-> UnifyResult
tcUnifyTyKisFG :: BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTyKisFG BindFun
bind_fn [Type]
tys1 [Type]
tys2
= Bool -> BindFun -> [Type] -> [Type] -> UnifyResult
tc_unify_tys_fg Bool
True BindFun
bind_fn [Type]
tys1 [Type]
tys2
tc_unify_tys_fg :: Bool
-> BindFun
-> [Type] -> [Type]
-> UnifyResult
tc_unify_tys_fg :: Bool -> BindFun -> [Type] -> [Type] -> UnifyResult
tc_unify_tys_fg Bool
match_kis BindFun
bind_fn [Type]
tys1 [Type]
tys2
= do { (TvSubstEnv
env, CvSubstEnv
_) <- BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys BindFun
bind_fn Bool
True Bool
False Bool
match_kis RnEnv2
rn_env
TvSubstEnv
emptyTvSubstEnv CvSubstEnv
emptyCvSubstEnv
[Type]
tys1 [Type]
tys2
; Subst -> UnifyResult
forall a. a -> UnifyResultM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> UnifyResult) -> Subst -> UnifyResult
forall a b. (a -> b) -> a -> b
$ InScopeSet -> TvSubstEnv -> Subst
niFixSubst InScopeSet
in_scope TvSubstEnv
env }
where
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys1 VarSet -> VarSet -> VarSet
`unionVarSet` [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys2
rn_env :: RnEnv2
rn_env = InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope
tc_unify_tys :: BindFun
-> AmIUnifying
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type] -> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys :: BindFun
-> Bool
-> Bool
-> Bool
-> RnEnv2
-> TvSubstEnv
-> CvSubstEnv
-> [Type]
-> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys BindFun
bind_fn Bool
unif Bool
inj_check Bool
match_kis RnEnv2
rn_env TvSubstEnv
tv_env CvSubstEnv
cv_env [Type]
tys1 [Type]
tys2
= TvSubstEnv
-> CvSubstEnv
-> UM (TvSubstEnv, CvSubstEnv)
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
forall a. TvSubstEnv -> CvSubstEnv -> UM a -> UnifyResultM a
initUM TvSubstEnv
tv_env CvSubstEnv
cv_env (UM (TvSubstEnv, CvSubstEnv)
-> UnifyResultM (TvSubstEnv, CvSubstEnv))
-> UM (TvSubstEnv, CvSubstEnv)
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
forall a b. (a -> b) -> a -> b
$
do { Bool -> UM () -> UM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
match_kis (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$
UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
kis1 [Type]
kis2
; UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
tys1 [Type]
tys2
; (,) (TvSubstEnv -> CvSubstEnv -> (TvSubstEnv, CvSubstEnv))
-> UM TvSubstEnv -> UM (CvSubstEnv -> (TvSubstEnv, CvSubstEnv))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UM TvSubstEnv
getTvSubstEnv UM (CvSubstEnv -> (TvSubstEnv, CvSubstEnv))
-> UM CvSubstEnv -> UM (TvSubstEnv, CvSubstEnv)
forall a b. UM (a -> b) -> UM a -> UM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UM CvSubstEnv
getCvSubstEnv }
where
env :: UMEnv
env = UMEnv { um_bind_fun :: BindFun
um_bind_fun = BindFun
bind_fn
, um_skols :: VarSet
um_skols = VarSet
emptyVarSet
, um_unif :: Bool
um_unif = Bool
unif
, um_inj_tf :: Bool
um_inj_tf = Bool
inj_check
, um_rn_env :: RnEnv2
um_rn_env = RnEnv2
rn_env }
kis1 :: [Type]
kis1 = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (() :: Constraint) => Type -> Type
Type -> Type
typeKind [Type]
tys1
kis2 :: [Type]
kis2 = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (() :: Constraint) => Type -> Type
Type -> Type
typeKind [Type]
tys2
instance Outputable a => Outputable (UnifyResultM a) where
ppr :: UnifyResultM a -> SDoc
ppr UnifyResultM a
SurelyApart = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"SurelyApart"
ppr (Unifiable a
x) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Unifiable" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
x
ppr (MaybeApart MaybeApartReason
r a
x) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"MaybeApart" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> MaybeApartReason -> SDoc
forall a. Outputable a => a -> SDoc
ppr MaybeApartReason
r SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
x
niFixSubst :: InScopeSet -> TvSubstEnv -> Subst
niFixSubst :: InScopeSet -> TvSubstEnv -> Subst
niFixSubst InScopeSet
in_scope TvSubstEnv
tenv
| Bool
not_fixpoint = InScopeSet -> TvSubstEnv -> Subst
niFixSubst InScopeSet
in_scope ((Type -> Type) -> TvSubstEnv -> TvSubstEnv
forall a b. (a -> b) -> VarEnv a -> VarEnv b
mapVarEnv ((() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) TvSubstEnv
tenv)
| Bool
otherwise = Subst
subst
where
range_fvs :: FV
range_fvs :: FV
range_fvs = [Type] -> FV
tyCoFVsOfTypes (TvSubstEnv -> [Type]
forall key elt. UniqFM key elt -> [elt]
nonDetEltsUFM TvSubstEnv
tenv)
range_tvs :: [TyVar]
range_tvs :: [OutTyVar]
range_tvs = FV -> [OutTyVar]
fvVarList FV
range_fvs
not_fixpoint :: Bool
not_fixpoint = (OutTyVar -> Bool) -> [OutTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any OutTyVar -> Bool
in_domain [OutTyVar]
range_tvs
in_domain :: OutTyVar -> Bool
in_domain OutTyVar
tv = OutTyVar
tv OutTyVar -> TvSubstEnv -> Bool
forall a. OutTyVar -> VarEnv a -> Bool
`elemVarEnv` TvSubstEnv
tenv
free_tvs :: [OutTyVar]
free_tvs = [OutTyVar] -> [OutTyVar]
scopedSort ((OutTyVar -> Bool) -> [OutTyVar] -> [OutTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut OutTyVar -> Bool
in_domain [OutTyVar]
range_tvs)
subst :: Subst
subst = (Subst -> OutTyVar -> Subst) -> Subst -> [OutTyVar] -> Subst
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Subst -> OutTyVar -> Subst
add_free_tv
(InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
in_scope TvSubstEnv
tenv)
[OutTyVar]
free_tvs
add_free_tv :: Subst -> TyVar -> Subst
add_free_tv :: Subst -> OutTyVar -> Subst
add_free_tv Subst
subst OutTyVar
tv
= Subst -> OutTyVar -> Type -> Subst
extendTvSubst Subst
subst OutTyVar
tv (OutTyVar -> Type
mkTyVarTy OutTyVar
tv')
where
tv' :: OutTyVar
tv' = (Type -> Type) -> OutTyVar -> OutTyVar
updateTyVarKind ((() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) OutTyVar
tv
niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
niSubstTvSet :: TvSubstEnv -> VarSet -> VarSet
niSubstTvSet TvSubstEnv
tsubst VarSet
tvs
= (OutTyVar -> VarSet -> VarSet) -> VarSet -> VarSet -> VarSet
forall elt a. (elt -> a -> a) -> a -> UniqSet elt -> a
nonDetStrictFoldUniqSet (VarSet -> VarSet -> VarSet
unionVarSet (VarSet -> VarSet -> VarSet)
-> (OutTyVar -> VarSet) -> OutTyVar -> VarSet -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutTyVar -> VarSet
get) VarSet
emptyVarSet VarSet
tvs
where
get :: OutTyVar -> VarSet
get OutTyVar
tv
| Just Type
ty <- TvSubstEnv -> OutTyVar -> Maybe Type
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv TvSubstEnv
tsubst OutTyVar
tv
= TvSubstEnv -> VarSet -> VarSet
niSubstTvSet TvSubstEnv
tsubst (Type -> VarSet
tyCoVarsOfType Type
ty)
| Bool
otherwise
= OutTyVar -> VarSet
unitVarSet OutTyVar
tv
type AmIUnifying = Bool
unify_ty :: UMEnv
-> Type -> Type
-> CoercionN
-> UM ()
unify_ty :: UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
_env (TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 []) CoercionN
_kco
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
unify_ty UMEnv
env Type
ty1 Type
ty2 CoercionN
kco
| Just Type
ty1' <- Type -> Maybe Type
coreView Type
ty1 = UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1' Type
ty2 CoercionN
kco
| Just Type
ty2' <- Type -> Maybe Type
coreView Type
ty2 = UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1 Type
ty2' CoercionN
kco
| CastTy Type
ty1' CoercionN
co <- Type
ty1 = if UMEnv -> Bool
um_unif UMEnv
env
then UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1' Type
ty2 (CoercionN
co CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
kco)
else
do { Subst
subst <- UMEnv -> UM Subst
getSubst UMEnv
env
; let co' :: CoercionN
co' = (() :: Constraint) => Subst -> CoercionN -> CoercionN
Subst -> CoercionN -> CoercionN
substCo Subst
subst CoercionN
co
; UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1' Type
ty2 (CoercionN
co' CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
kco) }
| CastTy Type
ty2' CoercionN
co <- Type
ty2 = UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1 Type
ty2' (CoercionN
kco CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN -> CoercionN
mkSymCo CoercionN
co)
unify_ty UMEnv
env (TyVarTy OutTyVar
tv1) Type
ty2 CoercionN
kco
= UMEnv -> OutTyVar -> Type -> CoercionN -> UM ()
uVar UMEnv
env OutTyVar
tv1 Type
ty2 CoercionN
kco
unify_ty UMEnv
env Type
ty1 (TyVarTy OutTyVar
tv2) CoercionN
kco
| UMEnv -> Bool
um_unif UMEnv
env
= UMEnv -> OutTyVar -> Type -> CoercionN -> UM ()
uVar (UMEnv -> UMEnv
umSwapRn UMEnv
env) OutTyVar
tv2 Type
ty1 (CoercionN -> CoercionN
mkSymCo CoercionN
kco)
unify_ty UMEnv
env Type
ty1 Type
ty2 CoercionN
_kco
| Just (TyCon
tc1, [Type]
tys1) <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp Maybe (TyCon, [Type])
mb_tc_app1
, Just (TyCon
tc2, [Type]
tys2) <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp Maybe (TyCon, [Type])
mb_tc_app2
, TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= do { let inj :: [Bool]
inj = case TyCon -> Injectivity
tyConInjectivityInfo TyCon
tc1 of
Injectivity
NotInjective -> Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False
Injective [Bool]
bs -> [Bool]
bs
([Type]
inj_tys1, [Type]
noninj_tys1) = [Bool] -> [Type] -> ([Type], [Type])
forall a. [Bool] -> [a] -> ([a], [a])
partitionByList [Bool]
inj [Type]
tys1
([Type]
inj_tys2, [Type]
noninj_tys2) = [Bool] -> [Type] -> ([Type], [Type])
forall a. [Bool] -> [a] -> ([a], [a])
partitionByList [Bool]
inj [Type]
tys2
; UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
inj_tys1 [Type]
inj_tys2
; Bool -> UM () -> UM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (UMEnv -> Bool
um_inj_tf UMEnv
env) (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$
MaybeApartReason -> UM () -> UM ()
don'tBeSoSure MaybeApartReason
MARTypeFamily (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$ UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
noninj_tys1 [Type]
noninj_tys2 }
| Just (TyCon, [Type])
_ <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp Maybe (TyCon, [Type])
mb_tc_app1
= MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARTypeFamily
| Just (TyCon, [Type])
_ <- Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp Maybe (TyCon, [Type])
mb_tc_app2
= if UMEnv -> Bool
um_unif UMEnv
env then MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARTypeFamily else UM ()
forall a. UM a
surelyApart
| Just (TyCon
tc1, [Type]
_) <- Maybe (TyCon, [Type])
mb_tc_app1
, TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1
= if | Just (Type
ty1a, Type
ty1b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty1
, Just (Type
ty2a, Type
ty2b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty2
-> UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1a [Type
ty1b] Type
ty2a [Type
ty2b]
| Bool
otherwise -> UM ()
forall a. UM a
surelyApart
| Just (TyCon
tc2, [Type]
_) <- Maybe (TyCon, [Type])
mb_tc_app2
, TyCon -> Bool
isTypeFamilyTyCon TyCon
tc2
= if | Just (Type
ty1a, Type
ty1b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty1
, Just (Type
ty2a, Type
ty2b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty2
-> UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1a [Type
ty1b] Type
ty2a [Type
ty2b]
| Bool
otherwise -> UM ()
forall a. UM a
surelyApart
| Just (TyCon
tc1, [Type]
tys1) <- Maybe (TyCon, [Type])
mb_tc_app1
, Just (TyCon
tc2, [Type]
tys2) <- Maybe (TyCon, [Type])
mb_tc_app2
, TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= do { Bool -> SDoc -> UM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr (TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc1 Role
Nominal) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc1)
; UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
tys1 [Type]
tys2
}
| Just {} <- Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
ty1
, Just {} <- Type -> Maybe (TypeOrConstraint, Type)
sORTKind_maybe Type
ty2
= MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARTypeVsConstraint
| FunTy {} <- Type
ty1
, FunTy {} <- Type
ty2
= MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARTypeVsConstraint
where
mb_tc_app1 :: Maybe (TyCon, [Type])
mb_tc_app1 = (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
mb_tc_app2 :: Maybe (TyCon, [Type])
mb_tc_app2 = (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty2
unify_ty UMEnv
env (AppTy Type
ty1a Type
ty1b) Type
ty2 CoercionN
_kco
| Just (Type
ty2a, Type
ty2b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty2
= UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1a [Type
ty1b] Type
ty2a [Type
ty2b]
unify_ty UMEnv
env Type
ty1 (AppTy Type
ty2a Type
ty2b) CoercionN
_kco
| Just (Type
ty1a, Type
ty1b) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty1
= UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1a [Type
ty1b] Type
ty2a [Type
ty2b]
unify_ty UMEnv
_ (LitTy TyLit
x) (LitTy TyLit
y) CoercionN
_kco | TyLit
x TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
y = () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
unify_ty UMEnv
env (ForAllTy (Bndr OutTyVar
tv1 ForAllTyFlag
_) Type
ty1) (ForAllTy (Bndr OutTyVar
tv2 ForAllTyFlag
_) Type
ty2) CoercionN
kco
= do { UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env (OutTyVar -> Type
varType OutTyVar
tv1) (OutTyVar -> Type
varType OutTyVar
tv2) (Type -> CoercionN
mkNomReflCo Type
liftedTypeKind)
; let env' :: UMEnv
env' = UMEnv -> OutTyVar -> OutTyVar -> UMEnv
umRnBndr2 UMEnv
env OutTyVar
tv1 OutTyVar
tv2
; UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env' Type
ty1 Type
ty2 CoercionN
kco }
unify_ty UMEnv
env (CoercionTy CoercionN
co1) (CoercionTy CoercionN
co2) CoercionN
kco
= do { CvSubstEnv
c_subst <- UM CvSubstEnv
getCvSubstEnv
; case CoercionN
co1 of
CoVarCo OutTyVar
cv
| Bool -> Bool
not (UMEnv -> Bool
um_unif UMEnv
env)
, Bool -> Bool
not (OutTyVar
cv OutTyVar -> CvSubstEnv -> Bool
forall a. OutTyVar -> VarEnv a -> Bool
`elemVarEnv` CvSubstEnv
c_subst)
, let (CoercionN
_, CoercionN
co_l, CoercionN
co_r) = (() :: Constraint) =>
CoercionN -> (CoercionN, CoercionN, CoercionN)
CoercionN -> (CoercionN, CoercionN, CoercionN)
decomposeFunCo CoercionN
kco
rhs_co :: CoercionN
rhs_co = CoercionN
co_l CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
co2 CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN -> CoercionN
mkSymCo CoercionN
co_r
, BindFlag
BindMe <- UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
cv (CoercionN -> Type
CoercionTy CoercionN
rhs_co)
-> do { UMEnv -> VarSet -> UM ()
checkRnEnv UMEnv
env (CoercionN -> VarSet
tyCoVarsOfCo CoercionN
co2)
; OutTyVar -> CoercionN -> UM ()
extendCvEnv OutTyVar
cv CoercionN
rhs_co }
CoercionN
_ -> () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return () }
unify_ty UMEnv
_ Type
_ Type
_ CoercionN
_ = UM ()
forall a. UM a
surelyApart
unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1 [Type]
ty1args Type
ty2 [Type]
ty2args
| Just (Type
ty1', Type
ty1a) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty1
, Just (Type
ty2', Type
ty2a) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty2
= UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
unify_ty_app UMEnv
env Type
ty1' (Type
ty1a Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ty1args) Type
ty2' (Type
ty2a Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ty2args)
| Bool
otherwise
= do { let ki1 :: Type
ki1 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty1
ki2 :: Type
ki2 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty2
; UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ki1 Type
ki2 (Type -> CoercionN
mkNomReflCo Type
liftedTypeKind)
; UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty1 Type
ty2 (Type -> CoercionN
mkNomReflCo Type
ki2)
; UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
ty1args [Type]
ty2args }
unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
unify_tys UMEnv
env [Type]
orig_xs [Type]
orig_ys
= [Type] -> [Type] -> UM ()
go [Type]
orig_xs [Type]
orig_ys
where
go :: [Type] -> [Type] -> UM ()
go [] [] = () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go (Type
x:[Type]
xs) (Type
y:[Type]
ys)
= do { UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
x Type
y (Type -> CoercionN
mkNomReflCo (Type -> CoercionN) -> Type -> CoercionN
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
y)
; [Type] -> [Type] -> UM ()
go [Type]
xs [Type]
ys }
go [Type]
_ [Type]
_ = UM ()
forall a. UM a
surelyApart
isSatTyFamApp :: Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp :: Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
isSatTyFamApp tapp :: Maybe (TyCon, [Type])
tapp@(Just (TyCon
tc, [Type]
tys))
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
Bool -> Bool -> Bool
&& Bool -> Bool
not ([Type]
tys [Type] -> Arity -> Bool
forall a. [a] -> Arity -> Bool
`lengthExceeds` TyCon -> Arity
tyConArity TyCon
tc)
= Maybe (TyCon, [Type])
tapp
isSatTyFamApp Maybe (TyCon, [Type])
_ = Maybe (TyCon, [Type])
forall a. Maybe a
Nothing
uVar :: UMEnv
-> InTyVar
-> Type
-> Coercion
-> UM ()
uVar :: UMEnv -> OutTyVar -> Type -> CoercionN -> UM ()
uVar UMEnv
env OutTyVar
tv1 Type
ty CoercionN
kco
= do {
let tv1' :: OutTyVar
tv1' = UMEnv -> OutTyVar -> OutTyVar
umRnOccL UMEnv
env OutTyVar
tv1
; TvSubstEnv
subst <- UM TvSubstEnv
getTvSubstEnv
; case (TvSubstEnv -> OutTyVar -> Maybe Type
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv TvSubstEnv
subst OutTyVar
tv1') of
Just Type
ty' | UMEnv -> Bool
um_unif UMEnv
env
-> UMEnv -> Type -> Type -> CoercionN -> UM ()
unify_ty UMEnv
env Type
ty' Type
ty CoercionN
kco
| Bool
otherwise
->
Bool -> UM () -> UM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Type
ty' Type -> CoercionN -> Type
`mkCastTy` CoercionN
kco) (() :: Constraint) => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty) (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$
UM ()
forall a. UM a
surelyApart
Maybe Type
Nothing -> UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
uUnrefined UMEnv
env OutTyVar
tv1' Type
ty Type
ty CoercionN
kco }
uUnrefined :: UMEnv
-> OutTyVar
-> Type
-> Type
-> Coercion
-> UM ()
uUnrefined :: UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
uUnrefined UMEnv
env OutTyVar
tv1' Type
ty2 Type
ty2' CoercionN
kco
| Just Type
ty2'' <- Type -> Maybe Type
coreView Type
ty2'
= UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
uUnrefined UMEnv
env OutTyVar
tv1' Type
ty2 Type
ty2'' CoercionN
kco
| TyVarTy OutTyVar
tv2 <- Type
ty2'
= do { let tv2' :: OutTyVar
tv2' = UMEnv -> OutTyVar -> OutTyVar
umRnOccR UMEnv
env OutTyVar
tv2
; Bool -> UM () -> UM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (OutTyVar
tv1' OutTyVar -> OutTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== OutTyVar
tv2' Bool -> Bool -> Bool
&& UMEnv -> Bool
um_unif UMEnv
env) (UM () -> UM ()) -> UM () -> UM ()
forall a b. (a -> b) -> a -> b
$ do
{ TvSubstEnv
subst <- UM TvSubstEnv
getTvSubstEnv
; case TvSubstEnv -> OutTyVar -> Maybe Type
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv TvSubstEnv
subst OutTyVar
tv2 of
{ Just Type
ty' | UMEnv -> Bool
um_unif UMEnv
env -> UMEnv -> OutTyVar -> Type -> Type -> CoercionN -> UM ()
uUnrefined UMEnv
env OutTyVar
tv1' Type
ty' Type
ty' CoercionN
kco
; Maybe Type
_ ->
do {
; let rhs1 :: Type
rhs1 = Type
ty2 Type -> CoercionN -> Type
`mkCastTy` CoercionN -> CoercionN
mkSymCo CoercionN
kco
rhs2 :: Type
rhs2 = Type
ty1 Type -> CoercionN -> Type
`mkCastTy` CoercionN
kco
b1 :: BindFlag
b1 = UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
tv1' Type
rhs1
b2 :: BindFlag
b2 = UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
tv2' Type
rhs2
ty1 :: Type
ty1 = OutTyVar -> Type
mkTyVarTy OutTyVar
tv1'
; case (BindFlag
b1, BindFlag
b2) of
(BindFlag
BindMe, BindFlag
_) -> UMEnv -> OutTyVar -> Type -> UM ()
bindTv UMEnv
env OutTyVar
tv1' Type
rhs1
(BindFlag
_, BindFlag
BindMe) | UMEnv -> Bool
um_unif UMEnv
env
-> UMEnv -> OutTyVar -> Type -> UM ()
bindTv (UMEnv -> UMEnv
umSwapRn UMEnv
env) OutTyVar
tv2 Type
rhs2
(BindFlag, BindFlag)
_ | OutTyVar
tv1' OutTyVar -> OutTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== OutTyVar
tv2' -> () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(BindFlag, BindFlag)
_ -> UM ()
forall a. UM a
surelyApart
}}}}
uUnrefined UMEnv
env OutTyVar
tv1' Type
ty2 Type
_ CoercionN
kco
= case UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
tv1' Type
rhs of
BindFlag
Apart -> UM ()
forall a. UM a
surelyApart
BindFlag
BindMe -> UMEnv -> OutTyVar -> Type -> UM ()
bindTv UMEnv
env OutTyVar
tv1' Type
rhs
where
rhs :: Type
rhs = Type
ty2 Type -> CoercionN -> Type
`mkCastTy` CoercionN -> CoercionN
mkSymCo CoercionN
kco
bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
bindTv UMEnv
env OutTyVar
tv1 Type
ty2
= do { let free_tvs2 :: VarSet
free_tvs2 = Type -> VarSet
tyCoVarsOfType Type
ty2
; UMEnv -> VarSet -> UM ()
checkRnEnv UMEnv
env VarSet
free_tvs2
; Bool
occurs <- UMEnv -> OutTyVar -> VarSet -> UM Bool
occursCheck UMEnv
env OutTyVar
tv1 VarSet
free_tvs2
; if Bool
occurs then MaybeApartReason -> UM ()
maybeApart MaybeApartReason
MARInfinite
else OutTyVar -> Type -> UM ()
extendTvEnv OutTyVar
tv1 Type
ty2 }
occursCheck :: UMEnv -> TyVar -> VarSet -> UM Bool
occursCheck :: UMEnv -> OutTyVar -> VarSet -> UM Bool
occursCheck UMEnv
env OutTyVar
tv VarSet
free_tvs
| UMEnv -> Bool
um_unif UMEnv
env
= do { TvSubstEnv
tsubst <- UM TvSubstEnv
getTvSubstEnv
; Bool -> UM Bool
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return (OutTyVar
tv OutTyVar -> VarSet -> Bool
`elemVarSet` TvSubstEnv -> VarSet -> VarSet
niSubstTvSet TvSubstEnv
tsubst VarSet
free_tvs) }
| Bool
otherwise
= Bool -> UM Bool
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
data BindFlag
= BindMe
| Apart
deriving BindFlag -> BindFlag -> Bool
(BindFlag -> BindFlag -> Bool)
-> (BindFlag -> BindFlag -> Bool) -> Eq BindFlag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BindFlag -> BindFlag -> Bool
== :: BindFlag -> BindFlag -> Bool
$c/= :: BindFlag -> BindFlag -> Bool
/= :: BindFlag -> BindFlag -> Bool
Eq
data UMEnv
= UMEnv { UMEnv -> Bool
um_unif :: AmIUnifying
, UMEnv -> Bool
um_inj_tf :: Bool
, UMEnv -> RnEnv2
um_rn_env :: RnEnv2
, UMEnv -> VarSet
um_skols :: TyVarSet
, UMEnv -> BindFun
um_bind_fun :: BindFun
}
data UMState = UMState
{ UMState -> TvSubstEnv
um_tv_env :: TvSubstEnv
, UMState -> CvSubstEnv
um_cv_env :: CvSubstEnv }
newtype UM a
= UM' { forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM :: UMState -> UnifyResultM (UMState, a) }
deriving ((forall a b. (a -> b) -> UM a -> UM b)
-> (forall a b. a -> UM b -> UM a) -> Functor UM
forall a b. a -> UM b -> UM a
forall a b. (a -> b) -> UM a -> UM 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) -> UM a -> UM b
fmap :: forall a b. (a -> b) -> UM a -> UM b
$c<$ :: forall a b. a -> UM b -> UM a
<$ :: forall a b. a -> UM b -> UM a
Functor)
pattern UM :: (UMState -> UnifyResultM (UMState, a)) -> UM a
pattern $mUM :: forall {r} {a}.
UM a
-> ((UMState -> UnifyResultM (UMState, a)) -> r)
-> ((# #) -> r)
-> r
$bUM :: forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM m <- UM' m
where
UM UMState -> UnifyResultM (UMState, a)
m = (UMState -> UnifyResultM (UMState, a)) -> UM a
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM' ((UMState -> UnifyResultM (UMState, a))
-> UMState -> UnifyResultM (UMState, a)
forall a b. (a -> b) -> a -> b
oneShot UMState -> UnifyResultM (UMState, a)
m)
instance Applicative UM where
pure :: forall a. a -> UM a
pure a
a = (UMState -> UnifyResultM (UMState, a)) -> UM a
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
s -> (UMState, a) -> UnifyResultM (UMState, a)
forall a. a -> UnifyResultM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UMState
s, a
a))
<*> :: forall a b. UM (a -> b) -> UM a -> UM b
(<*>) = UM (a -> b) -> UM a -> UM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad UM where
{-# INLINE (>>=) #-}
UM a
m >>= :: forall a b. UM a -> (a -> UM b) -> UM b
>>= a -> UM b
k = (UMState -> UnifyResultM (UMState, b)) -> UM b
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
state ->
do { (UMState
state', a
v) <- UM a -> UMState -> UnifyResultM (UMState, a)
forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM UM a
m UMState
state
; UM b -> UMState -> UnifyResultM (UMState, b)
forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM (a -> UM b
k a
v) UMState
state' })
instance MonadFail UM where
fail :: forall a. String -> UM a
fail String
_ = (UMState -> UnifyResultM (UMState, a)) -> UM a
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
_ -> UnifyResultM (UMState, a)
forall a. UnifyResultM a
SurelyApart)
initUM :: TvSubstEnv
-> CvSubstEnv
-> UM a -> UnifyResultM a
initUM :: forall a. TvSubstEnv -> CvSubstEnv -> UM a -> UnifyResultM a
initUM TvSubstEnv
subst_env CvSubstEnv
cv_subst_env UM a
um
= case UM a -> UMState -> UnifyResultM (UMState, a)
forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM UM a
um UMState
state of
Unifiable (UMState
_, a
subst) -> a -> UnifyResultM a
forall a. a -> UnifyResultM a
Unifiable a
subst
MaybeApart MaybeApartReason
r (UMState
_, a
subst) -> MaybeApartReason -> a -> UnifyResultM a
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart MaybeApartReason
r a
subst
UnifyResultM (UMState, a)
SurelyApart -> UnifyResultM a
forall a. UnifyResultM a
SurelyApart
where
state :: UMState
state = UMState { um_tv_env :: TvSubstEnv
um_tv_env = TvSubstEnv
subst_env
, um_cv_env :: CvSubstEnv
um_cv_env = CvSubstEnv
cv_subst_env }
tvBindFlag :: UMEnv -> OutTyVar -> Type -> BindFlag
tvBindFlag :: UMEnv -> BindFun
tvBindFlag UMEnv
env OutTyVar
tv Type
rhs
| OutTyVar
tv OutTyVar -> VarSet -> Bool
`elemVarSet` UMEnv -> VarSet
um_skols UMEnv
env = BindFlag
Apart
| Bool
otherwise = UMEnv -> BindFun
um_bind_fun UMEnv
env OutTyVar
tv Type
rhs
getTvSubstEnv :: UM TvSubstEnv
getTvSubstEnv :: UM TvSubstEnv
getTvSubstEnv = (UMState -> UnifyResultM (UMState, TvSubstEnv)) -> UM TvSubstEnv
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, TvSubstEnv)) -> UM TvSubstEnv)
-> (UMState -> UnifyResultM (UMState, TvSubstEnv)) -> UM TvSubstEnv
forall a b. (a -> b) -> a -> b
$ \UMState
state -> (UMState, TvSubstEnv) -> UnifyResultM (UMState, TvSubstEnv)
forall a. a -> UnifyResultM a
Unifiable (UMState
state, UMState -> TvSubstEnv
um_tv_env UMState
state)
getCvSubstEnv :: UM CvSubstEnv
getCvSubstEnv :: UM CvSubstEnv
getCvSubstEnv = (UMState -> UnifyResultM (UMState, CvSubstEnv)) -> UM CvSubstEnv
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, CvSubstEnv)) -> UM CvSubstEnv)
-> (UMState -> UnifyResultM (UMState, CvSubstEnv)) -> UM CvSubstEnv
forall a b. (a -> b) -> a -> b
$ \UMState
state -> (UMState, CvSubstEnv) -> UnifyResultM (UMState, CvSubstEnv)
forall a. a -> UnifyResultM a
Unifiable (UMState
state, UMState -> CvSubstEnv
um_cv_env UMState
state)
getSubst :: UMEnv -> UM Subst
getSubst :: UMEnv -> UM Subst
getSubst UMEnv
env = do { TvSubstEnv
tv_env <- UM TvSubstEnv
getTvSubstEnv
; CvSubstEnv
cv_env <- UM CvSubstEnv
getCvSubstEnv
; let in_scope :: InScopeSet
in_scope = RnEnv2 -> InScopeSet
rnInScopeSet (UMEnv -> RnEnv2
um_rn_env UMEnv
env)
; Subst -> UM Subst
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return (InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst
mkSubst InScopeSet
in_scope TvSubstEnv
tv_env CvSubstEnv
cv_env IdSubstEnv
emptyIdSubstEnv) }
extendTvEnv :: TyVar -> Type -> UM ()
extendTvEnv :: OutTyVar -> Type -> UM ()
extendTvEnv OutTyVar
tv Type
ty = (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, ())) -> UM ())
-> (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a b. (a -> b) -> a -> b
$ \UMState
state ->
(UMState, ()) -> UnifyResultM (UMState, ())
forall a. a -> UnifyResultM a
Unifiable (UMState
state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
extendCvEnv :: CoVar -> Coercion -> UM ()
extendCvEnv :: OutTyVar -> CoercionN -> UM ()
extendCvEnv OutTyVar
cv CoercionN
co = (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, ())) -> UM ())
-> (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a b. (a -> b) -> a -> b
$ \UMState
state ->
(UMState, ()) -> UnifyResultM (UMState, ())
forall a. a -> UnifyResultM a
Unifiable (UMState
state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
umRnBndr2 :: UMEnv -> OutTyVar -> OutTyVar -> UMEnv
umRnBndr2 UMEnv
env OutTyVar
v1 OutTyVar
v2
= UMEnv
env { um_rn_env = rn_env', um_skols = um_skols env `extendVarSet` v' }
where
(RnEnv2
rn_env', OutTyVar
v') = RnEnv2 -> OutTyVar -> OutTyVar -> (RnEnv2, OutTyVar)
rnBndr2_var (UMEnv -> RnEnv2
um_rn_env UMEnv
env) OutTyVar
v1 OutTyVar
v2
checkRnEnv :: UMEnv -> VarSet -> UM ()
checkRnEnv :: UMEnv -> VarSet -> UM ()
checkRnEnv UMEnv
env VarSet
varset
| VarSet -> Bool
isEmptyVarSet VarSet
skol_vars = () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| VarSet
varset VarSet -> VarSet -> Bool
`disjointVarSet` VarSet
skol_vars = () -> UM ()
forall a. a -> UM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = UM ()
forall a. UM a
surelyApart
where
skol_vars :: VarSet
skol_vars = UMEnv -> VarSet
um_skols UMEnv
env
don'tBeSoSure :: MaybeApartReason -> UM () -> UM ()
don'tBeSoSure :: MaybeApartReason -> UM () -> UM ()
don'tBeSoSure MaybeApartReason
r UM ()
um = (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM ((UMState -> UnifyResultM (UMState, ())) -> UM ())
-> (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a b. (a -> b) -> a -> b
$ \ UMState
state ->
case UM () -> UMState -> UnifyResultM (UMState, ())
forall a. UM a -> UMState -> UnifyResultM (UMState, a)
unUM UM ()
um UMState
state of
UnifyResultM (UMState, ())
SurelyApart -> MaybeApartReason -> (UMState, ()) -> UnifyResultM (UMState, ())
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart MaybeApartReason
r (UMState
state, ())
UnifyResultM (UMState, ())
other -> UnifyResultM (UMState, ())
other
umRnOccL :: UMEnv -> TyVar -> TyVar
umRnOccL :: UMEnv -> OutTyVar -> OutTyVar
umRnOccL UMEnv
env OutTyVar
v = RnEnv2 -> OutTyVar -> OutTyVar
rnOccL (UMEnv -> RnEnv2
um_rn_env UMEnv
env) OutTyVar
v
umRnOccR :: UMEnv -> TyVar -> TyVar
umRnOccR :: UMEnv -> OutTyVar -> OutTyVar
umRnOccR UMEnv
env OutTyVar
v = RnEnv2 -> OutTyVar -> OutTyVar
rnOccR (UMEnv -> RnEnv2
um_rn_env UMEnv
env) OutTyVar
v
umSwapRn :: UMEnv -> UMEnv
umSwapRn :: UMEnv -> UMEnv
umSwapRn UMEnv
env = UMEnv
env { um_rn_env = rnSwap (um_rn_env env) }
maybeApart :: MaybeApartReason -> UM ()
maybeApart :: MaybeApartReason -> UM ()
maybeApart MaybeApartReason
r = (UMState -> UnifyResultM (UMState, ())) -> UM ()
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
state -> MaybeApartReason -> (UMState, ()) -> UnifyResultM (UMState, ())
forall a. MaybeApartReason -> a -> UnifyResultM a
MaybeApart MaybeApartReason
r (UMState
state, ()))
surelyApart :: UM a
surelyApart :: forall a. UM a
surelyApart = (UMState -> UnifyResultM (UMState, a)) -> UM a
forall a. (UMState -> UnifyResultM (UMState, a)) -> UM a
UM (\UMState
_ -> UnifyResultM (UMState, a)
forall a. UnifyResultM a
SurelyApart)
data MatchEnv = ME { MatchEnv -> VarSet
me_tmpls :: TyVarSet
, MatchEnv -> RnEnv2
me_env :: RnEnv2 }
liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
liftCoMatch :: VarSet -> Type -> CoercionN -> Maybe LiftingContext
liftCoMatch VarSet
tmpls Type
ty CoercionN
co
= do { CvSubstEnv
cenv1 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
forall a. VarEnv a
emptyVarEnv Type
ki CoercionN
ki_co CoercionN
ki_ki_co CoercionN
ki_ki_co
; CvSubstEnv
cenv2 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
cenv1 Type
ty CoercionN
co
(Type -> CoercionN
mkNomReflCo Type
co_lkind) (Type -> CoercionN
mkNomReflCo Type
co_rkind)
; LiftingContext -> Maybe LiftingContext
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> CvSubstEnv -> LiftingContext
LC (InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope) CvSubstEnv
cenv2) }
where
menv :: MatchEnv
menv = ME { me_tmpls :: VarSet
me_tmpls = VarSet
tmpls, me_env :: RnEnv2
me_env = InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope }
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet
tmpls VarSet -> VarSet -> VarSet
`unionVarSet` CoercionN -> VarSet
tyCoVarsOfCo CoercionN
co)
ki :: Type
ki = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty
ki_co :: CoercionN
ki_co = CoercionN -> CoercionN
promoteCoercion CoercionN
co
ki_ki_co :: CoercionN
ki_ki_co = Type -> CoercionN
mkNomReflCo Type
liftedTypeKind
Pair Type
co_lkind Type
co_rkind = CoercionN -> Pair Type
coercionKind CoercionN
ki_co
ty_co_match :: MatchEnv
-> LiftCoEnv
-> Type
-> Coercion
-> Coercion
-> Coercion
-> Maybe LiftCoEnv
ty_co_match :: MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co CoercionN
lkco CoercionN
rkco
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty' CoercionN
co CoercionN
lkco CoercionN
rkco
| Type -> VarSet
tyCoVarsOfType Type
ty VarSet -> CvSubstEnv -> Bool
forall a. VarSet -> VarEnv a -> Bool
`isNotInDomainOf` CvSubstEnv
subst
, Just (Type
ty', Role
_) <- CoercionN -> Maybe (Type, Role)
isReflCo_maybe CoercionN
co
, Type
ty Type -> Type -> Bool
`eqType` Type
ty'
= CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just CvSubstEnv
subst
where
isNotInDomainOf :: VarSet -> VarEnv a -> Bool
isNotInDomainOf :: forall a. VarSet -> VarEnv a -> Bool
isNotInDomainOf VarSet
set VarEnv a
env
= (OutTyVar -> Bool) -> VarSet -> Bool
noneSet (\OutTyVar
v -> OutTyVar -> VarEnv a -> Bool
forall a. OutTyVar -> VarEnv a -> Bool
elemVarEnv OutTyVar
v VarEnv a
env) VarSet
set
noneSet :: (Var -> Bool) -> VarSet -> Bool
noneSet :: (OutTyVar -> Bool) -> VarSet -> Bool
noneSet OutTyVar -> Bool
f = (OutTyVar -> Bool) -> VarSet -> Bool
allVarSet (Bool -> Bool
not (Bool -> Bool) -> (OutTyVar -> Bool) -> OutTyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutTyVar -> Bool
f)
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co CoercionN
lkco CoercionN
rkco
| CastTy Type
ty' CoercionN
co' <- Type
ty
= let empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst (RnEnv2 -> InScopeSet
rnInScopeSet (MatchEnv -> RnEnv2
me_env MatchEnv
menv))
substed_co_l :: CoercionN
substed_co_l = (() :: Constraint) => Subst -> CoercionN -> CoercionN
Subst -> CoercionN -> CoercionN
substCo (Subst -> CvSubstEnv -> Subst
liftEnvSubstLeft Subst
empty_subst CvSubstEnv
subst) CoercionN
co'
substed_co_r :: CoercionN
substed_co_r = (() :: Constraint) => Subst -> CoercionN -> CoercionN
Subst -> CoercionN -> CoercionN
substCo (Subst -> CvSubstEnv -> Subst
liftEnvSubstRight Subst
empty_subst CvSubstEnv
subst) CoercionN
co'
in
MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty' CoercionN
co (CoercionN
substed_co_l CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
lkco)
(CoercionN
substed_co_r CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
rkco)
| SymCo CoercionN
co' <- CoercionN
co
= CvSubstEnv -> CvSubstEnv
swapLiftCoEnv (CvSubstEnv -> CvSubstEnv) -> Maybe CvSubstEnv -> Maybe CvSubstEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv (CvSubstEnv -> CvSubstEnv
swapLiftCoEnv CvSubstEnv
subst) Type
ty CoercionN
co' CoercionN
rkco CoercionN
lkco
ty_co_match MatchEnv
menv CvSubstEnv
subst (TyVarTy OutTyVar
tv1) CoercionN
co CoercionN
lkco CoercionN
rkco
| Just CoercionN
co1' <- CvSubstEnv -> OutTyVar -> Maybe CoercionN
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv CvSubstEnv
subst OutTyVar
tv1'
= if RnEnv2 -> CoercionN -> CoercionN -> Bool
eqCoercionX (RnEnv2 -> RnEnv2
nukeRnEnvL RnEnv2
rn_env) CoercionN
co1' CoercionN
co
then CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just CvSubstEnv
subst
else Maybe CvSubstEnv
forall a. Maybe a
Nothing
| OutTyVar
tv1' OutTyVar -> VarSet -> Bool
`elemVarSet` MatchEnv -> VarSet
me_tmpls MatchEnv
menv
= if (OutTyVar -> Bool) -> [OutTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RnEnv2 -> OutTyVar -> Bool
inRnEnvR RnEnv2
rn_env) (CoercionN -> [OutTyVar]
tyCoVarsOfCoList CoercionN
co)
then Maybe CvSubstEnv
forall a. Maybe a
Nothing
else CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just (CvSubstEnv -> Maybe CvSubstEnv) -> CvSubstEnv -> Maybe CvSubstEnv
forall a b. (a -> b) -> a -> b
$ CvSubstEnv -> OutTyVar -> CoercionN -> CvSubstEnv
forall a. VarEnv a -> OutTyVar -> a -> VarEnv a
extendVarEnv CvSubstEnv
subst OutTyVar
tv1' (CoercionN -> CvSubstEnv) -> CoercionN -> CvSubstEnv
forall a b. (a -> b) -> a -> b
$
CoercionN -> CoercionN -> CoercionN -> CoercionN
castCoercionKind CoercionN
co (CoercionN -> CoercionN
mkSymCo CoercionN
lkco) (CoercionN -> CoercionN
mkSymCo CoercionN
rkco)
| Bool
otherwise
= Maybe CvSubstEnv
forall a. Maybe a
Nothing
where
rn_env :: RnEnv2
rn_env = MatchEnv -> RnEnv2
me_env MatchEnv
menv
tv1' :: OutTyVar
tv1' = RnEnv2 -> OutTyVar -> OutTyVar
rnOccL RnEnv2
rn_env OutTyVar
tv1
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty (SubCo CoercionN
co) CoercionN
lkco CoercionN
rkco
= MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co CoercionN
lkco CoercionN
rkco
ty_co_match MatchEnv
menv CvSubstEnv
subst (AppTy Type
ty1a Type
ty1b) CoercionN
co CoercionN
_lkco CoercionN
_rkco
| Just (CoercionN
co2, CoercionN
arg2) <- CoercionN -> Maybe (CoercionN, CoercionN)
splitAppCo_maybe CoercionN
co
= MatchEnv
-> CvSubstEnv
-> Type
-> [Type]
-> CoercionN
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_app MatchEnv
menv CvSubstEnv
subst Type
ty1a [Type
ty1b] CoercionN
co2 [CoercionN
arg2]
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty1 (AppCo CoercionN
co2 CoercionN
arg2) CoercionN
_lkco CoercionN
_rkco
| Just (Type
ty1a, Type
ty1b) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty1
= MatchEnv
-> CvSubstEnv
-> Type
-> [Type]
-> CoercionN
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_app MatchEnv
menv CvSubstEnv
subst Type
ty1a [Type
ty1b] CoercionN
co2 [CoercionN
arg2]
ty_co_match MatchEnv
menv CvSubstEnv
subst (TyConApp TyCon
tc1 [Type]
tys) (TyConAppCo Role
_ TyCon
tc2 [CoercionN]
cos) CoercionN
_lkco CoercionN
_rkco
= MatchEnv
-> CvSubstEnv
-> TyCon
-> [Type]
-> TyCon
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_tc MatchEnv
menv CvSubstEnv
subst TyCon
tc1 [Type]
tys TyCon
tc2 [CoercionN]
cos
ty_co_match MatchEnv
menv CvSubstEnv
subst (FunTy { ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
(FunCo { fco_mult :: CoercionN -> CoercionN
fco_mult = CoercionN
co_w, fco_arg :: CoercionN -> CoercionN
fco_arg = CoercionN
co1, fco_res :: CoercionN -> CoercionN
fco_res = CoercionN
co2 }) CoercionN
_lkco CoercionN
_rkco
= MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst [Type
w, Type
rep1, Type
rep2, Type
ty1, Type
ty2]
[CoercionN
co_w, CoercionN
co1_rep, CoercionN
co2_rep, CoercionN
co1, CoercionN
co2]
where
rep1 :: Type
rep1 = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty1
rep2 :: Type
rep2 = (() :: Constraint) => Type -> Type
Type -> Type
getRuntimeRep Type
ty2
co1_rep :: CoercionN
co1_rep = (() :: Constraint) => CoercionN -> CoercionN
CoercionN -> CoercionN
mkRuntimeRepCo CoercionN
co1
co2_rep :: CoercionN
co2_rep = (() :: Constraint) => CoercionN -> CoercionN
CoercionN -> CoercionN
mkRuntimeRepCo CoercionN
co2
ty_co_match MatchEnv
menv CvSubstEnv
subst (ForAllTy (Bndr OutTyVar
tv1 ForAllTyFlag
_) Type
ty1)
(ForAllCo OutTyVar
tv2 CoercionN
kind_co2 CoercionN
co2)
CoercionN
lkco CoercionN
rkco
| OutTyVar -> Bool
isTyVar OutTyVar
tv1 Bool -> Bool -> Bool
&& OutTyVar -> Bool
isTyVar OutTyVar
tv2
= do { CvSubstEnv
subst1 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst (OutTyVar -> Type
tyVarKind OutTyVar
tv1) CoercionN
kind_co2
CoercionN
ki_ki_co CoercionN
ki_ki_co
; let rn_env0 :: RnEnv2
rn_env0 = MatchEnv -> RnEnv2
me_env MatchEnv
menv
rn_env1 :: RnEnv2
rn_env1 = RnEnv2 -> OutTyVar -> OutTyVar -> RnEnv2
rnBndr2 RnEnv2
rn_env0 OutTyVar
tv1 OutTyVar
tv2
menv' :: MatchEnv
menv' = MatchEnv
menv { me_env = rn_env1 }
; MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv' CvSubstEnv
subst1 Type
ty1 CoercionN
co2 CoercionN
lkco CoercionN
rkco }
where
ki_ki_co :: CoercionN
ki_ki_co = Type -> CoercionN
mkNomReflCo Type
liftedTypeKind
ty_co_match MatchEnv
_ CvSubstEnv
subst (CoercionTy {}) CoercionN
_ CoercionN
_ CoercionN
_
= CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just CvSubstEnv
subst
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty (GRefl Role
r Type
t (MCo CoercionN
co)) CoercionN
lkco CoercionN
rkco
= MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty (Role -> Type -> MCoercion -> CoercionN
GRefl Role
r Type
t MCoercion
MRefl) CoercionN
lkco (CoercionN
rkco CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN -> CoercionN
mkSymCo CoercionN
co)
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co1 CoercionN
lkco CoercionN
rkco
| Just (CastTy Type
t CoercionN
co, Role
r) <- CoercionN -> Maybe (Type, Role)
isReflCo_maybe CoercionN
co1
= let kco' :: CoercionN
kco' = CoercionN -> CoercionN
mkSymCo CoercionN
co
in MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty (Role -> Type -> CoercionN
mkReflCo Role
r Type
t) (CoercionN
lkco CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
kco')
(CoercionN
rkco CoercionN -> CoercionN -> CoercionN
`mkTransCo` CoercionN
kco')
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co CoercionN
lkco CoercionN
rkco
| Just CoercionN
co' <- CoercionN -> Maybe CoercionN
pushRefl CoercionN
co = MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
co' CoercionN
lkco CoercionN
rkco
| Bool
otherwise = Maybe CvSubstEnv
forall a. Maybe a
Nothing
ty_co_match_tc :: MatchEnv -> LiftCoEnv
-> TyCon -> [Type]
-> TyCon -> [Coercion]
-> Maybe LiftCoEnv
ty_co_match_tc :: MatchEnv
-> CvSubstEnv
-> TyCon
-> [Type]
-> TyCon
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_tc MatchEnv
menv CvSubstEnv
subst TyCon
tc1 [Type]
tys1 TyCon
tc2 [CoercionN]
cos2
= do { Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2)
; MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst [Type]
tys1 [CoercionN]
cos2 }
ty_co_match_app :: MatchEnv -> LiftCoEnv
-> Type -> [Type] -> Coercion -> [Coercion]
-> Maybe LiftCoEnv
ty_co_match_app :: MatchEnv
-> CvSubstEnv
-> Type
-> [Type]
-> CoercionN
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_app MatchEnv
menv CvSubstEnv
subst Type
ty1 [Type]
ty1args CoercionN
co2 [CoercionN]
co2args
| Just (Type
ty1', Type
ty1a) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
ty1
, Just (CoercionN
co2', CoercionN
co2a) <- CoercionN -> Maybe (CoercionN, CoercionN)
splitAppCo_maybe CoercionN
co2
= MatchEnv
-> CvSubstEnv
-> Type
-> [Type]
-> CoercionN
-> [CoercionN]
-> Maybe CvSubstEnv
ty_co_match_app MatchEnv
menv CvSubstEnv
subst Type
ty1' (Type
ty1a Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ty1args) CoercionN
co2' (CoercionN
co2a CoercionN -> [CoercionN] -> [CoercionN]
forall a. a -> [a] -> [a]
: [CoercionN]
co2args)
| Bool
otherwise
= do { CvSubstEnv
subst1 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ki1 CoercionN
ki2 CoercionN
ki_ki_co CoercionN
ki_ki_co
; let Pair CoercionN
lkco CoercionN
rkco = Type -> CoercionN
mkNomReflCo (Type -> CoercionN) -> Pair Type -> Pair CoercionN
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoercionN -> Pair Type
coercionKind CoercionN
ki2
; CvSubstEnv
subst2 <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst1 Type
ty1 CoercionN
co2 CoercionN
lkco CoercionN
rkco
; MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst2 [Type]
ty1args [CoercionN]
co2args }
where
ki1 :: Type
ki1 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty1
ki2 :: CoercionN
ki2 = CoercionN -> CoercionN
promoteCoercion CoercionN
co2
ki_ki_co :: CoercionN
ki_ki_co = Type -> CoercionN
mkNomReflCo Type
liftedTypeKind
ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type] -> [Coercion]
-> Maybe LiftCoEnv
ty_co_match_args :: MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst (Type
ty:[Type]
tys) (CoercionN
arg:[CoercionN]
args)
= do { let Pair Type
lty Type
rty = CoercionN -> Pair Type
coercionKind CoercionN
arg
lkco :: CoercionN
lkco = Type -> CoercionN
mkNomReflCo ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
lty)
rkco :: CoercionN
rkco = Type -> CoercionN
mkNomReflCo ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
rty)
; CvSubstEnv
subst' <- MatchEnv
-> CvSubstEnv
-> Type
-> CoercionN
-> CoercionN
-> CoercionN
-> Maybe CvSubstEnv
ty_co_match MatchEnv
menv CvSubstEnv
subst Type
ty CoercionN
arg CoercionN
lkco CoercionN
rkco
; MatchEnv -> CvSubstEnv -> [Type] -> [CoercionN] -> Maybe CvSubstEnv
ty_co_match_args MatchEnv
menv CvSubstEnv
subst' [Type]
tys [CoercionN]
args }
ty_co_match_args MatchEnv
_ CvSubstEnv
subst [] [] = CvSubstEnv -> Maybe CvSubstEnv
forall a. a -> Maybe a
Just CvSubstEnv
subst
ty_co_match_args MatchEnv
_ CvSubstEnv
_ [Type]
_ [CoercionN]
_ = Maybe CvSubstEnv
forall a. Maybe a
Nothing
pushRefl :: Coercion -> Maybe Coercion
pushRefl :: CoercionN -> Maybe CoercionN
pushRefl CoercionN
co =
case (CoercionN -> Maybe (Type, Role)
isReflCo_maybe CoercionN
co) of
Just (AppTy Type
ty1 Type
ty2, Role
Nominal)
-> CoercionN -> Maybe CoercionN
forall a. a -> Maybe a
Just (CoercionN -> CoercionN -> CoercionN
AppCo (Role -> Type -> CoercionN
mkReflCo Role
Nominal Type
ty1) (Type -> CoercionN
mkNomReflCo Type
ty2))
Just (FunTy FunTyFlag
af Type
w Type
ty1 Type
ty2, Role
r)
-> CoercionN -> Maybe CoercionN
forall a. a -> Maybe a
Just (Role
-> FunTyFlag
-> FunTyFlag
-> CoercionN
-> CoercionN
-> CoercionN
-> CoercionN
FunCo Role
r FunTyFlag
af FunTyFlag
af (Role -> Type -> CoercionN
mkReflCo Role
r Type
w) (Role -> Type -> CoercionN
mkReflCo Role
r Type
ty1) (Role -> Type -> CoercionN
mkReflCo Role
r Type
ty2))
Just (TyConApp TyCon
tc [Type]
tys, Role
r)
-> CoercionN -> Maybe CoercionN
forall a. a -> Maybe a
Just (Role -> TyCon -> [CoercionN] -> CoercionN
TyConAppCo Role
r TyCon
tc ((Role -> Type -> CoercionN) -> [Role] -> [Type] -> [CoercionN]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> CoercionN
mkReflCo (Role -> TyCon -> [Role]
tyConRoleListX Role
r TyCon
tc) [Type]
tys))
Just (ForAllTy (Bndr OutTyVar
tv ForAllTyFlag
_) Type
ty, Role
r)
-> CoercionN -> Maybe CoercionN
forall a. a -> Maybe a
Just (OutTyVar -> CoercionN -> CoercionN -> CoercionN
ForAllCo OutTyVar
tv (Type -> CoercionN
mkNomReflCo (OutTyVar -> Type
varType OutTyVar
tv)) (Role -> Type -> CoercionN
mkReflCo Role
r Type
ty))
Maybe (Type, Role)
_ -> Maybe CoercionN
forall a. Maybe a
Nothing
data FlattenEnv
= FlattenEnv { FlattenEnv -> TypeMap (OutTyVar, TyCon, [Type])
fe_type_map :: TypeMap (TyVar, TyCon, [Type])
, FlattenEnv -> InScopeSet
fe_in_scope :: InScopeSet }
emptyFlattenEnv :: InScopeSet -> FlattenEnv
emptyFlattenEnv :: InScopeSet -> FlattenEnv
emptyFlattenEnv InScopeSet
in_scope
= FlattenEnv { fe_type_map :: TypeMap (OutTyVar, TyCon, [Type])
fe_type_map = TypeMap (OutTyVar, TyCon, [Type])
forall a. TypeMap a
emptyTypeMap
, fe_in_scope :: InScopeSet
fe_in_scope = InScopeSet
in_scope }
updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet FlattenEnv
env InScopeSet -> InScopeSet
upd = FlattenEnv
env { fe_in_scope = upd (fe_in_scope env) }
flattenTys :: InScopeSet -> [Type] -> [Type]
flattenTys :: InScopeSet -> [Type] -> [Type]
flattenTys InScopeSet
in_scope [Type]
tys = ([Type], TyVarEnv (TyCon, [Type])) -> [Type]
forall a b. (a, b) -> a
fst (InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
flattenTysX InScopeSet
in_scope [Type]
tys)
flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
flattenTysX InScopeSet
in_scope [Type]
tys
= let (FlattenEnv
env, [Type]
result) = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
emptyTvSubstEnv (InScopeSet -> FlattenEnv
emptyFlattenEnv InScopeSet
in_scope) [Type]
tys in
([Type]
result, TypeMap (OutTyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
build_env (FlattenEnv -> TypeMap (OutTyVar, TyCon, [Type])
fe_type_map FlattenEnv
env))
where
build_env :: TypeMap (TyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
build_env :: TypeMap (OutTyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
build_env TypeMap (OutTyVar, TyCon, [Type])
env_in
= ((OutTyVar, TyCon, [Type])
-> TyVarEnv (TyCon, [Type]) -> TyVarEnv (TyCon, [Type]))
-> TypeMap (OutTyVar, TyCon, [Type])
-> TyVarEnv (TyCon, [Type])
-> TyVarEnv (TyCon, [Type])
forall a b. (a -> b -> b) -> TypeMap a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM (\(OutTyVar
tv, TyCon
tc, [Type]
tys) TyVarEnv (TyCon, [Type])
env_out -> TyVarEnv (TyCon, [Type])
-> OutTyVar -> (TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
forall a. VarEnv a -> OutTyVar -> a -> VarEnv a
extendVarEnv TyVarEnv (TyCon, [Type])
env_out OutTyVar
tv (TyCon
tc, [Type]
tys))
TypeMap (OutTyVar, TyCon, [Type])
env_in TyVarEnv (TyCon, [Type])
forall a. VarEnv a
emptyVarEnv
coreFlattenTys :: TvSubstEnv -> FlattenEnv
-> [Type] -> (FlattenEnv, [Type])
coreFlattenTys :: TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
subst = (FlattenEnv -> Type -> (FlattenEnv, Type))
-> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL (TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst)
coreFlattenTy :: TvSubstEnv -> FlattenEnv
-> Type -> (FlattenEnv, Type)
coreFlattenTy :: TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst = FlattenEnv -> Type -> (FlattenEnv, Type)
go
where
go :: FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty'
go FlattenEnv
env (TyVarTy OutTyVar
tv)
| Just Type
ty <- TvSubstEnv -> OutTyVar -> Maybe Type
forall a. VarEnv a -> OutTyVar -> Maybe a
lookupVarEnv TvSubstEnv
subst OutTyVar
tv = (FlattenEnv
env, Type
ty)
| Bool
otherwise = let (FlattenEnv
env', Type
ki) = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env (OutTyVar -> Type
tyVarKind OutTyVar
tv) in
(FlattenEnv
env', OutTyVar -> Type
mkTyVarTy (OutTyVar -> Type) -> OutTyVar -> Type
forall a b. (a -> b) -> a -> b
$ OutTyVar -> Type -> OutTyVar
setTyVarKind OutTyVar
tv Type
ki)
go FlattenEnv
env (AppTy Type
ty1 Type
ty2) = let (FlattenEnv
env1, Type
ty1') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty1
(FlattenEnv
env2, Type
ty2') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env1 Type
ty2 in
(FlattenEnv
env2, Type -> Type -> Type
AppTy Type
ty1' Type
ty2')
go FlattenEnv
env (TyConApp TyCon
tc [Type]
tys)
| Bool -> Bool
not (TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc Role
Nominal)
= TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type)
coreFlattenTyFamApp TvSubstEnv
subst FlattenEnv
env TyCon
tc [Type]
tys
| Bool
otherwise
= let (FlattenEnv
env', [Type]
tys') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
subst FlattenEnv
env [Type]
tys in
(FlattenEnv
env', TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys')
go FlattenEnv
env ty :: Type
ty@(FunTy { ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
= let (FlattenEnv
env1, Type
ty1') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty1
(FlattenEnv
env2, Type
ty2') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env1 Type
ty2
(FlattenEnv
env3, Type
mult') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env2 Type
mult in
(FlattenEnv
env3, Type
ty { ft_mult = mult', ft_arg = ty1', ft_res = ty2' })
go FlattenEnv
env (ForAllTy (Bndr OutTyVar
tv ForAllTyFlag
vis) Type
ty)
= let (FlattenEnv
env1, TvSubstEnv
subst', OutTyVar
tv') = TvSubstEnv
-> FlattenEnv -> OutTyVar -> (FlattenEnv, TvSubstEnv, OutTyVar)
coreFlattenVarBndr TvSubstEnv
subst FlattenEnv
env OutTyVar
tv
(FlattenEnv
env2, Type
ty') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst' FlattenEnv
env1 Type
ty in
(FlattenEnv
env2, VarBndr OutTyVar ForAllTyFlag -> Type -> Type
ForAllTy (OutTyVar -> ForAllTyFlag -> VarBndr OutTyVar ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr OutTyVar
tv' ForAllTyFlag
vis) Type
ty')
go FlattenEnv
env ty :: Type
ty@(LitTy {}) = (FlattenEnv
env, Type
ty)
go FlattenEnv
env (CastTy Type
ty CoercionN
co)
= let (FlattenEnv
env1, Type
ty') = FlattenEnv -> Type -> (FlattenEnv, Type)
go FlattenEnv
env Type
ty
(FlattenEnv
env2, CoercionN
co') = TvSubstEnv -> FlattenEnv -> CoercionN -> (FlattenEnv, CoercionN)
coreFlattenCo TvSubstEnv
subst FlattenEnv
env1 CoercionN
co in
(FlattenEnv
env2, Type -> CoercionN -> Type
CastTy Type
ty' CoercionN
co')
go FlattenEnv
env (CoercionTy CoercionN
co)
= let (FlattenEnv
env', CoercionN
co') = TvSubstEnv -> FlattenEnv -> CoercionN -> (FlattenEnv, CoercionN)
coreFlattenCo TvSubstEnv
subst FlattenEnv
env CoercionN
co in
(FlattenEnv
env', CoercionN -> Type
CoercionTy CoercionN
co')
coreFlattenCo :: TvSubstEnv -> FlattenEnv
-> Coercion -> (FlattenEnv, Coercion)
coreFlattenCo :: TvSubstEnv -> FlattenEnv -> CoercionN -> (FlattenEnv, CoercionN)
coreFlattenCo TvSubstEnv
subst FlattenEnv
env CoercionN
co
= (FlattenEnv
env2, OutTyVar -> CoercionN
mkCoVarCo OutTyVar
covar)
where
(FlattenEnv
env1, Type
kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst FlattenEnv
env (CoercionN -> Type
coercionType CoercionN
co)
covar :: OutTyVar
covar = InScopeSet -> Type -> OutTyVar
mkFlattenFreshCoVar (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env1) Type
kind'
env2 :: FlattenEnv
env2 = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet FlattenEnv
env1 ((InScopeSet -> OutTyVar -> InScopeSet)
-> OutTyVar -> InScopeSet -> InScopeSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip InScopeSet -> OutTyVar -> InScopeSet
extendInScopeSet OutTyVar
covar)
coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
-> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar)
coreFlattenVarBndr :: TvSubstEnv
-> FlattenEnv -> OutTyVar -> (FlattenEnv, TvSubstEnv, OutTyVar)
coreFlattenVarBndr TvSubstEnv
subst FlattenEnv
env OutTyVar
tv
= (FlattenEnv
env2, TvSubstEnv
subst', OutTyVar
tv')
where
kind :: Type
kind = OutTyVar -> Type
varType OutTyVar
tv
(FlattenEnv
env1, Type
kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type)
coreFlattenTy TvSubstEnv
subst FlattenEnv
env Type
kind
tv' :: OutTyVar
tv' = InScopeSet -> OutTyVar -> OutTyVar
uniqAway (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env1) (OutTyVar -> Type -> OutTyVar
setVarType OutTyVar
tv Type
kind')
subst' :: TvSubstEnv
subst' = TvSubstEnv -> OutTyVar -> Type -> TvSubstEnv
forall a. VarEnv a -> OutTyVar -> a -> VarEnv a
extendVarEnv TvSubstEnv
subst OutTyVar
tv (OutTyVar -> Type
mkTyVarTy OutTyVar
tv')
env2 :: FlattenEnv
env2 = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
updateInScopeSet FlattenEnv
env1 ((InScopeSet -> OutTyVar -> InScopeSet)
-> OutTyVar -> InScopeSet -> InScopeSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip InScopeSet -> OutTyVar -> InScopeSet
extendInScopeSet OutTyVar
tv')
coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
-> TyCon
-> [Type]
-> (FlattenEnv, Type)
coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type)
coreFlattenTyFamApp TvSubstEnv
tv_subst FlattenEnv
env TyCon
fam_tc [Type]
fam_args
= case TypeMap (OutTyVar, TyCon, [Type])
-> Type -> Maybe (OutTyVar, TyCon, [Type])
forall a. TypeMap a -> Type -> Maybe a
lookupTypeMap TypeMap (OutTyVar, TyCon, [Type])
type_map Type
fam_ty of
Just (OutTyVar
tv, TyCon
_, [Type]
_) -> (FlattenEnv
env', Type -> [Type] -> Type
mkAppTys (OutTyVar -> Type
mkTyVarTy OutTyVar
tv) [Type]
leftover_args')
Maybe (OutTyVar, TyCon, [Type])
Nothing ->
let tyvar_name :: Name
tyvar_name = TyCon -> Name
forall a. Uniquable a => a -> Name
mkFlattenFreshTyName TyCon
fam_tc
tv :: OutTyVar
tv = InScopeSet -> OutTyVar -> OutTyVar
uniqAway InScopeSet
in_scope (OutTyVar -> OutTyVar) -> OutTyVar -> OutTyVar
forall a b. (a -> b) -> a -> b
$
Name -> Type -> OutTyVar
mkTyVar Name
tyvar_name ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
fam_ty)
ty' :: Type
ty' = Type -> [Type] -> Type
mkAppTys (OutTyVar -> Type
mkTyVarTy OutTyVar
tv) [Type]
leftover_args'
env'' :: FlattenEnv
env'' = FlattenEnv
env' { fe_type_map = extendTypeMap type_map fam_ty
(tv, fam_tc, sat_fam_args)
, fe_in_scope = extendInScopeSet in_scope tv }
in (FlattenEnv
env'', Type
ty')
where
arity :: Arity
arity = TyCon -> Arity
tyConArity TyCon
fam_tc
tcv_subst :: Subst
tcv_subst = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (FlattenEnv -> InScopeSet
fe_in_scope FlattenEnv
env) IdSubstEnv
emptyIdSubstEnv TvSubstEnv
tv_subst CvSubstEnv
forall a. VarEnv a
emptyVarEnv
([Type]
sat_fam_args, [Type]
leftover_args) = Bool -> ([Type], [Type]) -> ([Type], [Type])
forall a. HasCallStack => Bool -> a -> a
assert (Arity
arity Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
<= [Type] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Type]
fam_args) (([Type], [Type]) -> ([Type], [Type]))
-> ([Type], [Type]) -> ([Type], [Type])
forall a b. (a -> b) -> a -> b
$
Arity -> [Type] -> ([Type], [Type])
forall a. Arity -> [a] -> ([a], [a])
splitAt Arity
arity [Type]
fam_args
sat_fam_args' :: [Type]
sat_fam_args' = (() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
tcv_subst [Type]
sat_fam_args
(FlattenEnv
env', [Type]
leftover_args') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type])
coreFlattenTys TvSubstEnv
tv_subst FlattenEnv
env [Type]
leftover_args
fam_ty :: Type
fam_ty = TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
sat_fam_args'
FlattenEnv { fe_type_map :: FlattenEnv -> TypeMap (OutTyVar, TyCon, [Type])
fe_type_map = TypeMap (OutTyVar, TyCon, [Type])
type_map
, fe_in_scope :: FlattenEnv -> InScopeSet
fe_in_scope = InScopeSet
in_scope } = FlattenEnv
env'
mkFlattenFreshTyName :: Uniquable a => a -> Name
mkFlattenFreshTyName :: forall a. Uniquable a => a -> Name
mkFlattenFreshTyName a
unq
= Unique -> FastString -> Name
mkSysTvName (a -> Unique
forall a. Uniquable a => a -> Unique
getUnique a
unq) (String -> FastString
fsLit String
"flt")
mkFlattenFreshCoVar :: InScopeSet -> Kind -> CoVar
mkFlattenFreshCoVar :: InScopeSet -> Type -> OutTyVar
mkFlattenFreshCoVar InScopeSet
in_scope Type
kind
= let uniq :: Unique
uniq = InScopeSet -> Unique
unsafeGetFreshLocalUnique InScopeSet
in_scope
name :: Name
name = Unique -> FastString -> Name
mkSystemVarName Unique
uniq (String -> FastString
fsLit String
"flc")
in Name -> Type -> OutTyVar
mkCoVar Name
name Type
kind