Agda.TypeChecking.Polarity

Polarity lattice.

(/\) :: Polarity -> Polarity -> Polarity

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

neg :: Polarity -> Polarity

Polarity negation, swapping monotone and antitone.

composePol :: Polarity -> Polarity -> Polarity

What is the polarity of a function composition?

polFromOcc :: Occurrence -> Polarity

Auxiliary functions

nextPolarity :: [Polarity] -> (Polarity, [Polarity])

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

purgeNonvariant :: [Polarity] -> [Polarity]

Replace Nonvariant by Invariant.

Computing the polarity of a symbol.

computePolarity :: QName -> TCM ()

Main function of this module.

enablePhantomTypes :: Defn -> [Polarity] -> [Polarity]

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

dependentPolarity :: Type -> [Polarity] -> TCM [Polarity]

Make arguments Invariant if the type of a not-Nonvariant later argument depends on it.

relevantInIgnoringNonvariant :: Nat -> Type -> [Polarity] -> TCM Bool

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

Turn polarity Nonvariant into relevance UnusedArg

mkUnused :: Relevance -> Relevance

Record information that an argument is unused in Relevance.

nonvariantToUnusedArg :: [Polarity] -> Type -> TCM Type

Improve Relevance information in a type by polarity information. Nonvariant becomes UnusedArg.

nonvariantToUnusedArgInDef :: [Polarity] -> Defn -> Defn

Propagate Nonvariant Polarity to Relevance information in Args of a defined symbol.

nonvariantToUnusedArgInClause :: [Polarity] -> Clause -> Clause

Sized types

sizePolarity :: QName -> [Polarity] -> TCM [Polarity]

Hack for polarity of size indices.

checkSizeIndex :: Nat -> Nat -> Type -> TCM Bool

class HasPolarity a where

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

Methods

polarities :: Nat -> a -> TCM [Polarity]

Instances

HasPolarity LevelAtom

HasPolarity PlusLevel

HasPolarity Level

HasPolarity Type

HasPolarity Term

HasPolarity a => HasPolarity [a]

HasPolarity a => HasPolarity (Arg a)

HasPolarity a => HasPolarity (Dom a)

HasPolarity a => HasPolarity (Abs a)

(HasPolarity a, HasPolarity b) => HasPolarity (a, b)

polarity :: HasPolarity a => Nat -> a -> TCM Polarity

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