Method subst_univ

crates/kernel/src/tc.rs:779–809

Substitute universe params in a universe level. Fails with `UnivParamOutOfRange { idx, bound }` if an interior `Param(idx)` references beyond `us.len()`. In a well-typed kernel run, every call site supplies `us` whose length matches the arity of the enclosing constant (validated by `infer` at the Const gate), so this error never fires on well-formed input. It exists to turn any internal invariant

(
    &mut self,
    u: &KUniv<M>,
    us: &[KUniv<M>],
  )

    cache.insert(key, interned.clone());
    Ok(interned)
  }

  /// Substitute universe params in a universe level.
  ///
  /// Fails with `UnivParamOutOfRange { idx, bound }` if an interior
  /// `Param(idx)` references beyond `us.len()`. In a well-typed kernel
  /// run, every call site supplies `us` whose length matches the
  /// arity of the enclosing constant (validated by `infer` at the Const
  /// gate), so this error never fires on well-formed input. It exists
  /// to turn any internal invariant slip into a loud failure instead of
  /// a silent orphan `Param` propagating downstream.
  pub fn subst_univ(
    &mut self,
    u: &KUniv<M>,
    us: &[KUniv<M>],
  ) -> Result<KUniv<M>, TcError<M>> {
    match u.data() {
      UnivData::Zero(_) => Ok(u.clone()),
      UnivData::Param(i, _, _) => {
        match usize::try_from(*i).ok().and_then(|i| us.get(i)) {
          Some(v) => Ok(v.clone()),
          None => {
            Err(TcError::UnivParamOutOfRange { idx: *i, bound: us.len() })
          },
        }
      },
      UnivData::Succ(inner, _) => {
        let inner2 = self.subst_univ(inner, us)?;
        Ok(KUniv::succ(inner2))
      },
      UnivData::Max(a, b, _) => {
        let a2 = self.subst_univ(a, us)?;
        let b2 = self.subst_univ(b, us)?;
        Ok(KUniv::max(a2, b2))