Documentation

Mask any application patterns that match against a type that is not a data/record type; see issues agda#1023, agda#5910. The returned list always has the same number of elements of the input.

The behaviour of this function when computing the type to be used for the remainder of a pattern telescope is different between the top-level (the DeBruijnPattern instance) and in constructor patterns below that (maskNonDataArgsInPattern).

At toplevel, application patterns are treated as *neutrals* when computing the type to be used for the rest of the patterns. This is needed for agda#1023: after applying the first two arguments, the function looks like noo .WOne (Refl) : WOne → Zero so the next pattern wrap f would be treated as a datatype and considered for structural recursion, which allows the proof of false to go through.

When masking *inside* a constructor pattern, the arguments are treated as values. An example for the necessity of this difference is in testSucceedMaskSigmaRecursion. However, if this is allowed for *indexed* types, we recover a variant of Issue5910 again. Therefore, we only allow this for types that use all of their arguments with non-mixed positivity, see testfailIssue5910IxC.

If at any point it becomes impossible to compute the type of the rest of the telescope (e.g. because, at top-level, a pattern was skipped, and the function has a computed type from then on), every following (non-projection) pattern is treated as masked (see testFailMaskingComputedType).