ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Polarity

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

Polarity computation

1 declaration

valuecomputePolarity

Main function of this module.

4 declarations

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