Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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).