hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
160 stars 17 forks source link

Panic: type parameter out of range when instantiating #747

Open Nadrieril opened 1 month ago

Nadrieril commented 1 month ago

Minimized reproduction:

pub trait Trait {}

impl<T, U> Trait for Result<T, U>
where
    for<'a> &'a Result<T, U>: IntoIterator,
    for<'a> <&'a Result<T, U> as IntoIterator>::Item: Copy,
{
}

panics with

thread 'rustc' panicked at /rustc/6b0f4b5ec3aa707ecaa78230722117324a4ce23c/compiler/rustc_type_ir/src/binder.rs:713:9:
type parameter `U/#1` (U/#1/1) out of range when instantiating, args=[&'^0.Named(DefId(0:8 ~ derive_visitor[edb9]::{impl#0}::'a#1), "'a") std::result::Result<T/#0, U/#1>]
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: could not compile `derive-visitor` (lib)

This does not panic with a similar Option impl, which suggests there's something weird happening with the generics. This also does not panic if I replace the HRTBs with simple Result<T, U>: IntoIterator bounds.

W95Psp commented 1 month ago

I suspect that's the same issue as https://github.com/hacspec/hax/issues/683