ill-formed AIR: mutable reference used in equality

[tjhance]

struct X { }

fn test(a: &mut X)
    requires a == a,
{
}

thread '<unnamed>' panicked at rust_verify/src/verifier.rs:553:17:
internal error: ill-typed AIR code: error 'error 'use of undeclared variable a!' in expression 'a!'' in expression '(axiom_location ("failed precondition") (tx!test.) (= a! a!))'

[tjhance]

Part of the problem is the way we determine is_mut_ref_param in mk_vir_args (fn_call_to_vir.rs):

    let raw_inputs = bctx.ctxt.tcx.fn_sig(f).instantiate(tcx, node_substs).skip_binder().inputs();
    assert!(raw_inputs.len() == args.len());
    args.iter()
        .zip(raw_inputs)
        .map(|(arg, raw_param)| {
            let is_mut_ref_param = match raw_param.kind() {
                TyKind::Ref(_, _, rustc_hir::Mutability::Mut) => true,
                _ => false,
            }; 
            ...

So we have spec_eq which has type for<Lhs, Rhs> (Lhs, Rhs) -> bool. After instantiating that with the type params with Lhs and Rhs it becomes (&mut X, &mut X) -> bool and these are then interpreted as mutable params.

I think maybe we shouldn't be calling mk_vir_args at all for spec_eq ... I'm not sure if this is a problem more generally. Might be worth skipping this issue until next-gen mut-ref support anyway.