Adding unreachable guarded match arm triggers unsupported shallow borrows and masks verification errors

[lynae99]

Adding a semantically unreachable guarded match arm

_ if false => unreachable!(),

to a match expression changes Prusti’s verification behavior.
Without the guarded arm, Prusti correctly reports a failing assertion.
With the unreachable guarded arm added, Prusti instead fails with:

[Prusti: unsupported feature] unsupported creation of shallow borrows (implicitly created when lowering matches)

and no longer reports the assertion failure.
The additional guarded arm is semantically unreachable and does not change the program’s behavior. However, it changes the set and nature of verification diagnostics.
Reproduction

#![feature(nll)]
#![feature(box_patterns)]

use prusti_contracts::*;

enum List {
    Nil,
    Const { val: i32, next: Box<List> },
}

fn tail(list: List) -> Option<List> {
    let ret = match list {
        List::Nil => None,
        List::Const { val: _, box next } => Some(next),

        // Uncommenting the next line triggers the unsupported feature error
        // and prevents the assertion failure from being reported.
        // _ if false => unreachable!(),
    };

    assert!(false);

    ret
}

fn main() {}

Actual Behavior
Without _ if false:

• Prusti reports:

error: [Prusti: verification error] the asserted expression might not hold

With _ if false:

• Prusti reports:

[Prusti: unsupported feature] unsupported creation of shallow borrows (implicitly created when lowering matches)

• The assertion failure is no longer reported.

[lynae99]

The same problem happens in this example:

use prusti_contracts::*;

fn main() {}

pub struct List<T> {
    head: Link<T>,
}

type Link<T> = Option<Box<Node<T>>>;

struct Node<T> {
    elem: T,
    next: Link<T>,
}

impl<T> List<T> {
    #[pure]
    pub fn len(&self) -> usize {
        link_len(&self.head)
    }

    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> &T {
        link_lookup(&self.head, index)
    }
}

#[pure]
#[requires(index < link_len(link))]
fn link_lookup<T>(link: &Link<T>, index: usize) -> &T {
    match link {
        Some(node) => {
            if index == 0 {
                &node.elem
            } else {
                link_lookup(&node.next, index - 1)
            }
        }
        None => unreachable!(),

        // Uncommenting this line changes the reported diagnostics:
        // _ if false => unreachable!(),
    }
}

#[pure]
fn link_len<T>(link: &Link<T>) -> usize {
    match link {
        None => 0,
        Some(node) => 1 + link_len(&node.next),
    }
}

Without the guarded arm, Prusti reports:

1. A possible overflow in 1 + link_len(...)
2. That unreachable!() in the None arm of link_lookup might be reachable

After adding the unreachable guarded arm, Prusti instead:

1. Reports an unsupported feature error:

[Prusti: unsupported feature] unsupported creation of shallow borrows (implicitly created when lowering matches)

2. Reports a new failure:

[Prusti: verification error] precondition of pure function call might not hold.

3. No longer reports the earlier unreachable!(..) might be reachable diagnostic.