| 6682 | env.insert( |
| 6683 | mk_id("Tree"), |
| 6684 | KConst::Indc { |
| 6685 | name: (), |
| 6686 | level_params: (), |
| 6687 | lvls: 0, |
| 6688 | params: 0, |
| 6689 | indices: 0, |
| 6690 | is_unsafe: false, |
| 6691 | block: tree_block.clone(), |
| 6692 | member_idx: 0, |
| 6693 | ty: sort1(), |
| 6694 | ctors: vec![mk_id("Tree.node")], |
| 6695 | lean_all: (), |
| 6696 | }, |
| 6697 | ); |
| 6698 | |
| 6699 | // Tree.node : List.{1} Tree → Tree |
| 6700 | // List.{1} Tree : Sort 1 (List at universe 1, applied to Tree) |
| 6701 | let list_tree = |
| 6702 | app(cnst("List", &[AU::succ(AU::zero())]), cnst("Tree", &[])); |
| 6703 | let tree_node_ty = pi(list_tree, cnst("Tree", &[])); |
| 6704 | env.insert( |
| 6705 | mk_id("Tree.node"), |
| 6706 | KConst::Ctor { |
| 6707 | name: (), |
| 6708 | level_params: (), |
| 6709 | is_unsafe: false, |
| 6710 | lvls: 0, |
| 6711 | induct: mk_id("Tree"), |
| 6712 | cidx: 0, |
| 6713 | params: 0, |
| 6714 | fields: 1, |
| 6715 | ty: tree_node_ty, |
| 6716 | }, |
| 6717 | ); |
| 6718 | |
| 6719 | env.blocks.insert(tree_block, vec![mk_id("Tree"), mk_id("Tree.node")]); |
| 6720 | |
| 6721 | let mut tc = TypeChecker::new(&mut env); |
| 6722 | let result = tc.check_const(&mk_id("Tree")); |
| 6723 | assert!( |
| 6724 | result.is_ok(), |
| 6725 | "Tree with List nesting should be accepted, got: {:?}", |
| 6726 | result.err() |
| 6727 | ); |
| 6728 | } |
| 6729 | |
| 6730 | // --------------------------------------------------------------------- |
| 6731 | // Regression tests for the P1 soundness gaps closed in the 2026-04 |
| 6732 | // hardening pass. |
| 6733 | // --------------------------------------------------------------------- |
| 6734 | |
| 6735 | /// P1-1 regression: a recursor with a syntactically well-typed but |
| 6736 | /// semantically *swapped* rule RHS must be rejected by `check_recursor` |
| 6737 | /// at the `is_def_eq(&gen_rule.rhs, &stored_rule.rhs)` gate |
| 6738 | /// (see `inductive.rs:3218`). Without that gate, iota reduction could |
| 6739 | /// produce the wrong minor for a given constructor — the P1-1 scenario |
| 6740 | /// from the adversarial review. |
| 6741 | #[test] |