| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Polarity
Description
Computing the polarity (variance) of function arguments, for the sake of subtyping.
Synopsis
- computePolarity :: (HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m, MonadDebug m, MonadPretty m) => [QName] -> m ()
- composePol :: Polarity -> Polarity -> Polarity
- nextPolarity :: [Polarity] -> (Polarity, [Polarity])
- purgeNonvariant :: [Polarity] -> [Polarity]
- polFromOcc :: Occurrence -> Polarity
Polarity computation
computePolarity :: (HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m, MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m, MonadDebug m, MonadPretty m) => [QName] -> m () Source #
Main function of this module.
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).
polFromOcc :: Occurrence -> Polarity Source #