Merge frontend improvements

[Nadrieril]

These are the changes I made to the frontend for the purposes of Charon over the last few weeks. In rough order, the changes looks like:

• Add an explicit Self: Trait clause to trait methods and consts (replaces Add an explicit Self: Trait clause to trait assoc items #1541);
• Fix ImplExpr::Builtin that had some type errors (replaces Fix ImplExpr::Builtin #1543);
• Improve the translation of Drop information;
• Add variance information to type parameters (replaces Add variance information to generic parameters #1547);
• Cleanup the State infrastructure a little bit (this is opinionated, you might disagree);
• Add information about the metadata to use in unsize coercions;
• Resolve dyn Trait predicates;
• Many improvements to FullDef;
• Add infrastructure to get a monomorphized FullDef; this is used in charon to monomorphize a crate graph.

I fixed import_thir.ml but not all the engine tests pass. I'll leave that to you.

The branch consists of a merge of about 10 branches that each could have been a PR; you can review merge-commit-by-merge-commit if you want, the bullet points above would be roughly the PR titles.

[W95Psp]

Wow, thank you, that's a lot of work!
I will take some time to do some reviews tomorrow morning, not sure I'll be able to go through everything though ^^'

[W95Psp]

Looks great, thank you!
I've merged main and fixed a few regressions, but now I'm looking into more regressions on libcrux.
Will post an update whenever this is fixed.

[W95Psp]

I pushed another fix for the treatment of the new Self bounds in the engine.
Now, I expect some hashes to change in libcrux, but we currently have a regression.
So let's wait for that regression to be fixed, then we will merge this PR (after patching libcrux, probably).

[Nadrieril]

@W95Psp what's the status of this?

[W95Psp]

Looking at it again now, should be ok!
Sorry for the long waiting time :(

Running:

• https://github.com/cryspen/libcrux/actions/runs/17576567816
• https://github.com/cryspen/libcrux/actions/runs/17576572593

Those failed because of hashes, now I'm patching them.

---

I fixed libcrux hashes in frontend-upgrades-hash-fixes, now running the jobs again:

• https://github.com/cryspen/libcrux/actions/runs/17582184377
• https://github.com/cryspen/libcrux/actions/runs/17582173571

[W95Psp]

The CI from libcrux is green, let's see what hax' CI says.
(It will fail at ML-KEM, I'm running it for the other tests, will force merge after that)

[W95Psp]

I pushed cryspen/libcrux#1136, let's merge this one.