Cannot verify a constant function if crate has `effect` feature enabled

[celinval]

I tried this code:

#![feature(effects)]

#[kani::requires(kani::mem::can_dereference(arg))]
const unsafe fn dummy<T>(arg: *const T) -> T {
    std::ptr::read(arg)
}

#[kani::proof_for_contract(dummy)]
fn check() {
    unsafe { dummy(&kani::any::<u8>()) };
}

using the following command line invocation:

kani -Z function-contracts -Z mem-predicates contract.rs

with Kani version:

I expected to see this happen: Verification should pass;

Instead, this happened: Compilation fails

error: mismatch in the number of generic parameters: original function/method `dummy` takes 2 generic parameters(s), stub `dummy_recursion_wrapper_8b0f77` takes 1
  --> constant.rs:15:1
   |
15 | #[kani::proof_for_contract(dummy)]
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)

[celinval]

Note: For effects feature, the compiler inserts an extra constant parameter named "host". More implementation details here:

rust-lang/rust#113210
rust-lang/rust#118605