Supposely unreachable place in the Rust AST. The label is "PlaceConstantIndexNotSlice".

[msprotz]

Repro:

// Something more representative of libcrux, with additional parameters
trait KeccakItem<const N: usize>: Clone + Copy {
    fn zero() -> Self;
    fn split_at_mut_n(a: [&mut [u8]; N], mid: usize) -> ([&mut [u8]; N], [&mut [u8]; N]);
    fn store_block<const BLOCKSIZE: usize>(a: &[[Self; 5]; 5], b: [&mut [u8]; N]);
}

struct KeccakState<const N: usize, T: KeccakItem<N>> {
    st: [[T; 5]; 5],
}

impl<const N: usize, T: KeccakItem<N>> core::ops::Index<usize> for KeccakState<N, T> {
    type Output = [T; 5];

    fn index(&self, index: usize) -> &Self::Output {
        &self.st[index]
    }
}

impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
    /// Create a new Shake128 x4 state.
    #[inline(always)]
    fn new() -> Self {
        Self {
            st: [[T::zero(); 5]; 5],
        }
    }
}

fn squeeze_first_three_blocks<const N: usize, T: KeccakItem<N>, const RATE: usize>(
    s: &mut KeccakState<N, T>,
    out: [&mut [u8]; N],
) {
    let (o0, _o1) = T::split_at_mut_n(out, RATE);
    T::store_block::<RATE>(&s.st, o0)
}


fn split_at_mut_1(out: [&mut [u8]; 1], mid: usize) -> ([&mut [u8]; 1], [&mut [u8]; 1]) {
    let [out0] = out;
    let (out00, out01) = out0.split_at_mut(mid);
    ([out00], [out01])
}

fn store_block<const RATE: usize>(s: &[[u64; 5]; 5], out: [&mut [u8]; 1]) {
    for i in 0..RATE / 8 {
        out[0][8 * i..8 * i + 8].copy_from_slice(&s[i / 5][i % 5].to_le_bytes());
    }
}

impl KeccakItem<1> for u64 {
    fn zero() -> Self {
        0
    }
    fn store_block<const BLOCKSIZE: usize>(a: &[[Self; 5]; 5], b: [&mut [u8]; 1]) {
        store_block::<BLOCKSIZE>(a, b)
    }
    fn split_at_mut_n(a: [&mut [u8]; 1], mid: usize) -> ([&mut [u8]; 1], [&mut [u8]; 1]) {
        split_at_mut_1(a, mid)
    }
}

fn test_fancy_example() {
    let mut s: KeccakState<1, u64> = KeccakState::new();
    let mut out = [0u8; 1];
    squeeze_first_three_blocks::<1, u64, 1>(&mut s, [&mut out]);
}

I obtain:

error[HaxFront]: Supposely unreachable place in the Rust AST. The label is "PlaceConstantIndexNotSlice".
                 This error report happend because some assumption about the Rust AST was broken.

                 Context:
                  - current_ty: [&mut [u8]; 1]
                  - current_kind: Local(
                     Local(
                         1,
                     ),
                 )
                  - elem: ConstantIndex {
                     offset: 0,
                     min_length: 1,
                     from_end: false,
                 }
  |
  = note: ⚠️ This is a bug in Hax's frontend.
          Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!

error: Thread panicked when extracting body.
  --> src/main.rs:67:1
   |
67 | fn split_at_mut_1(out: [&mut [u8]; 1], mid: usize) -> ([&mut [u8]; 1], [&mut [u8]; 1]) {
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[ ERROR charon_driver:200] The extraction encountered 1 errors
error: could not compile `where_clauses_simple` (bin "where_clauses_simple") due to 2 previous errors

[msprotz]

I am on Charon revision ed5047fd07e6c6aa8e7b9f352637f91977adacbe