Find impl witnesses in facets #5060

josh11b · 2025-03-03T19:56:42Z

Impl lookup for an interface I for a facet with facet type requiring an interface I will now succeed, getting the witness from the facet.

danakj · 2025-03-03T19:58:33Z

toolchain/check/impl_lookup.cpp

+    -> SemIR::InstId {
+  SemIR::InstId facet_inst_id =
+      context.constant_values().GetInstId(facet_const_id);
+  // FIXME: Should we convert from a FacetAccessType to its facet here?


Should this become a TODO, or are you intending to resolve it before landing?

Made a TODO. This PR is useful even without adding this change, so we can discover later if handling FacetAccessType is useful.

danakj · 2025-03-03T20:00:17Z

toolchain/check/impl_lookup.cpp

+  SemIR::InstId facet_inst_id =
+      context.constant_values().GetInstId(facet_const_id);
+  // FIXME: Should we convert from a FacetAccessType to its facet here?
+  SemIR::Inst facet_inst = context.insts().Get(facet_inst_id);


nit: i'd maybe consider calling .type_id() on this immediate and skip the facet_inst local variable

toolchain/check/impl_lookup.cpp

danakj · 2025-03-03T20:21:00Z

toolchain/check/impl_lookup.cpp

+      const auto& complete_facet_type =
+          context.complete_facet_types().Get(complete_facet_type_id);
+      for (auto interface : complete_facet_type.required_interfaces) {
+        if (interface == specific_interface) {


I suspect we should only do this if other_requirements is false for them both? Otherwise we would return an incorrect witness sometimes (which is noted by the TODO you've added at the end). I think it's a better incremental state to reject code incorrectly than to accept things that shouldn't typecheck and cause further errors later?

If there is an other_requirements we can also fall back to the constant values of the facet type and the query, if you'd like (which is ultimately type_const_id == interface_const_id in this case), as we're doing in #5047. Then where conditions that match can also return a correct witness, as long as there's only a single interface in both facet types. Otherwise it will (incorrectly) reject them, which is okay for now.

I don't think other_requirements are relevant here. As long as the interface id and specific id match, we can use the resulting witness. There is a question of whether that witness satisfies the requirements of the query facet type, but that is necessarily a distinct check and will happen in LookupImplWitness, not here. In general, we won't expect requirements to match -- for example, a witness for an interface may not have any other requirements, but still the values of the associated constants in that witness can satisfy the requirements.

Ah, it sounds like your vision for how to test other conditions is different than what I was expecting, which is fine.

Do you think we could add some tests in this PR for impl lookup on a facet type with where .. impls, where .. .X == Y and where .. .X = Y?

To clarify, we could have tests that should pass and that should fail (won't match) for each of these cases? I think we only have the should-pass for where .. impls at the moment.

What cases are you thinking about? I was having trouble finding a test that would cause RequireCompleteFacetType to fail.

Ok I think we're now on the same page and where clauses are not working as much as I thought. That said if you can write tests hitting the different features of where I think it would be helpful. I was not thinking about making RequireCompleteFacetType fail but rather cases where the comparison/matching of the impl with the query should either pass or fail while considering those different features of where: rewrite constraint, conditional constraint, or impls contraint.

This PR doesn't do anything about where constraints. I did add some tests to toolchain/check/testdata/builtin_conversions/no_prelude/convert_facet_value_to_narrowed_facet_type.carbon that cover some more cases. Note that one of them fails, but it appears to be due to code that wasn't from this PR:

// in impl_lookup.cpp, GetWitnessIdForImpl(): auto deduced_self_const_id = SemIR::GetConstantValueInSpecific( context.sem_ir(), specific_id, impl.self_id); if (type_const_id != deduced_self_const_id) {

Co-authored-by: Dana Jansens <danakj@orodu.net>

toolchain/check/impl_lookup.cpp

josh11b · 2025-03-04T01:38:14Z

~~I think #5054 will make the test diffs clearer, once it is submitted and merged into this branch.~~

toolchain/check/testdata/impl/lookup/no_prelude/impl_forall.carbon

danakj · 2025-03-04T14:04:33Z

toolchain/check/impl_lookup.cpp

+      const auto& complete_facet_type =
+          context.complete_facet_types().Get(complete_facet_type_id);
+      for (auto interface : complete_facet_type.required_interfaces) {
+        if (interface == specific_interface) {


To clarify, we could have tests that should pass and that should fail (won't match) for each of these cases? I think we only have the should-pass for where .. impls at the moment.

…g impl witnesses in facets (#5054) Here are some test changes so the diffs that come from my upcoming functionality changes are easier to see. Upcoming functionality includes: * Compound member access with non-instance associated constants will change to comply with the design https://docs.carbon-lang.dev/docs/design/expressions/member_access.html#impl-lookup-for-compound-member-access in #5059 . * Impl lookup will add support for finding impl witnesses in facets #5060 I'm also making the toolchain/check/testdata/impl/compound.carbon test into a no_prelude version, and adding a version that tests with importing. --------- Co-authored-by: Josh L <josh11b@users.noreply.github.com>

danakj · 2025-03-04T18:11:51Z

toolchain/check/impl_lookup.cpp

+    if (complete_facet_type_id.has_value()) {
+      const auto& complete_facet_type =
+          context.complete_facet_types().Get(complete_facet_type_id);
+      for (auto interface : complete_facet_type.required_interfaces) {


Just to note from our offline convo, if the query specific_interface has other_requirements then we don't want to match anything with it, so we return none. And if the facet type's interface has other_requirements then we want to skip trying to match it.

Agreed, I haven't made those changes yet. I might end up merging your PR first and then make those changes. since this involves stuff you are touching.

I've merged your changes and it should now handle other_requirements as we discussed.

…cet_type.carbon Now that BitAnd for tpes exists, we should get an error about type conversion, not about BitAnd not existing. Add `type.and` to the Core package in the test in order to improve the error message. This test will likely be made to pass by carbon-language#5060.

…cet_type.carbon Now that BitAnd for types exists, we should get an error about type conversion, not about BitAnd not existing. Add `type.and` to the Core package in the test in order to improve the error message. This test will likely be made to pass by carbon-language#5060.

…cet_type.carbon (#5077) Now that BitAnd for types exists, we should get an error about type conversion, not about BitAnd not existing. Add `type.and` to the Core package in the test in order to improve the error message. This test will likely be made to pass by #5060.

josh11b

I synced your changes and this PR is now more capable. I added some tests of this new capability, but one of them fails. That failure isn't due to this PR though, so I think this is ready for re-review.

josh11b · 2025-03-06T00:10:58Z

toolchain/check/impl_lookup.cpp

+    if (complete_facet_type_id.has_value()) {
+      const auto& complete_facet_type =
+          context.complete_facet_types().Get(complete_facet_type_id);
+      for (auto interface : complete_facet_type.required_interfaces) {


I've merged your changes and it should now handle other_requirements as we discussed.

josh11b · 2025-03-06T00:14:51Z

toolchain/check/impl_lookup.cpp

+      const auto& complete_facet_type =
+          context.complete_facet_types().Get(complete_facet_type_id);
+      for (auto interface : complete_facet_type.required_interfaces) {
+        if (interface == specific_interface) {


This PR doesn't do anything about where constraints. I did add some tests to toolchain/check/testdata/builtin_conversions/no_prelude/convert_facet_value_to_narrowed_facet_type.carbon that cover some more cases. Note that one of them fails, but it appears to be due to code that wasn't from this PR:

// in impl_lookup.cpp, GetWitnessIdForImpl(): auto deduced_self_const_id = SemIR::GetConstantValueInSpecific( context.sem_ir(), specific_id, impl.self_id); if (type_const_id != deduced_self_const_id) {

FindWitnessInFacet

5571836

josh11b requested a review from danakj March 3, 2025 19:56

github-actions bot added the toolchain label Mar 3, 2025

github-actions bot requested a review from dwblaikie March 3, 2025 19:56

josh11b mentioned this pull request Mar 3, 2025

Update tests for upcoming #5059 and #5060 on member access and finding impl witnesses in facets #5054

Merged

josh11b removed the request for review from dwblaikie March 3, 2025 20:00

josh11b mentioned this pull request Mar 3, 2025

Perform member lookup on FacetAccessType #5058

Merged

danakj reviewed Mar 3, 2025

View reviewed changes

josh11b and others added 2 commits March 3, 2025 14:08

Apply suggestions from code review

270cf96

Co-authored-by: Dana Jansens <danakj@orodu.net>

Fix formatting

5c5c819

CarbonInfraBot reviewed Mar 3, 2025

View reviewed changes

toolchain/check/impl_lookup.cpp Outdated Show resolved Hide resolved

toolchain/check/impl_lookup.cpp Outdated Show resolved Hide resolved

josh11b added 2 commits March 3, 2025 22:16

Implement suggestions

3e6ff2f

Remove unreachable diagnostic

717e5f5

josh11b added the dependent Depends on another issue/PR label Mar 4, 2025

danakj reviewed Mar 4, 2025

View reviewed changes

Remove redundant test

a9dac17

danakj reviewed Mar 4, 2025

View reviewed changes

Checkpoint progress.

0659c62

josh11b removed the dependent Depends on another issue/PR label Mar 4, 2025

danakj mentioned this pull request Mar 5, 2025

Fix the error message in fail_todo_convert_facet_value_to_narrowed_facet_type.carbon #5077

Merged

josh11b added 5 commits March 5, 2025 23:41

Merge remote-tracking branch 'upstream/trunk' into facetwitness

1a4dde9

Update test

1bd19b8

Test with more facet types

a4d0d3c

Test with more facet types

dd671dc

Test with more facet types

25d9541

Test currently fails

ca8fbb3

josh11b commented Mar 6, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Find impl witnesses in facets #5060

Find impl witnesses in facets #5060

josh11b commented Mar 3, 2025

danakj Mar 3, 2025

josh11b Mar 3, 2025

danakj Mar 3, 2025

josh11b Mar 3, 2025

danakj Mar 3, 2025

josh11b Mar 3, 2025

danakj Mar 4, 2025

danakj Mar 4, 2025

josh11b Mar 4, 2025

danakj Mar 4, 2025

josh11b Mar 6, 2025

josh11b commented Mar 4, 2025 •

edited

Loading

danakj Mar 4, 2025

danakj Mar 4, 2025

josh11b Mar 4, 2025

josh11b Mar 6, 2025

josh11b left a comment

josh11b Mar 6, 2025

josh11b Mar 6, 2025

Find impl witnesses in facets #5060

Are you sure you want to change the base?

Find impl witnesses in facets #5060

Conversation

josh11b commented Mar 3, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

josh11b commented Mar 4, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

josh11b left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

josh11b commented Mar 4, 2025 •

edited

Loading