    -- | Occurrences.

    module Agda.TypeChecking.Positivity.Occurrence
      ( Occurrence(..)
      , OccursWhere(..)
      , Where(..)
      , boundToEverySome
      , productOfEdgesInBoundedWalk
      ) where

    import Control.DeepSeq
    import Control.Monad

    import Data.Data (Data)

    import Data.Foldable (toList)

    import Data.Map.Strict (Map)
    import qualified Data.Map.Strict as Map
    import Data.Sequence (Seq)

    import GHC.Generics (Generic)

    import Agda.Syntax.Common
    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Position

    import Agda.Utils.Graph.AdjacencyMap.Unidirectional (Graph)
    import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
    import Agda.Utils.Null
    import Agda.Utils.Pretty
    import Agda.Utils.SemiRing
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    -- Specification of occurrences -------------------------------------------

    -- Operations and instances in Agda.TypeChecking.Positivity.

    -- | Description of an occurrence.
    data OccursWhere
      = OccursWhere Range (Seq Where) (Seq Where)
        -- ^ The elements of the sequences, read from left to right,
        -- explain how to get to the occurrence. The second sequence
        -- includes the main information, and if the first sequence is
        -- non-empty, then it includes information about the context of
        -- the second sequence.
      deriving (Nat -> OccursWhere -> ShowS
    [OccursWhere] -> ShowS
    OccursWhere -> String
    (Nat -> OccursWhere -> ShowS)
    -> (OccursWhere -> String)
    -> ([OccursWhere] -> ShowS)
    -> Show OccursWhere
    forall a.
    (Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [OccursWhere] -> ShowS
    $cshowList :: [OccursWhere] -> ShowS
    show :: OccursWhere -> String
    $cshow :: OccursWhere -> String
    showsPrec :: Nat -> OccursWhere -> ShowS
    $cshowsPrec :: Nat -> OccursWhere -> ShowS
    Show, OccursWhere -> OccursWhere -> Bool
    (OccursWhere -> OccursWhere -> Bool)
    -> (OccursWhere -> OccursWhere -> Bool) -> Eq OccursWhere
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: OccursWhere -> OccursWhere -> Bool
    $c/= :: OccursWhere -> OccursWhere -> Bool
    == :: OccursWhere -> OccursWhere -> Bool
    $c== :: OccursWhere -> OccursWhere -> Bool
    Eq, Eq OccursWhere
    Eq OccursWhere
    -> (OccursWhere -> OccursWhere -> Ordering)
    -> (OccursWhere -> OccursWhere -> Bool)
    -> (OccursWhere -> OccursWhere -> Bool)
    -> (OccursWhere -> OccursWhere -> Bool)
    -> (OccursWhere -> OccursWhere -> Bool)
    -> (OccursWhere -> OccursWhere -> OccursWhere)
    -> (OccursWhere -> OccursWhere -> OccursWhere)
    -> Ord OccursWhere
    OccursWhere -> OccursWhere -> Bool
    OccursWhere -> OccursWhere -> Ordering
    OccursWhere -> OccursWhere -> OccursWhere
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: OccursWhere -> OccursWhere -> OccursWhere
    $cmin :: OccursWhere -> OccursWhere -> OccursWhere
    max :: OccursWhere -> OccursWhere -> OccursWhere
    $cmax :: OccursWhere -> OccursWhere -> OccursWhere
    >= :: OccursWhere -> OccursWhere -> Bool
    $c>= :: OccursWhere -> OccursWhere -> Bool
    > :: OccursWhere -> OccursWhere -> Bool
    $c> :: OccursWhere -> OccursWhere -> Bool
    <= :: OccursWhere -> OccursWhere -> Bool
    $c<= :: OccursWhere -> OccursWhere -> Bool
    < :: OccursWhere -> OccursWhere -> Bool
    $c< :: OccursWhere -> OccursWhere -> Bool
    compare :: OccursWhere -> OccursWhere -> Ordering
    $ccompare :: OccursWhere -> OccursWhere -> Ordering
    Ord, Typeable OccursWhere
    Typeable OccursWhere
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> OccursWhere -> c OccursWhere)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c OccursWhere)
    -> (OccursWhere -> Constr)
    -> (OccursWhere -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c OccursWhere))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c OccursWhere))
    -> ((forall b. Data b => b -> b) -> OccursWhere -> OccursWhere)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r)
    -> (forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u])
    -> (forall u.
        Nat -> (forall d. Data d => d -> u) -> OccursWhere -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere)
    -> Data OccursWhere
    OccursWhere -> DataType
    OccursWhere -> Constr
    (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Nat -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Nat -> (forall d. Data d => d -> u) -> OccursWhere -> u
    forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OccursWhere
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OccursWhere)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c OccursWhere)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> OccursWhere -> m OccursWhere
    gmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> OccursWhere -> u
    $cgmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> OccursWhere -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> OccursWhere -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> OccursWhere -> r
    gmapT :: (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere
    $cgmapT :: (forall b. Data b => b -> b) -> OccursWhere -> OccursWhere
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c OccursWhere)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c OccursWhere)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OccursWhere)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c OccursWhere)
    dataTypeOf :: OccursWhere -> DataType
    $cdataTypeOf :: OccursWhere -> DataType
    toConstr :: OccursWhere -> Constr
    $ctoConstr :: OccursWhere -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OccursWhere
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c OccursWhere
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> OccursWhere -> c OccursWhere
    Data, (forall x. OccursWhere -> Rep OccursWhere x)
    -> (forall x. Rep OccursWhere x -> OccursWhere)
    -> Generic OccursWhere
    forall x. Rep OccursWhere x -> OccursWhere
    forall x. OccursWhere -> Rep OccursWhere x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep OccursWhere x -> OccursWhere
    $cfrom :: forall x. OccursWhere -> Rep OccursWhere x
    Generic)

    instance NFData OccursWhere

    -- | One part of the description of an occurrence.
    data Where
      = LeftOfArrow
      | DefArg QName Nat -- ^ in the nth argument of a define constant
      | UnderInf         -- ^ in the principal argument of built-in ∞
      | VarArg           -- ^ as an argument to a bound variable
      | MetaArg          -- ^ as an argument of a metavariable
      | ConArgType QName -- ^ in the type of a constructor
      | IndArgType QName -- ^ in a datatype index of a constructor
      | InClause Nat     -- ^ in the nth clause of a defined function
      | Matched          -- ^ matched against in a clause of a defined function
      | IsIndex          -- ^ is an index of an inductive family
      | InDefOf QName    -- ^ in the definition of a constant
      deriving (Nat -> Where -> ShowS
    [Where] -> ShowS
    Where -> String
    (Nat -> Where -> ShowS)
    -> (Where -> String) -> ([Where] -> ShowS) -> Show Where
    forall a.
    (Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Where] -> ShowS
    $cshowList :: [Where] -> ShowS
    show :: Where -> String
    $cshow :: Where -> String
    showsPrec :: Nat -> Where -> ShowS
    $cshowsPrec :: Nat -> Where -> ShowS
    Show, Where -> Where -> Bool
    (Where -> Where -> Bool) -> (Where -> Where -> Bool) -> Eq Where
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Where -> Where -> Bool
    $c/= :: Where -> Where -> Bool
    == :: Where -> Where -> Bool
    $c== :: Where -> Where -> Bool
    Eq, Eq Where
    Eq Where
    -> (Where -> Where -> Ordering)
    -> (Where -> Where -> Bool)
    -> (Where -> Where -> Bool)
    -> (Where -> Where -> Bool)
    -> (Where -> Where -> Bool)
    -> (Where -> Where -> Where)
    -> (Where -> Where -> Where)
    -> Ord Where
    Where -> Where -> Bool
    Where -> Where -> Ordering
    Where -> Where -> Where
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Where -> Where -> Where
    $cmin :: Where -> Where -> Where
    max :: Where -> Where -> Where
    $cmax :: Where -> Where -> Where
    >= :: Where -> Where -> Bool
    $c>= :: Where -> Where -> Bool
    > :: Where -> Where -> Bool
    $c> :: Where -> Where -> Bool
    <= :: Where -> Where -> Bool
    $c<= :: Where -> Where -> Bool
    < :: Where -> Where -> Bool
    $c< :: Where -> Where -> Bool
    compare :: Where -> Where -> Ordering
    $ccompare :: Where -> Where -> Ordering
    Ord, Typeable Where
    Typeable Where
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> Where -> c Where)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Where)
    -> (Where -> Constr)
    -> (Where -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Where))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where))
    -> ((forall b. Data b => b -> b) -> Where -> Where)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Where -> [u])
    -> (forall u. Nat -> (forall d. Data d => d -> u) -> Where -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Where -> m Where)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Where -> m Where)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Where -> m Where)
    -> Data Where
    Where -> DataType
    Where -> Constr
    (forall b. Data b => b -> b) -> Where -> Where
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Nat -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Nat -> (forall d. Data d => d -> u) -> Where -> u
    forall u. (forall d. Data d => d -> u) -> Where -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Where -> m Where
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Where -> m Where
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Where
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Where -> c Where
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Where)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Where -> m Where
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Where -> m Where
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Where -> m Where
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Where -> m Where
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Where -> m Where
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Where -> m Where
    gmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> Where -> u
    $cgmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> Where -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Where -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Where -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
    gmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Where -> r
    gmapT :: (forall b. Data b => b -> b) -> Where -> Where
    $cgmapT :: (forall b. Data b => b -> b) -> Where -> Where
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Where)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Where)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Where)
    dataTypeOf :: Where -> DataType
    $cdataTypeOf :: Where -> DataType
    toConstr :: Where -> Constr
    $ctoConstr :: Where -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Where
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Where
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Where -> c Where
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Where -> c Where
    Data, (forall x. Where -> Rep Where x)
    -> (forall x. Rep Where x -> Where) -> Generic Where
    forall x. Rep Where x -> Where
    forall x. Where -> Rep Where x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Where x -> Where
    $cfrom :: forall x. Where -> Rep Where x
    Generic)

    instance NFData Where

    -- | Subterm occurrences for positivity checking.
    --   The constructors are listed in increasing information they provide:
    --   @Mixed <= JustPos <= StrictPos <= GuardPos <= Unused@
    --   @Mixed <= JustNeg <= Unused@.
    data Occurrence
      = Mixed     -- ^ Arbitrary occurrence (positive and negative).
      | JustNeg   -- ^ Negative occurrence.
      | JustPos   -- ^ Positive occurrence, but not strictly positive.
      | StrictPos -- ^ Strictly positive occurrence.
      | GuardPos  -- ^ Guarded strictly positive occurrence (i.e., under ∞).  For checking recursive records.
      | Unused    --  ^ No occurrence.
      deriving (Typeable Occurrence
    Typeable Occurrence
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> Occurrence -> c Occurrence)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Occurrence)
    -> (Occurrence -> Constr)
    -> (Occurrence -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Occurrence))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c Occurrence))
    -> ((forall b. Data b => b -> b) -> Occurrence -> Occurrence)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Occurrence -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Occurrence -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Occurrence -> [u])
    -> (forall u.
        Nat -> (forall d. Data d => d -> u) -> Occurrence -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence)
    -> Data Occurrence
    Occurrence -> DataType
    Occurrence -> Constr
    (forall b. Data b => b -> b) -> Occurrence -> Occurrence
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Nat -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Nat -> (forall d. Data d => d -> u) -> Occurrence -> u
    forall u. (forall d. Data d => d -> u) -> Occurrence -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Occurrence -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Occurrence -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Occurrence
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Occurrence -> c Occurrence
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Occurrence)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Occurrence -> m Occurrence
    gmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> Occurrence -> u
    $cgmapQi :: forall u. Nat -> (forall d. Data d => d -> u) -> Occurrence -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Occurrence -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Occurrence -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Occurrence -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Occurrence -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Occurrence -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Occurrence -> r
    gmapT :: (forall b. Data b => b -> b) -> Occurrence -> Occurrence
    $cgmapT :: (forall b. Data b => b -> b) -> Occurrence -> Occurrence
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Occurrence)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Occurrence)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Occurrence)
    dataTypeOf :: Occurrence -> DataType
    $cdataTypeOf :: Occurrence -> DataType
    toConstr :: Occurrence -> Constr
    $ctoConstr :: Occurrence -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Occurrence
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Occurrence
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Occurrence -> c Occurrence
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Occurrence -> c Occurrence
    Data, Nat -> Occurrence -> ShowS
    [Occurrence] -> ShowS
    Occurrence -> String
    (Nat -> Occurrence -> ShowS)
    -> (Occurrence -> String)
    -> ([Occurrence] -> ShowS)
    -> Show Occurrence
    forall a.
    (Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Occurrence] -> ShowS
    $cshowList :: [Occurrence] -> ShowS
    show :: Occurrence -> String
    $cshow :: Occurrence -> String
    showsPrec :: Nat -> Occurrence -> ShowS
    $cshowsPrec :: Nat -> Occurrence -> ShowS
    Show, Occurrence -> Occurrence -> Bool
    (Occurrence -> Occurrence -> Bool)
    -> (Occurrence -> Occurrence -> Bool) -> Eq Occurrence
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Occurrence -> Occurrence -> Bool
    $c/= :: Occurrence -> Occurrence -> Bool
    == :: Occurrence -> Occurrence -> Bool
    $c== :: Occurrence -> Occurrence -> Bool
    Eq, Eq Occurrence
    Eq Occurrence
    -> (Occurrence -> Occurrence -> Ordering)
    -> (Occurrence -> Occurrence -> Bool)
    -> (Occurrence -> Occurrence -> Bool)
    -> (Occurrence -> Occurrence -> Bool)
    -> (Occurrence -> Occurrence -> Bool)
    -> (Occurrence -> Occurrence -> Occurrence)
    -> (Occurrence -> Occurrence -> Occurrence)
    -> Ord Occurrence
    Occurrence -> Occurrence -> Bool
    Occurrence -> Occurrence -> Ordering
    Occurrence -> Occurrence -> Occurrence
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Occurrence -> Occurrence -> Occurrence
    $cmin :: Occurrence -> Occurrence -> Occurrence
    max :: Occurrence -> Occurrence -> Occurrence
    $cmax :: Occurrence -> Occurrence -> Occurrence
    >= :: Occurrence -> Occurrence -> Bool
    $c>= :: Occurrence -> Occurrence -> Bool
    > :: Occurrence -> Occurrence -> Bool
    $c> :: Occurrence -> Occurrence -> Bool
    <= :: Occurrence -> Occurrence -> Bool
    $c<= :: Occurrence -> Occurrence -> Bool
    < :: Occurrence -> Occurrence -> Bool
    $c< :: Occurrence -> Occurrence -> Bool
    compare :: Occurrence -> Occurrence -> Ordering
    $ccompare :: Occurrence -> Occurrence -> Ordering
    Ord, Nat -> Occurrence
    Occurrence -> Nat
    Occurrence -> [Occurrence]
    Occurrence -> Occurrence
    Occurrence -> Occurrence -> [Occurrence]
    Occurrence -> Occurrence -> Occurrence -> [Occurrence]
    (Occurrence -> Occurrence)
    -> (Occurrence -> Occurrence)
    -> (Nat -> Occurrence)
    -> (Occurrence -> Nat)
    -> (Occurrence -> [Occurrence])
    -> (Occurrence -> Occurrence -> [Occurrence])
    -> (Occurrence -> Occurrence -> [Occurrence])
    -> (Occurrence -> Occurrence -> Occurrence -> [Occurrence])
    -> Enum Occurrence
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Nat -> a)
    -> (a -> Nat)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence]
    $cenumFromThenTo :: Occurrence -> Occurrence -> Occurrence -> [Occurrence]
    enumFromTo :: Occurrence -> Occurrence -> [Occurrence]
    $cenumFromTo :: Occurrence -> Occurrence -> [Occurrence]
    enumFromThen :: Occurrence -> Occurrence -> [Occurrence]
    $cenumFromThen :: Occurrence -> Occurrence -> [Occurrence]
    enumFrom :: Occurrence -> [Occurrence]
    $cenumFrom :: Occurrence -> [Occurrence]
    fromEnum :: Occurrence -> Nat
    $cfromEnum :: Occurrence -> Nat
    toEnum :: Nat -> Occurrence
    $ctoEnum :: Nat -> Occurrence
    pred :: Occurrence -> Occurrence
    $cpred :: Occurrence -> Occurrence
    succ :: Occurrence -> Occurrence
    $csucc :: Occurrence -> Occurrence
    Enum, Occurrence
    Occurrence -> Occurrence -> Bounded Occurrence
    forall a. a -> a -> Bounded a
    maxBound :: Occurrence
    $cmaxBound :: Occurrence
    minBound :: Occurrence
    $cminBound :: Occurrence
    Bounded)

    -- Pretty instances.

    instance Pretty Occurrence where
      pretty :: Occurrence -> Doc
    pretty = String -> Doc
    text (String -> Doc) -> (Occurrence -> String) -> Occurrence -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case
        Occurrence
    Unused    -> String
    "_"
        Occurrence
    Mixed     -> String
    "*"
        Occurrence
    JustNeg   -> String
    "-"
        Occurrence
    JustPos   -> String
    "+"
        Occurrence
    StrictPos -> String
    "++"
        Occurrence
    GuardPos  -> String
    "g+"

    instance Pretty Where where
      pretty :: Where -> Doc
    pretty = \case
        Where
    LeftOfArrow  -> Doc
    "LeftOfArrow"
        DefArg QName
    q Nat
    i   -> Doc
    "DefArg"     Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q Doc -> Doc -> Doc
    <+> Nat -> Doc
    forall a. Pretty a => a -> Doc
    pretty Nat
    i
        Where
    UnderInf     -> Doc
    "UnderInf"
        Where
    VarArg       -> Doc
    "VarArg"
        Where
    MetaArg      -> Doc
    "MetaArg"
        ConArgType QName
    q -> Doc
    "ConArgType" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q
        IndArgType QName
    q -> Doc
    "IndArgType" Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q
        InClause Nat
    i   -> Doc
    "InClause"   Doc -> Doc -> Doc
    <+> Nat -> Doc
    forall a. Pretty a => a -> Doc
    pretty Nat
    i
        Where
    Matched      -> Doc
    "Matched"
        Where
    IsIndex      -> Doc
    "IsIndex"
        InDefOf QName
    q    -> Doc
    "InDefOf"    Doc -> Doc -> Doc
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q

    instance Pretty OccursWhere where
      pretty :: OccursWhere -> Doc
    pretty = \case
        OccursWhere Range
    _r Seq Where
    ws1 Seq Where
    ws2 ->
          Doc
    "OccursWhere _" Doc -> Doc -> Doc
    <+> [Where] -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Seq Where -> [Where]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList Seq Where
    ws1) Doc -> Doc -> Doc
    <+> [Where] -> Doc
    forall a. Pretty a => a -> Doc
    pretty (Seq Where -> [Where]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList Seq Where
    ws2)

    -- Other instances for 'Occurrence'.

    instance NFData Occurrence where rnf :: Occurrence -> ()
    rnf Occurrence
    x = Occurrence -> () -> ()
    seq Occurrence
    x ()

    instance KillRange Occurrence where
      killRange :: Occurrence -> Occurrence
    killRange = Occurrence -> Occurrence
    forall a. a -> a
    id

    -- | 'Occurrence' is a complete lattice with least element 'Mixed'
    --   and greatest element 'Unused'.
    --
    --   It forms a commutative semiring where 'oplus' is meet (glb)
    --   and 'otimes' is composition. Both operations are idempotent.
    --
    --   For 'oplus', 'Unused' is neutral (zero) and 'Mixed' is dominant.
    --   For 'otimes', 'StrictPos' is neutral (one) and 'Unused' is dominant.

    instance SemiRing Occurrence where
      ozero :: Occurrence
    ozero = Occurrence
    Unused
      oone :: Occurrence
    oone  = Occurrence
    StrictPos

      oplus :: Occurrence -> Occurrence -> Occurrence
    oplus Occurrence
    Mixed Occurrence
    _           = Occurrence
    Mixed     -- dominant
      oplus Occurrence
    _ Occurrence
    Mixed           = Occurrence
    Mixed
      oplus Occurrence
    Unused Occurrence
    o          = Occurrence
    o         -- neutral
      oplus Occurrence
    o Occurrence
    Unused          = Occurrence
    o
      oplus Occurrence
    JustNeg  Occurrence
    JustNeg  = Occurrence
    JustNeg
      oplus Occurrence
    JustNeg  Occurrence
    o        = Occurrence
    Mixed     -- negative and any form of positve
      oplus Occurrence
    o        Occurrence
    JustNeg  = Occurrence
    Mixed
      oplus Occurrence
    GuardPos Occurrence
    o        = Occurrence
    o         -- second-rank neutral
      oplus Occurrence
    o Occurrence
    GuardPos        = Occurrence
    o
      oplus Occurrence
    StrictPos Occurrence
    o       = Occurrence
    o         -- third-rank neutral
      oplus Occurrence
    o Occurrence
    StrictPos       = Occurrence
    o
      oplus Occurrence
    JustPos Occurrence
    JustPos   = Occurrence
    JustPos

      otimes :: Occurrence -> Occurrence -> Occurrence
    otimes Occurrence
    Unused Occurrence
    _            = Occurrence
    Unused     -- dominant
      otimes Occurrence
    _ Occurrence
    Unused            = Occurrence
    Unused
      otimes Occurrence
    Mixed Occurrence
    _             = Occurrence
    Mixed      -- second-rank dominance
      otimes Occurrence
    _ Occurrence
    Mixed             = Occurrence
    Mixed
      otimes Occurrence
    JustNeg Occurrence
    JustNeg     = Occurrence
    JustPos
      otimes Occurrence
    JustNeg Occurrence
    _           = Occurrence
    JustNeg    -- third-rank dominance
      otimes Occurrence
    _ Occurrence
    JustNeg           = Occurrence
    JustNeg
      otimes Occurrence
    JustPos Occurrence
    _           = Occurrence
    JustPos    -- fourth-rank dominance
      otimes Occurrence
    _ Occurrence
    JustPos           = Occurrence
    JustPos
      otimes Occurrence
    GuardPos Occurrence
    _          = Occurrence
    GuardPos   -- _ `elem` [StrictPos, GuardPos]
      otimes Occurrence
    _ Occurrence
    GuardPos          = Occurrence
    GuardPos
      otimes Occurrence
    StrictPos Occurrence
    StrictPos = Occurrence
    StrictPos  -- neutral

    instance StarSemiRing Occurrence where
      ostar :: Occurrence -> Occurrence
    ostar Occurrence
    Mixed     = Occurrence
    Mixed
      ostar Occurrence
    JustNeg   = Occurrence
    Mixed
      ostar Occurrence
    JustPos   = Occurrence
    JustPos
      ostar Occurrence
    StrictPos = Occurrence
    StrictPos
      ostar Occurrence
    GuardPos  = Occurrence
    StrictPos
      ostar Occurrence
    Unused    = Occurrence
    StrictPos

    instance Null Occurrence where
      empty :: Occurrence
    empty = Occurrence
    Unused

    -- Other instances for 'OccursWhere'.

    -- There is an orphan PrettyTCM instance for Seq OccursWhere in
    -- Agda.TypeChecking.Positivity.

    instance Sized OccursWhere where
      size :: OccursWhere -> Nat
    size (OccursWhere Range
    _ Seq Where
    cs Seq Where
    os) = Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Seq Where -> Nat
    forall a. Sized a => a -> Nat
    size Seq Where
    cs Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Seq Where -> Nat
    forall a. Sized a => a -> Nat
    size Seq Where
    os

    -- | The map contains bindings of the form @bound |-> ess@, satisfying
    -- the following property: for every non-empty list @w@,
    -- @'foldr1' 'otimes' w '<=' bound@ iff
    -- @'or' [ 'all' every w '&&' 'any' some w | (every, some) <- ess ]@.

    boundToEverySome ::
      Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
    boundToEverySome :: Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
    boundToEverySome = ([(Occurrence -> Bool, Occurrence -> Bool)]
     -> [(Occurrence -> Bool, Occurrence -> Bool)]
     -> [(Occurrence -> Bool, Occurrence -> Bool)])
    -> [(Occurrence, [(Occurrence -> Bool, Occurrence -> Bool)])]
    -> Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith [(Occurrence -> Bool, Occurrence -> Bool)]
    -> [(Occurrence -> Bool, Occurrence -> Bool)]
    -> [(Occurrence -> Bool, Occurrence -> Bool)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      [ ( Occurrence
    JustPos
        , [((Occurrence -> Occurrence -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Occurrence
    Unused), (Occurrence -> [Occurrence] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Occurrence
    Mixed, Occurrence
    JustNeg, Occurrence
    JustPos]))]
        )
      , ( Occurrence
    StrictPos
        , [ ((Occurrence -> Occurrence -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Occurrence
    Unused), (Occurrence -> [Occurrence] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Occurrence
    Mixed, Occurrence
    JustNeg, Occurrence
    JustPos]))
          , ((Bool -> Bool
    not (Bool -> Bool) -> (Occurrence -> Bool) -> Occurrence -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Occurrence -> [Occurrence] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Occurrence
    Unused, Occurrence
    GuardPos])), Bool -> Occurrence -> Bool
    forall a b. a -> b -> a
    const Bool
    True)
          ]
        )
      , ( Occurrence
    GuardPos
        , [((Occurrence -> Occurrence -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Occurrence
    Unused), Bool -> Occurrence -> Bool
    forall a b. a -> b -> a
    const Bool
    True)]
        )
      ]

    -- | @productOfEdgesInBoundedWalk occ g u v bound@ returns a value
    -- distinct from 'Nothing' iff there is a walk @c@ (a list of edges)
    -- in @g@, from @u@ to @v@, for which the product @'foldr1' 'otimes'
    -- ('map' occ c) '<=' bound@. In this case the returned value is
    -- @'Just' ('foldr1' 'otimes' c)@ for one such walk @c@.
    --
    -- Preconditions: @u@ and @v@ must belong to @g@, and @bound@ must
    -- belong to the domain of @boundToEverySome@.

    -- There is a property for this function in
    -- Internal.Utils.Graph.AdjacencyMap.Unidirectional.

    productOfEdgesInBoundedWalk ::
      (SemiRing e, Ord n) =>
      (e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
    productOfEdgesInBoundedWalk :: forall e n.
    (SemiRing e, Ord n) =>
    (e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
    productOfEdgesInBoundedWalk e -> Occurrence
    occ Graph n e
    g n
    u n
    v Occurrence
    bound =
      case Occurrence
    -> Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
    -> Maybe [(Occurrence -> Bool, Occurrence -> Bool)]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Occurrence
    bound Map Occurrence [(Occurrence -> Bool, Occurrence -> Bool)]
    boundToEverySome of
        Maybe [(Occurrence -> Bool, Occurrence -> Bool)]
    Nothing  -> Maybe e
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Just [(Occurrence -> Bool, Occurrence -> Bool)]
    ess ->
          case [Maybe [Edge n e]] -> Maybe [Edge n e]
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum [ (Edge n e -> Bool)
    -> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e]
    forall n e.
    Ord n =>
    (Edge n e -> Bool)
    -> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e]
    Graph.walkSatisfying
                        (Occurrence -> Bool
    every (Occurrence -> Bool)
    -> (Edge n e -> Occurrence) -> Edge n e -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . e -> Occurrence
    occ (e -> Occurrence) -> (Edge n e -> e) -> Edge n e -> Occurrence
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Edge n e -> e
    forall n e. Edge n e -> e
    Graph.label)
                        (Occurrence -> Bool
    some (Occurrence -> Bool)
    -> (Edge n e -> Occurrence) -> Edge n e -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . e -> Occurrence
    occ (e -> Occurrence) -> (Edge n e -> e) -> Edge n e -> Occurrence
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Edge n e -> e
    forall n e. Edge n e -> e
    Graph.label)
                        Graph n e
    g n
    u n
    v
                    | (Occurrence -> Bool
    every, Occurrence -> Bool
    some) <- [(Occurrence -> Bool, Occurrence -> Bool)]
    ess
                    ] of
            Just es :: [Edge n e]
    es@(Edge n e
    _ : [Edge n e]
    _) -> e -> Maybe e
    forall a. a -> Maybe a
    Just ((e -> e -> e) -> [e] -> e
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 e -> e -> e
    forall a. SemiRing a => a -> a -> a
    otimes ((Edge n e -> e) -> [Edge n e] -> [e]
    forall a b. (a -> b) -> [a] -> [b]
    map Edge n e -> e
    forall n e. Edge n e -> e
    Graph.label [Edge n e]
    es))
            Just []         -> Maybe e
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            Maybe [Edge n e]
    Nothing         -> Maybe e
    forall a. Maybe a
    Nothing