Method peel_proj_forall

crates/kernel/src/infer.rs:463–476

Peel the leading `Π` binder from `e`, returning `(domain, body)`. Tries the syntactic fast path first: if `e` is already `ExprData::All(..)`, no WHNF call is made. Only on miss does it fall back to full `whnf` and re-check. This is the audit Tier 1 #2 fix (`infer.rs:218, 281, 299`); the per-iteration full WHNF on a body mutated by `subst` rarely hits the WHNF cache and re-traverses the substitute

(
    &mut self,
    e: &KExpr<M>,
    err: &'static str,
  )

  /// parameter rather than baking one in.
  fn peel_proj_forall(
    &mut self,
    e: &KExpr<M>,
    err: &'static str,
  ) -> Result<(KExpr<M>, KExpr<M>), TcError<M>> {
    if let ExprData::All(_, _, dom, body, _) = e.data() {
      return Ok((dom.clone(), body.clone()));
    }
    let w = self.whnf(e)?;
    match w.data() {
      ExprData::All(_, _, dom, body, _) => Ok((dom.clone(), body.clone())),
      _ => Err(TcError::Other(err.into())),
    }
  }

  fn infer_nat_type(&mut self) -> KExpr<M> {
    self.intern(KExpr::cnst(self.prims.nat.clone(), Box::new([])))
  }