Frontend: panic on default traits bounds

[W95Psp]

The following piece of code:

trait Foo: Bar {
    type U;
}
trait Bar<T = <Self as Foo>::U> {}

Yields a panic in the frontend.

[W95Psp]

This is still the case, with:

error[E9999]: Cannot handle error `Unimplemented` selecting `Binder { value: <Self as Foo>, bound_vars: [] }`
 --> literals/src/lib.rs:4:1
  |
4 | trait Bar<T = <Self as Foo>::U> {}
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |
  = 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)!

[W95Psp]

This was silenced as a warning by PR #898, but this is still an issue.

[Nadrieril]

Rustc always gives us the right parameters when referring to a trait, right? Can we ignore the default parameters entirely?

[W95Psp]

Ah, that's true, you're right, we don't do anything with this information, and rust always inline parameters at use site.

So dropping default parameters would be an easy fix! I guess I can push a PR that disables that with a comment: in an ideal world I'd like that info to be exported since we "have" it, but we don't have unlimited time :sweat_smile: