I added the option --no-occurrence-analysis, which turns off the occurrence analysis for functions. I have a mutual block that is 1762 lines long, and before I enabled the option I did not see Agda succeed in checking that block.

I also tried to enable the flag for the full development. I could type-check quite a lot of code before Agda complained. The speedup was something like 5%.

I placed the help text for the option in the section "Modalities". That is not a perfect fit. An alternative would be to add a new section. Any opinions?

In the documentation I connect the analysis to positivity checking and to the unused argument feature. Is the analysis used for something else that should be mentioned in the documentation?

Given that bugs in the positivity checker can lead to inconsistencies I suggest that someone checks that the implementation makes sense. The main change was to treat every function argument as "matched":

      -- Perform automated occurrence analysis for functions?
      performAnalysis <- optOccurrence <$> pragmaOptions
      if performAnalysis then
        Concat . zipWith (OccursAs . InClause) [0..] <$>
          mapM (getOccurrences []) cs
       else
        return $ case cs of
          []     -> __IMPOSSIBLE__
          cl : _ ->
            Concat
              [ OccursAs Matched (OccursHere (AnArg i []))
              | (i, _) <- zip [0..] (namedClausePats cl)
              ]

By the way, is the use of __IMPOSSIBLE__ above safe? The documentation of _funClauses does not state that a function must have at least one clause, but it seems as if functions without clauses are handled differently.

It might make sense to have a pragma as well, but I do not currently plan to implement that feature.

@martinescardo, the flag --no-occurrence-analysis turns off some Agda features that you might not want to rely on.