Method infer_proj

crates/kernel/src/infer.rs:329–448

(
    &mut self,
    struct_id: &KId<M>,
    field: u64,
    val: &KExpr<M>,
    val_ty: &KExpr<M>,
  )

  fn infer_proj(
    &mut self,
    struct_id: &KId<M>,
    field: u64,
    val: &KExpr<M>,
    val_ty: &KExpr<M>,
  ) -> Result<KExpr<M>, TcError<M>> {
    use super::level::univ_eq;
    use super::tc::collect_app_spine;

    let wty = self.whnf(val_ty)?;
    let (head, args) = collect_app_spine(&wty);

    let head_id = match head.data() {
      ExprData::Const(id, _, _) => id,
      _ => {
        return Err(TcError::Other(
          "projection: struct type is not a constant".into(),
        ));
      },
    };
    if head_id.addr != struct_id.addr {
      return Err(TcError::Other(
        "projection: type mismatch with declared struct".into(),
      ));
    }

    let (i_levels, num_params, num_indices, ctors) = match self
      .try_get_const(head_id)?
    {
      Some(KConst::Indc { params, indices, ctors, .. }) => {
        let levels = match head.data() {
          ExprData::Const(_, us, _) => us.clone(),
          _ => unreachable!(),
        };
        (
          levels,
          u64_to_usize::<M>(params)?,
          u64_to_usize::<M>(indices)?,
          ctors.clone(),
        )
      },
      _ => {
        return Err(TcError::Other("projection: not an inductive type".into()));
      },
    };

    if ctors.len() != 1 {
      return Err(TcError::Other(
        "projection: inductive must have exactly one constructor".into(),
      ));
    }

    // Check if the structure lives in Prop. Do this from the inductive
    // declaration's result sort instead of inferring the full applied value
    // type: projection-heavy proof terms otherwise re-infer every parameter
    // and index argument just to recover a universe that is declaration-local.
    let is_prop_struct = self.inductive_app_is_prop(
      head_id,