Check whether a bound maches a bind. UName and BName match if they have the same name. UIx 0 _ and BAnon _ always match. Yields False for other combinations of bounds and binds.

namedBoundMatchesBind :: Eq n => Bound n -> Bind n -> BoolSource

Check whether a named bound matches a named bind. Yields False if they are not named or have different names.

takeSubstBoundOfBind :: Bind n -> Maybe (Bound n)Source

Convert a Bind to a Bound, ready for substitution.

Returns UName for BName, UIx 0 for BAnon and Nothing for BNone, because there's nothing to substitute.

takeSubstBoundsOfBinds :: [Bind n] -> [Bound n]Source

Convert some Binds to Bounds

replaceTypeOfBound :: Type n -> Bound n -> Bound nSource

If this Bound is a UPrim then replace it's embedded type with a new one, otherwise return it unharmed.

Kinds

kFun :: Kind n -> Kind n -> Kind nSource

Construct a kind function.

kFuns :: [Kind n] -> Kind n -> Kind nSource

Construct some kind functions.

takeKFun :: Kind n -> Maybe (Kind n, Kind n)Source

Destruct a kind function

takeKFuns :: Kind n -> ([Kind n], Kind n)Source

Destruct a chain of kind functions into the arguments

takeKFuns' :: Kind n -> [Kind n]Source

Like takeKFuns, but return argument and return kinds in the same list.

takeResultKind :: Kind n -> Kind nSource

Take the result kind of a kind function, or return the same kind unharmed if it's not a kind function.

Quantifiers

tForall :: Kind n -> (Type n -> Type n) -> Type nSource

Build an anonymous type abstraction, with a single parameter.

tForall' :: Int -> Kind n -> (Type n -> Type n) -> Type nSource

Build an anonymous type abstraction, with a single parameter. Starting the next index from the given value.

tForalls :: [Kind n] -> ([Type n] -> Type n) -> Type nSource

Build an anonymous type abstraction, with several parameters. Starting the next index from the given value.

tForalls' :: Int -> [Kind n] -> ([Type n] -> Type n) -> Type nSource

Build an anonymous type abstraction, with several parameters. Starting the next index from the given value.

takeTForalls :: Type n -> Maybe ([Bind n], Type n)Source

Split nested foralls from the front of a type, or Nothing if there was no outer forall.

eraseTForalls :: Ord n => Type n -> Type nSource

Erase all TForall quantifiers from a type.

Sums

tBot :: Kind n -> Type nSource

Construct an empty type sum.

tSum :: Ord n => Kind n -> [Type n] -> Type nSource

Applications

tApp :: Type n -> Type n -> Type nSource

Construct a type application.

($:) :: Type n -> Type n -> Type nSource

Construct a type application.

tApps :: Type n -> [Type n] -> Type nSource

Construct a sequence of type applications.

takeTApps :: Type n -> [Type n]Source

Flatten a sequence ot type applications into the function part and arguments, if any.

takeTyConApps :: Type n -> Maybe (TyCon n, [Type n])Source

Flatten a sequence of type applications, returning the type constructor and arguments, if there is one.

takePrimTyConApps :: Type n -> Maybe (n, [Type n])Source

Flatten a sequence of type applications, returning the type constructor and arguments, if there is one. Only accept primitive type constructors.

takeDataTyConApps :: Type n -> Maybe (TyCon n, [Type n])Source

Flatten a sequence of type applications, returning the type constructor and arguments, if there is one. Only accept data type constructors.

takePrimeRegion :: Type n -> Maybe (Type n)Source

Take the prime region variable of a data type. This corresponds to the region the outermost constructor is allocated into.

Functions

tFun :: Type n -> Type n -> Type nSource

Construct a pure function type.

tFunOfList :: [Type n] -> Maybe (Type n)Source

Construct a pure and empty function from a list containing the parameter and return type. Yields Nothing if the list is empty.

tFunPE :: Type n -> Type n -> Type nSource

Construct a pure and empty value type function.

tFunOfListPE :: [Type n] -> Maybe (Type n)Source

Construct a pure and empty function from a list containing the parameter and return type. Yields Nothing if the list is empty.

tFunEC :: Type n -> Effect n -> Closure n -> Type n -> Type nSource

Construct a value type function, with the provided effect and closure.

takeTFun :: Type n -> Maybe (Type n, Type n)Source

Yield the argument and result type of a function type.

Works for both TcConFun and TcConFunEC.

takeTFunEC :: Type n -> Maybe (Type n, Effect n, Closure n, Type n)Source

Yield the argument and result type of a function type.

takeTFunArgResult :: Type n -> ([Type n], Type n)Source

Destruct the type of a function, returning just the argument and result types.

Works for both TcConFun and TcConFunEC.

takeTFunWitArgResult :: Type n -> ([Type n], [Type n], Type n)Source

Destruct the type of a function, returning the witness argument, value argument and result types. The function type must have the witness implications before the value arguments, eg T1 => T2 -> T3 -> T4 -> T5.

Works for both TcConFun and TcConFunEC.

takeTFunAllArgResult :: Type n -> ([Type n], Type n)Source

Destruct the type of a possibly polymorphic function returning all kinds of quantifiers, witness arguments, and value arguments in the order they appear, along with the type of the result.

arityOfType :: Type n -> IntSource

Determine the arity of an expression by looking at its type. Count all the function arrows, and foralls.

This assumes the type is in prenex form, meaning that all the quantifiers are at the front.