A particular type argument can be either co- or contravariant with respect to subtyping.

The arity of a type constructor is a list of variances, expressing both how many type arguments the constructor takes, and the variance of each argument. This is used to decompose subtyping constraints.

For example, arity CArr = [Contra, Co] since function arrow is contravariant in its first argument and covariant in its second. That is, S1 -> T1 S2 - T2 (<: means "is a subtype of") if and only if S2 <: S1 and T1 <: T2.

A "qualifier" is kind of like a type class in Haskell; but unlike Haskell, disco users cannot define their own. Rather, there is a finite fixed list of qualifiers supported by disco. For example, QSub denotes types which support a subtraction operation. Each qualifier corresponds to a set of types which satisfy it (see hasQual and qualRules).

These qualifiers generally arise from uses of various operations. For example, the expression \x y. x - y would be inferred to have a type a -> a -> a [subtractive a], that is, a function of type a -> a -> a where a is any type that supports subtraction.

These qualifiers can appear in a CQual constraint; see Disco.Typecheck.Constraint.

A helper function that returns the appropriate qualifier for a binary arithmetic operation.

A Sort represents a set of qualifiers, and also represents a set of types (in general, the intersection of the sets corresponding to the qualifiers).

The special sort \(\top\) which includes all types.

A "direction" for the subtyping relation (either subtype or supertype).

Swap directions.

Check whether one atomic type is a subtype of the other. Returns True if either they are equal, or if they are base types and isSubB returns true.

Check whether one base type is a subtype of another.

Check whether one base type is a sub- or supertype of another.

List all the supertypes of a given base type.

List all the subtypes of a given base type.

List all the sub- or supertypes of a given base type.

Check whether a given base type satisfies a qualifier.

Check whether a base type has a certain sort, which simply amounts to whether it satisfies every qualifier in the sort.

Given a constructor T and a qualifier we want to hold of a type T t1 t2 ..., return a list of qualifiers that need to hold of t1, t2, ...

sortRules T s = [s1, ..., sn] means that sort s holds of type (T t1 ... tn) if and only if s1 t1 ... sn tn. For now this is just derived directly from qualRules.

This is the arity function described in section 4.1 of Traytel et al.

Pick a base type (generally the "simplest") that satisfies a given sort.