Method try_detect_nested

crates/kernel/src/inductive.rs:620–751

Check if a field domain is a nested inductive occurrence and, if so, add an auxiliary entry to the flat block. A nested occurrence is: after peeling foralls, the result is `ExtInd Ds is` where `ExtInd` is a previously-declared inductive (not in our block) and some param arg `Ds[i]` mentions a block inductive. Important: do not WHNF the domain here.** Compile-side `replace_if_nested` (and Lean's

(
    &mut self,
    dom: &KExpr<M>,
    block_addrs: &[Address],
    flat: &mut Vec<FlatBlockMember<M>>,
    aux_seen: &mut Vec<(Address, Vec<[u8; 32]>)>,
    univ_offset: u64,
    param_depth: usize

    Ok(flat)
  }

  /// Check if a field domain is a nested inductive occurrence and, if so,
  /// add an auxiliary entry to the flat block.
  ///
  /// A nested occurrence is: after peeling foralls, the result is `ExtInd Ds is`
  /// where `ExtInd` is a previously-declared inductive (not in our block) and
  /// some param arg `Ds[i]` mentions a block inductive.
  ///
  /// **Important: do not WHNF the domain here.** Compile-side
  /// `replace_if_nested` (and Lean's C++ `is_nested_inductive_app`,
  /// `inductive.cpp:920`) checks the head literally — if the head is a
  /// definition like `IO.Ref`, it is *not* a nested-inductive occurrence.
  /// WHNF would unfold `IO.Ref α` to `ST.Ref IO.RealWorld α`, which IS an
  /// inductive — the kernel would then synthesize auxiliaries (e.g.
  /// `_nested.ST_Ref_*`) that the compile side never generates, and
  /// `populate_recursor_rules_from_block` would fail with `rec_ids/flat
  /// count mismatch`. Peel `All` constructors structurally instead.
  fn try_detect_nested(
    &mut self,
    dom: &KExpr<M>,
    block_addrs: &[Address],
    flat: &mut Vec<FlatBlockMember<M>>,
    aux_seen: &mut Vec<(Address, Vec<KExpr<M>>)>,
    univ_offset: u64,
    param_depth: usize, // depth at the param context (before field locals)
    n_rec_params: u64, // number of inductive parameters (valid Var refs in spec_params)
  ) -> Result<(), TcError<M>> {
    let saved_lctx = self.lctx.len();
    let result = (|| -> Result<(), TcError<M>> {
      // Peel foralls structurally — no WHNF, see doc comment above. Open
      // each peeled binder with a temporary fvar so domain-local dependencies
      // in external inductive parameters are rejected by the same locality
      // check as field-local dependencies.
      let mut cur = dom.clone();
      while let ExprData::All(_, _, inner_dom, body, _) = cur.data() {
        let inner_dom = inner_dom.clone();
        let body = body.clone();
        let (open, _) = self.open_binder_anon(inner_dom, &body);
        cur = open;
      }

      let (head, args) = collect_app_spine(&cur);
      let head_id = match head.data() {
        ExprData::Const(id, _, _) => id.clone(),
        _ => return Ok(()),
      };

      // Skip if head is already a block member (direct recursive, not nested).
      if block_addrs.contains(&head_id.addr) {
        return Ok(());
      }
      // Also skip if head is already a flat block member (already detected).
      if flat.iter().any(|m| m.id.addr == head_id.addr && !m.is_aux) {
        return Ok(());
      }

      // Check if head is an external inductive.
      let (ext_params, ext_indices, ext_ctors, ext_lvls) =