Panic: type parameter out of range when instantiating

[Nadrieril]

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,
{
}

Open this code snippet in the playground

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]

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

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[Nadrieril]

With https://github.com/hacspec/hax/pull/906, the error becomes:

warning[E9999]: Hax frontend found a projected type with escaping bound vars. Please report https://github.com/hacspec/hax/issues/495
  |
  = note: ⚠️  This is a bug in Hax's frontend.
          Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!

error: Unimplemented: Alias(Alias { kind: Opaque, args: [Type(Ref(Region { kind: ReBound(0, BoundRegion { var: 0, kind: BrAnon }) }, Adt { generic_args: [Type(Param(ParamTy { index: 0, name: "T" })), Type(Param(ParamTy { index: 1, name: "U" }))], trait_refs: [ImplExpr { trait: Binder { value: TraitRef { def_id: core::marker::Sized, generic_args: [Type(Param(ParamTy { index: 0, name: "T" }))] }, bound_vars: [] }, impl: LocalBound { predicate_id: PredicateId(2260340255824257914), index: 0, trait: Binder { value: TraitRef { def_id: core::marker::Sized, generic_args: [Type(Param(ParamTy { index: 0, name: "T" }))] }, bound_vars: [] }, path: [] }, args: [] }, ImplExpr { trait: Binder { value: TraitRef { def_id: core::marker::Sized, generic_args: [Type(Param(ParamTy { index: 1, name: "U" }))] }, bound_vars: [] }, impl: LocalBound { predicate_id: PredicateId(12095651497061745849), index: 1, trait: Binder { value: TraitRef { def_id: core::marker::Sized, generic_args: [Type(Param(ParamTy { index: 1, name: "U" }))] }, bound_vars: [] }, path: [] }, args: [] }], def_id: core::result::Result }, false))], def_id: core::iter::traits::collect::IntoIterator::Item })
  --> tests/ui/issue-372-type-param-out-of-range.rs:32:55
   |
32 |     for<'a> <&'a Result<T, U> as IntoIterator>::Item: Copy,
   |                                                       ^^^^

(with added context coming from Charon)