Internal error when iterating on a Vec of slices

[ayhon]

When running

cargo check &&
    nix run github:aeneasverif/aeneas#charon -L -- --hide-marker-traits --remove-associated-types='*' &&
    nix run github:aeneasverif/aeneas -L -- -backend lean sha3.llbc

on a project, I encountered the following error

[Info ] Imported: sha3.llbc
[Info ] Generated the partial file (because of errors): ./Sha3.lean
[Error] Nested borrows are not supported yet (found in the signature of: core::slice::iter::{core::iter::traits::iterator::Iterator<&'a (@Slice<T>)> for core::slice::iter::Chunks<'a, T>}#71::next)
Source: '/rustc/library/core/src/slice/iter.rs', lines 1505:4-1505:41
[Error] Could not translate the function signature of 'core::slice::iter::{core::iter::traits::iterator::Iterator<&'a (@Slice<T>)> for core::slice::iter::Chunks<'a, T>}#71::next because of previous error
Name pattern: 'core::slice::iter::{core::iter::traits::iterator::Iterator<core::slice::iter::Chunks<''a, @T>, &''a [@T]>}::next'
Source: '/rustc/library/core/src/slice/iter.rs', lines 1505:4-1505:41
[Error] Nested borrows are not supported yet (found in the signature of: core::slice::iter::{core::iter::traits::iterator::Iterator<&'a (T)> for core::slice::iter::Iter<'a, T>}#182::next)
Source: '/rustc/library/core/src/slice/iter/macros.rs', lines 156:12-156:47
[Error] Could not translate the function signature of 'core::slice::iter::{core::iter::traits::iterator::Iterator<&'a (T)> for core::slice::iter::Iter<'a, T>}#182::next because of previous error
Name pattern: 'core::slice::iter::{core::iter::traits::iterator::Iterator<core::slice::iter::Iter<''a, @T>, &''a @T>}::next'
Source: '/rustc/library/core/src/slice/iter/macros.rs', lines 156:12-156:47
[Error] Nested borrows are not supported yet (found in the signature of: core::slice::iter::{core::iter::traits::iterator::Iterator<&'a mut (T)> for core::slice::iter::IterMut<'a, T>}#190::next)
Source: '/rustc/library/core/src/slice/iter/macros.rs', lines 156:12-156:47
[Error] Could not translate the function signature of 'core::slice::iter::{core::iter::traits::iterator::Iterator<&'a mut (T)> for core::slice::iter::IterMut<'a, T>}#190::next because of previous error
Name pattern: 'core::slice::iter::{core::iter::traits::iterator::Iterator<core::slice::iter::IterMut<''a, @T>, &''a mut @T>}::next'
Source: '/rustc/library/core/src/slice/iter/macros.rs', lines 156:12-156:47
[Error] Invalid inputs for binop
Source: 'src/simple.rs', lines 128:8-128:26
[Error] Invalid inputs for binop
Source: 'src/simple.rs', lines 149:8-149:41
[Error] Internal error, please file an issue
Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 595:4-598:24
[Error] Internal error, please file an issue
Source: '/rustc/library/alloc/src/vec/mod.rs', lines 3436:4-3436:40
[Error] Internal error, please file an issue
Source: '/rustc/library/alloc/src/vec/mod.rs', lines 3689:4-3689:64
[Error] Internal error, please file an issue
Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 1997:4-1999:20
[Error] Invalid inputs for binop
Source: 'src/simple.rs', lines 52:24-52:68
[Error] Invalid inputs for binop
Source: 'src/simple.rs', lines 44:8-44:44
[Error] Invalid inputs for binop
Source: 'src/simple.rs', lines 38:8-38:31
[Error] Invalid inputs for binop
Source: 'src/simple.rs', lines 114:53-114:73
[Error] Nested borrows are not supported yet (found in the signature of: core::slice::iter::{core::iter::traits::iterator::Iterator<&'a (@Slice<T>)> for core::slice::iter::Chunks<'a, T>}#71::next)
Source: '/rustc/library/core/src/slice/iter.rs', lines 1505:4-1505:41
[Error] Could not translate the function 'core::slice::iter::{core::iter::traits::iterator::Iterator<&'a (@Slice<T>)> for core::slice::iter::Chunks<'a, T>}#71::next because of previous error
Name pattern: 'core::slice::iter::{core::iter::traits::iterator::Iterator<core::slice::iter::Chunks<''a, @T>, &''a [@T]>}::next'
Source: '/rustc/library/core/src/slice/iter.rs', lines 1505:4-1505:41
[Error] Nested borrows are not supported yet (found in the signature of: core::slice::iter::{core::iter::traits::iterator::Iterator<&'a (T)> for core::slice::iter::Iter<'a, T>}#182::next)
Source: '/rustc/library/core/src/slice/iter/macros.rs', lines 156:12-156:47
[Error] Could not translate the function 'core::slice::iter::{core::iter::traits::iterator::Iterator<&'a (T)> for core::slice::iter::Iter<'a, T>}#182::next because of previous error
Name pattern: 'core::slice::iter::{core::iter::traits::iterator::Iterator<core::slice::iter::Iter<''a, @T>, &''a @T>}::next'
Source: '/rustc/library/core/src/slice/iter/macros.rs', lines 156:12-156:47
[Error] Nested borrows are not supported yet (found in the signature of: core::slice::iter::{core::iter::traits::iterator::Iterator<&'a mut (T)> for core::slice::iter::IterMut<'a, T>}#190::next)
Source: '/rustc/library/core/src/slice/iter/macros.rs', lines 156:12-156:47
[Error] Could not translate the function 'core::slice::iter::{core::iter::traits::iterator::Iterator<&'a mut (T)> for core::slice::iter::IterMut<'a, T>}#190::next because of previous error
Name pattern: 'core::slice::iter::{core::iter::traits::iterator::Iterator<core::slice::iter::IterMut<''a, @T>, &''a mut @T>}::next'
Source: '/rustc/library/core/src/slice/iter/macros.rs', lines 156:12-156:47
[Error] Name clash detected: the following identifiers are bound to the same name "core.iter.traits.collect.IntoIterator":
- trait_decl_id: 5
  Source: '/rustc/library/core/src/iter/traits/collect.rs', lines 318:0-318:22
- trait_impl_id: 4
  Source: '/rustc/library/core/src/iter/traits/collect.rs', lines 318:0-318:22
You may want to rename some of your definitions, or report an issue.
[Error] Error when registering the name for id: trait_impl_id: 4:
The chosen name is already in the names set: core.iter.traits.collect.IntoIterator
Source: '/rustc/library/core/src/iter/traits/collect.rs', lines 318:0-318:22
[Error] Mutually recursive trait declarations are not supported

As requested in the error messages, I'm opening up an issue. See the previous link for the exact commit on which I encounter this problem.

[ayhon]

I managed to minimize it to

#![allow(dead_code)]

fn sponge_absorb(chunks: Vec<&[bool]>, s: &mut [bool; 16]) {
    for chunk in chunks {
    }
}