Explicit trigger with `spec_fn` causes ill-typed AIR code

The following code produces the following error:

#![allow(unused_imports)]
use builtin::*;
use builtin_macros::*;
use vstd::prelude::*;
use vstd::pcm::*;

verus! {

pub enum EntryResourceValue {
    Empty,
    Invalid,
}

impl PCM for EntryResourceValue {
    open spec fn valid(self) -> bool {
        !(self is Invalid)
    }

    open spec fn op(self, other: Self) -> Self {
        match (self, other) {
            (EntryResourceValue::Empty, _) => other,
            (_, EntryResourceValue::Empty) => self,
            (_, _) => EntryResourceValue::Invalid {  },
        }
    }

    open spec fn unit() -> Self {
        EntryResourceValue::Empty {  }
    }

    proof fn closed_under_incl(a: Self, b: Self) {}
    proof fn commutative(a: Self, b: Self) {}
    proof fn associative(a: Self, b: Self, c: Self) {}
    proof fn op_unit(a: Self) {}
    proof fn unit_valid() {}
}

pub struct ResourceValue {
    pub m: spec_fn(int) -> EntryResourceValue,
}

impl ResourceValue {
    pub open spec fn valid(self) -> bool {
        forall |i| #![trigger (self.m)(i)] (self.m)(i).valid()
    }
}

fn main()
{
}

}

thread '<unnamed>' panicked at rust_verify\src\verifier.rs:517:17:
internal error: ill-typed AIR code: error 'error 'in call to =>, argument #2 has type "Poly" when it should have type "Bool"' in expression '(=>
 (has_type i$ INT)
 (vstd!pcm.PCM.valid.? $ TYPE%main!EntryResourceValue. (apply Poly (main!ResourceValue./ResourceValue/m
    (%Poly%main!ResourceValue. self!)
   ) i$
)))'' in expression '(=>
 (fuel_bool fuel%main!impl&%1.valid.)
 (forall ((self! Poly)) (!
   (= (main!impl&%1.valid.? self!) (forall ((i$ Poly)) (!
      (=>
       (has_type i$ INT)
       (vstd!pcm.PCM.valid.? $ TYPE%main!EntryResourceValue. (apply Poly (main!ResourceValue./ResourceValue/m
          (%Poly%main!ResourceValue. self!)
         ) i$
      )))
      :pattern ((apply Poly (main!ResourceValue./ResourceValue/m (%Poly%main!ResourceValue.
          self!
         )
        ) i$
      ))
      :qid user_main__ResourceValue__valid_0
      :skolemid skolem_user_main__ResourceValue__valid_0
   )))
   :pattern ((main!impl&%1.valid.? self!))
   :qid internal_main!impl&__1.valid.?_definition
   :skolemid skolem_internal_main!impl&__1.valid.?_definition
)))'
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread '<unnamed>' panicked at rust_verify\src\verifier.rs:339:17:
dropped, expected call to `into_inner` instead
stack backtrace:
   0:     0x7ff9a6d622c2 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h7851e041f2b8bcc2
   1:     0x7ff9a6d94cdd - core::fmt::write::h1642dfca37b49735
   2:     0x7ff9a6d58ca1 - <std::io::IoSlice as core::fmt::Debug>::fmt::h7801514a6fc13a4a
   3:     0x7ff9a6d620ea - std::sys_common::backtrace::lock::h8caaa69a6cc2258b
   4:     0x7ff9a6d65529 - std::panicking::default_hook::h67f6260a0bf37eca
   5:     0x7ff9a6d651e5 - std::panicking::default_hook::h67f6260a0bf37eca
   6:     0x7ff9a6d65b14 - std::panicking::rust_panic_with_hook::h870983d929e74e12
   7:     0x7ff77795504e - std::thread::spawn::hb70439decf7df413
   8:     0x7ff777950159 - <<&mut bincode::de::Deserializer<R,O> as serde::de::Deserializer>::deserialize_tuple::Access<R,O> as serde::de::SeqAccess>::next_element_seed::h5ba860ae8260c504
   9:     0x7ff7781a87bd - std::panicking::begin_panic::hf8117e11b83ce5e9
  10:     0x7ff7779ad4f3 - core::ptr::drop_in_place<indexmap::map::IndexMap<rustc_type_ir::BoundVar,rustc_middle::ty::sty::BoundVariableKind,core::hash::BuildHasherDefault<rustc_hash::FxHasher>>>::hfb2e6caef48a5825
  11:     0x7ff7779d49bf - rust_verify::verifier::Verifier::merge::h5466702f989e3b40
  12:     0x7ffa0f2b1060 - <unknown>
  13:     0x7ffa0f2b53ea - is_exception_typeof
  14:     0x7ffa0f2bfb80 - _C_specific_handler
  15:     0x7ffa0f2b45f0 - is_exception_typeof
  16:     0x7ffa0f2c04b1 - _CxxFrameHandler3
  17:     0x7ffa34cf448f - _chkstk
  18:     0x7ffa34c6fd54 - RtlUnwindEx
  19:     0x7ffa0f2c0046 - _C_specific_handler
  20:     0x7ffa0f2b3245 - is_exception_typeof
  21:     0x7ffa0f2b3666 - is_exception_typeof
  22:     0x7ffa0f2b46ec - is_exception_typeof
  23:     0x7ffa0f2c04b1 - _CxxFrameHandler3
  24:     0x7ffa34cf440f - _chkstk
  25:     0x7ffa34c6e466 - RtlFindCharInUnicodeString
  26:     0x7ffa34ca4465 - RtlRaiseException
  27:     0x7ffa320453ac - RaiseException
  28:     0x7ff9a6dad3e8 - _umodti3
  29:     0x7ff9a6d7bc8e - _rust_start_panic
  30:     0x7ff9a6d65e79 - rust_panic
  31:     0x7ff9a6d65b7d - std::panicking::rust_panic_with_hook::h870983d929e74e12
  32:     0x7ff9a6d659e9 - <std::panicking::begin_panic_handler::StaticStrPayload as core::panic::PanicPayload>::take_box::h971268ed26284d4c
  33:     0x7ff9a6d62bc9 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h7851e041f2b8bcc2
  34:     0x7ff9a6d656b2 - rust_begin_unwind
  35:     0x7ff9a6dba447 - core::panicking::panic_fmt::ha5dd7a91f3010b68
  36:     0x7ff7779baa18 - rust_verify::verifier::Verifier::merge::h5466702f989e3b40
  37:     0x7ff7779c060e - rust_verify::verifier::Verifier::merge::h5466702f989e3b40
  38:     0x7ff7779c3b87 - rust_verify::verifier::Verifier::merge::h5466702f989e3b40
  39:     0x7ff7779e8f0c - rust_verify::verifier::Verifier::verify_bucket_outer::h88b3b101a5181ea6
  40:     0x7ff7779503d2 - <<&mut bincode::de::Deserializer<R,O> as serde::de::Deserializer>::deserialize_tuple::Access<R,O> as serde::de::SeqAccess>::next_element_seed::h5ba860ae8260c504
  41:     0x7ff777955934 - core::ops::function::impls::<impl core::ops::function::FnMut<A> for &mut F>::call_mut::hd401a0fac03e6a69
  42:     0x7ff9a6d77ebc - std::sys::windows::thread::Thread::new::h827e23232df84eef
  43:     0x7ffa333b257d - BaseThreadInitThunk
  44:     0x7ffa34caaa48 - RtlUserThreadStart

verus-lang / verus

Explicit trigger with `spec_fn` causes ill-typed AIR code #1110