    {-# LANGUAGE NondecreasingIndentation #-}

    -- | 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.Reader ( MonadReader(..), asks, ReaderT, runReaderT )

    import Data.Either
    import qualified Data.Foldable as Fold
    import Data.Function (on)
    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 Data.Strict.These

    import Debug.Trace

    import Agda.Interaction.Options.Base ( optPolarity )
    import Agda.Syntax.Common
    import qualified Agda.Syntax.Info as Info
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern
    import Agda.Syntax.Position (HasRange(..), noRange)
    import Agda.TypeChecking.Datatypes ( isDataOrRecordType )
    import Agda.TypeChecking.Functions
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Patterns.Match ( properlyMatching )
    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 qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import qualified Agda.Syntax.Common.Pretty as P
    import Agda.Syntax.Common.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.
    --
    --   Find polarity of datatypes parameters and indices.
    --
    --   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
    forall (m :: * -> *). MonadPretty m => [QName] -> m Doc
    prettyTCM [QName]
    qs
      g <- Set QName -> TCM (Graph Node (Edge OccursWhere))
    buildOccurrenceGraph Set QName
    qset
      let (gstar, sccs) =
            Graph.gaussJordanFloydWarshallMcNaughtonYamada $ fmap occ g
      reportSDoc "tc.pos.tick" 100 $ "constructed graph"
      reportSLn "tc.pos.graph" 5 $ "Positivity graph: N=" ++ show (size $ Graph.nodes g) ++
                                   " E=" ++ show (length $ Graph.edges g)
      reportSDoc "tc.pos.graph" 10 $ vcat
        [ "positivity graph for" <+> fsep (map prettyTCM qs)
        , nest 2 $ prettyTCM g
        ]
      reportSLn "tc.pos.graph" 5 $
        "Positivity graph (completed): E=" ++ show (length $ Graph.edges gstar)
      reportSDoc "tc.pos.graph" 50 $ vcat
        [ "transitive closure of positivity graph for" <+>
          prettyTCM qs
        , nest 2 $ prettyTCM gstar
        ]

      -- remember argument occurrences for qs in the signature
      setArgOccs qset qs gstar
      reportSDoc "tc.pos.tick" 100 $ "set args"

      -- check positivity for all strongly connected components of the graph for qs
      reportSDoc "tc.pos.graph.sccs" 10 $ do
        let (triv, others) = partitionEithers $ for sccs $ \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
        sep [ text $ show (length triv) ++ " trivial sccs"
            , text $ show (length others) ++ " non-trivial sccs with lengths " ++
                show (map length others)
            ]
      reportSLn "tc.pos.graph.sccs" 15 $
        "  sccs = " ++ prettyShow [ scc | CyclicSCC scc <- sccs ]

      -- #7133: Note that the graph doesn't necessarily contain all of qs in the case where there are no
      -- occurrences of a name, but we still need to setMutual for them.
      let sccMap = [Map QName [QName]] -> Map QName [QName]
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions [ case SCC Node
    scc of
                                  AcyclicSCC (DefNode QName
    q) -> QName -> [QName] -> Map QName [QName]
    forall k a. k -> a -> Map k a
    Map.singleton QName
    q []
                                  AcyclicSCC ArgNode{}   -> Map QName [QName]
    forall a. Monoid a => a
    mempty
                                  CyclicSCC [Node]
    scc          -> [(QName, [QName])] -> Map QName [QName]
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (QName
    q, [QName]
    qs) | QName
    q <- [QName]
    qs ]
                                    where qs :: [QName]
    qs = [ QName
    q | DefNode QName
    q <- [Node]
    scc ]
                              | SCC Node
    scc <- [SCC Node]
    sccs ]
      inAbstractMode $ forM_ qs $ \ 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
          let qs :: [QName]
    qs = [QName] -> Maybe [QName] -> [QName]
    forall a. a -> Maybe a -> a
    fromMaybe [] (Maybe [QName] -> [QName]) -> Maybe [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ QName -> Map QName [QName] -> Maybe [QName]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    q Map QName [QName]
    sccMap
          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 " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++
                                         if | [QName] -> Bool
    forall a. Null a => a -> Bool
    null [QName]
    qs        -> ArgName
    "non-recursive"
                                            | [QName] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [QName]
    qs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    1 -> ArgName
    "recursive"
                                            | Bool
    otherwise      -> ArgName
    "mutually recursive"
          QName -> [QName] -> TCM ()
    setMutual QName
    q [QName]
    qs

      mapM_ (checkPos g gstar) qs
      reportSDoc "tc.pos.tick" 100 $ "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
          Maybe DataOrRecord -> (DataOrRecord -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (Definition -> Maybe DataOrRecord
    isDatatype Definition
    def) ((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
    forall (m :: * -> *). MonadPretty m => QName -> 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 a b. (a -> b) -> Graph Node a -> Graph Node b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((OccursWhere -> Seq OccursWhere)
    -> Edge OccursWhere -> Edge (Seq OccursWhere)
    forall a b. (a -> b) -> Edge a -> Edge b
    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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    forall (m :: * -> *). MonadPretty m => Seq OccursWhere -> 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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
    forall (m :: * -> *). MonadPretty m => QName -> 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 a. a -> TCMT IO a
    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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    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 ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TypeError
    RecursiveRecordNeedsInductivity QName
    q

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

        isDatatype :: Definition -> Maybe DataOrRecord
        isDatatype :: Definition -> Maybe DataOrRecord
    isDatatype Definition
    def = do
          case Definition -> Defn
    theDef Definition
    def of
            Datatype{dataClause :: Defn -> Maybe Clause
    dataClause = Maybe Clause
    Nothing} -> DataOrRecord -> Maybe DataOrRecord
    forall a. a -> Maybe a
    Just DataOrRecord
    forall p. DataOrRecord' p
    IsData
            Record  {recClause :: Defn -> Maybe Clause
    recClause  = Maybe Clause
    Nothing, PatternOrCopattern
    recPatternMatching :: PatternOrCopattern
    recPatternMatching :: Defn -> 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
    forall p. p -> DataOrRecord' p
    IsRecord PatternOrCopattern
    recPatternMatching
            Defn
    _ -> Maybe DataOrRecord
    forall a. Maybe a
    Nothing

        -- 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q
            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
    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 = -- 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

            reportSDoc "tc.pos.args" 10 $ sep
              [ "args of" <+> prettyTCM q <+> "="
              , nest 2 $ prettyList $ map prettyTCM 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.
            modifyArgOccurrences q (mergeOccs $!! args)

          where
          mergeOccs :: [Occurrence] -> [Occurrence] -> [Occurrence]
          mergeOccs :: [Occurrence] -> [Occurrence] -> [Occurrence]
    mergeOccs [Occurrence]
    poccs [Occurrence]
    toccs =
            -- Lucas, 2022-12-01:
            -- `poccs` are the occurences computed by the positivity-checker
            -- `toccs` are the occurences/polarities explicitely given by the user
            --   (and enforced through type-checking)
            -- We consider the polarities explicitely given (toccs) to take priority over the ones
            -- found out by the positivity checker.
            -- Note: Alas, this is hard to enforce given that non-annotated variables are
            -- always annotated with Mixed polarity. If the annotated polarity is Mixed,
            -- for now we always rely on the result from the positivity analysis.
            [Occurrence] -> [Occurrence] -> [These Occurrence Occurrence]
    forall a b. [a] -> [b] -> [These a b]
    align [Occurrence]
    poccs [Occurrence]
    toccs [These Occurrence Occurrence]
    -> (These Occurrence Occurrence -> Occurrence) -> [Occurrence]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> (Occurrence -> Occurrence -> Occurrence)
    -> These Occurrence Occurrence -> Occurrence
    forall a. (a -> a -> a) -> These a a -> a
    mergeThese (\Occurrence
    a Occurrence
    b -> if Occurrence
    b Occurrence -> Occurrence -> Bool
    forall a. Eq a => a -> a -> Bool
    == Occurrence
    Mixed then Occurrence
    a else Occurrence
    b)

          -- 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
      TelV tel _ <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView (Definition -> Type
    defType Definition
    def)
      return $ size tel - projectionArgs def

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

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

    instance HasRange Item where
      getRange :: Item -> Range
    getRange (AnArg Nat
    _ [Occurrence]
    _) = 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 [Occurrence]
    t) = 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
    forall a. Doc a -> Doc a -> Doc a
    P.<+> Nat -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty Nat
    i Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.<+> [Occurrence] -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty [Occurrence]
    t
      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
    forall a. Doc a -> Doc a -> Doc a
    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 a. a -> Maybe a
    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 b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    guard Bool
    keep
          OccurrencesBuilder' -> Maybe OccurrencesBuilder'
    forall a. a -> Maybe a
    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 [Occurrence]
    _) -> 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 a b. (a -> b -> b) -> b -> [a] -> b
    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 = ReaderT OccEnv ReduceM

    instance (Semigroup a, Monoid a) => Monoid (OccM a) where
      mempty :: OccM a
    mempty  = a -> OccM a
    forall a. a -> ReaderT OccEnv ReduceM 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 ReduceM [a]) -> [OccM a] -> OccM a
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> [OccM a] -> ReaderT OccEnv ReduceM [a]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [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 ReduceM a -> ReaderT OccEnv ReduceM a
    forall a.
    (OccEnv -> OccEnv)
    -> ReaderT OccEnv ReduceM a -> ReaderT OccEnv ReduceM a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((OccEnv -> OccEnv)
     -> ReaderT OccEnv ReduceM a -> ReaderT OccEnv ReduceM a)
    -> (OccEnv -> OccEnv)
    -> ReaderT OccEnv ReduceM a
    -> ReaderT OccEnv ReduceM a
    forall a b. (a -> b) -> a -> b
    $ \ OccEnv
    e -> OccEnv
    e { vars = is ++ vars 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
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    a
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.pos.var" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "variables in context: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Maybe Item] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Maybe Item]
    vars
      env <- [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 a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CoinductionKit -> QName
    nameOfInf (Maybe CoinductionKit -> OccEnv)
    -> TCMT IO (Maybe CoinductionKit) -> TCMT IO OccEnv
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe CoinductionKit)
    coinductionKit
      runReduceM $ runReaderT (occurrences a) env

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

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

    instance ComputeOccurrences Clause where
      occurrences :: Clause -> ReaderT OccEnv ReduceM 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
        -- TODO #3733: handle hcomp/transp clauses properly
        if NAPs -> Bool
    hasDefP NAPs
    ps then OccurrencesBuilder -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a. a -> ReaderT OccEnv ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return OccurrencesBuilder
    forall a. Monoid a => a
    mempty else do
          argOccs <- ((Nat, NamedArg DeBruijnPattern)
     -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder))
    -> [(Nat, NamedArg DeBruijnPattern)]
    -> ReaderT OccEnv ReduceM [OccurrencesBuilder]
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m (Maybe b)) -> [a] -> m [b]
    mapMaybeM (Nat, NamedArg DeBruijnPattern)
    -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder)
    forall a.
    (Nat, NamedArg (Pattern' a))
    -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder)
    matching ([(Nat, NamedArg DeBruijnPattern)]
     -> ReaderT OccEnv ReduceM [OccurrencesBuilder])
    -> [(Nat, NamedArg DeBruijnPattern)]
    -> ReaderT OccEnv ReduceM [OccurrencesBuilder]
    forall a b. (a -> b) -> a -> b
    $ [Nat] -> NAPs -> [(Nat, NamedArg DeBruijnPattern)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Nat
    0..] NAPs
    ps
          (Concat argOccs <>) <$> do
          withExtendedOccEnv' items $
            occurrences $ clauseBody cl
        where
          matching :: (Int, NamedArg (Pattern' a)) -> OccM (Maybe OccurrencesBuilder)
          matching :: forall a.
    (Nat, NamedArg (Pattern' a))
    -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder)
    matching (Nat
    i, NamedArg (Pattern' a)
    p) = do
            Pattern' a -> ReaderT OccEnv ReduceM Bool
    forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
    properlyMatching (Named NamedName (Pattern' a) -> Pattern' a
    forall name a. Named name a -> a
    namedThing (Named NamedName (Pattern' a) -> Pattern' a)
    -> Named NamedName (Pattern' a) -> Pattern' a
    forall a b. (a -> b) -> a -> b
    $ NamedArg (Pattern' a) -> Named NamedName (Pattern' a)
    forall e. Arg e -> e
    unArg NamedArg (Pattern' a)
    p) ReaderT OccEnv ReduceM Bool
    -> (Bool -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder))
    -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder)
    forall a b.
    ReaderT OccEnv ReduceM a
    -> (a -> ReaderT OccEnv ReduceM b) -> ReaderT OccEnv ReduceM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Bool
    True -> Maybe OccurrencesBuilder
    -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder)
    forall a. a -> ReaderT OccEnv ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe OccurrencesBuilder
     -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder))
    -> Maybe OccurrencesBuilder
    -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder)
    forall a b. (a -> b) -> a -> b
    $ 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 -> [Occurrence] -> Item
    AnArg Nat
    i []
              Bool
    False -> Maybe OccurrencesBuilder
    -> ReaderT OccEnv ReduceM (Maybe OccurrencesBuilder)
    forall a. a -> ReaderT OccEnv ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return 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 -> NamedArg DeBruijnPattern -> IntMap (Maybe Item))
    -> [Nat] -> NAPs -> [IntMap (Maybe Item)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Nat -> NamedArg 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 -> NamedArg DeBruijnPattern -> IntMap (Maybe Item)
    patItem Nat
    i NamedArg DeBruijnPattern
    p = (Nat -> IntMap (Maybe Item)) -> [Nat] -> IntMap (Maybe Item)
    forall m a. Monoid m => (a -> m) -> [a] -> m
    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)
    -> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamedArg 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 -> [Occurrence] -> Item
    AnArg Nat
    i [])

    instance ComputeOccurrences Term where
      occurrences :: Term -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Term
    v = case Term -> Term
    unSpine Term
    v of
        Var Nat
    i Elims
    args ->
          (OccEnv -> OccurrencesBuilder)
    -> ReaderT OccEnv ReduceM 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) ReaderT OccEnv ReduceM OccurrencesBuilder
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a. Semigroup a => a -> a -> a
    <> do
            occs <- (Elim -> ReaderT OccEnv ReduceM OccurrencesBuilder)
    -> Elims -> ReaderT OccEnv ReduceM [OccurrencesBuilder]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Elims
    args

            -- Lucas, 2022-12-01: Now, variables may have the polarities of their arguments
            -- stored in the context (say, if the variable refers to a datatype parameter)
            item <- reader ((!! i) . vars)

            let getPol Nat
    i = Occurrence -> Maybe Occurrence -> Occurrence
    forall a. a -> Maybe a -> a
    fromMaybe Occurrence
    Mixed (Maybe Occurrence -> Occurrence) -> Maybe Occurrence -> Occurrence
    forall a b. (a -> b) -> a -> b
    $ do
                  AnArg _ aoccs <- Maybe Item
    item
                  aoccs !!! i

            return $ Concat $ zipWith (\Nat
    i -> Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs (Occurrence -> Nat -> Where
    VarArg (Nat -> Occurrence
    getPol Nat
    i) Nat
    i)) [0..] occs
          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
          inf <- (OccEnv -> Maybe QName) -> ReaderT OccEnv ReduceM (Maybe QName)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks OccEnv -> Maybe QName
    inf
          let 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)
          occs <- mapM occurrences args
          return . Concat $ OccursHere (ADef d) : zipWith occsAs [0..] occs

        Con ConHead
    _ ConInfo
    _ Elims
    args -> Elims -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Elims
    args
        MetaV MetaId
    _ Elims
    args -> Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    MetaArg (OccurrencesBuilder -> OccurrencesBuilder)
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Elims
    args
        Pi Dom Type
    a Abs Type
    b       -> (Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    LeftOfArrow (OccurrencesBuilder -> OccurrencesBuilder)
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Dom Type
    a) ReaderT OccEnv ReduceM OccurrencesBuilder
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a. Semigroup a => a -> a -> a
    <> Abs Type -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Abs Type
    b
        Lam ArgInfo
    _ Abs Term
    b      -> Abs Term -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Abs Term
    b
        Level Level
    l      -> Level -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Level
    l
        Lit{}        -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a. Monoid a => a
    mempty
        Sort{}       -> ReaderT OccEnv ReduceM 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 -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Term
    v
        Dummy{}      -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a. Monoid a => a
    mempty

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

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

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

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

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

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

    instance (ComputeOccurrences x, ComputeOccurrences a) => ComputeOccurrences (Boundary' x a) where
      occurrences :: Boundary' x a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences = [(x, (a, a))] -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences ([(x, (a, a))] -> ReaderT OccEnv ReduceM OccurrencesBuilder)
    -> (Boundary' x a -> [(x, (a, a))])
    -> Boundary' x a
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Boundary' x a -> [(x, (a, a))]
    forall x a. Boundary' x a -> [(x, (a, a))]
    theBoundary

    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) -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences (a
    x, b
    y) = a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences a
    x ReaderT OccEnv ReduceM OccurrencesBuilder
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a. Semigroup a => a -> a -> a
    <> b -> ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a.
    ComputeOccurrences a =>
    a -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences b
    y

    instance ComputeOccurrences Int where
      occurrences :: Nat -> ReaderT OccEnv ReduceM OccurrencesBuilder
    occurrences Nat
    _ = ReaderT OccEnv ReduceM OccurrencesBuilder
    forall a. Monoid a => a
    mempty

    -- | 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
        m <- (TCEnv -> AbstractMode) -> TCMT IO AbstractMode
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> AbstractMode
    envAbstractMode
        cur <- asksTC envCurrentModule
        o <- asksTC envCurrentOpaqueId
        "computeOccurrences" <+> prettyTCM q <+> text (show a) <+> text (show o) <+> text (show m)
          <+> prettyTCM 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
          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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Clause -> TCMT IO Clause
    forall (tcm :: * -> *). PureTCM 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
          Concat . zipWith (OccursAs . InClause) [0..] <$>
            mapM (getOccurrences []) 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, dataTranspIx :: Defn -> Maybe QName
    dataTranspIx = Maybe QName
    trx} -> do
          -- Andreas, 2013-02-27 (later edited by someone else): First,
          -- include each index of an inductive family.
          TelV telD _ <- 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
          sizeIndex <- caseList (drop np0 $ telToList telD) (return 0) $ \ 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)
    forall (m :: * -> *).
    (HasOptions m, HasBuiltins m) =>
    Dom (ArgName, Type) -> m (Maybe BoundedSize)
    isSizeType Dom (ArgName, Type)
    dom) (Nat -> TCM Nat
    forall a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    1
          let np = Nat
    np0 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    sizeIndex
          let xs = [Nat
    np .. Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    telD Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1] -- argument positions corresponding to indices

          let 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 (\Nat
    i -> Item -> OccurrencesBuilder
    OccursHere (Item -> OccurrencesBuilder) -> Item -> OccurrencesBuilder
    forall a b. (a -> b) -> a -> b
    $ Nat -> [Occurrence] -> Item
    AnArg Nat
    i []) [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 (\Nat
    i -> Where -> OccurrencesBuilder -> OccurrencesBuilder
    OccursAs Where
    IsIndex (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 -> [Occurrence] -> Item
    AnArg Nat
    i []) [Nat]
    xs

          -- Then, we compute the occurrences in the constructor types.
          let 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 tel t, bnd) <- AllowedReductions
    -> TCMT IO (TelV Type, Boundary) -> TCMT IO (TelV Type, Boundary)
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    AllowedReductions -> m a -> m a
    putAllowedReductions AllowedReductions
    allReductions (TCMT IO (TelV Type, Boundary) -> TCMT IO (TelV Type, Boundary))
    -> TCMT IO (TelV Type, Boundary) -> TCMT IO (TelV Type, Boundary)
    forall a b. (a -> b) -> a -> b
    $
                  Type -> TCMT IO (TelV Type, Boundary)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type, Boundary)
    telViewPathBoundary (Type -> TCMT IO (TelV Type, Boundary))
    -> (Definition -> Type)
    -> Definition
    -> TCMT IO (TelV Type, Boundary)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Type
    defType (Definition -> TCMT IO (TelV Type, Boundary))
    -> TCMT IO Definition -> TCMT IO (TelV Type, Boundary)
    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 (tel0,tel1) = splitTelescopeAt np 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.)
                tel1' <- addContext tel0 $ normalise $ tel1

                -- Make parameters into context items, with polarity info
                pvars <- parametersToItems tel0 np
                let telvars = Nat -> Maybe Item -> [Maybe Item]
    forall a. Nat -> a -> [a]
    replicate (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel1') Maybe Item
    forall a. Maybe a
    Nothing [Maybe Item] -> [Maybe Item] -> [Maybe Item]
    forall a. [a] -> [a] -> [a]
    ++ [Maybe Item]
    pvars

                reportSLn "tc.pos.params" 50 $ "Adding datatypes parameters in context " ++ prettyShow pvars

                -- Occurrences in the types of the constructor arguments.
                (OccursAs (ConArgType c) <$> getOccurrences pvars tel1') <>
                  (OccursAs (ConEndpoint c) <$> getOccurrences telvars bnd) <> 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'.
                  case unEl 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 [Maybe Item]
    telvars [Arg Term]
    indices
                      | Bool
    otherwise -> TCMT IO OccurrencesBuilder
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- 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__

          -- If the data type has a transport constructor (i.e. it's an
          -- indexed family in cubical mode) we should also consider it for
          -- positivity.
          mconcat $ pure ioccs : map conOcc (cs ++ maybeToList trx)

        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
          pvars <- Tele (Dom Type) -> Nat -> TCM [Maybe Item]
    parametersToItems Tele (Dom Type)
    tel0 Nat
    np
          getOccurrences pvars =<< addContext tel0 (normalise 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__
      where
        parametersToItems :: Telescope -> Nat -> TCM [Maybe Item]
        parametersToItems :: Tele (Dom Type) -> Nat -> TCM [Maybe Item]
    parametersToItems Tele (Dom Type)
    tel Nat
    n = [Maybe Item] -> [Maybe Item]
    forall a. [a] -> [a]
    reverse ([Maybe Item] -> [Maybe Item])
    -> TCM [Maybe Item] -> TCM [Maybe Item]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
          (Nat -> Type -> TCMT IO (Maybe Item))
    -> [Nat] -> [Type] -> TCM [Maybe Item]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (\Nat
    i -> ([Occurrence] -> Maybe Item)
    -> TCMT IO [Occurrence] -> TCMT IO (Maybe Item)
    forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Item -> Maybe Item
    forall a. a -> Maybe a
    Just (Item -> Maybe Item)
    -> ([Occurrence] -> Item) -> [Occurrence] -> Maybe Item
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> [Occurrence] -> Item
    AnArg Nat
    i) (TCMT IO [Occurrence] -> TCMT IO (Maybe Item))
    -> (Type -> TCMT IO [Occurrence]) -> Type -> TCMT IO (Maybe Item)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> TCMT IO [Occurrence]
    getOccurrencesFromType)
            [Nat
    0 .. Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1]
            ((ArgName, Type) -> Type
    forall a b. (a, b) -> b
    snd ((ArgName, Type) -> Type)
    -> (Dom (ArgName, Type) -> (ArgName, Type))
    -> Dom (ArgName, Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (ArgName, Type) -> (ArgName, Type)
    forall t e. Dom' t e -> e
    unDom (Dom (ArgName, Type) -> Type) -> [Dom (ArgName, Type)] -> [Type]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Tele (Dom Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel)

    -- 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
    $c== :: Node -> Node -> Bool
    == :: Node -> Node -> Bool
    $c/= :: Node -> Node -> Bool
    /= :: 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
    $ccompare :: Node -> Node -> Ordering
    compare :: Node -> Node -> Ordering
    $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
    >= :: Node -> Node -> Bool
    $cmax :: Node -> Node -> Node
    max :: Node -> Node -> Node
    $cmin :: Node -> Node -> Node
    min :: Node -> Node -> Node
    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
    $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
    /= :: 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
    $ccompare :: forall a. Ord a => Edge a -> Edge a -> Ordering
    compare :: Edge a -> Edge a -> Ordering
    $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
    >= :: Edge a -> Edge a -> Bool
    $cmax :: forall a. Ord a => Edge a -> Edge a -> Edge a
    max :: Edge a -> Edge a -> Edge a
    $cmin :: forall a. Ord a => Edge a -> Edge a -> Edge a
    min :: Edge a -> Edge a -> Edge a
    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
    $cshowsPrec :: forall a. Show a => Nat -> Edge a -> ArgName -> ArgName
    showsPrec :: Nat -> Edge a -> ArgName -> ArgName
    $cshow :: forall a. Show a => Edge a -> ArgName
    show :: Edge a -> ArgName
    $cshowList :: forall a. Show a => [Edge a] -> ArgName -> ArgName
    showList :: [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
    $cfmap :: forall a b. (a -> b) -> Edge a -> Edge b
    fmap :: forall a b. (a -> b) -> Edge a -> Edge b
    $c<$ :: forall a b. a -> Edge b -> Edge a
    <$ :: forall a b. a -> Edge b -> Edge a
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
          occs <- QName -> TCMT IO OccurrencesBuilder
    computeOccurrences' QName
    q

          reportSDoc "tc.pos.occs" 40 $
            (("Occurrences in" <+> prettyTCM q) <> ":")
              $+$
            nest 2 (vcat $
               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") $
               List.sortBy (compare `on` snd) $
               Map.toList (flatten occs))

          -- Placing this line before the reportSDoc lines above creates a
          -- space leak: occs is retained for too long.
          es <- computeEdges qs q occs

          reportSDoc "tc.pos.occs.edges" 60 $
            "Edges:"
              $+$
            nest 2 (vcat $
               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
    forall (m :: * -> *). MonadPretty m => Node -> 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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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
    forall (m :: * -> *). MonadPretty m => Node -> m Doc
    prettyTCM (Edge Node (Edge OccursWhere) -> Node
    forall n e. Edge n e -> n
    Graph.target Edge Node (Edge OccursWhere)
    e))
                   es)

          return 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 a b. (a -> b -> b) -> b -> [a] -> b
    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 a. a -> TCMT IO a
    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
          (to', pol) <- Node -> Occurrence -> Where -> TCM (Maybe Node, Occurrence)
    mkEdge' Node
    to Occurrence
    pol Where
    w
          let mk = Occurrence
    -> OccurrencesBuilder'
    -> Node
    -> Seq Where
    -> Seq Where
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    mkEdge Occurrence
    pol OccurrencesBuilder'
    ob
          case 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 [Occurrence]
    t ->
              ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    -> TCMT
         IO
         ([Edge Node (Edge OccursWhere)] -> [Edge Node (Edge OccursWhere)])
    forall a. a -> TCMT IO a
    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 b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless (Occurrence -> Bool
    forall a. Null a => a -> Bool
    null Occurrence
    pol) (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 a. a -> TCMT IO a
    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 b a. IsBool b => b -> (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)
                (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
        VarArg Occurrence
    p Nat
    i     -> Occurrence -> TCM (Maybe Node, Occurrence)
    addPol Occurrence
    p
        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
          pol' <- QName -> TCMT IO Occurrence
    isGuarding QName
    d
          if Set.member d muts
            then return (Just (ArgNode d i), pol')
            else addPol =<< otimes pol' <$> getArgOccurrence d 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
        ConEndpoint QName
    _  -> TCM (Maybe Node, Occurrence)
    keepGoing
        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
          pol' <- QName -> TCMT IO Occurrence
    isGuarding QName
    d
          return (Just (DefNode d), pol')
        where
        keepGoing :: TCM (Maybe Node, Occurrence)
    keepGoing   = (Maybe Node, Occurrence) -> TCM (Maybe Node, Occurrence)
    forall a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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
        QName -> TCM (Maybe DataOrRecord)
    isDataOrRecordType QName
    d TCM (Maybe DataOrRecord)
    -> (Maybe DataOrRecord -> Occurrence) -> TCMT IO Occurrence
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
          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
    forall a. ArgName -> Doc a
    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 a. a -> m a
    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
    forall (m :: * -> *). MonadPretty m => Occurrence -> 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
    forall (m :: * -> *). MonadPretty m => n -> 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 a. a -> m a
    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 a b. (a -> b) -> m a -> m b
    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 a. Seq a -> [a]
    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 = (NonEmpty OccursWhere -> OccursWhere)
    -> [NonEmpty OccursWhere] -> [OccursWhere]
    forall a b. (a -> b) -> [a] -> [b]
    map NonEmpty OccursWhere -> OccursWhere
    forall a. NonEmpty a -> a
    List1.head ([NonEmpty OccursWhere] -> [OccursWhere])
    -> ([OccursWhere] -> [NonEmpty OccursWhere])
    -> [OccursWhere]
    -> [OccursWhere]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (OccursWhere -> OccursWhere -> Bool)
    -> [OccursWhere] -> [NonEmpty OccursWhere]
    forall (f :: * -> *) a.
    Foldable f =>
    (a -> a -> Bool) -> f a -> [NonEmpty a]
    List1.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
            (s, d) <- OccursWhere -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    OccursWhere -> m (ArgName, Doc)
    prettyOW OccursWhere
    o
            return (s, d <> ".")
          prettyOWs (OccursWhere
    o:[OccursWhere]
    os) = do
            (s1, d1) <- OccursWhere -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    OccursWhere -> m (ArgName, Doc)
    prettyOW  OccursWhere
    o
            (s2, d2) <- prettyOWs os
            return (s1, d1 <> ("," P.<+> "which" P.<+> P.text s2 P.$$ 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
                (s, d1) <- Seq Where -> m (ArgName, Doc)
    forall (m :: * -> *).
    MonadPretty m =>
    Seq Where -> m (ArgName, Doc)
    prettyWs Seq Where
    ws
                (_, d2) <- prettyWs cs
                return (s, d1 P.$$ "(" <> d2 <> ")")

          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 a. Seq a -> [a]
    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
    forall (m :: * -> *). MonadPretty m => QName -> 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 a. a -> m a
    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
    forall (m :: * -> *). MonadPretty m => QName -> 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
                                inf <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinInf
                                prettyTCM inf]
            VarArg Occurrence
    p Nat
    i   -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "in an argument of a bound variable at position" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Nat -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Nat -> m Doc
    prettyTCM 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
    "which uses its argument with polarity" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++ [ Occurrence -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Occurrence
    p ]
            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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    c]
            ConEndpoint QName
    c
                         -> ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "in an endpoint of the target of the" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
                            ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "higher 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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    forall (m :: * -> *). MonadPretty m => QName -> 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