    -- | Check that a datatype is strictly positive.
    module Agda.TypeChecking.Positivity where

    import Prelude hiding ( null )

    import Control.Applicative hiding (empty)
    import Control.DeepSeq
    import Control.Monad        ( forM_, guard, liftM2 )
    import Control.Monad.Reader ( MonadReader(..), asks, Reader, runReader )

    import Data.Either
    import qualified Data.Foldable as Fold
    import Data.Function
    import Data.Graph (SCC(..))
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Sequence (Seq)
    import qualified Data.Sequence as DS
    import Data.Set (Set)
    import qualified Data.Set as Set

    import Debug.Trace

    import Agda.Syntax.Common
    import qualified Agda.Syntax.Info as Info
    import Agda.Syntax.Internal
    import Agda.Syntax.Position (HasRange(..), noRange)
    import Agda.TypeChecking.Datatypes ( isDataOrRecordType )
    import Agda.TypeChecking.Functions
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Warnings

    import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
    import Agda.Utils.Function (applyUnless)
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Pretty (Pretty, prettyShow)
    import Agda.Utils.SemiRing
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    type Graph n e = Graph.Graph n e

    -- | Check that the datatypes in the mutual block containing the given
    --   declarations are strictly positive.
    --
    --   Also add information about positivity and recursivity of records
    --   to the signature.
    checkStrictlyPositive :: Info.MutualInfo -> Set QName -> TCM ()
    checkStrictlyPositive :: MutualInfo -> Set QName -> TCM ()
    checkStrictlyPositive MutualInfo
    mi Set QName
    qset = do
      -- compute the occurrence graph for qs
      let qs :: [QName]
    qs = Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    qset
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.tick" Nat
    100 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "positivity of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [QName] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [QName]
    qs
      Graph Node (Edge OccursWhere)
    g <- Set QName -> TCM (Graph Node (Edge OccursWhere))
    buildOccurrenceGraph Set QName
    qset
      let (Graph Node Occurrence
    gstar, [SCC Node]
    sccs) =
            Graph Node Occurrence -> (Graph Node Occurrence, [SCC Node])
    forall n e.
    (Ord n, Eq e, StarSemiRing e) =>
    Graph n e -> (Graph n e, [SCC n])
    Graph.gaussJordanFloydWarshallMcNaughtonYamada (Graph Node Occurrence -> (Graph Node Occurrence, [SCC Node]))
    -> Graph Node Occurrence -> (Graph Node Occurrence, [SCC Node])
    forall a b. (a -> b) -> a -> b
    $ (Edge OccursWhere -> Occurrence)
    -> Graph Node (Edge OccursWhere) -> Graph Node Occurrence
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Edge OccursWhere -> Occurrence
    forall {a}. Edge a -> Occurrence
    occ Graph Node (Edge OccursWhere)
    g
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.tick" Nat
    100 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "constructed graph"
      ArgName -> Nat -> ArgName -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> ArgName -> m ()
    reportSLn ArgName
    "tc.pos.graph" Nat
    5 (ArgName -> TCM ()) -> ArgName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "Positivity graph: N=" ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Nat -> ArgName
    forall a. Show a => a -> ArgName
    show (Set Node -> Nat
    forall a. Sized a => a -> Nat
    size (Set Node -> Nat) -> Set Node -> Nat
    forall a b. (a -> b) -> a -> b
    $ Graph Node (Edge OccursWhere) -> Set Node
    forall n e. Graph n e -> Set n
    Graph.nodes Graph Node (Edge OccursWhere)
    g) ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++
                                   ArgName
    " E=" ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Nat -> ArgName
    forall a. Show a => a -> ArgName
    show ([Edge Node (Edge OccursWhere)] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length ([Edge Node (Edge OccursWhere)] -> Nat)
    -> [Edge Node (Edge OccursWhere)] -> Nat
    forall a b. (a -> b) -> a -> b
    $ Graph Node (Edge OccursWhere) -> [Edge Node (Edge OccursWhere)]
    forall n e. Graph n e -> [Edge n e]
    Graph.edges Graph Node (Edge OccursWhere)
    g)
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.graph" Nat
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "positivity graph for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ((QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [QName]
    qs)
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Graph Node (Edge OccursWhere) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Graph Node (Edge OccursWhere)
    g
        ]
      ArgName -> Nat -> ArgName -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> ArgName -> m ()
    reportSLn ArgName
    "tc.pos.graph" Nat
    5 (ArgName -> TCM ()) -> ArgName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        ArgName
    "Positivity graph (completed): E=" ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Nat -> ArgName
    forall a. Show a => a -> ArgName
    show ([Edge Node Occurrence] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length ([Edge Node Occurrence] -> Nat) -> [Edge Node Occurrence] -> Nat
    forall a b. (a -> b) -> a -> b
    $ Graph Node Occurrence -> [Edge Node Occurrence]
    forall n e. Graph n e -> [Edge n e]
    Graph.edges Graph Node Occurrence
    gstar)
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.graph" Nat
    50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "transitive closure of positivity graph for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
          [QName] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [QName]
    qs
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Graph Node Occurrence -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Graph Node Occurrence
    gstar
        ]

      -- remember argument occurrences for qs in the signature
      Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
    setArgOccs Set QName
    qset [QName]
    qs Graph Node Occurrence
    gstar
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.tick" Nat
    100 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "set args"

      -- check positivity for all strongly connected components of the graph for qs
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.graph.sccs" Nat
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let ([Node]
    triv, [[Node]]
    others) = [Either Node [Node]] -> ([Node], [[Node]])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either Node [Node]] -> ([Node], [[Node]]))
    -> [Either Node [Node]] -> ([Node], [[Node]])
    forall a b. (a -> b) -> a -> b
    $ [SCC Node]
    -> (SCC Node -> Either Node [Node]) -> [Either Node [Node]]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [SCC Node]
    sccs ((SCC Node -> Either Node [Node]) -> [Either Node [Node]])
    -> (SCC Node -> Either Node [Node]) -> [Either Node [Node]]
    forall a b. (a -> b) -> a -> b
    $ \case
              AcyclicSCC Node
    v -> Node -> Either Node [Node]
    forall a b. a -> Either a b
    Left Node
    v
              CyclicSCC [Node]
    vs -> [Node] -> Either Node [Node]
    forall a b. b -> Either a b
    Right [Node]
    vs
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Nat -> ArgName
    forall a. Show a => a -> ArgName
    show ([Node] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Node]
    triv) ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " trivial sccs"
            , ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Nat -> ArgName
    forall a. Show a => a -> ArgName
    show ([[Node]] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [[Node]]
    others) ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " non-trivial sccs with lengths " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++
                [Nat] -> ArgName
    forall a. Show a => a -> ArgName
    show (([Node] -> Nat) -> [[Node]] -> [Nat]
    forall a b. (a -> b) -> [a] -> [b]
    map [Node] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [[Node]]
    others)
            ]
      ArgName -> Nat -> ArgName -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> ArgName -> m ()
    reportSLn ArgName
    "tc.pos.graph.sccs" Nat
    15 (ArgName -> TCM ()) -> ArgName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        ArgName
    "  sccs = " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ [[Node]] -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow [ [Node]
    scc | CyclicSCC [Node]
    scc <- [SCC Node]
    sccs ]
      [SCC Node] -> (SCC Node -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [SCC Node]
    sccs ((SCC Node -> TCM ()) -> TCM ()) -> (SCC Node -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \case
        -- If the mutuality information has never been set, we set it to []
        AcyclicSCC (DefNode QName
    q) -> TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Maybe [QName] -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe [QName] -> Bool) -> TCMT IO (Maybe [QName]) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (Maybe [QName])
    getMutual QName
    q) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          ArgName -> Nat -> ArgName -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> ArgName -> m ()
    reportSLn ArgName
    "tc.pos.mutual" Nat
    10 (ArgName -> TCM ()) -> ArgName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "setting " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow QName
    q ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " to non-recursive"
          -- Andreas, 2017-04-26, issue #2555
          -- We should not have @DefNode@s pointing outside our formal mutual block.
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    q Set QName
    qset) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          QName -> [QName] -> TCM ()
    setMutual QName
    q []
        AcyclicSCC (ArgNode{}) -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        CyclicSCC [Node]
    scc          -> [QName] -> TCM ()
    setMut [ QName
    q | DefNode QName
    q <- [Node]
    scc ]
      (QName -> TCM ()) -> [QName] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Graph Node (Edge OccursWhere)
    -> Graph Node Occurrence -> QName -> TCM ()
    checkPos Graph Node (Edge OccursWhere)
    g Graph Node Occurrence
    gstar) [QName]
    qs
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.tick" Nat
    100 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checked positivity"

      where
        checkPos :: Graph Node (Edge OccursWhere) ->
                    Graph Node Occurrence ->
                    QName -> TCM ()
        checkPos :: Graph Node (Edge OccursWhere)
    -> Graph Node Occurrence -> QName -> TCM ()
    checkPos Graph Node (Edge OccursWhere)
    g Graph Node Occurrence
    gstar QName
    q = QName -> (Definition -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    q ((Definition -> TCM ()) -> TCM ())
    -> (Definition -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    _def -> do
          -- we check positivity only for data or record definitions
          TCMT IO (Maybe DataOrRecord) -> (DataOrRecord -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (QName -> TCMT IO (Maybe DataOrRecord)
    isDatatype QName
    q) ((DataOrRecord -> TCM ()) -> TCM ())
    -> (DataOrRecord -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ DataOrRecord
    dr -> do
            ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.check" Nat
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Checking positivity of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q

            let loop :: Maybe Occurrence
                loop :: Maybe Occurrence
    loop = Node -> Node -> Graph Node Occurrence -> Maybe Occurrence
    forall n e. Ord n => n -> n -> Graph n e -> Maybe e
    Graph.lookup (QName -> Node
    DefNode QName
    q) (QName -> Node
    DefNode QName
    q) Graph Node Occurrence
    gstar

                g' :: Graph Node (Edge (Seq OccursWhere))
                g' :: Graph Node (Edge (Seq OccursWhere))
    g' = (Edge OccursWhere -> Edge (Seq OccursWhere))
    -> Graph Node (Edge OccursWhere)
    -> Graph Node (Edge (Seq OccursWhere))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((OccursWhere -> Seq OccursWhere)
    -> Edge OccursWhere -> Edge (Seq OccursWhere)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap OccursWhere -> Seq OccursWhere
    forall a. a -> Seq a
    DS.singleton) Graph Node (Edge OccursWhere)
    g

                -- Note the property
                -- Internal.Utils.Graph.AdjacencyMap.Unidirectional.prop_productOfEdgesInBoundedWalk,
                -- which relates productOfEdgesInBoundedWalk to
                -- gaussJordanFloydWarshallMcNaughtonYamada.

                reason :: Occurrence -> Seq OccursWhere
    reason Occurrence
    bound =
                  case (Edge (Seq OccursWhere) -> Occurrence)
    -> Graph Node (Edge (Seq OccursWhere))
    -> Node
    -> Node
    -> Occurrence
    -> Maybe (Edge (Seq OccursWhere))
    forall e n.
    (SemiRing e, Ord n) =>
    (e -> Occurrence) -> Graph n e -> n -> n -> Occurrence -> Maybe e
    productOfEdgesInBoundedWalk
                         Edge (Seq OccursWhere) -> Occurrence
    forall {a}. Edge a -> Occurrence
    occ Graph Node (Edge (Seq OccursWhere))
    g' (QName -> Node
    DefNode QName
    q) (QName -> Node
    DefNode QName
    q) Occurrence
    bound of
                    Just (Edge Occurrence
    _ Seq OccursWhere
    how) -> Seq OccursWhere
    how
                    Maybe (Edge (Seq OccursWhere))
    Nothing           -> Seq OccursWhere
    forall a. HasCallStack => a
    __IMPOSSIBLE__

                how :: String -> Occurrence -> TCM Doc
                how :: ArgName -> Occurrence -> TCMT IO Doc
    how ArgName
    msg Occurrence
    bound = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
                      [QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++ ArgName -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "is" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
                      ArgName -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords (ArgName
    msg ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    ", because it occurs") [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
                      [Seq OccursWhere -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Occurrence -> Seq OccursWhere
    reason Occurrence
    bound)]

            -- if we have a negative loop, raise error

            -- ASR (23 December 2015). We don't raise a strictly positive
            -- error if the NO_POSITIVITY_CHECK pragma was set on in the
            -- mutual block. See Issue 1614.
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (MutualInfo -> PositivityCheck
    Info.mutualPositivityCheck MutualInfo
    mi PositivityCheck -> PositivityCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == PositivityCheck
    YesPositivityCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    positivityCheckEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                case Maybe Occurrence
    loop of
                Just Occurrence
    o | Occurrence
    o Occurrence -> Occurrence -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Occurrence
    JustPos ->
                  Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Seq OccursWhere -> Warning
    NotStrictlyPositive QName
    q (Occurrence -> Seq OccursWhere
    reason Occurrence
    JustPos)
                Maybe Occurrence
    _ -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

            -- if we find an unguarded record, mark it as such
            case DataOrRecord
    dr of
              DataOrRecord
    IsData -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              IsRecord PatternOrCopattern
    pat -> case Maybe Occurrence
    loop of
                Just Occurrence
    o | Occurrence
    o Occurrence -> Occurrence -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Occurrence
    StrictPos -> do
                  ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.record" Nat
    5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Occurrence -> TCMT IO Doc
    how ArgName
    "not guarded" Occurrence
    StrictPos
                  QName -> PatternOrCopattern -> TCM ()
    unguardedRecord QName
    q PatternOrCopattern
    pat
                  QName -> TCM ()
    checkInduction QName
    q
                -- otherwise, if the record is recursive, mark it as well
                Just Occurrence
    o | Occurrence
    o Occurrence -> Occurrence -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Occurrence
    GuardPos -> do
                  ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.record" Nat
    5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Occurrence -> TCMT IO Doc
    how ArgName
    "recursive" Occurrence
    GuardPos
                  QName -> TCM ()
    recursiveRecord QName
    q
                  QName -> TCM ()
    checkInduction QName
    q
                -- If the record is not recursive, switch on eta
                -- unless it is coinductive or a no-eta-equality record.
                Maybe Occurrence
    Nothing -> do
                  ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.record" Nat
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                    TCMT IO Doc
    "record type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                    TCMT IO Doc
    "is not recursive"
                  QName -> TCM ()
    nonRecursiveRecord QName
    q
                Maybe Occurrence
    _ -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

        checkInduction :: QName -> TCM ()
        checkInduction :: QName -> TCM ()
    checkInduction QName
    q =
          -- ASR (01 January 2016). We don't raise this error if the
          -- NO_POSITIVITY_CHECK pragma was set on in the record. See
          -- Issue 1760.
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (MutualInfo -> PositivityCheck
    Info.mutualPositivityCheck MutualInfo
    mi PositivityCheck -> PositivityCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == PositivityCheck
    YesPositivityCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    positivityCheckEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            -- Check whether the recursive record has been declared as
            -- 'Inductive' or 'Coinductive'.  Otherwise, error.
            TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (Maybe Induction -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Induction -> Bool)
    -> (Definition -> Maybe Induction) -> Definition -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Defn -> Maybe Induction
    recInduction (Defn -> Maybe Induction)
    -> (Definition -> Defn) -> Definition -> Maybe Induction
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Bool) -> TCMT IO Definition -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              Range -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (Name -> Range
    nameBindingSite (Name -> Range) -> Name -> Range
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    q) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                  TCMT IO Doc
    "Recursive record" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                  TCMT IO Doc
    "needs to be declared as either inductive or coinductive"

        occ :: Edge a -> Occurrence
    occ (Edge Occurrence
    o a
    _) = Occurrence
    o

        isDatatype :: QName -> TCM (Maybe DataOrRecord)
        isDatatype :: QName -> TCMT IO (Maybe DataOrRecord)
    isDatatype QName
    q = do
          Defn
    def <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
          Maybe DataOrRecord -> TCMT IO (Maybe DataOrRecord)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe DataOrRecord -> TCMT IO (Maybe DataOrRecord))
    -> Maybe DataOrRecord -> TCMT IO (Maybe DataOrRecord)
    forall a b. (a -> b) -> a -> b
    $ case Defn
    def of
            Datatype{dataClause :: Defn -> Maybe Clause
    dataClause = Maybe Clause
    Nothing} -> DataOrRecord -> Maybe DataOrRecord
    forall a. a -> Maybe a
    Just DataOrRecord
    IsData
            Record  {recClause :: Defn -> Maybe Clause
    recClause  = Maybe Clause
    Nothing, PatternOrCopattern
    recPatternMatching :: Defn -> PatternOrCopattern
    recPatternMatching :: PatternOrCopattern
    recPatternMatching } -> DataOrRecord -> Maybe DataOrRecord
    forall a. a -> Maybe a
    Just (DataOrRecord -> Maybe DataOrRecord)
    -> DataOrRecord -> Maybe DataOrRecord
    forall a b. (a -> b) -> a -> b
    $ PatternOrCopattern -> DataOrRecord
    IsRecord PatternOrCopattern
    recPatternMatching
            Defn
    _ -> Maybe DataOrRecord
    forall a. Maybe a
    Nothing

        -- Set the mutually recursive identifiers for a SCC.
        setMut :: [QName] -> TCM ()
        setMut :: [QName] -> TCM ()
    setMut [] = () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()  -- nothing to do
        setMut [QName]
    qs = [QName] -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [QName]
    qs ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    q -> do
          ArgName -> Nat -> ArgName -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> ArgName -> m ()
    reportSLn ArgName
    "tc.pos.mutual" Nat
    10 (ArgName -> TCM ()) -> ArgName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "setting " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow QName
    q ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " to (mutually) recursive"
          QName -> [QName] -> TCM ()
    setMutual QName
    q [QName]
    qs
          -- TODO: The previous line produces data of quadratic size
          -- (which has to be processed upon serialization).  Presumably qs is
          -- usually short, but in some cases (for instance for generated
          -- code) it may be long. Wouldn't it be better to assign a
          -- unique identifier to each SCC, and avoid storing lists?

        -- Set the polarity of the arguments to a couple of definitions
        setArgOccs :: Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
        setArgOccs :: Set QName -> [QName] -> Graph Node Occurrence -> TCM ()
    setArgOccs Set QName
    qset [QName]
    qs Graph Node Occurrence
    g = do
          -- Andreas, 2018-05-11, issue #3049: we need to be pessimistic about
          -- argument polarity beyond the formal arity of the function.
          --
          -- -- Compute a map from each name in q to the maximal argument index
          -- let maxs = Map.fromListWith max
          --      [ (q, i) | ArgNode q i <- Set.toList $ Graph.nodes g, q `Set.member` qset ]
          [QName] -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [QName]
    qs ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    q -> QName -> (Definition -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    q ((Definition -> TCM ()) -> TCM ())
    -> (Definition -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    def -> Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Defn -> Bool
    hasDefinition (Defn -> Bool) -> Defn -> Bool
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.args" Nat
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checking args of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q
            Nat
    n <- Definition -> TCM Nat
    getDefArity Definition
    def
            -- If there is no outgoing edge @ArgNode q i@, all @n@ arguments are @Unused@.
            -- Otherwise, we obtain the occurrences from the Graph.
            let findOcc :: Nat -> Occurrence
    findOcc Nat
    i = Occurrence -> Maybe Occurrence -> Occurrence
    forall a. a -> Maybe a -> a
    fromMaybe Occurrence
    Unused (Maybe Occurrence -> Occurrence) -> Maybe Occurrence -> Occurrence
    forall a b. (a -> b) -> a -> b
    $ Node -> Node -> Graph Node Occurrence -> Maybe Occurrence
    forall n e. Ord n => n -> n -> Graph n e -> Maybe e
    Graph.lookup (QName -> Nat -> Node
    ArgNode QName
    q Nat
    i) (QName -> Node
    DefNode QName
    q) Graph Node Occurrence
    g
                args :: [Occurrence]
    args = -- caseMaybe (Map.lookup q maxs) (replicate n Unused) $ \ m ->
                  (Nat -> Occurrence) -> [Nat] -> [Occurrence]
    forall a b. (a -> b) -> [a] -> [b]
    map Nat -> Occurrence
    findOcc [Nat
    0 .. Nat
    nNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1]  -- [0 .. max m (n - 1)] -- triggers issue #3049
            ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.args" Nat
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
              [ TCMT IO Doc
    "args of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "="
              , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Occurrence -> TCMT IO Doc) -> [Occurrence] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Occurrence -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Occurrence]
    args
              ]
            -- The list args can take a long time to compute, but contains
            -- small elements, and is stored in the interface (right?), so
            -- it is computed deep-strictly.
            QName -> [Occurrence] -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> [Occurrence] -> m ()
    setArgOccurrences QName
    q ([Occurrence] -> TCM ()) -> [Occurrence] -> TCM ()
    forall a b. NFData a => (a -> b) -> a -> b
    $!! [Occurrence]
    args
          where
          -- Andreas, 2018-11-23, issue #3404
          -- Only assign argument occurrences to things which have a definition.
          -- Things without a definition would be judged "constant" in all arguments,
          -- since no occurrence could possibly be found, naturally.
          hasDefinition :: Defn -> Bool
          hasDefinition :: Defn -> Bool
    hasDefinition = \case
            Axiom{}            -> Bool
    False
            DataOrRecSig{}     -> Bool
    False
            GeneralizableVar{} -> Bool
    False
            AbstractDefn{}     -> Bool
    False
            Primitive{}        -> Bool
    False
            PrimitiveSort{}    -> Bool
    False
            Constructor{}      -> Bool
    False
            Function{}         -> Bool
    True
            Datatype{}         -> Bool
    True
            Record{}           -> Bool
    True

    getDefArity :: Definition -> TCM Int
    getDefArity :: Definition -> TCM Nat
    getDefArity Definition
    def = do
      Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    subtract (Definition -> Nat
    projectionArgs Definition
    def) (Nat -> Nat) -> TCM Nat -> TCM Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCM Nat
    arity' (Definition -> Type
    defType Definition
    def)
      where
      -- A variant of "\t -> arity <$> instantiateFull t".
      arity' :: Type -> TCM Int
      arity' :: Type -> TCM Nat
    arity' Type
    t = do
        Type
    t <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Type
    t
        case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
          Pi Dom Type
    _ Abs Type
    t -> Nat -> Nat
    forall a. Enum a => a -> a
    succ (Nat -> Nat) -> TCM Nat -> TCM Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCM Nat
    arity' (Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    t)
          Term
    _      -> Nat -> TCM Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    0

    -- Computing occurrences --------------------------------------------------

    data Item = AnArg Nat
              | ADef QName
      deriving (Item -> Item -> Bool
    (Item -> Item -> Bool) -> (Item -> Item -> Bool) -> Eq Item
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Item -> Item -> Bool
    $c/= :: Item -> Item -> Bool
    == :: Item -> Item -> Bool
    $c== :: Item -> Item -> Bool
    Eq, Eq Item
    Eq Item
    -> (Item -> Item -> Ordering)
    -> (Item -> Item -> Bool)
    -> (Item -> Item -> Bool)
    -> (Item -> Item -> Bool)
    -> (Item -> Item -> Bool)
    -> (Item -> Item -> Item)
    -> (Item -> Item -> Item)
    -> Ord Item
    Item -> Item -> Bool
    Item -> Item -> Ordering
    Item -> Item -> Item
    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 :: Item -> Item -> Item
    $cmin :: Item -> Item -> Item
    max :: Item -> Item -> Item
    $cmax :: Item -> Item -> Item
    >= :: Item -> Item -> Bool
    $c>= :: Item -> Item -> Bool
    > :: Item -> Item -> Bool
    $c> :: Item -> Item -> Bool
    <= :: Item -> Item -> Bool
    $c<= :: Item -> Item -> Bool
    < :: Item -> Item -> Bool
    $c< :: Item -> Item -> Bool
    compare :: Item -> Item -> Ordering
    $ccompare :: Item -> Item -> Ordering
    Ord, Nat -> Item -> ArgName -> ArgName
    [Item] -> ArgName -> ArgName
    Item -> ArgName
    (Nat -> Item -> ArgName -> ArgName)
    -> (Item -> ArgName) -> ([Item] -> ArgName -> ArgName) -> Show Item
    forall a.
    (Nat -> a -> ArgName -> ArgName)
    -> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
    showList :: [Item] -> ArgName -> ArgName
    $cshowList :: [Item] -> ArgName -> ArgName
    show :: Item -> ArgName
    $cshow :: Item -> ArgName
    showsPrec :: Nat -> Item -> ArgName -> ArgName
    $cshowsPrec :: Nat -> Item -> ArgName -> ArgName
    Show)

    instance HasRange Item where
      getRange :: Item -> Range
    getRange (AnArg Nat
    _) = Range
    forall a. Range' a
    noRange
      getRange (ADef QName
    qn)   = QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    qn

    instance Pretty Item where
      prettyPrec :: Nat -> Item -> Doc
    prettyPrec Nat
    p (AnArg Nat
    i) = Bool -> Doc -> Doc
    P.mparens (Nat
    p Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "AnArg" Doc -> Doc -> Doc
    P.<+> Nat -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty Nat
    i
      prettyPrec Nat
    p (ADef QName
    qn) = Bool -> Doc -> Doc
    P.mparens (Nat
    p Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    9) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    "ADef"  Doc -> Doc -> Doc
    P.<+> QName -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty QName
    qn

    type Occurrences = Map Item [OccursWhere]

    -- | Used to build 'Occurrences' and occurrence graphs.
    data OccurrencesBuilder
      = Concat [OccurrencesBuilder]
      | OccursAs Where OccurrencesBuilder
      | OccursHere Item
      | OnlyVarsUpTo Nat OccurrencesBuilder
        -- ^ @OnlyVarsUpTo n occs@ discards occurrences of de Bruijn index
        -- @>= n@.

    -- | Used to build 'Occurrences' and occurrence graphs.
    data OccurrencesBuilder'
      = Concat' [OccurrencesBuilder']
      | OccursAs' Where OccurrencesBuilder'
      | OccursHere' Item

    -- | The semigroup laws only hold up to flattening of 'Concat'.
    instance Semigroup OccurrencesBuilder where
      OccurrencesBuilder
    occs1 <> :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
    <> OccurrencesBuilder
    occs2 = [OccurrencesBuilder] -> OccurrencesBuilder
    Concat [OccurrencesBuilder
    occs1, OccurrencesBuilder
    occs2]

    -- | The monoid laws only hold up to flattening of 'Concat'.
    instance Monoid OccurrencesBuilder where
      mempty :: OccurrencesBuilder
    mempty  = [OccurrencesBuilder] -> OccurrencesBuilder
    Concat []
      mappend :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
    mappend = OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
    forall a. Semigroup a => a -> a -> a
    (<>)
      mconcat :: [OccurrencesBuilder] -> OccurrencesBuilder
    mconcat = [OccurrencesBuilder] -> OccurrencesBuilder
    Concat

    -- | Removes 'OnlyVarsUpTo' entries.
    preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
    preprocess :: OccurrencesBuilder -> OccurrencesBuilder'
    preprocess OccurrencesBuilder
    ob = case Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
    pp Maybe Nat
    forall a. Maybe a
    Nothing OccurrencesBuilder
    ob of
      Maybe OccurrencesBuilder'
    Nothing -> [OccurrencesBuilder'] -> OccurrencesBuilder'
    Concat' []
      Just OccurrencesBuilder'
    ob -> OccurrencesBuilder'
    ob
      where
      pp :: Maybe Nat  -- Variables larger than or equal to this number, if any,
                       -- are not retained.
         -> OccurrencesBuilder
         -> Maybe OccurrencesBuilder'
      pp :: Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
    pp !Maybe Nat
    m = \case
        Concat [OccurrencesBuilder]
    obs -> case (OccurrencesBuilder -> Maybe OccurrencesBuilder')
    -> [OccurrencesBuilder] -> [OccurrencesBuilder']
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
    pp Maybe Nat
    m) [OccurrencesBuilder]
    obs of
          []  -> Maybe OccurrencesBuilder'
    forall a. Maybe a
    Nothing
          [OccurrencesBuilder']
    obs -> OccurrencesBuilder' -> Maybe OccurrencesBuilder'
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([OccurrencesBuilder'] -> OccurrencesBuilder'
    Concat' [OccurrencesBuilder']
    obs)

        OccursAs Where
    w OccurrencesBuilder
    ob -> Where -> OccurrencesBuilder' -> OccurrencesBuilder'
    OccursAs' Where
    w (OccurrencesBuilder' -> OccurrencesBuilder')
    -> Maybe OccurrencesBuilder' -> Maybe OccurrencesBuilder'
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
    pp Maybe Nat
    m OccurrencesBuilder
    ob

        OnlyVarsUpTo Nat
    n OccurrencesBuilder
    ob -> Maybe Nat -> OccurrencesBuilder -> Maybe OccurrencesBuilder'
    pp (Nat -> Maybe Nat
    forall a. a -> Maybe a
    Just (Nat -> Maybe Nat) -> Nat -> Maybe Nat
    forall a b. (a -> b) -> a -> b
    $! Nat -> (Nat -> Nat) -> Maybe Nat -> Nat
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Nat
    n (Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    min Nat
    n) Maybe Nat
    m) OccurrencesBuilder
    ob

        OccursHere Item
    i -> do
          Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard Bool
    keep
          OccurrencesBuilder' -> Maybe OccurrencesBuilder'
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Item -> OccurrencesBuilder'
    OccursHere' Item
    i)
          where
          keep :: Bool
    keep = case (Maybe Nat
    m, Item
    i) of
            (Maybe Nat
    Nothing, Item
    _)      -> Bool
    True
            (Maybe Nat
    _, ADef QName
    _)       -> Bool
    True
            (Just Nat
    m, AnArg Nat
    i) -> Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    m

    -- | An interpreter for 'OccurrencesBuilder'.
    --
    -- WARNING: There can be lots of sharing between the generated
    -- 'OccursWhere' entries. Traversing all of these entries could be
    -- expensive. (See 'computeEdges' for an example.)
    flatten :: OccurrencesBuilder -> Map Item Integer
    flatten :: OccurrencesBuilder -> Map Item Integer
    flatten =
      (Integer -> Integer -> Integer)
    -> [(Item, Integer)] -> Map Item Integer
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (+) ([(Item, Integer)] -> Map Item Integer)
    -> (OccurrencesBuilder -> [(Item, Integer)])
    -> OccurrencesBuilder
    -> Map Item Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
      (OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)])
    -> [(Item, Integer)] -> OccurrencesBuilder' -> [(Item, Integer)]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)]
    flatten' [] (OccurrencesBuilder' -> [(Item, Integer)])
    -> (OccurrencesBuilder -> OccurrencesBuilder')
    -> OccurrencesBuilder
    -> [(Item, Integer)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
      OccurrencesBuilder -> OccurrencesBuilder'
    preprocess
      where
      flatten'
        :: OccurrencesBuilder'
        -> [(Item, Integer)]
        -> [(Item, Integer)]
      flatten' :: OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)]
    flatten' (Concat' [OccurrencesBuilder']
    obs)    = (OccurrencesBuilder'
     -> ([(Item, Integer)] -> [(Item, Integer)])
     -> [(Item, Integer)]
     -> [(Item, Integer)])
    -> ([(Item, Integer)] -> [(Item, Integer)])
    -> [OccurrencesBuilder']
    -> [(Item, Integer)]
    -> [(Item, Integer)]
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\OccurrencesBuilder'
    occs [(Item, Integer)] -> [(Item, Integer)]
    f -> OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)]
    flatten' OccurrencesBuilder'
    occs ([(Item, Integer)] -> [(Item, Integer)])
    -> ([(Item, Integer)] -> [(Item, Integer)])
    -> [(Item, Integer)]
    -> [(Item, Integer)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(Item, Integer)] -> [(Item, Integer)]
    f) [(Item, Integer)] -> [(Item, Integer)]
    forall a. a -> a
    id [OccurrencesBuilder']
    obs
      flatten' (OccursAs' Where
    _ OccurrencesBuilder'
    ob) = OccurrencesBuilder' -> [(Item, Integer)] -> [(Item, Integer)]
    flatten' OccurrencesBuilder'
    ob
      flatten' (OccursHere' Item
    i)  = ((Item
    i, Integer
    1) (Item, Integer) -> [(Item, Integer)] -> [(Item, Integer)]
    forall a. a -> [a] -> [a]
    :)

    -- | Context for computing occurrences.
    data OccEnv = OccEnv
      { OccEnv -> [Maybe Item]
    vars :: [Maybe Item]
        -- ^ Items corresponding to the free variables.
        --
        --   Potential invariant: It seems as if the list has the form
        --   @'genericReplicate' n 'Nothing' ++ 'map' ('Just' . 'AnArg') is@,
        --   for some @n@ and @is@, where @is@ is decreasing
        --   (non-strictly).
      , OccEnv -> Maybe QName
    inf  :: Maybe QName
        -- ^ Name for ∞ builtin.
      }

    -- | Monad for computing occurrences.
    type OccM = Reader OccEnv

    instance (Semigroup a, Monoid a) => Monoid (OccM a) where
      mempty :: OccM a
    mempty  = a -> OccM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    forall a. Monoid a => a
    mempty
      mappend :: OccM a -> OccM a -> OccM a
    mappend = OccM a -> OccM a -> OccM a
    forall a. Semigroup a => a -> a -> a
    (<>)
      mconcat :: [OccM a] -> OccM a
    mconcat = [a] -> a
    forall a. Monoid a => [a] -> a
    mconcat ([a] -> a)
    -> ([OccM a] -> ReaderT OccEnv Identity [a]) -> [OccM a] -> OccM a
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> [OccM a] -> ReaderT OccEnv Identity [a]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence

    withExtendedOccEnv :: Maybe Item -> OccM a -> OccM a
    withExtendedOccEnv :: forall a. Maybe Item -> OccM a -> OccM a
    withExtendedOccEnv Maybe Item
    i = [Maybe Item] -> OccM a -> OccM a
    forall a. [Maybe Item] -> OccM a -> OccM a
    withExtendedOccEnv' [Maybe Item
    i]

    withExtendedOccEnv' :: [Maybe Item] -> OccM a -> OccM a
    withExtendedOccEnv' :: forall a. [Maybe Item] -> OccM a -> OccM a
    withExtendedOccEnv' [Maybe Item]
    is = (OccEnv -> OccEnv)
    -> ReaderT OccEnv Identity a -> ReaderT OccEnv Identity a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((OccEnv -> OccEnv)
     -> ReaderT OccEnv Identity a -> ReaderT OccEnv Identity a)
    -> (OccEnv -> OccEnv)
    -> ReaderT OccEnv Identity a
    -> ReaderT OccEnv Identity a
    forall a b. (a -> b) -> a -> b
    $ \ OccEnv
    e -> OccEnv
    e { vars :: [Maybe Item]
    vars = [Maybe Item]
    is [Maybe Item] -> [Maybe Item] -> [Maybe Item]
    forall a. [a] -> [a] -> [a]
    ++ OccEnv -> [Maybe Item]
    vars OccEnv
    e }

    -- | Running the monad
    getOccurrences
      :: (Show a, PrettyTCM a, ComputeOccurrences a)
      => [Maybe Item]  -- ^ Extension of the 'OccEnv', usually a local variable context.
      -> a
      -> TCM OccurrencesBuilder
    getOccurrences :: forall a.
    (Show a, PrettyTCM a, ComputeOccurrences a) =>
    [Maybe Item] -> a -> TCMT IO OccurrencesBuilder
    getOccurrences [Maybe Item]
    vars a
    a = do
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.occ" Nat
    70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "computing occurrences in " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (a -> ArgName
    forall a. Show a => a -> ArgName
    show a
    a)
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.occ" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "computing occurrences in " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    a
      Reader OccEnv OccurrencesBuilder -> OccEnv -> OccurrencesBuilder
    forall r a. Reader r a -> r -> a
    runReader (a -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences a
    a) (OccEnv -> OccurrencesBuilder)
    -> (Maybe CoinductionKit -> OccEnv)
    -> Maybe CoinductionKit
    -> OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Maybe Item] -> Maybe QName -> OccEnv
    OccEnv [Maybe Item]
    vars (Maybe QName -> OccEnv)
    -> (Maybe CoinductionKit -> Maybe QName)
    -> Maybe CoinductionKit
    -> OccEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CoinductionKit -> QName
    nameOfInf (Maybe CoinductionKit -> OccurrencesBuilder)
    -> TCMT IO (Maybe CoinductionKit) -> TCMT IO OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe CoinductionKit)
    coinductionKit

    class ComputeOccurrences a where
      occurrences :: a -> OccM OccurrencesBuilder

      default occurrences :: (Foldable t, ComputeOccurrences b, t b ~ a) => a -> OccM OccurrencesBuilder
      occurrences = (b -> Reader OccEnv OccurrencesBuilder)
    -> t b -> Reader OccEnv OccurrencesBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap b -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences

    instance ComputeOccurrences Clause where
      occurrences :: Clause -> Reader OccEnv OccurrencesBuilder
    occurrences Clause
    cl = do
        let ps :: NAPs
    ps    = Clause -> NAPs
    namedClausePats Clause
    cl
            items :: [Maybe Item]
    items = IntMap (Maybe Item) -> [Maybe Item]
    forall a. IntMap a -> [a]
    IntMap.elems (IntMap (Maybe Item) -> [Maybe Item])
    -> IntMap (Maybe Item) -> [Maybe Item]
    forall a b. (a -> b) -> a -> b
    $ NAPs -> IntMap (Maybe Item)
    patItems NAPs
    ps -- sorted from low to high DBI
        ([OccurrencesBuilder] -> OccurrencesBuilder
    Concat (((Nat, Arg (Named NamedName DeBruijnPattern))
     -> Maybe OccurrencesBuilder)
    -> [(Nat, Arg (Named NamedName DeBruijnPattern))]
    -> [OccurrencesBuilder]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (Nat, Arg (Named NamedName DeBruijnPattern))
    -> Maybe OccurrencesBuilder
    forall {name} {a}.
    (Nat, Arg (Named name (Pattern' a))) -> Maybe OccurrencesBuilder
    matching ([Nat] -> NAPs -> [(Nat, Arg (Named NamedName DeBruijnPattern))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Nat
    0..] NAPs
    ps)) OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder
    forall a. Semigroup a => a -> a -> a
    <>) (OccurrencesBuilder -> OccurrencesBuilder)
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          [Maybe Item]
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall a. [Maybe Item] -> OccM a -> OccM a
    withExtendedOccEnv' [Maybe Item]
    items (Reader OccEnv OccurrencesBuilder
     -> Reader OccEnv OccurrencesBuilder)
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $
            Maybe Term -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences (Maybe Term -> Reader OccEnv OccurrencesBuilder)
    -> Maybe Term -> Reader OccEnv OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Term
    clauseBody Clause
    cl
        where
          matching :: (Nat, Arg (Named name (Pattern' a))) -> Maybe OccurrencesBuilder
    matching (Nat
    i, Arg (Named name (Pattern' a))
    p)
            | Pattern' a -> Bool
    forall a. Pattern' a -> Bool
    properlyMatching (Named name (Pattern' a) -> Pattern' a
    forall name a. Named name a -> a
    namedThing (Named name (Pattern' a) -> Pattern' a)
    -> Named name (Pattern' a) -> Pattern' a
    forall a b. (a -> b) -> a -> b
    $ Arg (Named name (Pattern' a)) -> Named name (Pattern' a)
    forall e. Arg e -> e
    unArg Arg (Named name (Pattern' a))
    p) =
                OccurrencesBuilder -> Maybe OccurrencesBuilder
    forall a. a -> Maybe a
    Just (OccurrencesBuilder -> Maybe OccurrencesBuilder)
    -> OccurrencesBuilder -> Maybe OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    Matched (OccurrencesBuilder -> OccurrencesBuilder)
    -> OccurrencesBuilder -> OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ Item -> OccurrencesBuilder
    OccursHere (Item -> OccurrencesBuilder) -> Item -> OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ Nat -> Item
    AnArg Nat
    i
            | Bool
    otherwise                  = Maybe OccurrencesBuilder
    forall a. Maybe a
    Nothing

          -- @patItems ps@ creates a map from the pattern variables of @ps@
          -- to the index of the argument they are bound in.
          patItems :: NAPs -> IntMap (Maybe Item)
    patItems NAPs
    ps = [IntMap (Maybe Item)] -> IntMap (Maybe Item)
    forall a. Monoid a => [a] -> a
    mconcat ([IntMap (Maybe Item)] -> IntMap (Maybe Item))
    -> [IntMap (Maybe Item)] -> IntMap (Maybe Item)
    forall a b. (a -> b) -> a -> b
    $ (Nat
     -> Arg (Named NamedName DeBruijnPattern) -> IntMap (Maybe Item))
    -> [Nat] -> NAPs -> [IntMap (Maybe Item)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Nat -> Arg (Named NamedName DeBruijnPattern) -> IntMap (Maybe Item)
    patItem [Nat
    0..] NAPs
    ps

          -- @patItem i p@ assigns index @i@ to each pattern variable in @p@
          patItem :: Int -> NamedArg DeBruijnPattern -> IntMap (Maybe Item)
          patItem :: Nat -> Arg (Named NamedName DeBruijnPattern) -> IntMap (Maybe Item)
    patItem Nat
    i Arg (Named NamedName DeBruijnPattern)
    p = (Nat -> IntMap (Maybe Item)) -> [Nat] -> IntMap (Maybe Item)
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    Fold.foldMap Nat -> IntMap (Maybe Item)
    makeEntry [Nat]
    ixs
            where
              ixs :: [Nat]
    ixs = (DBPatVar -> Nat) -> [DBPatVar] -> [Nat]
    forall a b. (a -> b) -> [a] -> [b]
    map DBPatVar -> Nat
    dbPatVarIndex ([DBPatVar] -> [Nat]) -> [DBPatVar] -> [Nat]
    forall a b. (a -> b) -> a -> b
    $ [Either DBPatVar Term] -> [DBPatVar]
    forall a b. [Either a b] -> [a]
    lefts ([Either DBPatVar Term] -> [DBPatVar])
    -> [Either DBPatVar Term] -> [DBPatVar]
    forall a b. (a -> b) -> a -> b
    $ (Arg (Either DBPatVar Term) -> Either DBPatVar Term)
    -> [Arg (Either DBPatVar Term)] -> [Either DBPatVar Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg (Either DBPatVar Term) -> Either DBPatVar Term
    forall e. Arg e -> e
    unArg ([Arg (Either DBPatVar Term)] -> [Either DBPatVar Term])
    -> [Arg (Either DBPatVar Term)] -> [Either DBPatVar Term]
    forall a b. (a -> b) -> a -> b
    $ Arg DeBruijnPattern
    -> [Arg (Either (PatternVarOut (Arg DeBruijnPattern)) Term)]
    forall a.
    PatternVars a =>
    a -> [Arg (Either (PatternVarOut a) Term)]
    patternVars (Arg DeBruijnPattern
     -> [Arg (Either (PatternVarOut (Arg DeBruijnPattern)) Term)])
    -> Arg DeBruijnPattern
    -> [Arg (Either (PatternVarOut (Arg DeBruijnPattern)) Term)]
    forall a b. (a -> b) -> a -> b
    $ Named NamedName DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> Arg (Named NamedName DeBruijnPattern) -> Arg DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg (Named NamedName DeBruijnPattern)
    p

              makeEntry :: Nat -> IntMap (Maybe Item)
    makeEntry Nat
    x = (Nat, Maybe Item) -> IntMap (Maybe Item)
    forall el coll. Singleton el coll => el -> coll
    singleton (Nat
    x, Item -> Maybe Item
    forall a. a -> Maybe a
    Just (Item -> Maybe Item) -> Item -> Maybe Item
    forall a b. (a -> b) -> a -> b
    $ Nat -> Item
    AnArg Nat
    i)

    instance ComputeOccurrences Term where
      occurrences :: Term -> Reader OccEnv OccurrencesBuilder
    occurrences Term
    v = case Term -> Term
    unSpine Term
    v of
        Var Nat
    i Elims
    args -> ((OccEnv -> OccurrencesBuilder) -> Reader OccEnv OccurrencesBuilder
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ([Maybe Item] -> OccurrencesBuilder
    occI ([Maybe Item] -> OccurrencesBuilder)
    -> (OccEnv -> [Maybe Item]) -> OccEnv -> OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OccEnv -> [Maybe Item]
    vars)) Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall a. Semigroup a => a -> a -> a
    <> (Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    VarArg (OccurrencesBuilder -> OccurrencesBuilder)
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Elims
    args)
          where
          occI :: [Maybe Item] -> OccurrencesBuilder
    occI [Maybe Item]
    vars = OccurrencesBuilder
    -> (Item -> OccurrencesBuilder) -> Maybe Item -> OccurrencesBuilder
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe OccurrencesBuilder
    forall a. Monoid a => a
    mempty Item -> OccurrencesBuilder
    OccursHere (Maybe Item -> OccurrencesBuilder)
    -> Maybe Item -> OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ Maybe Item -> [Maybe Item] -> Nat -> Maybe Item
    forall a. a -> [a] -> Nat -> a
    indexWithDefault Maybe Item
    unbound [Maybe Item]
    vars Nat
    i
          unbound :: Maybe Item
    unbound = (ArgName -> Maybe Item -> Maybe Item)
    -> Maybe Item -> ArgName -> Maybe Item
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ArgName -> Maybe Item -> Maybe Item
    forall a. ArgName -> a -> a
    trace Maybe Item
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (ArgName -> Maybe Item) -> ArgName -> Maybe Item
    forall a b. (a -> b) -> a -> b
    $
                  ArgName
    "impossible: occurrence of de Bruijn index " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Nat -> ArgName
    forall a. Show a => a -> ArgName
    show Nat
    i ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++
                  ArgName
    " in vars " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ (OccEnv -> [Maybe Item]) -> ArgName
    forall a. Show a => a -> ArgName
    show OccEnv -> [Maybe Item]
    vars ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " is unbound"

        Def QName
    d Elims
    args   -> do
          Maybe QName
    inf <- (OccEnv -> Maybe QName) -> ReaderT OccEnv Identity (Maybe QName)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks OccEnv -> Maybe QName
    inf
          let occsAs :: Nat -> OccurrencesBuilder -> OccurrencesBuilder
    occsAs = if QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    d Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Maybe QName
    inf then Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs (Where -> OccurrencesBuilder -> OccurrencesBuilder)
    -> (Nat -> Where)
    -> Nat
    -> OccurrencesBuilder
    -> OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Nat -> Where
    DefArg QName
    d else \ Nat
    n ->
                -- the principal argument of builtin INF (∞) is the second (n==1)
                -- the first is a level argument (n==0, counting from 0!)
                if Nat
    n Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    1 then Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    UnderInf else Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs (QName -> Nat -> Where
    DefArg QName
    d Nat
    n)
          [OccurrencesBuilder]
    occs <- (Elim -> Reader OccEnv OccurrencesBuilder)
    -> Elims -> ReaderT OccEnv Identity [OccurrencesBuilder]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Elim -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Elims
    args
          OccurrencesBuilder -> Reader OccEnv OccurrencesBuilder
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OccurrencesBuilder -> Reader OccEnv OccurrencesBuilder)
    -> ([OccurrencesBuilder] -> OccurrencesBuilder)
    -> [OccurrencesBuilder]
    -> Reader OccEnv OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [OccurrencesBuilder] -> OccurrencesBuilder
    Concat ([OccurrencesBuilder] -> Reader OccEnv OccurrencesBuilder)
    -> [OccurrencesBuilder] -> Reader OccEnv OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ Item -> OccurrencesBuilder
    OccursHere (QName -> Item
    ADef QName
    d) OccurrencesBuilder -> [OccurrencesBuilder] -> [OccurrencesBuilder]
    forall a. a -> [a] -> [a]
    : (Nat -> OccurrencesBuilder -> OccurrencesBuilder)
    -> [Nat] -> [OccurrencesBuilder] -> [OccurrencesBuilder]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Nat -> OccurrencesBuilder -> OccurrencesBuilder
    occsAs [Nat
    0..] [OccurrencesBuilder]
    occs

        Con ConHead
    _ ConInfo
    _ Elims
    args -> Elims -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Elims
    args
        MetaV MetaId
    _ Elims
    args -> Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    MetaArg (OccurrencesBuilder -> OccurrencesBuilder)
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Elims
    args
        Pi Dom Type
    a Abs Type
    b       -> (Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    LeftOfArrow (OccurrencesBuilder -> OccurrencesBuilder)
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Dom Type
    a) Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall a. Semigroup a => a -> a -> a
    <> Abs Type -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Abs Type
    b
        Lam ArgInfo
    _ Abs Term
    b      -> Abs Term -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Abs Term
    b
        Level Level
    l      -> Level -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Level
    l
        Lit{}        -> Reader OccEnv OccurrencesBuilder
    forall a. Monoid a => a
    mempty
        Sort{}       -> Reader OccEnv OccurrencesBuilder
    forall a. Monoid a => a
    mempty
        -- Jesper, 2020-01-12: this information is also used for the
        -- occurs check, so we need to look under DontCare (see #4371)
        DontCare Term
    v   -> Term -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Term
    v
        Dummy{}      -> Reader OccEnv OccurrencesBuilder
    forall a. Monoid a => a
    mempty

    instance ComputeOccurrences Level where
      occurrences :: Level -> Reader OccEnv OccurrencesBuilder
    occurrences (Max Integer
    _ [PlusLevel' Term]
    as) = [PlusLevel' Term] -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences [PlusLevel' Term]
    as

    instance ComputeOccurrences PlusLevel where
      occurrences :: PlusLevel' Term -> Reader OccEnv OccurrencesBuilder
    occurrences (Plus Integer
    _ Term
    l) = Term -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Term
    l

    instance ComputeOccurrences Type where
      occurrences :: Type -> Reader OccEnv OccurrencesBuilder
    occurrences (El Sort' Term
    _ Term
    v) = Term -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Term
    v

    instance ComputeOccurrences a => ComputeOccurrences (Tele a) where
      occurrences :: Tele a -> Reader OccEnv OccurrencesBuilder
    occurrences Tele a
    EmptyTel        = Reader OccEnv OccurrencesBuilder
    forall a. Monoid a => a
    mempty
      occurrences (ExtendTel a
    a Abs (Tele a)
    b) = (a, Abs (Tele a)) -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences (a
    a, Abs (Tele a)
    b)

    instance ComputeOccurrences a => ComputeOccurrences (Abs a) where
      occurrences :: Abs a -> Reader OccEnv OccurrencesBuilder
    occurrences (Abs   ArgName
    _ a
    b) = Maybe Item
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall a. Maybe Item -> OccM a -> OccM a
    withExtendedOccEnv Maybe Item
    forall a. Maybe a
    Nothing (Reader OccEnv OccurrencesBuilder
     -> Reader OccEnv OccurrencesBuilder)
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ a -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences a
    b
      occurrences (NoAbs ArgName
    _ a
    b) = a -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences a
    b

    instance ComputeOccurrences a => ComputeOccurrences (Elim' a) where
      occurrences :: Elim' a -> Reader OccEnv OccurrencesBuilder
    occurrences Proj{}         = Reader OccEnv OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- unSpine
      occurrences (Apply Arg a
    a)      = Arg a -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences Arg a
    a
      occurrences (IApply a
    x a
    y a
    a) = (a, (a, a)) -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences (a
    x,(a
    y,a
    a)) -- TODO Andrea: conservative

    instance ComputeOccurrences a => ComputeOccurrences (Arg a)   where
    instance ComputeOccurrences a => ComputeOccurrences (Dom a)   where
    instance ComputeOccurrences a => ComputeOccurrences [a]       where
    instance ComputeOccurrences a => ComputeOccurrences (Maybe a) where

    instance (ComputeOccurrences a, ComputeOccurrences b) => ComputeOccurrences (a, b) where
      occurrences :: (a, b) -> Reader OccEnv OccurrencesBuilder
    occurrences (a
    x, b
    y) = a -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences a
    x Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    -> Reader OccEnv OccurrencesBuilder
    forall a. Semigroup a => a -> a -> a
    <> b -> Reader OccEnv OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> Reader OccEnv OccurrencesBuilder
    occurrences b
    y

    -- | Computes the number of occurrences of different 'Item's in the
    -- given definition.
    --
    -- WARNING: There can be lots of sharing between the 'OccursWhere'
    -- entries. Traversing all of these entries could be expensive. (See
    -- 'computeEdges' for an example.)
    computeOccurrences :: QName -> TCM (Map Item Integer)
    computeOccurrences :: QName -> TCM (Map Item Integer)
    computeOccurrences QName
    q = OccurrencesBuilder -> Map Item Integer
    flatten (OccurrencesBuilder -> Map Item Integer)
    -> TCMT IO OccurrencesBuilder -> TCM (Map Item Integer)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO OccurrencesBuilder
    computeOccurrences' QName
    q

    -- | Computes the occurrences in the given definition.
    computeOccurrences' :: QName -> TCM OccurrencesBuilder
    computeOccurrences' :: QName -> TCMT IO OccurrencesBuilder
    computeOccurrences' QName
    q = QName
    -> (Definition -> TCMT IO OccurrencesBuilder)
    -> TCMT IO OccurrencesBuilder
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    q ((Definition -> TCMT IO OccurrencesBuilder)
     -> TCMT IO OccurrencesBuilder)
    -> (Definition -> TCMT IO OccurrencesBuilder)
    -> TCMT IO OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    def -> do
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos" Nat
    25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let a :: IsAbstract
    a = Definition -> IsAbstract
    defAbstract Definition
    def
        AbstractMode
    m <- (TCEnv -> AbstractMode) -> TCMT IO AbstractMode
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> AbstractMode
    envAbstractMode
        ModuleName
    cur <- (TCEnv -> ModuleName) -> TCMT IO ModuleName
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> ModuleName
    envCurrentModule
        TCMT IO Doc
    "computeOccurrences" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (IsAbstract -> ArgName
    forall a. Show a => a -> ArgName
    show IsAbstract
    a) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (AbstractMode -> ArgName
    forall a. Show a => a -> ArgName
    show AbstractMode
    m)
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    cur
      Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs (QName -> Where
    InDefOf QName
    q) (OccurrencesBuilder -> OccurrencesBuilder)
    -> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> case Definition -> Defn
    theDef Definition
    def of

        Function{funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs} -> do
          [Clause]
    cs <- (Clause -> TCMT IO Clause) -> [Clause] -> TCMT IO [Clause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Clause -> TCMT IO Clause
    forall (tcm :: * -> *). MonadTCM tcm => Clause -> tcm Clause
    etaExpandClause ([Clause] -> TCMT IO [Clause])
    -> TCMT IO [Clause] -> TCMT IO [Clause]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Clause] -> TCMT IO [Clause]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull [Clause]
    cs
          [OccurrencesBuilder] -> OccurrencesBuilder
    Concat ([OccurrencesBuilder] -> OccurrencesBuilder)
    -> ([OccurrencesBuilder] -> [OccurrencesBuilder])
    -> [OccurrencesBuilder]
    -> OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Nat -> OccurrencesBuilder -> OccurrencesBuilder)
    -> [Nat] -> [OccurrencesBuilder] -> [OccurrencesBuilder]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs (Where -> OccurrencesBuilder -> OccurrencesBuilder)
    -> (Nat -> Where)
    -> Nat
    -> OccurrencesBuilder
    -> OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Where
    InClause) [Nat
    0..] ([OccurrencesBuilder] -> OccurrencesBuilder)
    -> TCMT IO [OccurrencesBuilder] -> TCMT IO OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
            (Clause -> TCMT IO OccurrencesBuilder)
    -> [Clause] -> TCMT IO [OccurrencesBuilder]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ([Maybe Item] -> Clause -> TCMT IO OccurrencesBuilder
    forall a.
    (Show a, PrettyTCM a, ComputeOccurrences a) =>
    [Maybe Item] -> a -> TCMT IO OccurrencesBuilder
    getOccurrences []) [Clause]
    cs

        Datatype{dataClause :: Defn -> Maybe Clause
    dataClause = Just Clause
    c} -> [Maybe Item] -> Clause -> TCMT IO OccurrencesBuilder
    forall a.
    (Show a, PrettyTCM a, ComputeOccurrences a) =>
    [Maybe Item] -> a -> TCMT IO OccurrencesBuilder
    getOccurrences [] (Clause -> TCMT IO OccurrencesBuilder)
    -> TCMT IO Clause -> TCMT IO OccurrencesBuilder
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Clause -> TCMT IO Clause
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Clause
    c
        Datatype{dataPars :: Defn -> Nat
    dataPars = Nat
    np0, dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs}       -> do
          -- Andreas, 2013-02-27 (later edited by someone else): First,
          -- include each index of an inductive family.
          TelV Tele (Dom Type)
    tel Type
    _ <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def
          -- Andreas, 2017-04-26, issue #2554: count first index as parameter if it has type Size.
          -- We compute sizeIndex=1 if first first index has type Size, otherwise sizeIndex==0
          Nat
    sizeIndex <- [Dom (ArgName, Type)]
    -> TCM Nat
    -> (Dom (ArgName, Type) -> [Dom (ArgName, Type)] -> TCM Nat)
    -> TCM Nat
    forall a b. [a] -> b -> (a -> [a] -> b) -> b
    caseList (Nat -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a. Nat -> [a] -> [a]
    drop Nat
    np0 ([Dom (ArgName, Type)] -> [Dom (ArgName, Type)])
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel) (Nat -> TCM Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    0) ((Dom (ArgName, Type) -> [Dom (ArgName, Type)] -> TCM Nat)
     -> TCM Nat)
    -> (Dom (ArgName, Type) -> [Dom (ArgName, Type)] -> TCM Nat)
    -> TCM Nat
    forall a b. (a -> b) -> a -> b
    $ \ Dom (ArgName, Type)
    dom [Dom (ArgName, Type)]
    _ -> do
            TCMT IO (Maybe BoundedSize)
    -> TCM Nat -> (BoundedSize -> TCM Nat) -> TCM Nat
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Dom (ArgName, Type) -> TCMT IO (Maybe BoundedSize)
    forall a (m :: * -> *).
    (IsSizeType a, HasOptions m, HasBuiltins m) =>
    a -> m (Maybe BoundedSize)
    isSizeType Dom (ArgName, Type)
    dom) (Nat -> TCM Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    0) ((BoundedSize -> TCM Nat) -> TCM Nat)
    -> (BoundedSize -> TCM Nat) -> TCM Nat
    forall a b. (a -> b) -> a -> b
    $ \ BoundedSize
    _ -> Nat -> TCM Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    1
          let np :: Nat
    np = Nat
    np0 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    sizeIndex
          let xs :: [Nat]
    xs = [Nat
    np .. Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1] -- argument positions corresponding to indices
          let ioccs :: OccurrencesBuilder
    ioccs = [OccurrencesBuilder] -> OccurrencesBuilder
    Concat ([OccurrencesBuilder] -> OccurrencesBuilder)
    -> [OccurrencesBuilder] -> OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ (Nat -> OccurrencesBuilder) -> [Nat] -> [OccurrencesBuilder]
    forall a b. (a -> b) -> [a] -> [b]
    map (Item -> OccurrencesBuilder
    OccursHere (Item -> OccurrencesBuilder)
    -> (Nat -> Item) -> Nat -> OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Item
    AnArg) [Nat
    np0 .. Nat
    np Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]
                            [OccurrencesBuilder]
    -> [OccurrencesBuilder] -> [OccurrencesBuilder]
    forall a. [a] -> [a] -> [a]
    ++ (Nat -> OccurrencesBuilder) -> [Nat] -> [OccurrencesBuilder]
    forall a b. (a -> b) -> [a] -> [b]
    map (Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    IsIndex (OccurrencesBuilder -> OccurrencesBuilder)
    -> (Nat -> OccurrencesBuilder) -> Nat -> OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Item -> OccurrencesBuilder
    OccursHere (Item -> OccurrencesBuilder)
    -> (Nat -> Item) -> Nat -> OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Item
    AnArg) [Nat]
    xs
          -- Then, we compute the occurrences in the constructor types.
          let conOcc :: QName -> TCMT IO OccurrencesBuilder
    conOcc QName
    c = do
                -- Andreas, 2020-02-15, issue #4447:
                -- Allow UnconfimedReductions here to make sure we get the constructor type
                -- in same way as it was obtained when the data types was checked.
                TelV Tele (Dom Type)
    tel Type
    t <- AllowedReductions -> TCMT IO (TelV Type) -> TCMT IO (TelV Type)
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    AllowedReductions -> m a -> m a
    putAllowedReductions AllowedReductions
    allReductions (TCMT IO (TelV Type) -> TCMT IO (TelV Type))
    -> TCMT IO (TelV Type) -> TCMT IO (TelV Type)
    forall a b. (a -> b) -> a -> b
    $
                  Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath (Type -> TCMT IO (TelV Type))
    -> (Definition -> Type) -> Definition -> TCMT IO (TelV Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Type
    defType (Definition -> TCMT IO (TelV Type))
    -> TCMT IO Definition -> TCMT IO (TelV Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    c
                let (Tele (Dom Type)
    tel0,Tele (Dom Type)
    tel1) = Nat -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
    splitTelescopeAt Nat
    np Tele (Dom Type)
    tel
                -- Do not collect occurrences in the data parameters.
                -- Normalization needed e.g. for test/succeed/Bush.agda.
                -- (Actually, for Bush.agda, reducing the parameters should be sufficient.)
                Tele (Dom Type)
    tel1' <- Tele (Dom Type)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel0 (TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type)))
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise (Tele (Dom Type) -> TCMT IO (Tele (Dom Type)))
    -> Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type)
    tel1
                let vars :: Nat -> [Maybe Item]
    vars = (Nat -> Maybe Item) -> [Nat] -> [Maybe Item]
    forall a b. (a -> b) -> [a] -> [b]
    map (Item -> Maybe Item
    forall a. a -> Maybe a
    Just (Item -> Maybe Item) -> (Nat -> Item) -> Nat -> Maybe Item
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Item
    AnArg) ([Nat] -> [Maybe Item]) -> (Nat -> [Nat]) -> Nat -> [Maybe Item]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom
                -- Occurrences in the types of the constructor arguments.
                TCMT IO OccurrencesBuilder
    -> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
    forall a. Monoid a => a -> a -> a
    mappend (Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs (QName -> Where
    ConArgType QName
    c) (OccurrencesBuilder -> OccurrencesBuilder)
    -> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Maybe Item] -> Tele (Dom Type) -> TCMT IO OccurrencesBuilder
    forall a.
    (Show a, PrettyTCM a, ComputeOccurrences a) =>
    [Maybe Item] -> a -> TCMT IO OccurrencesBuilder
    getOccurrences (Nat -> [Maybe Item]
    vars Nat
    np) Tele (Dom Type)
    tel1') (TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder)
    -> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ do
                  -- Occurrences in the indices of the data type the constructor targets.
                  -- Andreas, 2020-02-15, issue #4447:
                  -- WAS: @t@ is not necessarily a data type, but it could be something
                  -- that reduces to a data type once UnconfirmedReductions are confirmed
                  -- as safe by the termination checker.
                  -- In any case, if @t@ is not showing itself as the data type, we need to
                  -- do something conservative.  We will just collect *all* occurrences
                  -- and flip their sign (variance) using 'LeftOfArrow'.
                  let fallback :: TCMT IO OccurrencesBuilder
    fallback = Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    LeftOfArrow (OccurrencesBuilder -> OccurrencesBuilder)
    -> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Maybe Item] -> Type -> TCMT IO OccurrencesBuilder
    forall a.
    (Show a, PrettyTCM a, ComputeOccurrences a) =>
    [Maybe Item] -> a -> TCMT IO OccurrencesBuilder
    getOccurrences (Nat -> [Maybe Item]
    vars (Nat -> [Maybe Item]) -> Nat -> [Maybe Item]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel) Type
    t -- NB::Defined but not used
                  case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
                    Def QName
    q' Elims
    vs
                      | QName
    q QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    q' -> do
                          let indices :: [Arg Term]
    indices = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims (Elims -> Maybe [Arg Term]) -> Elims -> Maybe [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Nat -> Elims -> Elims
    forall a. Nat -> [a] -> [a]
    drop Nat
    np Elims
    vs
                          Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs (QName -> Where
    IndArgType QName
    c) (OccurrencesBuilder -> OccurrencesBuilder)
    -> (OccurrencesBuilder -> OccurrencesBuilder)
    -> OccurrencesBuilder
    -> OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> OccurrencesBuilder -> OccurrencesBuilder
    OnlyVarsUpTo Nat
    np (OccurrencesBuilder -> OccurrencesBuilder)
    -> TCMT IO OccurrencesBuilder -> TCMT IO OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Maybe Item] -> [Arg Term] -> TCMT IO OccurrencesBuilder
    forall a.
    (Show a, PrettyTCM a, ComputeOccurrences a) =>
    [Maybe Item] -> a -> TCMT IO OccurrencesBuilder
    getOccurrences (Nat -> [Maybe Item]
    vars (Nat -> [Maybe Item]) -> Nat -> [Maybe Item]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel) [Arg Term]
    indices
                      | Bool
    otherwise -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- fallback -- this ought to be impossible now (but wasn't, see #4447)
                    Pi{}       -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- eliminated  by telView
                    MetaV{}    -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- not a constructor target; should have been solved by now
                    Var{}      -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- not a constructor target
                    Sort{}     -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- not a constructor target
                    Lam{}      -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- not a type
                    Lit{}      -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- not a type
                    Con{}      -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- not a type
                    Level{}    -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- not a type
                    DontCare{} -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- not a type
                    Dummy{}    -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          [TCMT IO OccurrencesBuilder] -> TCMT IO OccurrencesBuilder
    forall a. Monoid a => [a] -> a
    mconcat ([TCMT IO OccurrencesBuilder] -> TCMT IO OccurrencesBuilder)
    -> [TCMT IO OccurrencesBuilder] -> TCMT IO OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ OccurrencesBuilder -> TCMT IO OccurrencesBuilder
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure OccurrencesBuilder
    ioccs TCMT IO OccurrencesBuilder
    -> [TCMT IO OccurrencesBuilder] -> [TCMT IO OccurrencesBuilder]
    forall a. a -> [a] -> [a]
    : (QName -> TCMT IO OccurrencesBuilder)
    -> [QName] -> [TCMT IO OccurrencesBuilder]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCMT IO OccurrencesBuilder
    conOcc [QName]
    cs

        Record{recClause :: Defn -> Maybe Clause
    recClause = Just Clause
    c} -> [Maybe Item] -> Clause -> TCMT IO OccurrencesBuilder
    forall a.
    (Show a, PrettyTCM a, ComputeOccurrences a) =>
    [Maybe Item] -> a -> TCMT IO OccurrencesBuilder
    getOccurrences [] (Clause -> TCMT IO OccurrencesBuilder)
    -> TCMT IO Clause -> TCMT IO OccurrencesBuilder
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Clause -> TCMT IO Clause
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Clause
    c
        Record{recPars :: Defn -> Nat
    recPars = Nat
    np, recTel :: Defn -> Tele (Dom Type)
    recTel = Tele (Dom Type)
    tel} -> do
          let (Tele (Dom Type)
    tel0,Tele (Dom Type)
    tel1) = Nat -> Tele (Dom Type) -> (Tele (Dom Type), Tele (Dom Type))
    splitTelescopeAt Nat
    np Tele (Dom Type)
    tel
              vars :: [Maybe Item]
    vars = (Nat -> Maybe Item) -> [Nat] -> [Maybe Item]
    forall a b. (a -> b) -> [a] -> [b]
    map (Item -> Maybe Item
    forall a. a -> Maybe a
    Just (Item -> Maybe Item) -> (Nat -> Item) -> Nat -> Maybe Item
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Item
    AnArg) ([Nat] -> [Maybe Item]) -> [Nat] -> [Maybe Item]
    forall a b. (a -> b) -> a -> b
    $ Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom Nat
    np
          [Maybe Item] -> Tele (Dom Type) -> TCMT IO OccurrencesBuilder
    forall a.
    (Show a, PrettyTCM a, ComputeOccurrences a) =>
    [Maybe Item] -> a -> TCMT IO OccurrencesBuilder
    getOccurrences [Maybe Item]
    vars (Tele (Dom Type) -> TCMT IO OccurrencesBuilder)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO OccurrencesBuilder
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Tele (Dom Type)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel0 (Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise Tele (Dom Type)
    tel1) -- Andreas, 2017-01-01, issue #1899, treat like data types

        -- Arguments to other kinds of definitions are hard-wired.
        Constructor{}      -> TCMT IO OccurrencesBuilder
    forall a. Monoid a => a
    mempty
        Axiom{}            -> TCMT IO OccurrencesBuilder
    forall a. Monoid a => a
    mempty
        DataOrRecSig{}     -> TCMT IO OccurrencesBuilder
    forall a. Monoid a => a
    mempty
        Primitive{}        -> TCMT IO OccurrencesBuilder
    forall a. Monoid a => a
    mempty
        PrimitiveSort{}    -> TCMT IO OccurrencesBuilder
    forall a. Monoid a => a
    mempty
        GeneralizableVar{} -> TCMT IO OccurrencesBuilder
    forall a. Monoid a => a
    mempty
        AbstractDefn{}     -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- Building the occurrence graph ------------------------------------------

    data Node = DefNode !QName
              | ArgNode !QName !Nat
      deriving (Node -> Node -> Bool
    (Node -> Node -> Bool) -> (Node -> Node -> Bool) -> Eq Node
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Node -> Node -> Bool
    $c/= :: Node -> Node -> Bool
    == :: Node -> Node -> Bool
    $c== :: Node -> Node -> Bool
    Eq, Eq Node
    Eq Node
    -> (Node -> Node -> Ordering)
    -> (Node -> Node -> Bool)
    -> (Node -> Node -> Bool)
    -> (Node -> Node -> Bool)
    -> (Node -> Node -> Bool)
    -> (Node -> Node -> Node)
    -> (Node -> Node -> Node)
    -> Ord Node
    Node -> Node -> Bool
    Node -> Node -> Ordering
    Node -> Node -> Node
    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 :: Node -> Node -> Node
    $cmin :: Node -> Node -> Node
    max :: Node -> Node -> Node
    $cmax :: Node -> Node -> Node
    >= :: Node -> Node -> Bool
    $c>= :: Node -> Node -> Bool
    > :: Node -> Node -> Bool
    $c> :: Node -> Node -> Bool
    <= :: Node -> Node -> Bool
    $c<= :: Node -> Node -> Bool
    < :: Node -> Node -> Bool
    $c< :: Node -> Node -> Bool
    compare :: Node -> Node -> Ordering
    $ccompare :: Node -> Node -> Ordering
    Ord)

    -- | Edge labels for the positivity graph.
    data Edge a = Edge !Occurrence a
      deriving (Edge a -> Edge a -> Bool
    (Edge a -> Edge a -> Bool)
    -> (Edge a -> Edge a -> Bool) -> Eq (Edge a)
    forall a. Eq a => Edge a -> Edge a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Edge a -> Edge a -> Bool
    $c/= :: forall a. Eq a => Edge a -> Edge a -> Bool
    == :: Edge a -> Edge a -> Bool
    $c== :: forall a. Eq a => Edge a -> Edge a -> Bool
    Eq, Eq (Edge a)
    Eq (Edge a)
    -> (Edge a -> Edge a -> Ordering)
    -> (Edge a -> Edge a -> Bool)
    -> (Edge a -> Edge a -> Bool)
    -> (Edge a -> Edge a -> Bool)
    -> (Edge a -> Edge a -> Bool)
    -> (Edge a -> Edge a -> Edge a)
    -> (Edge a -> Edge a -> Edge a)
    -> Ord (Edge a)
    Edge a -> Edge a -> Bool
    Edge a -> Edge a -> Ordering
    Edge a -> Edge a -> Edge a
    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
    forall {a}. Ord a => Eq (Edge a)
    forall a. Ord a => Edge a -> Edge a -> Bool
    forall a. Ord a => Edge a -> Edge a -> Ordering
    forall a. Ord a => Edge a -> Edge a -> Edge a
    min :: Edge a -> Edge a -> Edge a
    $cmin :: forall a. Ord a => Edge a -> Edge a -> Edge a
    max :: Edge a -> Edge a -> Edge a
    $cmax :: forall a. Ord a => Edge a -> Edge a -> Edge a
    >= :: Edge a -> Edge a -> Bool
    $c>= :: forall a. Ord a => Edge a -> Edge a -> Bool
    > :: Edge a -> Edge a -> Bool
    $c> :: forall a. Ord a => Edge a -> Edge a -> Bool
    <= :: Edge a -> Edge a -> Bool
    $c<= :: forall a. Ord a => Edge a -> Edge a -> Bool
    < :: Edge a -> Edge a -> Bool
    $c< :: forall a. Ord a => Edge a -> Edge a -> Bool
    compare :: Edge a -> Edge a -> Ordering
    $ccompare :: forall a. Ord a => Edge a -> Edge a -> Ordering
    Ord, Nat -> Edge a -> ArgName -> ArgName
    [Edge a] -> ArgName -> ArgName
    Edge a -> ArgName
    (Nat -> Edge a -> ArgName -> ArgName)
    -> (Edge a -> ArgName)
    -> ([Edge a] -> ArgName -> ArgName)
    -> Show (Edge a)
    forall a. Show a => Nat -> Edge a -> ArgName -> ArgName
    forall a. Show a => [Edge a] -> ArgName -> ArgName
    forall a. Show a => Edge a -> ArgName
    forall a.
    (Nat -> a -> ArgName -> ArgName)
    -> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
    showList :: [Edge a] -> ArgName -> ArgName
    $cshowList :: forall a. Show a => [Edge a] -> ArgName -> ArgName
    show :: Edge a -> ArgName
    $cshow :: forall a. Show a => Edge a -> ArgName
    showsPrec :: Nat -> Edge a -> ArgName -> ArgName
    $cshowsPrec :: forall a. Show a => Nat -> Edge a -> ArgName -> ArgName
    Show, (forall a b. (a -> b) -> Edge a -> Edge b)
    -> (forall a b. a -> Edge b -> Edge a) -> Functor Edge
    forall a b. a -> Edge b -> Edge a
    forall a b. (a -> b) -> Edge a -> Edge b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> Edge b -> Edge a
    $c<$ :: forall a b. a -> Edge b -> Edge a
    fmap :: forall a b. (a -> b) -> Edge a -> Edge b
    $cfmap :: forall a b. (a -> b) -> Edge a -> Edge b
    Functor)

    -- | Merges two edges between the same source and target.

    mergeEdges :: Edge a -> Edge a -> Edge a
    mergeEdges :: forall a. Edge a -> Edge a -> Edge a
    mergeEdges Edge a
    _                    e :: Edge a
    e@(Edge Occurrence
    Mixed a
    _)     = Edge a
    e -- dominant
    mergeEdges e :: Edge a
    e@(Edge Occurrence
    Mixed a
    _)     Edge a
    _                    = Edge a
    e
    mergeEdges (Edge Occurrence
    Unused a
    _)      Edge a
    e                    = Edge a
    e -- neutral
    mergeEdges Edge a
    e                    (Edge Occurrence
    Unused a
    _)      = Edge a
    e
    mergeEdges (Edge Occurrence
    JustNeg a
    _)     e :: Edge a
    e@(Edge Occurrence
    JustNeg a
    _)   = Edge a
    e
    mergeEdges Edge a
    _                    e :: Edge a
    e@(Edge Occurrence
    JustNeg a
    w)   = Occurrence -> a -> Edge a
    forall a. Occurrence -> a -> Edge a
    Edge Occurrence
    Mixed a
    w
    mergeEdges e :: Edge a
    e@(Edge Occurrence
    JustNeg a
    w)   Edge a
    _                    = Occurrence -> a -> Edge a
    forall a. Occurrence -> a -> Edge a
    Edge Occurrence
    Mixed a
    w
    mergeEdges Edge a
    _                    e :: Edge a
    e@(Edge Occurrence
    JustPos a
    _)   = Edge a
    e -- dominates strict pos.
    mergeEdges e :: Edge a
    e@(Edge Occurrence
    JustPos a
    _)   Edge a
    _                    = Edge a
    e
    mergeEdges Edge a
    _                    e :: Edge a
    e@(Edge Occurrence
    StrictPos a
    _) = Edge a
    e -- dominates 'GuardPos'
    mergeEdges e :: Edge a
    e@(Edge Occurrence
    StrictPos a
    _) Edge a
    _                    = Edge a
    e
    mergeEdges (Edge Occurrence
    GuardPos a
    _)    e :: Edge a
    e@(Edge Occurrence
    GuardPos a
    _)  = Edge a
    e

    -- | These operations form a semiring if we quotient by the relation
    -- \"the 'Occurrence' components are equal\".

    instance SemiRing (Edge (Seq OccursWhere)) where
      ozero :: Edge (Seq OccursWhere)
    ozero = Occurrence -> Seq OccursWhere -> Edge (Seq OccursWhere)
    forall a. Occurrence -> a -> Edge a
    Edge Occurrence
    forall a. SemiRing a => a
    ozero Seq OccursWhere
    forall a. Seq a
    DS.empty
      oone :: Edge (Seq OccursWhere)
    oone  = Occurrence -> Seq OccursWhere -> Edge (Seq OccursWhere)
    forall a. Occurrence -> a -> Edge a
    Edge Occurrence
    forall a. SemiRing a => a
    oone  Seq OccursWhere
    forall a. Seq a
    DS.empty

      oplus :: Edge (Seq OccursWhere)
    -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)
    oplus = Edge (Seq OccursWhere)
    -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)
    forall a. Edge a -> Edge a -> Edge a
    mergeEdges

      otimes :: Edge (Seq OccursWhere)
    -> Edge (Seq OccursWhere) -> Edge (Seq OccursWhere)
    otimes (Edge Occurrence
    o1 Seq OccursWhere
    w1) (Edge Occurrence
    o2 Seq OccursWhere
    w2) = Occurrence -> Seq OccursWhere -> Edge (Seq OccursWhere)
    forall a. Occurrence -> a -> Edge a
    Edge (Occurrence -> Occurrence -> Occurrence
    forall a. SemiRing a => a -> a -> a
    otimes Occurrence
    o1 Occurrence
    o2) (Seq OccursWhere
    w1 Seq OccursWhere -> Seq OccursWhere -> Seq OccursWhere
    forall a. Seq a -> Seq a -> Seq a
    DS.>< Seq OccursWhere
    w2)

    -- | WARNING: There can be lots of sharing between the 'OccursWhere'
    -- entries in the edges. Traversing all of these entries could be
    -- expensive. (See 'computeEdges' for an example.)
    buildOccurrenceGraph :: Set QName -> TCM (Graph Node (Edge OccursWhere))
    buildOccurrenceGraph :: Set QName -> TCM (Graph Node (Edge OccursWhere))
    buildOccurrenceGraph Set QName
    qs =
      (Edge OccursWhere -> Edge OccursWhere -> Edge OccursWhere)
    -> [Edge Node (Edge OccursWhere)] -> Graph Node (Edge OccursWhere)
    forall n e. Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e
    Graph.fromEdgesWith Edge OccursWhere -> Edge OccursWhere -> Edge OccursWhere
    forall a. Edge a -> Edge a -> Edge a
    mergeEdges ([Edge Node (Edge OccursWhere)] -> Graph Node (Edge OccursWhere))
    -> ([[Edge Node (Edge OccursWhere)]]
        -> [Edge Node (Edge OccursWhere)])
    -> [[Edge Node (Edge OccursWhere)]]
    -> Graph Node (Edge OccursWhere)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[Edge Node (Edge OccursWhere)]] -> [Edge Node (Edge OccursWhere)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Edge Node (Edge OccursWhere)]] -> Graph Node (Edge OccursWhere))
    -> TCMT IO [[Edge Node (Edge OccursWhere)]]
    -> TCM (Graph Node (Edge OccursWhere))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
        (QName -> TCMT IO [Edge Node (Edge OccursWhere)])
    -> [QName] -> TCMT IO [[Edge Node (Edge OccursWhere)]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM QName -> TCMT IO [Edge Node (Edge OccursWhere)]
    defGraph (Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    qs)
      where
        defGraph :: QName -> TCM [Graph.Edge Node (Edge OccursWhere)]
        defGraph :: QName -> TCMT IO [Edge Node (Edge OccursWhere)]
    defGraph QName
    q = QName
    -> (Definition -> TCMT IO [Edge Node (Edge OccursWhere)])
    -> TCMT IO [Edge Node (Edge OccursWhere)]
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    q ((Definition -> TCMT IO [Edge Node (Edge OccursWhere)])
     -> TCMT IO [Edge Node (Edge OccursWhere)])
    -> (Definition -> TCMT IO [Edge Node (Edge OccursWhere)])
    -> TCMT IO [Edge Node (Edge OccursWhere)]
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    _def -> do
          OccurrencesBuilder
    occs <- QName -> TCMT IO OccurrencesBuilder
    computeOccurrences' QName
    q

          ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.occs" Nat
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            ((TCMT IO Doc
    "Occurrences in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    ":")
              TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $+$
            Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
               ((Item, Integer) -> TCMT IO Doc)
    -> [(Item, Integer)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Item
    i, Integer
    n) ->
                       (Item -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Item
    i TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    ":") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Integer -> ArgName
    forall a. Show a => a -> ArgName
    show Integer
    n) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                       TCMT IO Doc
    "occurrences") ([(Item, Integer)] -> [TCMT IO Doc])
    -> [(Item, Integer)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $
               ((Item, Integer) -> (Item, Integer) -> Ordering)
    -> [(Item, Integer)] -> [(Item, Integer)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Integer -> Integer -> Ordering)
    -> ((Item, Integer) -> Integer)
    -> (Item, Integer)
    -> (Item, Integer)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Item, Integer) -> Integer
    forall a b. (a, b) -> b
    snd) ([(Item, Integer)] -> [(Item, Integer)])
    -> [(Item, Integer)] -> [(Item, Integer)]
    forall a b. (a -> b) -> a -> b
    $
               Map Item Integer -> [(Item, Integer)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (OccurrencesBuilder -> Map Item Integer
    flatten OccurrencesBuilder
    occs))

          -- Placing this line before the reportSDoc lines above creates a
          -- space leak: occs is retained for too long.
          [Edge Node (Edge OccursWhere)]
    es <- Set QName
    -> QName
    -> OccurrencesBuilder
    -> TCMT IO [Edge Node (Edge OccursWhere)]
    computeEdges Set QName
    qs QName
    q OccurrencesBuilder
    occs

          ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.occs.edges" Nat
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "Edges:"
              TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $+$
            Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
               (Edge Node (Edge OccursWhere) -> TCMT IO Doc)
    -> [Edge Node (Edge OccursWhere)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Edge Node (Edge OccursWhere)
    e ->
                       let Edge Occurrence
    o OccursWhere
    w = Edge Node (Edge OccursWhere) -> Edge OccursWhere
    forall n e. Edge n e -> e
    Graph.label Edge Node (Edge OccursWhere)
    e in
                       Node -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Edge Node (Edge OccursWhere) -> Node
    forall n e. Edge n e -> n
    Graph.source Edge Node (Edge OccursWhere)
    e) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                       TCMT IO Doc
    "-[" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Occurrence -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty Occurrence
    o) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    ",") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                                     Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OccursWhere -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty OccursWhere
    w) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "]->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                       Node -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Edge Node (Edge OccursWhere) -> Node
    forall n e. Edge n e -> n
    Graph.target Edge Node (Edge OccursWhere)
    e))
                   [Edge Node (Edge OccursWhere)]
    es)

          [Edge Node (Edge OccursWhere)]
    -> TCMT IO [Edge Node (Edge OccursWhere)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Edge Node (Edge OccursWhere)]
    es

    -- | Computes all non-'ozero' occurrence graph edges represented by
    -- the given 'OccurrencesBuilder'.
    --
    -- WARNING: There can be lots of sharing between the 'OccursWhere'
    -- entries in the edges. Traversing all of these entries could be
    -- expensive. For instance, for the function @F@ in
    -- @benchmark/misc/SlowOccurrences.agda@ a large number of edges from
    -- the argument @X@ to the function @F@ are computed. These edges have
    -- polarity 'StrictPos', 'JustNeg' or 'JustPos', and contain the
    -- following 'OccursWhere' elements:
    --
    -- * @'OccursWhere' _ 'DS.empty' ('DS.fromList' ['InDefOf' "F", 'InClause' 0])@,
    --
    -- * @'OccursWhere' _ 'DS.empty' ('DS.fromList' ['InDefOf' "F", 'InClause' 0, 'LeftOfArrow'])@,
    --
    -- * @'OccursWhere' _ 'DS.empty' ('DS.fromList' ['InDefOf' "F", 'InClause' 0, 'LeftOfArrow', 'LeftOfArrow'])@,
    --
    -- * @'OccursWhere' _ 'DS.empty' ('DS.fromList' ['InDefOf' "F", 'InClause' 0, 'LeftOfArrow', 'LeftOfArrow', 'LeftOfArrow'])@,
    --
    -- * and so on.
    computeEdges
      :: Set QName
         -- ^ The names in the current mutual block.
      -> QName
         -- ^ The current name.
      -> OccurrencesBuilder
      -> TCM [Graph.Edge Node (Edge OccursWhere)]
    computeEdges :: Set QName
    -> QName
    -> OccurrencesBuilder
    -> TCMT IO [Edge Node (Edge OccursWhere)]
    computeEdges Set QName
    muts QName
    q OccurrencesBuilder
    ob =
      (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> [Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]
    forall a b. (a -> b) -> a -> b
    $ []) (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
     -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> TCMT IO [Edge Node (Edge OccursWhere)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Occurrence
    -> OccurrencesBuilder'
    -> Node
    -> Seq Where
    -> Seq Where
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    mkEdge Occurrence
    StrictPos (OccurrencesBuilder -> OccurrencesBuilder'
    preprocess OccurrencesBuilder
    ob)
                        Node
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Seq Where
    forall a. Seq a
    DS.empty Seq Where
    forall a. Seq a
    DS.empty
      where
      mkEdge
         :: Occurrence
         -> OccurrencesBuilder'
         -> Node          -- The current target node.
         -> DS.Seq Where  -- 'Where' information encountered before the current target
                          -- node was (re)selected.
         -> DS.Seq Where  -- 'Where' information encountered after the current target
                          -- node was (re)selected.
         -> TCM ([Graph.Edge Node (Edge OccursWhere)] ->
                 [Graph.Edge Node (Edge OccursWhere)])
      mkEdge :: Occurrence
    -> OccurrencesBuilder'
    -> Node
    -> Seq Where
    -> Seq Where
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    mkEdge !Occurrence
    pol OccurrencesBuilder'
    ob Node
    to Seq Where
    cs Seq Where
    os = case OccurrencesBuilder'
    ob of
        Concat' [OccurrencesBuilder']
    obs ->
          (TCMT
       IO
       ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
     -> TCMT
          IO
          ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
     -> TCMT
          IO
          ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]))
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> [TCMT
          IO
          ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])]
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
     -> ([Edge Node (Edge OccursWhere)]
         -> [Edge Node (Edge OccursWhere)])
     -> [Edge Node (Edge OccursWhere)]
     -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> ([Edge Node (Edge OccursWhere)]
        -> [Edge Node (Edge OccursWhere)])
    -> [Edge Node (Edge OccursWhere)]
    -> [Edge Node (Edge OccursWhere)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.)) (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]
    forall a. a -> a
    id)
                [ Occurrence
    -> OccurrencesBuilder'
    -> Node
    -> Seq Where
    -> Seq Where
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    mkEdge Occurrence
    pol OccurrencesBuilder'
    ob Node
    to Seq Where
    cs Seq Where
    os | OccurrencesBuilder'
    ob <- [OccurrencesBuilder']
    obs ]

        OccursAs' Where
    w OccurrencesBuilder'
    ob -> do
          (Maybe Node
    to', Occurrence
    pol) <- Node -> Occurrence -> Where -> TCM (Maybe Node, Occurrence)
    mkEdge' Node
    to Occurrence
    pol Where
    w
          let mk :: Node
    -> Seq Where
    -> Seq Where
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    mk = Occurrence
    -> OccurrencesBuilder'
    -> Node
    -> Seq Where
    -> Seq Where
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    mkEdge Occurrence
    pol OccurrencesBuilder'
    ob
          case Maybe Node
    to' of
            Maybe Node
    Nothing -> Node
    -> Seq Where
    -> Seq Where
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    mk Node
    to Seq Where
    cs            (Seq Where
    os Seq Where -> Where -> Seq Where
    forall a. Seq a -> a -> Seq a
    DS.|> Where
    w)
            Just Node
    to -> Node
    -> Seq Where
    -> Seq Where
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    mk Node
    to (Seq Where
    cs Seq Where -> Seq Where -> Seq Where
    forall a. Seq a -> Seq a -> Seq a
    DS.>< Seq Where
    os) (Where -> Seq Where
    forall a. a -> Seq a
    DS.singleton Where
    w)

        OccursHere' Item
    i ->
          let o :: OccursWhere
    o = Range -> Seq Where -> Seq Where -> OccursWhere
    OccursWhere (Item -> Range
    forall a. HasRange a => a -> Range
    getRange Item
    i) Seq Where
    cs Seq Where
    os in
          case Item
    i of
            AnArg Nat
    i ->
              ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
     -> TCMT
          IO
          ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]))
    -> ([Edge Node (Edge OccursWhere)]
        -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    forall a b. (a -> b) -> a -> b
    $ Bool
    -> ([Edge Node (Edge OccursWhere)]
        -> [Edge Node (Edge OccursWhere)])
    -> [Edge Node (Edge OccursWhere)]
    -> [Edge Node (Edge OccursWhere)]
    forall a. Bool -> (a -> a) -> a -> a
    applyUnless (Occurrence -> Bool
    forall a. Null a => a -> Bool
    null Occurrence
    pol) (Edge :: forall n e. n -> n -> e -> Edge n e
    Graph.Edge
                { source :: Node
    Graph.source = QName -> Nat -> Node
    ArgNode QName
    q Nat
    i
                , target :: Node
    Graph.target = Node
    to
                , label :: Edge OccursWhere
    Graph.label  = Occurrence -> OccursWhere -> Edge OccursWhere
    forall a. Occurrence -> a -> Edge a
    Edge Occurrence
    pol OccursWhere
    o
                } Edge Node (Edge OccursWhere)
    -> [Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]
    forall a. a -> [a] -> [a]
    :)
            ADef QName
    q' ->
              -- Andreas, 2017-04-26, issue #2555
              -- Skip nodes pointing outside the mutual block.
              ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
     -> TCMT
          IO
          ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]))
    -> ([Edge Node (Edge OccursWhere)]
        -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    forall a b. (a -> b) -> a -> b
    $ Bool
    -> ([Edge Node (Edge OccursWhere)]
        -> [Edge Node (Edge OccursWhere)])
    -> [Edge Node (Edge OccursWhere)]
    -> [Edge Node (Edge OccursWhere)]
    forall a. Bool -> (a -> a) -> a -> a
    applyUnless (Occurrence -> Bool
    forall a. Null a => a -> Bool
    null Occurrence
    pol Bool -> Bool -> Bool
    || QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.notMember QName
    q' Set QName
    muts)
                (Edge :: forall n e. n -> n -> e -> Edge n e
    Graph.Edge
                   { source :: Node
    Graph.source = QName -> Node
    DefNode QName
    q'
                   , target :: Node
    Graph.target = Node
    to
                   , label :: Edge OccursWhere
    Graph.label  = Occurrence -> OccursWhere -> Edge OccursWhere
    forall a. Occurrence -> a -> Edge a
    Edge Occurrence
    pol OccursWhere
    o
                   } Edge Node (Edge OccursWhere)
    -> [Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)]
    forall a. a -> [a] -> [a]
    :)

      -- This function might return a new target node.
      mkEdge'
        :: Node  -- The current target node.
        -> Occurrence
        -> Where
        -> TCM (Maybe Node, Occurrence)
      mkEdge' :: Node -> Occurrence -> Where -> TCM (Maybe Node, Occurrence)
    mkEdge' Node
    to !Occurrence
    pol = \case
        Where
    VarArg         -> TCM (Maybe Node, Occurrence)
    forall {a}. TCMT IO (Maybe a, Occurrence)
    mixed
        Where
    MetaArg        -> TCM (Maybe Node, Occurrence)
    forall {a}. TCMT IO (Maybe a, Occurrence)
    mixed
        Where
    LeftOfArrow    -> TCM (Maybe Node, Occurrence)
    negative
        DefArg QName
    d Nat
    i     -> do
          Occurrence
    pol' <- QName -> TCMT IO Occurrence
    isGuarding QName
    d
          if QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    d Set QName
    muts
            then (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Node -> Maybe Node
    forall a. a -> Maybe a
    Just (QName -> Nat -> Node
    ArgNode QName
    d Nat
    i), Occurrence
    pol')
            else Occurrence -> TCM (Maybe Node, Occurrence)
    addPol (Occurrence -> TCM (Maybe Node, Occurrence))
    -> TCMT IO Occurrence -> TCM (Maybe Node, Occurrence)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Occurrence -> Occurrence -> Occurrence
    forall a. SemiRing a => a -> a -> a
    otimes Occurrence
    pol' (Occurrence -> Occurrence)
    -> TCMT IO Occurrence -> TCMT IO Occurrence
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> Nat -> TCMT IO Occurrence
    getArgOccurrence QName
    d Nat
    i
        Where
    UnderInf       -> Occurrence -> TCM (Maybe Node, Occurrence)
    addPol Occurrence
    GuardPos -- Andreas, 2012-06-09: ∞ is guarding
        ConArgType QName
    _   -> TCM (Maybe Node, Occurrence)
    keepGoing
        IndArgType QName
    _   -> TCM (Maybe Node, Occurrence)
    forall {a}. TCMT IO (Maybe a, Occurrence)
    mixed
        InClause Nat
    _     -> TCM (Maybe Node, Occurrence)
    keepGoing
        Where
    Matched        -> TCM (Maybe Node, Occurrence)
    forall {a}. TCMT IO (Maybe a, Occurrence)
    mixed -- consider arguments matched against as used
        Where
    IsIndex        -> TCM (Maybe Node, Occurrence)
    forall {a}. TCMT IO (Maybe a, Occurrence)
    mixed -- And similarly for indices.
        InDefOf QName
    d      -> do
          Occurrence
    pol' <- QName -> TCMT IO Occurrence
    isGuarding QName
    d
          (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Node -> Maybe Node
    forall a. a -> Maybe a
    Just (QName -> Node
    DefNode QName
    d), Occurrence
    pol')
        where
        keepGoing :: TCM (Maybe Node, Occurrence)
    keepGoing   = (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Node
    forall a. Maybe a
    Nothing, Occurrence
    pol)
        mixed :: TCMT IO (Maybe a, Occurrence)
    mixed       = (Maybe a, Occurrence) -> TCMT IO (Maybe a, Occurrence)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a
    forall a. Maybe a
    Nothing, Occurrence
    Mixed)
        negative :: TCM (Maybe Node, Occurrence)
    negative    = (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Node
    forall a. Maybe a
    Nothing, Occurrence -> Occurrence -> Occurrence
    forall a. SemiRing a => a -> a -> a
    otimes Occurrence
    pol Occurrence
    JustNeg)
        addPol :: Occurrence -> TCM (Maybe Node, Occurrence)
    addPol Occurrence
    pol' = (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Node
    forall a. Maybe a
    Nothing, Occurrence -> Occurrence -> Occurrence
    forall a. SemiRing a => a -> a -> a
    otimes Occurrence
    pol Occurrence
    pol')

      isGuarding :: QName -> TCMT IO Occurrence
    isGuarding QName
    d = do
        Maybe DataOrRecord
    isDR <- QName -> TCMT IO (Maybe DataOrRecord)
    isDataOrRecordType QName
    d
        Occurrence -> TCMT IO Occurrence
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Occurrence -> TCMT IO Occurrence)
    -> Occurrence -> TCMT IO Occurrence
    forall a b. (a -> b) -> a -> b
    $ case Maybe DataOrRecord
    isDR of
          Just DataOrRecord
    IsData -> Occurrence
    GuardPos  -- a datatype is guarding
          Maybe DataOrRecord
    _           -> Occurrence
    StrictPos

    -- Pretty-printing -----------------------------------------------------

    instance Pretty Node where
      pretty :: Node -> Doc
    pretty = \case
        DefNode QName
    q   -> QName -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty QName
    q
        ArgNode QName
    q Nat
    i -> QName -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty QName
    q Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> ArgName -> Doc
    P.text (ArgName
    "." ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Nat -> ArgName
    forall a. Show a => a -> ArgName
    show Nat
    i)

    instance PrettyTCM Node where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Node -> m Doc
    prettyTCM = Doc -> m Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> m Doc) -> (Node -> Doc) -> Node -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Node -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty

    instance PrettyTCMWithNode (Edge OccursWhere) where
      prettyTCMWithNode :: forall n (m :: * -> *).
    (PrettyTCM n, MonadPretty m) =>
    WithNode n (Edge OccursWhere) -> m Doc
    prettyTCMWithNode (WithNode n
    n (Edge Occurrence
    o OccursWhere
    w)) = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ Occurrence -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Occurrence
    o m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> n -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM n
    n
        , Nat -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> m Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> m Doc) -> Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ OccursWhere -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty OccursWhere
    w
        ]

    instance PrettyTCM (Seq OccursWhere) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Seq OccursWhere -> m Doc
    prettyTCM =
        ((ArgName, Doc) -> Doc) -> m (ArgName, Doc) -> m Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgName, Doc) -> Doc
    forall a b. (a, b) -> b
    snd (m (ArgName, Doc) -> m Doc)
    -> (Seq OccursWhere -> m (ArgName, Doc))
    -> Seq OccursWhere
    -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [OccursWhere] -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    [OccursWhere] -> m (ArgName, Doc)
    prettyOWs ([OccursWhere] -> m (ArgName, Doc))
    -> (Seq OccursWhere -> [OccursWhere])
    -> Seq OccursWhere
    -> m (ArgName, Doc)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (OccursWhere -> OccursWhere) -> [OccursWhere] -> [OccursWhere]
    forall a b. (a -> b) -> [a] -> [b]
    map OccursWhere -> OccursWhere
    adjustLeftOfArrow ([OccursWhere] -> [OccursWhere])
    -> (Seq OccursWhere -> [OccursWhere])
    -> Seq OccursWhere
    -> [OccursWhere]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [OccursWhere] -> [OccursWhere]
    uniq ([OccursWhere] -> [OccursWhere])
    -> (Seq OccursWhere -> [OccursWhere])
    -> Seq OccursWhere
    -> [OccursWhere]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Seq OccursWhere -> [OccursWhere]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Fold.toList
        where
          nth :: a -> [m Doc]
    nth a
    0 = ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "first"
          nth a
    1 = ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "second"
          nth a
    2 = ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "third"
          nth a
    n = ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords (ArgName -> [m Doc]) -> ArgName -> [m Doc]
    forall a b. (a -> b) -> a -> b
    $ a -> ArgName
    forall a. Show a => a -> ArgName
    show (a
    n a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1) ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    "th"

          -- Removes consecutive duplicates.
          uniq :: [OccursWhere] -> [OccursWhere]
          uniq :: [OccursWhere] -> [OccursWhere]
    uniq = ([OccursWhere] -> OccursWhere) -> [[OccursWhere]] -> [OccursWhere]
    forall a b. (a -> b) -> [a] -> [b]
    map [OccursWhere] -> OccursWhere
    forall a. [a] -> a
    head ([[OccursWhere]] -> [OccursWhere])
    -> ([OccursWhere] -> [[OccursWhere]])
    -> [OccursWhere]
    -> [OccursWhere]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (OccursWhere -> OccursWhere -> Bool)
    -> [OccursWhere] -> [[OccursWhere]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    List.groupBy (Seq Where -> Seq Where -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Seq Where -> Seq Where -> Bool)
    -> (OccursWhere -> Seq Where) -> OccursWhere -> OccursWhere -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` OccursWhere -> Seq Where
    snd')
            where
            snd' :: OccursWhere -> Seq Where
    snd' (OccursWhere Range
    _ Seq Where
    _ Seq Where
    ws) = Seq Where
    ws

          prettyOWs :: MonadPretty m => [OccursWhere] -> m (String, Doc)
          prettyOWs :: forall (m :: * -> *).
    MonadPretty m =>
    [OccursWhere] -> m (ArgName, Doc)
    prettyOWs []  = m (ArgName, Doc)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          prettyOWs [OccursWhere
    o] = do
            (ArgName
    s, Doc
    d) <- OccursWhere -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    OccursWhere -> m (ArgName, Doc)
    prettyOW OccursWhere
    o
            (ArgName, Doc) -> m (ArgName, Doc)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ArgName
    s, Doc
    d Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ".")
          prettyOWs (OccursWhere
    o:[OccursWhere]
    os) = do
            (ArgName
    s1, Doc
    d1) <- OccursWhere -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    OccursWhere -> m (ArgName, Doc)
    prettyOW  OccursWhere
    o
            (ArgName
    s2, Doc
    d2) <- [OccursWhere] -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    [OccursWhere] -> m (ArgName, Doc)
    prettyOWs [OccursWhere]
    os
            (ArgName, Doc) -> m (ArgName, Doc)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ArgName
    s1, Doc
    d1 Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> (Doc
    "," Doc -> Doc -> Doc
    P.<+> Doc
    "which" Doc -> Doc -> Doc
    P.<+> ArgName -> Doc
    P.text ArgName
    s2 Doc -> Doc -> Doc
    P.$$ Doc
    d2))

          prettyOW :: MonadPretty m => OccursWhere -> m (String, Doc)
          prettyOW :: forall (m :: * -> *).
    MonadPretty m =>
    OccursWhere -> m (ArgName, Doc)
    prettyOW (OccursWhere Range
    _ Seq Where
    cs Seq Where
    ws)
            | Seq Where -> Bool
    forall a. Null a => a -> Bool
    null Seq Where
    cs   = Seq Where -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    Seq Where -> m (ArgName, Doc)
    prettyWs Seq Where
    ws
            | Bool
    otherwise = do
                (ArgName
    s, Doc
    d1) <- Seq Where -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    Seq Where -> m (ArgName, Doc)
    prettyWs Seq Where
    ws
                (ArgName
    _, Doc
    d2) <- Seq Where -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    Seq Where -> m (ArgName, Doc)
    prettyWs Seq Where
    cs
                (ArgName, Doc) -> m (ArgName, Doc)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ArgName
    s, Doc
    d1 Doc -> Doc -> Doc
    P.$$ Doc
    "(" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    d2 Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ")")

          prettyWs :: MonadPretty m => Seq Where -> m (String, Doc)
          prettyWs :: forall (m :: * -> *).
    MonadPretty m =>
    Seq Where -> m (ArgName, Doc)
    prettyWs Seq Where
    ws = case Seq Where -> [Where]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    Fold.toList Seq Where
    ws of
            [InDefOf QName
    d, Where
    IsIndex] ->
              (,) ArgName
    "is" (Doc -> (ArgName, Doc)) -> m Doc -> m (ArgName, Doc)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "an index of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    d])
            [Where]
    _ ->
              (,) ArgName
    "occurs" (Doc -> (ArgName, Doc)) -> m Doc -> m (ArgName, Doc)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                (Where -> Doc -> m Doc) -> Doc -> Seq Where -> m Doc
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> b -> m b) -> b -> t a -> m b
    Fold.foldrM (\Where
    w Doc
    d -> Doc -> m Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return Doc
    d m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (Where -> [m Doc]
    forall (m :: * -> *). MonadPretty m => Where -> [m Doc]
    prettyW Where
    w)) Doc
    forall a. Null a => a
    empty Seq Where
    ws

          prettyW :: MonadPretty m => Where -> [m Doc]
          prettyW :: forall (m :: * -> *). MonadPretty m => Where -> [m Doc]
    prettyW = \case
            Where
    LeftOfArrow  -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "to the left of an arrow"
            DefArg QName
    q Nat
    i   -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "in the" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [m Doc]
    forall {a} {m :: * -> *}.
    (Eq a, Num a, Applicative m, Show a) =>
    a -> [m Doc]
    nth Nat
    i [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "argument of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
                              [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q]
            Where
    UnderInf     -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "under" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
                            [do -- this cannot fail if an 'UnderInf' has been generated
                                Def QName
    inf Elims
    _ <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
    getBuiltin' ArgName
    builtinInf
                                QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    inf]
            Where
    VarArg       -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "in an argument of a bound variable"
            Where
    MetaArg      -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "in an argument of a metavariable"
            ConArgType QName
    c -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "in the type of the constructor" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    c]
            IndArgType QName
    c -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "in an index of the target type of the constructor" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    c]
            InClause Nat
    i   -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "in the" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [m Doc]
    forall {a} {m :: * -> *}.
    (Eq a, Num a, Applicative m, Show a) =>
    a -> [m Doc]
    nth Nat
    i [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "clause"
            Where
    Matched      -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "as matched against"
            Where
    IsIndex      -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "as an index"
            InDefOf QName
    d    -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "in the definition of" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    d]

          adjustLeftOfArrow :: OccursWhere -> OccursWhere
          adjustLeftOfArrow :: OccursWhere -> OccursWhere
    adjustLeftOfArrow (OccursWhere Range
    r Seq Where
    cs Seq Where
    os) =
            Range -> Seq Where -> Seq Where -> OccursWhere
    OccursWhere Range
    r ((Where -> Bool) -> Seq Where -> Seq Where
    forall a. (a -> Bool) -> Seq a -> Seq a
    DS.filter (Bool -> Bool
    not (Bool -> Bool) -> (Where -> Bool) -> Where -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Where -> Bool
    isArrow) Seq Where
    cs) (Seq Where -> OccursWhere) -> Seq Where -> OccursWhere
    forall a b. (a -> b) -> a -> b
    $
              Seq Where
    noArrows
                Seq Where -> Seq Where -> Seq Where
    forall a. Seq a -> Seq a -> Seq a
    DS.><
              case Seq Where -> ViewL Where
    forall a. Seq a -> ViewL a
    DS.viewl Seq Where
    startsWithArrow of
                ViewL Where
    DS.EmptyL  -> Seq Where
    forall a. Seq a
    DS.empty
                Where
    w DS.:< Seq Where
    ws -> Where
    w Where -> Seq Where -> Seq Where
    forall a. a -> Seq a -> Seq a
    DS.<| (Where -> Bool) -> Seq Where -> Seq Where
    forall a. (a -> Bool) -> Seq a -> Seq a
    DS.filter (Bool -> Bool
    not (Bool -> Bool) -> (Where -> Bool) -> Where -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Where -> Bool
    isArrow) Seq Where
    ws
            where
            (Seq Where
    noArrows, Seq Where
    startsWithArrow) = (Where -> Bool) -> Seq Where -> (Seq Where, Seq Where)
    forall a. (a -> Bool) -> Seq a -> (Seq a, Seq a)
    DS.breakl Where -> Bool
    isArrow Seq Where
    os

            isArrow :: Where -> Bool
    isArrow LeftOfArrow{} = Bool
    True
            isArrow Where
    _             = Bool
    False