Hi, thanks for your PR! Sorry for the delay, the week is quite busy... will try to look into those tests tomorrow!

Ok, I'm in a rush and so I rushed the review as well... I wanted to merge too fast, and actually I think there is a problem with the PR. Let me comment on the issue.

@W95Psp
As discussed in the issue, I'm trying to import the trait goal alongside the information stored in ImplExprAtom.

However, this seems to break the uses of ppx_inline in many of the modules in lib/phases. I guess it's caused by incorrect inlining of the code in subtype.ml. And I'm not sure how to fix this.

Any suggestions would be greatly appreciated!

@W95Psp As discussed in the issue, I'm trying to import the trait goal alongside the information stored in ImplExprAtom.

However, this seems to break the uses of ppx_inline in many of the modules in lib/phases. I guess it's caused by incorrect inlining of the code in subtype.ml. And I'm not sure how to fix this.

Any suggestions would be greatly appreciated!

Forget what I said here, I think I just needed to run dune clean before building.

After some back and forth, I decided to only import the trait goal for the concrete case for now. This avoids storing redundant copies of this trait goal since we are not using the ImplExprAtom pattern as in the exporter.

I'm not sure if it's actually needed for the other cases. If such a need arises in the future, we can reconsider how to import this information again.

All tests pass now. The only change is that the traits test for f* added a line of implicit dependency.

Hi @paulmure, I'm reviewing this PR this morning, and I think I did something similar recently... #827
Sorry for the duplicate work... (the last month has been pretty work intensive toward a verification project...)

Wdyt, shall we close this one or is it still needed?

That looks like the information we need. Thank you!