Build env with List (1 param, 2 ctors including recursive cons). List.{u} : Sort u → Sort u List.nil.{u} : ∀ (α : Sort u), List.{u} α List.cons.{u} : ∀ (α : Sort u), α → List.{u} α → List.{u} α
()
| 4932 | } |
| 4933 | |
| 4934 | let gen_rec = selected_idx.map(|i| &generated[i]); |
| 4935 | match gen_rec { |
| 4936 | Some(g) => { |
| 4937 | if declared_lvls != g.lvls { |
| 4938 | return Err(TcError::Other(format!( |
| 4939 | "check_recursor: universe arity mismatch: stored={declared_lvls}, generated={}", |
| 4940 | g.lvls |
| 4941 | ))); |
| 4942 | } |
| 4943 | if declared_is_unsafe != g.is_unsafe { |
| 4944 | return Err(TcError::Other(format!( |
| 4945 | "check_recursor: safety mismatch: stored={declared_is_unsafe}, generated={}", |
| 4946 | g.is_unsafe |
| 4947 | ))); |
| 4948 | } |
| 4949 | if (params, motives, minors, indices) |
| 4950 | != (g.params, g.motives, g.minors, g.indices) |
| 4951 | { |
| 4952 | return Err(TcError::Other(format!( |
| 4953 | "check_recursor: arity metadata mismatch: \ |
| 4954 | stored=(params={params}, motives={motives}, minors={minors}, indices={indices}), \ |
| 4955 | generated=(params={}, motives={}, minors={}, indices={})", |
| 4956 | g.params, g.motives, g.minors, g.indices |
| 4957 | ))); |
| 4958 | } |
| 4959 | if !self.is_def_eq(&g.ty, &ty)? { |
| 4960 | // When `IX_TYPE_DIFF` is set, walk the binder chain to find the |
| 4961 | // first divergent binder and print a readable gen/sto diff. Off |
| 4962 | // by default: in alpha-collapse regimes or for mutual blocks |
| 4963 | // with near-identical peers, every such mismatch ends up in |
| 4964 | // `stt.ungrounded` (non-fatal), and printing them all drowns |
| 4965 | // stderr under tens of thousands of lines. The walk only runs |
| 4966 | // when the env var is set to keep the common path cheap. |
| 4967 | // |
| 4968 | // Uses `KExpr::Display` (Name.Pretty@shorthex for consts, |
| 4969 | // `#idx` / `name` for vars, `(f a b …)` for spines, etc.) — |
| 4970 | // the same formatter `TcError::AppTypeMismatch` uses — so the |
| 4971 | // output format matches the rest of the kernel's diagnostic |
| 4972 | // surface. |
| 4973 | if *IX_TYPE_DIFF { |
| 4974 | let mut gc = g.ty.clone(); |
| 4975 | let mut sc = ty.clone(); |
| 4976 | let mut bi = 0u64; |
| 4977 | loop { |
| 4978 | match (gc.data(), sc.data()) { |
| 4979 | ( |
| 4980 | ExprData::All(_, _, gd, gb, _), |
| 4981 | ExprData::All(_, _, sd, sb, _), |
| 4982 | ) => { |
| 4983 | if !self.is_def_eq(gd, sd).unwrap_or(false) { |
| 4984 | let label = if bi < params { |
| 4985 | "param" |
| 4986 | } else if bi < params + motives { |
| 4987 | "motive" |
| 4988 | } else if bi < params + motives + minors { |
| 4989 | "minor" |
| 4990 | } else { |
| 4991 | "idx/major" |