fix(engine/lib): import associated item projection on generic bounds

[paulmure]

Partially address #549.

The importer in the engine now imports projections defined in hax_frontend_exporter::types::copied::ClauseKind.

This is done by adding a variant to the Ast.Rust.generic_constraint enum to include projections, which necessitates changing the interface of import_clause in engine/lib/import_thir.mli to return Ast.Rust.generic_constraint instead of Ast.Rust.impl_ident.

As a result, all functions that previously expect an Ast.Rust.impl_ident from c_clause_kind now do some additional filtering.

Remaining issues:

• Each backend still need to add their own support to process associated item projections. For now, I just added a call to Error.unimplemented with reference to Associated types are not extracted correctly in general #549.
• Printing generic constraints still need to be polished as part of more principled generic printer #533.

[paulmure]

@W95Psp, the fstar backend currently fails the traits test as I do not know how this additional feature should be dealt with there. Please let me know if you have any ideas on how to push this forward.

[W95Psp]

Hi! Thanks for your PR!

It looks good to me, I can add the missing bits for the F* backend, or we can just filter that out for now (I'm not entirely sure about what is the best encoding in F*). Do you want to take care of the filtering in the F* and Coq backends?

For now, let's not feature-gate this new variant, let's see if that makes sense at some point for some backends.

(What's up with the git history though? 👀)

[paulmure]

Hi! Thanks for your PR!

It looks good to me, I can add the missing bits for the F* backend, or we can just filter that out for now (I'm not entirely sure about what is the best encoding in F*). Do you want to take care of the filtering in the F* and Coq backends?

For now, let's not feature-gate this new variant, let's see if that makes sense at some point for some backends.

(What's up with the git history though? 👀)

The coq backend is surprisingly unaffected by this change. The ssprove backend is though, so I just called Error.unimplemented there.

For the F* backend, I filtered GCProjections out with a TODO comment linking to #785.

The git history was probably because I accidentally merged some changes in main...

[W95Psp]

Great, thanks!
Ok, that will be a merge commit anyway, let's merge as is!