Issue with fold_right and polymorphism

[amarshah1]

Running this code:

    pub closed spec fn pred<T> (seq1 : Seq<T>, seq2 : Seq<T>) -> bool
        where T: std::marker::Copy + Integer,
    {
        seq1.fold_right(|x, acc : nat| acc + (x as nat), 0) == seq2.fold_right(|x, acc : nat| acc + (x as nat), 0)
    }

    proof fn test (seq1 : Seq<u8>, seq2 : Seq<u8>)
        requires pred(seq1, seq2)
        ensures 
            seq1.fold_right(|x, acc : nat| acc + (x as nat), 0) == seq2.fold_right(|x, acc : nat| acc + (x as nat), 0)
    {}

Results in the verification failing:

error: postcondition not satisfied
  --> minimum_issue.rs:17:5
   |
16 |             seq1.fold_right(|x, acc : nat| acc + (x as nat), 0) == seq2.fold_right(|x, acc : nat| acc + (x as nat), 0)
   |             ---------------------------------------------------------------------------------------------------------- failed this postcondition
17 |     {}
   |     ^^ at the end of the function body

error: aborting due to 1 previous error

verification results:: 0 verified, 1 errors

We think this is an issue with the relationship between fold_right and polymorphism. It verifies if we get rid of the polymorphism. It also verifies if we just replace the body with seq1.fold_right(|x, acc : nat| acc + acc, 0) == seq2.fold_right(|x, acc : nat| acc + acc, 0)

See attached zip file. Thanks!
2024-09-27-16-09-22.zip