| 955 | // Build a position map for O(1) fvar → position lookup. For typical |
| 956 | // usage (n ≤ 16), a linear scan would also be fine, but the map keeps |
| 957 | // the cost predictable for inductive validation paths that abstract |
| 958 | // larger fvar sets. |
| 959 | let mut pos: FxHashMap<FVarId, u64> = FxHashMap::default(); |
| 960 | pos.reserve(fvars.len()); |
| 961 | for (i, fv) in fvars.iter().enumerate() { |
| 962 | // Innermost (last) gets position 0; outermost (first) gets position |
| 963 | // `n - 1`, matching the `instantiate_rev` convention. |
| 964 | pos.insert(*fv, (fvars.len() - 1 - i) as u64); |
| 965 | } |
| 966 | |
| 967 | let mut cache = std::mem::take(&mut env.subst_scratch); |
| 968 | cache.clear(); |
| 969 | let n = fvars.len() as u64; |