Infimum on the information lattice. Invariant is bottom (dominant for inf), Nonvariant is top (neutral for inf).

Polarity negation, swapping monotone and antitone.

What is the polarity of a function composition?

Get the next polarity from a list, Invariant if empty.

Replace Nonvariant by Covariant. (Arbitrary bias, but better than Invariant, see issue 1596).

A quick transliterations of occurrences to polarities.

Main function of this module.

Data and record parameters are used as phantom arguments all over the test suite (and possibly in user developments). enablePhantomTypes turns Nonvariant parameters to Covariant to enable phantoms.

Make arguments Invariant if the type of a not-Nonvariant later argument depends on it. Also, enable phantom types by turning Nonvariant into something else if it is a data/record parameter but not a size argument. [See issue 1596]

Precondition: the "phantom" polarity list has the same length as the polarity list.

Check whether a variable is relevant in a type expression, ignoring domains of non-variant arguments.

Hack for polarity of size indices. As a side effect, this sets the positivity of the size index. See testsucceedPolaritySizeSucData.agda for a case where this is needed.

checkSizeIndex d i a checks that constructor target type a has form d ps (↑ⁿ i) idxs where |ps| = np(d).

Precondition: a is reduced and of form d ps idxs0.

polarities i a computes the list of polarities of de Bruijn index i in syntactic entity a.

polarity i a computes the polarity of de Bruijn index i in syntactic entity a by taking the infimum of all polarities.