ICE: "expected array or slice type"

[enjhnsn2]

The following implementation of a memcpy-like function causes an ICE:

pub fn copy_to_slice(dest: &mut [u8], src: &[std::cell::Cell<u8>]){
    if src.len() != dest.len() {
        return;
    } else {
        for (i, b) in src.iter().enumerate() {
            dest[i] = b.get();
        };
    }
}

This code fails with:

error: internal compiler error: crates/flux-refineck/src/checker.rs:980:18: expected array or slice type
  --> src/main.rs:95:13
   |
95 |             dest[i] = b.get();
   |             ^^^^^^^

[nilehmann]

Mir for the function

fn copy_to_slice(_1: &mut [u8], _2: &[std::cell::Cell<u8>]) -> () {
    debug dest => _1;
    debug src => _2;
    let mut _0: ();
    let mut _3: bool;
    let mut _4: usize;
    let mut _5: &[std::cell::Cell<u8>];
    let mut _6: usize;
    let mut _7: &[u8];
    let mut _8: !;
    let _9: ();
    let mut _10: std::iter::Enumerate<std::slice::Iter<'_, std::cell::Cell<u8>>>;
    let mut _11: std::iter::Enumerate<std::slice::Iter<'_, std::cell::Cell<u8>>>;
    let mut _12: std::slice::Iter<'_, std::cell::Cell<u8>>;
    let mut _13: &[std::cell::Cell<u8>];
    let mut _14: std::iter::Enumerate<std::slice::Iter<'_, std::cell::Cell<u8>>>;
    let mut _15: ();
    let _16: ();
    let mut _17: std::option::Option<(usize, &std::cell::Cell<u8>)>;
    let mut _18: &mut std::iter::Enumerate<std::slice::Iter<'_, std::cell::Cell<u8>>>;
    let mut _19: &mut std::iter::Enumerate<std::slice::Iter<'_, std::cell::Cell<u8>>>;
    let mut _20: isize;
    let mut _21: !;
    let mut _24: u8;
    let mut _25: &std::cell::Cell<u8>;
    let _26: usize;
    let mut _27: usize;
    let mut _28: bool;
    scope 1 {
        debug iter => _14;
        let _22: usize;
        let _23: &std::cell::Cell<u8>;
        scope 2 {
            debug i => _22;
            debug b => _23;
        }
    }

    bb0: {
        _5 = &(*_2);
        _4 = core::slice::<impl [std::cell::Cell<u8>]>::len(move _5) -> [return: bb1, unwind: bb18];
    }

    bb1: {
        _7 = &(*_1);
        _6 = core::slice::<impl [u8]>::len(move _7) -> [return: bb2, unwind: bb18];
    }

    bb2: {
        _3 = Ne(move _4, move _6);
        switchInt(move _3) -> [0: bb4, otherwise: bb3];
    }

    bb3: {
        _0 = const ();
        goto -> bb17;
    }

    bb4: {
        _13 = &(*_2);
        _12 = core::slice::<impl [std::cell::Cell<u8>]>::iter(move _13) -> [return: bb5, unwind: bb18];
    }

    bb5: {
        _11 = <std::slice::Iter<'_, std::cell::Cell<u8>> as std::iter::Iterator>::enumerate(move _12) -> [return: bb6, unwind: bb18];
    }

    bb6: {
        _10 = <std::iter::Enumerate<std::slice::Iter<'_, std::cell::Cell<u8>>> as std::iter::IntoIterator>::into_iter(move _11) -> [return: bb7, unwind: bb18];
    }

    bb7: {
        PlaceMention(_10);
        _14 = move _10;
        goto -> bb8;
    }

    bb8: {
        falseUnwind -> [real: bb9, unwind: bb18];
    }

    bb9: {
        _19 = &mut _14;
        _18 = &mut (*_19);
        _17 = <std::iter::Enumerate<std::slice::Iter<'_, std::cell::Cell<u8>>> as std::iter::Iterator>::next(move _18) -> [return: bb10, unwind: bb18];
    }

    bb10: {
        PlaceMention(_17);
        _20 = discriminant(_17);
        switchInt(move _20) -> [0: bb12, 1: bb13, otherwise: bb11];
    }

    bb11: {
        FakeRead(ForMatchedPlace(None), _17);
        unreachable;
    }

    bb12: {
        falseEdge -> [real: bb14, imaginary: bb13];
    }

    bb13: {
        _22 = (((_17 as Some).0: (usize, &std::cell::Cell<u8>)).0: usize);
        _23 = (((_17 as Some).0: (usize, &std::cell::Cell<u8>)).1: &std::cell::Cell<u8>);
        _25 = &(*_23);
        _24 = std::cell::Cell::<u8>::get(move _25) -> [return: bb15, unwind: bb18];
    }

    bb14: {
        _9 = const ();
        _0 = const ();
        goto -> bb17;
    }

    bb15: {
        _26 = _22;
        _27 = Len((*_1));
        _28 = Lt(_26, _27);
        assert(move _28, "index out of bounds: the length is {} but the index is {}", move _27, _26) -> [success: bb16, unwind: bb18];
    }

    bb16: {
        (*_1)[_26] = move _24;
        _16 = const ();
        _15 = const ();
        goto -> bb8;
    }

    bb17: {
        return;
    }

    bb18 (cleanup): {
        resume;
    }
}

[ranjitjhala]

Temporary workaround mark dest as strong

#[flux::sig(fn (dest: &strg [u8], src: &[std::cell::Cell<u8>]) ensures dest: [u8] )]