ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Polarity

Computing the polarity (variance) of function arguments, for the sake of subtyping.

Contents

Synopsis

Polarity computation

valuecomputePolarity

Main function of this module.

valuecomposePol :: Polarity -> Polarity -> Polarity

What is the polarity of a function composition?

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

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

valuepurgeNonvariant :: [Polarity] -> [Polarity]

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

valuepolFromOcc :: Occurrence -> Polarity