Make FacetAccessType evaluate to SymbolicBindingType for type-of a BindSymbolicName #6115

danakj · 2025-09-22T22:20:38Z

The SymbolicBindingType refers to the type value that will be substituted in for the BindSymbolicName, but holds onto the EntityNameId from the BindSymbolicName instead of (or in addition to, for now) the instruction.

The EntityNameId will be used to look in the ScopeStack to find the witnesses either from the BindSymbolicName instruction, or other instructions that specify impls constraints against the EntityName.

This will allow us to have the T in I(T) resolve to a .Self reference in the type so that we get type equality with the binding's type: T:! I(.Self).

danakj · 2025-09-22T22:20:52Z

Based on #6113, first commit is symbolic-binding-type

toolchain/sem_ir/typed_insts.h

toolchain/check/type.cpp

toolchain/sem_ir/typed_insts.h

toolchain/check/eval.cpp

zygoloid · 2025-09-26T23:33:51Z

toolchain/check/eval.cpp

+    if (auto value =
+            eval_context.GetCompileTimeBindValue(bind_name.bind_index());
+        value.has_value()) {
+      auto value_inst_id = eval_context.constant_values().GetInstId(value);
+      if (auto facet =
+              eval_context.insts().TryGetAs<SemIR::FacetValue>(value_inst_id)) {
+        // If the symbolic binding is replaced by a FacetValue (type + witness),
+        // evaluate to its type component.
+        return eval_context.constant_values().Get(facet->type_inst_id);
+      }


May be worth at least noting in a comment that this is effectively forming and evaluating a FacetAccessType? Given the small amount of duplicated code here I guess it's probably not worth attempting to share the implementation.

Yeah that's a good point to add, done. I hadn't considered sharing code by constructing said FacetAccessType. But for now I have just made it clear it's doing that operation.

toolchain/check/eval_inst.cpp

toolchain/check/type.cpp

toolchain/check/type.h

toolchain/check/testdata/facet/convert_facet_type_to_facet_value.carbon

zygoloid · 2025-09-27T00:22:09Z

toolchain/check/testdata/facet/convert_facet_value_value_to_generic_facet_value_value.carbon

 impl Goat as Animal {}

 fn Feed[Food:! Edible, T:! Eats(Food)](e: T, food: Food) {}
+// CHECK:STDERR: convert_facet_value_value_to_generic_facet_value_value.carbon:[[@LINE+7]]:64: error: cannot convert type `T` that implements `Animal` into type implementing `Eats(Food)` [ConversionFailureFacetToFacet]


Is this diagnostic expected? (If so I guess we need to rename this to fail_todo_)

No, thanks for spotting it.

Interestingly, if I change Eats parameter from Food:! type to Food:! Edible the error goes away. But I still don't think the error is correct. The impls constrain the parameter given to Eats to be Edible, but they also should work when Eats only requires type.

Details here: https://discord.com/channels/655572317891461132/941071822756143115/1423429988748623934

The tl;dr is that in deduce we substitute deduced arguments from previous bindings into future bindings. If your future binding has something like U(T as type), so there's a SymbolicBindingType in its specific, then we try to substitute the deduced argument for T into it, which is a facet value. That can replace the BindSymbolicName along with its EntityNameId, which would then cause FacetAccessType to be rebuilt too, but it doesn't do anything to the EntityNameId in SymbolicBindingType, and we don't have a substitution for the as type part of that. So we have to do something like what eval is doing to SymbolicBindingType. But we can't modify a SymbolicBindingType in the same way, so we have to make a new FacetAccessType with the replacement that gets evaluated back into a SymbolicBindingType.

Just to confirm, this was fixed, right?

Yep, this is fixed by: https://github.com/carbon-language/carbon-lang/pull/6115/files#diff-e75f19a6bc525cf4282ee3697a2dc7722b2163694f69643dc1ba50ad1587b988R427-R446

danakj

uploading progress so far

danakj · 2025-09-29T21:01:59Z

toolchain/check/eval.cpp

+    if (auto value =
+            eval_context.GetCompileTimeBindValue(bind_name.bind_index());
+        value.has_value()) {
+      auto value_inst_id = eval_context.constant_values().GetInstId(value);
+      if (auto facet =
+              eval_context.insts().TryGetAs<SemIR::FacetValue>(value_inst_id)) {
+        // If the symbolic binding is replaced by a FacetValue (type + witness),
+        // evaluate to its type component.
+        return eval_context.constant_values().Get(facet->type_inst_id);
+      }


Yeah that's a good point to add, done. I hadn't considered sharing code by constructing said FacetAccessType. But for now I have just made it clear it's doing that operation.

toolchain/check/eval.cpp

toolchain/check/eval_inst.cpp

toolchain/check/import_ref.cpp

toolchain/sem_ir/typed_insts.h

toolchain/check/type.cpp

toolchain/check/type.h

toolchain/check/testdata/facet/convert_facet_type_to_facet_value.carbon

danakj · 2025-10-02T16:39:15Z

toolchain/check/testdata/facet/convert_facet_value_value_to_generic_facet_value_value.carbon

 impl Goat as Animal {}

 fn Feed[Food:! Edible, T:! Eats(Food)](e: T, food: Food) {}
+// CHECK:STDERR: convert_facet_value_value_to_generic_facet_value_value.carbon:[[@LINE+7]]:64: error: cannot convert type `T` that implements `Animal` into type implementing `Eats(Food)` [ConversionFailureFacetToFacet]


No, thanks for spotting it.

Interestingly, if I change Eats parameter from Food:! type to Food:! Edible the error goes away. But I still don't think the error is correct. The impls constrain the parameter given to Eats to be Edible, but they also should work when Eats only requires type.

danakj · 2025-10-02T17:46:44Z

(not ready for more review yet)

Previously it performed two kinds of operations, with a boolean parameter to control whether it would unwrap FacetValue or not. This made the function hard to explain as "canonicalization". Now the contract of GetCanonicalFacetOrTypeValue is as follows: 1. For a facet value expression, it returns the canonical value of the facet value. 2. For a `<facet value> as type` it returns the canonical value of the `<facet value>`. 3. For other type expressions, it returns the canonical value of the type. 1 and 2 together collapse together two representations of a facet value (as a FacetType or as a TypeType) into a single canonical value, which is important for constant comparison of facet values where the `as type` is not meant to change the result. This is the case in impl lookups and `.Self` comparisons. The step of unwrapping `FacetValue` is only useful in the constant evaluation of `LookupImplWitness` and is used to collapse *symbolic* queries on `FacetValue(T)` and on `T` down to a single canonical value, since they produce the same result later when `T` is replaced with a facet value or type that can provide a concrete witness. This is now extensively documented in the constant evaluation of `LookupImplWitness`. This change came out of a request/discussion in #6115 (see comment #6115 (comment)).

danakj · 2025-10-03T17:53:41Z

I addressed a bunch of the comments here in other PRs, so I have rebased this on top of them (most of which have already landed). The first commit is still symbolic-binding-type. It's now based on #6163.

danakj · 2025-10-03T17:54:41Z

I've marked this for review again by @zygoloid but @geoffromer would you mind to pick up the review from where he had left off?

geoffromer

First batch of comments; I'm still reviewing the testdata.

geoffromer · 2025-10-03T18:34:07Z

toolchain/check/import_ref.cpp

+// canonical EntityName (even if they are present there).
+//
+// No new work is generated by calling this function.
+static auto GetLocalEntityNameId(ImportContext& context,


It looks like this function is only used with the names of symbolic bindings, and the implementation seems to assume that as well (e.g. using AddSymbolicBindingName, and omitting the NameScopeId). Should the name and comment explicitly restrict it to those names?

Yeah, most places don't import EntityNameId at all. We only import them for symbolic bindings. Putting something in the name here won't hurt.

Though note that the NameScopeId is not part of the canonical EntityNameId (see the comment on the function). So the other fields are not imported because we import canonical values.

geoffromer · 2025-10-03T18:54:00Z

toolchain/check/testdata/facet/convert_facet_value_value_to_generic_facet_value_value.carbon

 impl Goat as Animal {}

 fn Feed[Food:! Edible, T:! Eats(Food)](e: T, food: Food) {}
+// CHECK:STDERR: convert_facet_value_value_to_generic_facet_value_value.carbon:[[@LINE+7]]:64: error: cannot convert type `T` that implements `Animal` into type implementing `Eats(Food)` [ConversionFailureFacetToFacet]


Just to confirm, this was fixed, right?

toolchain/check/testdata/facet/convert_facet_value_value_to_generic_facet_value_value.carbon

toolchain/check/testdata/impl/use_assoc_const.carbon

toolchain/check/import_ref.cpp

danakj

PTAL

toolchain/check/testdata/facet/convert_facet_value_value_to_generic_facet_value_value.carbon

toolchain/check/import_ref.cpp

toolchain/check/testdata/impl/use_assoc_const.carbon

github-actions bot requested a review from dwblaikie September 22, 2025 22:20

github-actions bot added the toolchain label Sep 22, 2025

danakj requested review from zygoloid and removed request for dwblaikie September 22, 2025 22:20

danakj force-pushed the symbolic-binding-type branch from c629cab to d1f58ab Compare September 22, 2025 22:25

danakj commented Sep 23, 2025

View reviewed changes

toolchain/sem_ir/typed_insts.h Show resolved Hide resolved

danakj force-pushed the symbolic-binding-type branch 2 times, most recently from 0d4947f to 80f3f92 Compare September 23, 2025 15:16

danakj commented Sep 23, 2025

View reviewed changes

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

zygoloid reviewed Sep 27, 2025

View reviewed changes

danakj mentioned this pull request Oct 2, 2025

Make the GetCanonicalFacetOrTypeValue operation more crisp #6157

Merged

danakj requested a review from a team as a code owner October 2, 2025 17:45

danakj requested review from josh11b and removed request for a team October 2, 2025 17:46

danakj commented Oct 2, 2025

View reviewed changes

danakj removed the request for review from josh11b October 2, 2025 17:46

danakj added 2 commits October 3, 2025 13:50

name-lookup-facettype

16d5c54

symbolic-binding-type

2d59767

danakj force-pushed the symbolic-binding-type branch from a132167 to 2d59767 Compare October 3, 2025 17:52

danakj requested review from a team, geoffromer and zygoloid and removed request for a team October 3, 2025 17:53

geoffromer reviewed Oct 3, 2025

View reviewed changes

symbolic-name

7bcd117

danakj requested a review from geoffromer October 3, 2025 19:31

geoffromer reviewed Oct 3, 2025

View reviewed changes

toolchain/check/testdata/facet/convert_facet_value_value_to_generic_facet_value_value.carbon Show resolved Hide resolved

toolchain/check/testdata/impl/use_assoc_const.carbon Outdated Show resolved Hide resolved

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

danakj added 2 commits October 6, 2025 10:28

review

cc46309

shortcut

33681ef

danakj commented Oct 6, 2025

View reviewed changes

toolchain/check/testdata/facet/convert_facet_value_value_to_generic_facet_value_value.carbon Show resolved Hide resolved

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

toolchain/check/testdata/impl/use_assoc_const.carbon Outdated Show resolved Hide resolved

danakj requested a review from geoffromer October 6, 2025 14:30

geoffromer approved these changes Oct 6, 2025

View reviewed changes

danakj added this pull request to the merge queue Oct 6, 2025

Merged via the queue into carbon-language:trunk with commit fe020ee Oct 6, 2025
8 checks passed

danakj deleted the symbolic-binding-type branch October 6, 2025 19:38

Make FacetAccessType evaluate to SymbolicBindingType for type-of a BindSymbolicName #6115

Make FacetAccessType evaluate to SymbolicBindingType for type-of a BindSymbolicName #6115

Uh oh!

Conversation

danakj commented Sep 22, 2025

Uh oh!

danakj commented Sep 22, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

danakj Oct 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

danakj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

danakj commented Oct 2, 2025

Uh oh!

danakj commented Oct 3, 2025

Uh oh!

danakj commented Oct 3, 2025

Uh oh!

geoffromer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

danakj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

danakj Oct 3, 2025 •

edited

Loading