Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- tcMatchTy :: Type -> Type -> Maybe Subst
- tcMatchTyKi :: Type -> Type -> Maybe Subst
- tcMatchTys :: [Type] -> [Type] -> Maybe Subst
- tcMatchTyKis :: [Type] -> [Type] -> Maybe Subst
- tcMatchTyX :: Subst -> Type -> Type -> Maybe Subst
- tcMatchTysX :: Subst -> [Type] -> [Type] -> Maybe Subst
- tcMatchTyKisX :: Subst -> [Type] -> [Type] -> Maybe Subst
- tcMatchTyX_BM :: BindFun -> Subst -> Type -> Type -> Maybe Subst
- ruleMatchTyKiX :: TyCoVarSet -> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv
- tcUnifyTy :: Type -> Type -> Maybe Subst
- tcUnifyTyKi :: Type -> Type -> Maybe Subst
- tcUnifyTys :: BindFun -> [Type] -> [Type] -> Maybe Subst
- tcUnifyTyKis :: BindFun -> [Type] -> [Type] -> Maybe Subst
- tcUnifyTysFG :: BindFun -> [Type] -> [Type] -> UnifyResult
- tcUnifyTyWithTFs :: Bool -> InScopeSet -> Type -> Type -> Maybe Subst
- type BindFun = TyCoVar -> Type -> BindFlag
- data BindFlag
- matchBindFun :: TyCoVarSet -> BindFun
- alwaysBindFun :: BindFun
- type UnifyResult = UnifyResultM Subst
- data UnifyResultM a
- data MaybeApartReason
- typesCantMatch :: [(Type, Type)] -> Bool
- typesAreApart :: Type -> Type -> Bool
- liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
- flattenTys :: InScopeSet -> [Type] -> [Type]
- flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
Documentation
tcMatchTy :: Type -> Type -> Maybe Subst Source #
tcMatchTy t1 t2
produces a substitution (over fvs(t1))
s
such that s(t1)
equals t2
.
The returned substitution might bind coercion variables,
if the variable is an argument to a GADT constructor.
Precondition: typeKind ty1 eqType
typeKind ty2
We don't pass in a set of "template variables" to be bound by the match, because tcMatchTy (and similar functions) are always used on top-level types, so we can bind any of the free variables of the LHS. See also Note [tcMatchTy vs tcMatchTyKi]
tcMatchTyKi :: Type -> Type -> Maybe Subst Source #
Like tcMatchTy
, but allows the kinds of the types to differ,
and thus matches them as well.
See also Note [tcMatchTy vs tcMatchTyKi]
:: [Type] | Template |
-> [Type] | Target |
-> Maybe Subst | One-shot; in principle the template variables could be free in the target |
Like tcMatchTy
but over a list of types.
See also Note [tcMatchTy vs tcMatchTyKi]
Like tcMatchTyKi
but over a list of types.
See also Note [tcMatchTy vs tcMatchTyKi]
This is similar to tcMatchTy
, but extends a substitution
See also Note [tcMatchTy vs tcMatchTyKi]
Like tcMatchTys
, but extending a substitution
See also Note [tcMatchTy vs tcMatchTyKi]
Like tcMatchTyKis
, but extending a substitution
See also Note [tcMatchTy vs tcMatchTyKi]
:: TyCoVarSet | template variables |
-> RnEnv2 | |
-> TvSubstEnv | type substitution to extend |
-> Type | Template |
-> Type | Target |
-> Maybe TvSubstEnv |
This one is called from the expression matcher, which already has a MatchEnv in hand
tcUnifyTy :: Type -> Type -> Maybe Subst Source #
Simple unification of two types; all type variables are bindable Precondition: the kinds are already equal
tcUnifyTyKis :: BindFun -> [Type] -> [Type] -> Maybe Subst Source #
Like tcUnifyTys
but also unifies the kinds
tcUnifyTysFG :: BindFun -> [Type] -> [Type] -> UnifyResult Source #
tcUnifyTysFG bind_tv tys1 tys2
attempts to find a substitution s
(whose
domain elements all respond BindMe
to bind_tv
) such that
s(tys1)
and that of s(tys2)
are equal, as witnessed by the returned
Coercions. This version requires that the kinds of the types are the same,
if you unify left-to-right.
:: Bool | True = do two-way unification; False = do one-way matching. See end of sec 5.2 from the paper |
-> InScopeSet | |
-> Type | |
-> Type | |
-> Maybe Subst |
Unify two types, treating type family applications as possibly unifying with anything and looking through injective type family applications. Precondition: kinds are the same
type BindFun = TyCoVar -> Type -> BindFlag Source #
Some unification functions are parameterised by a BindFun
, which
says whether or not to allow a certain unification to take place.
A BindFun
takes the TyVar
involved along with the Type
it will
potentially be bound to.
It is possible for the variable to actually be a coercion variable
(Note [Matching coercion variables]), but only when one-way matching.
In this case, the Type
will be a CoercionTy
.
matchBindFun :: TyCoVarSet -> BindFun Source #
Allow binding only for any variable in the set. Variables may be bound to any type. Used when doing simple matching; e.g. can we find a substitution
S = [a :-> t1, b :-> t2] such that S( Maybe (a, b->Int ) = Maybe (Bool, Char -> Int)
alwaysBindFun :: BindFun Source #
Allow the binding of any variable to any type
type UnifyResult = UnifyResultM Subst Source #
data UnifyResultM a Source #
See Note [Unification result]
Instances
Applicative UnifyResultM Source # | |
Defined in GHC.Core.Unify pure :: a -> UnifyResultM a Source # (<*>) :: UnifyResultM (a -> b) -> UnifyResultM a -> UnifyResultM b Source # liftA2 :: (a -> b -> c) -> UnifyResultM a -> UnifyResultM b -> UnifyResultM c Source # (*>) :: UnifyResultM a -> UnifyResultM b -> UnifyResultM b Source # (<*) :: UnifyResultM a -> UnifyResultM b -> UnifyResultM a Source # | |
Functor UnifyResultM Source # | |
Defined in GHC.Core.Unify fmap :: (a -> b) -> UnifyResultM a -> UnifyResultM b Source # (<$) :: a -> UnifyResultM b -> UnifyResultM a Source # | |
Monad UnifyResultM Source # | |
Defined in GHC.Core.Unify (>>=) :: UnifyResultM a -> (a -> UnifyResultM b) -> UnifyResultM b Source # (>>) :: UnifyResultM a -> UnifyResultM b -> UnifyResultM b Source # return :: a -> UnifyResultM a Source # | |
Outputable a => Outputable (UnifyResultM a) Source # | |
Defined in GHC.Core.Unify ppr :: UnifyResultM a -> SDoc Source # |
data MaybeApartReason Source #
Why are two types MaybeApart
? MARInfinite
takes precedence:
This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv
As of Feb 2022, we never differentiate between MARTypeFamily and MARTypeVsConstraint;
it's really only MARInfinite that's interesting here.
MARTypeFamily | matching e.g. F Int ~? Bool |
MARInfinite | matching e.g. a ~? Maybe a |
MARTypeVsConstraint | matching Type ~? Constraint or the arrow types See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim |
Instances
Semigroup MaybeApartReason Source # | |
Defined in GHC.Core.Unify (<>) :: MaybeApartReason -> MaybeApartReason -> MaybeApartReason Source # sconcat :: NonEmpty MaybeApartReason -> MaybeApartReason Source # stimes :: Integral b => b -> MaybeApartReason -> MaybeApartReason Source # | |
Outputable MaybeApartReason Source # | |
Defined in GHC.Core.Unify ppr :: MaybeApartReason -> SDoc Source # |
typesCantMatch :: [(Type, Type)] -> Bool Source #
Given a list of pairs of types, are any two members of a pair surely apart, even after arbitrary type function evaluation and substitution?
liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext Source #
liftCoMatch
is sort of inverse to liftCoSubst
. In particular, if
liftCoMatch vars ty co == Just s
, then liftCoSubst s ty == co
,
where ==
there means that the result of liftCoSubst
has the same
type as the original co; but may be different under the hood.
That is, it matches a type against a coercion of the same
"shape", and returns a lifting substitution which could have been
used to produce the given coercion from the given type.
Note that this function is incomplete -- it might return Nothing
when there does indeed exist a possible lifting context.
This function is incomplete in that it doesn't respect the equality
in eqType
. That is, it's possible that this will succeed for t1 and
fail for t2, even when t1 eqType
t2. That's because it depends on
there being a very similar structure between the type and the coercion.
This incompleteness shouldn't be all that surprising, especially because
it depends on the structure of the coercion, which is a silly thing to do.
The lifting context produced doesn't have to be exacting in the roles of the mappings. This is because any use of the lifting context will also require a desired role. Thus, this algorithm prefers mapping to nominal coercions where it can do so.
flattenTys :: InScopeSet -> [Type] -> [Type] Source #
flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type])) Source #