hax 0.3.6 crashes on RPITIT

[cfm]

hax 0.3.6 crashes on the "return-position implementation trait in trait" (RPITIT) pattern available since Rust 1.75, e.g.:

pub trait MyTrait {
    fn succeeds(&self) -> u32;
    fn crashes(&self) -> impl Iterator<Item = u32>;
}

Expected behavior

Successful extraction or a HAXNNNN error about an unsupported Rust feature.

Actual behavior

$ cargo hax into fstar
# ...
Explicit_def_id: an invariant has been broken. Expected last path chunk to exist and be of type TypeNs.

did={ Explicit_def_id.T.is_constructor = false;
  def_id =
  { Types.index = (0, 0, None); is_local = true; kind = Types.AssocTy;
    krate = "bug_anonassocty";
    parent =
    (Some { Types.contents =
            { Types.id = 0;
              value =
              { Types.index = (0, 0, None); is_local = true;
                kind = Types.Trait; krate = "bug_anonassocty";
                parent =
                (Some { Types.contents =
                        { Types.id = 0;
                          value =
                          { Types.index = (0, 0, None); is_local = true;
                            kind = Types.Mod; krate = "bug_anonassocty";
                            parent = None; path = [] }
                          }
                        });
                path =
                [{ Types.data = (Types.TypeNs "MyTrait"); disambiguator = 0 }
                  ]
                }
              }
            });
    path =
    [{ Types.data = (Types.TypeNs "MyTrait"); disambiguator = 0 };
      { Types.data = (Types.AnonAssocTy "crashes"); disambiguator = 0 }]
    }
  }
# ...

Seemingly from:

hax/engine/lib/concrete_ident/concrete_ident_view.ml

Lines 22 to 27 in 2aeac99

	let type_ns (did : Explicit_def_id.t) =
	match List.last (Explicit_def_id.to_def_id did).path with
	(* This can be `None` for the anonymous types generated for `-> impl Trait` in traits. *)
	| Some { data = TypeNs data; disambiguator } ->
	DisambiguatedString.{ data; disambiguator }
	| _ -> broken_invariant "last path chunk to exist and be of type TypeNs" did

[maximebuyse]

I opened #1966 with a fix for the crash, adding a proper rejection with error message. Let's keep this issue open for reference of the missing support for this feature.

[cfm]

Thanks for the prompt confirmation! We'll plan accordingly. :-)