fn compute_exhaustiveness_and_usefulness<'a, 'p, Cx: PatCx>(
    mcx: &mut UsefulnessCtxt<'a, Cx>,
    matrix: &mut Matrix<'p, Cx>,
) -> Result<WitnessMatrix<Cx>, Cx::Error>
Expand description

The core of the algorithm.

This recursively computes witnesses of the non-exhaustiveness of matrix (if any). Also tracks usefulness of each row in the matrix (in row.useful). We track usefulness of each subpattern in mcx.useful_subpatterns.

The input Matrix and the output WitnessMatrix together match the type exhaustively.

The key steps are:

  • specialization, where we dig into the rows that have a specific constructor and call ourselves recursively;
  • unspecialization, where we lift the results from the previous step into results for this step (using apply_constructor and by updating row.useful for each parent row). This is all explained at the top of the file.