Validate an inductive type and its constructors.
(
&mut self,
id: &KId<M>,
)
| 146 | |
| 147 | /// Validate an inductive type and its constructors. |
| 148 | pub fn check_inductive_member( |
| 149 | &mut self, |
| 150 | id: &KId<M>, |
| 151 | ) -> Result<(), TcError<M>> { |
| 152 | let (params, indices, lvls, ctors, block, is_unsafe, ty) = match self |
| 153 | .get_const(id)? |
| 154 | { |
| 155 | KConst::Indc { |
| 156 | params, |
| 157 | indices, |
| 158 | lvls, |
| 159 | ctors, |
| 160 | block, |
| 161 | is_unsafe, |
| 162 | ty, |
| 163 | .. |
| 164 | } => ( |
| 165 | params, |
| 166 | indices, |
| 167 | lvls, |
| 168 | ctors.clone(), |
| 169 | block.clone(), |
| 170 | is_unsafe, |
| 171 | ty.clone(), |
| 172 | ), |
| 173 | _ => { |
| 174 | return Err(TcError::Other("check_inductive: not an inductive".into())); |
| 175 | }, |
| 176 | }; |
| 177 | |
| 178 | // Discover all inductives in the mutual block |
| 179 | let block_inds = self.discover_block_inductives(&block)?; |
| 180 | let block_addrs: Vec<Address> = |
| 181 | block_inds.iter().map(|id| id.addr.clone()).collect(); |
| 182 | |
| 183 | // Inductive type must reduce to a Sort after peeling params+indices. |
| 184 | // This must be checked even for inductives with no constructors. |
| 185 | let ind_level = |
| 186 | self.get_result_sort_level(&ty, u64_to_usize(params + indices)?)?; |
| 187 | |
| 188 | // S3 + S3b: Peer-agreement invariants for mutual inductives. |
| 189 | // |
| 190 | // S3: all peers live in the same result universe. |
| 191 | // S3b: all peers share the same parameter count and parameter-domain |
| 192 | // types. Without S3b, `build_rec_type` — which takes the shared |
| 193 | // param prefix uniformly from `ind_infos[0]` — would produce a |
| 194 | // generated recursor whose param binders misalign with a peer's |
| 195 | // ctor arguments, yielding de-Bruijn-shifted iota reductions and, |
| 196 | // in the limit, ill-typed stored terms. Enforcing agreement |
| 197 | // kernel-side removes the implicit compiler trust. |
| 198 | // |
| 199 | // References: lean4 `src/kernel/inductive.cpp:211–262 check_inductive_types` |
| 200 | // (line 230–231: "parameters of all inductive datatypes must match") |
| 201 | // and lean4lean `Lean4Lean/Inductive/Add.lean:80–82`. |
| 202 | // |
| 203 | // Memoization: the check is invariant across all peers of the block — |
| 204 | // if peer[0] agrees with each of peer[1..N], then by transitivity all |
| 205 | // pairs agree. Running this loop from *every* peer in the block yields |
no test coverage detected