Method get_result_sort_level

crates/kernel/src/inductive.rs:2090–2119

Get the result sort level of a type after peeling `n` foralls.

(
    &mut self,
    ty: &KExpr<M>,
    n: usize,
  )

      )));
    }
    match group.concrete_univs.as_deref() {
      Some(expected) => {
        if expected.len() != us.len()
          || !expected.iter().zip(us).all(|(a, b)| univ_eq(a, b))
        {
          return Err(TcError::Other(
            "positivity: recursive occurrence has non-uniform universe arguments"
              .into(),
          ));
        }
      },
      None => {
        for (i, u) in us.iter().enumerate() {
          let expected =
            KUniv::param(i as u64, M::meta_field(ix_common::env::Name::anon()));
          if !univ_eq(u, &expected) {
            return Err(TcError::Other(
              "positivity: recursive occurrence has non-uniform universe arguments"
                .into(),
            ));
          }
        }
      },
    }

    if group.params.len() != n_params {
      return Err(TcError::Other(
        "positivity: recursive occurrence parameter arity disagrees with its family"
          .into(),
      ));
    }
    for (i, (actual, expected)) in
      args[..n_params].iter().zip(&group.params).enumerate()