Agda-2.5.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Polarity

Contents

Synopsis

Polarity lattice.

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

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

neg :: Polarity -> Polarity Source #

Polarity negation, swapping monotone and antitone.

composePol :: Polarity -> Polarity -> Polarity Source #

What is the polarity of a function composition?

Auxiliary functions

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

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

purgeNonvariant :: [Polarity] -> [Polarity] Source #

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

polarityFromPositivity :: QName -> TCM () Source #

A quick transliterations of occurrences to polarities.

Computing the polarity of a symbol.

computePolarity :: [QName] -> TCM () Source #

Main function of this module.

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

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.

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

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.

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

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

Sized types

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

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 :: QName -> Nat -> Nat -> Type -> TCM Bool Source #

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

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

class HasPolarity a where Source #

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

Minimal complete definition

polarities

Methods

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

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

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