[F* backend] Associated types are not extracted correctly in general

[W95Psp]

The F* backend (and probably others) is not handling "non-trivial" associated type, e.g.:

pub trait Foo {
    type FooType;
}
pub trait Bar {
    type BarType: Foo;
    fn f() -> <Self::BarType as Foo>::FooType;
}

The F* backend doesn't leverage all the information contained in the impl_exprs.

This is related to #536

[paulmure]

There is a similar issue with projections. Here's an important example:

fn foo<F>(f: F) -> i32
where
    F: Fn(u64) -> i32,
{
    f(42)
}

The Fn trait is implemented as an extension of FnMut, which is itself an extension of FnOnce, and only FnOnce stores the output type as an associated type.

In the example above, figuring out the return type of f would require looking at the projection clause from the list of bounds on generic parameters.

This information is exported by the frontend here but ignored by the importer in the backend.

I don't think any backend correctly translates the example above at the moment.

[W95Psp]

Hi @paulmure, thanks for your comment! That's true, the engine doesn't support at all equality constraints. That would be great to add support for that! Let me open a new issue. This one was more about the F* extraction which is broken for even less complicated things :sweat_smile:

[maximebuyse]

I had an issue that seems to be related. The equality constraints inside a trait type argument are not translated to f*: https://hax-playground.cryspen.com/#fstar/3b38e61b99/gist=cc40e5e2c6579d215293f9378b9e871f

[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.