Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Polarity

Description

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

Synopsis

Polarity computation

Auxiliary functions

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

What is the polarity of a function composition?

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).