Computing the occurrence graph for a mutual block. This is used to compute polarities of arguments and to check positivity.

• We do a traversal over internal syntax.
• The occurrence graph is 'NodeMap (NodeMap Edge)', where NodeMap is a mutable hashtable keyed by graph nodes. The outer keys are sources and the inner keys are targets. We insert edges into the graph during the traversal.
• An edge from source to target means that source occurs in target.
• A graph node is either 'DefNode QName', which is a definition site of a mutual name, or 'ArgNode QName Int', which is an argument of a mutual name, indexed left-right starting from 0.
• An edge contains an Occurrence, the Range of the actual occurrence in the internal syntax and an OccursPath that can be used to produce a textual warning message.

The occurrence graph is imprecise in several ways.

• We only normalize types of data constructors and don't compute anything else.
• We have at most a single edge between two nodes. We aggregate multiple actual occurrences into a single edge, using mergeEdges.

Lastly, applications of mutual names to arguments is handled in a rather imprecise way. See Issue 1984 for illustration:

mutual
  record Fun (A : Set) (B : A → Set) : Set where
    field fun : (x : A) → B x

  data U : Set where
    Π : (A : U) (B : El A → U) → U

  El : U → Set
  El (Π A B) = Fun (El A) (λ x → El (B x))

In this case:

• Fun occurs in El.
• El A occurs in the first argument of Fun.
• The first argument of Fun occurs in Fun.

In short, when we apply a mutual name to an argument, we view that as if the argument was substituted inside the body of the mutual name definition.

Hence, Fun "occurs" in Fun, and it does so negatively. This is kinda bogus, because Fun could be moved outside of the mutual block.

A potential fix of this issue would be to first split the mutual block into strongly connected components based on only QName occurrences, and afterwards do the current occurrence analysis for each sub-block.

Immutable representation

Instead of using the mutable hashtable, we use immutable "generic" graphs from Unidirectional for printing warnings and debug messages, and also to define tests in internal property tests. One reason is convenience. Another reason is that the previous (less optimized) implementation before PR 8411 used the generic graphs, and we just reuse the old implementation for printing. See toGenericGraph and fromGenericGraph.