Method check_ctor_against_inductive

crates/kernel/src/inductive.rs:327–356

Validate a standalone constructor by checking its parent inductive block.

(
    &mut self,
    ctor_id: &KId<M>,
    induct_id: &KId<M>,
  )

        ctors.clone(),
        block.clone(),
        is_unsafe,
        ty.clone(),
      ),
      _ => {
        return Err(TcError::Other("check_inductive: not an inductive".into()));
      },
    };
    let ind_arity = checked_metadata_sum::<M>(
      "inductive params + indices",
      &[params, indices],
    )?;

    // Discover all inductives in the mutual block
    let block_inds = self.discover_block_inductives(&block)?;
    let block_addrs: Vec<Address> =
      block_inds.iter().map(|id| id.addr.clone()).collect();

    // Inductive type must reduce to a Sort after peeling params+indices.
    // This must be checked even for inductives with no constructors.
    let ind_level =
      self.get_result_sort_level(&ty, u64_to_usize(ind_arity)?)?;

    // S3 + S3b: Peer-agreement invariants for mutual inductives.
    //
    // S3:  all peers live in the same result universe.
    // S3b: all peers share the same parameter count and parameter-domain
    //      types. Without S3b, `build_rec_type` — which takes the shared
    //      param prefix uniformly from `ind_infos[0]` — would produce a
    //      generated recursor whose param binders misalign with a peer's
    //      ctor arguments, yielding de-Bruijn-shifted iota reductions and,
    //      in the limit, ill-typed stored terms. Enforcing agreement
    //      kernel-side removes the implicit compiler trust.
    //