Build an env with an external inductive `Wrap` that has its type param in a **negative** position: `Wrap.mk : ∀ (α : Type), (α → Bool) → Wrap α`. Then define `Evil : Type` with `Evil.mk : Wrap Evil → Evil`. This must be REJECTED: `Evil` appears negatively inside `Wrap`'s constructor.
()
| 6499 | // List.nil (0 fields, 0 IH), List.cons (2 fields + 2 IH = 4) |
| 6500 | // Wait — minors for Tree.rec include ALL ctors of ALL flat members. |
| 6501 | // Tree: leaf (0 binders), node (1 field + 1 IH = 2 binders) |
| 6502 | // List(aux): nil (0 binders), cons (2 fields + 2 IH = 4 binders) |
| 6503 | // But minors are individual forall types, not nested. Each minor is ONE forall domain. |
| 6504 | // So: 2 motives + 4 minors + 1 major = 7 binders total (0 params, 0 indices) |
| 6505 | let n = count_binders(&tree_rec.ty); |
| 6506 | assert_eq!( |
| 6507 | n, 7, |
| 6508 | "Tree.rec should have 7 binders (2 motives + 4 minors + 1 major), got {n}" |
| 6509 | ); |
| 6510 | |
| 6511 | // List auxiliary rec (member 1) |
| 6512 | let list_rec = &generated[1]; |
| 6513 | // List aux rec for List Tree: |
| 6514 | // 0 params + 2 motives + 4 minors + 0 indices + 1 major = 7 |
| 6515 | let n = count_binders(&list_rec.ty); |
| 6516 | assert_eq!(n, 7, "List aux rec should have 7 binders, got {n}"); |
| 6517 | } |
| 6518 | |
| 6519 | /// Polymorphic nested: PTree.{u} : Sort (u+1) → Sort (u+1) |
| 6520 | /// Like Tree but with one universe param and one type param. |
| 6521 | /// PTree.leaf.{u} : ∀ (α : Sort (u+1)), α → PTree.{u} α |
| 6522 | /// PTree.node.{u} : ∀ (α : Sort (u+1)), List.{u+1} (PTree.{u} α) → PTree.{u} α |
| 6523 | fn poly_nested_env() -> KEnv<Anon> { |
| 6524 | let mut env = KEnv::new(); |
| 6525 | let block = mk_id("PTree"); |
| 6526 | let su = || AU::succ(param(0)); // u+1 |
| 6527 | |
| 6528 | // PTree.{u} : Sort(u+1) → Sort(u+1) |
| 6529 | let ptree_ty = pi(AE::sort(su()), AE::sort(su())); |
| 6530 | env.insert( |
| 6531 | mk_id("PTree"), |
| 6532 | KConst::Indc { |
| 6533 | name: (), |
| 6534 | level_params: (), |
| 6535 | lvls: 1, |
| 6536 | params: 1, |
| 6537 | indices: 0, |
| 6538 | is_unsafe: false, |
| 6539 | block: block.clone(), |
| 6540 | member_idx: 0, |
| 6541 | ty: ptree_ty, |
| 6542 | ctors: vec![mk_id("PTree.leaf"), mk_id("PTree.node")], |
| 6543 | lean_all: (), |
| 6544 | }, |
| 6545 | ); |
| 6546 | |
| 6547 | // PTree.leaf : ∀ (α : Sort(u+1)), α → PTree.{u} α |
| 6548 | let leaf_ty = |
| 6549 | pi(AE::sort(su()), pi(var(0), app(cnst("PTree", &[param(0)]), var(1)))); |
| 6550 | env.insert( |
| 6551 | mk_id("PTree.leaf"), |
| 6552 | KConst::Ctor { |
| 6553 | name: (), |
| 6554 | level_params: (), |
| 6555 | is_unsafe: false, |
| 6556 | lvls: 1, |
| 6557 | induct: mk_id("PTree"), |
| 6558 | cidx: 0, |