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

danakj · 2025-09-23T15:19:27Z

toolchain/check/type.cpp

+auto GetCanonicalizedFacetTypeOrType(Context& context, SemIR::InstId inst_id)
+    -> SemIR::TypeInstId {
+  inst_id = GetCanonicalizedFacetOrTypeValue(context, inst_id);
+  auto type_id = context.insts().Get(inst_id).type_id();
+  if (context.types().Is<SemIR::TypeType>(type_id)) {
+    return context.types().GetAsTypeInstId(inst_id);
+  } else {
+    CARBON_CHECK(context.types().Is<SemIR::FacetType>(type_id));
+    return context.types().GetInstId(type_id);
+  }
+}
+
+auto MoveToFacetValue(Context& context, SemIR::InstId inst_id)
+    -> SemIR::InstId {
+  auto type_id = context.insts().Get(inst_id).type_id();
+  if (context.types().Is<SemIR::SymbolicBindingType>(type_id)) {
+    return GetCanonicalizedFacetOrTypeValue(context,
+                                            context.types().GetInstId(type_id));
+  }
+  return inst_id;
+}
+
+auto MoveToFacetType(Context& context, SemIR::InstId inst_id) -> SemIR::InstId {
+  auto facet_value_id = GetCanonicalizedFacetOrTypeValue(context, inst_id);
+  auto type_id = context.insts().Get(facet_value_id).type_id();
+  if (context.types().Is<SemIR::FacetType>(type_id)) {
+    return context.types().GetInstId(type_id);
+  }
+  return facet_value_id;
 }


There are these three operations which all want to move to the type of a facet value but in slightly different ways or with slightly different inputs. I want to figure out a way to consolidate them though...

I have merged two of them, need to think more about how to shape things with the third still, but it's not fundamental to the PR.

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.

zygoloid · 2025-09-26T23:46:46Z

toolchain/check/eval_inst.cpp

+        // TODO: This is to be removed, at which point replace NewSamePhase with
+        // NewAnyPhase.


NewAnyPhase would deduce the phase from the operands, which would give Concrete, whereas we want this to always be symbolic. I think we'd need a little more machinery here, or maybe we can just keep using NewSamePhase?

zygoloid · 2025-09-27T00:00:43Z

toolchain/check/type.cpp

  }

  CARBON_CHECK(!context.insts().Is<SemIR::FacetAccessType>(inst_id));
-  CARBON_CHECK(!context.insts().Is<SemIR::FacetValue>(inst_id));
+  CARBON_CHECK(!context.insts().Is<SemIR::SymbolicBindingType>(inst_id));

  return context.constant_values().GetConstantInstId(inst_id);


I wonder: can this function be rephrased as first mapping to the constant inst id, and then doing some postprocessing steps if needed? (Eg, mapping from a facet value -> its type component, or mapping from a symbolic binding type -> its facet value, depending on whether we want a facet-flavored result or a type-flavored result.) I guess it's not entirely clear to me what the contract is here, but I'd have expected that two instructions with the same constant value ought to produce the same canonicalized facet or type value, and going to the constant value first would guarantee that is the case.

zygoloid · 2025-09-27T00:06:49Z

toolchain/check/type.cpp

+auto GetTypeForFacetOrTypeValue(Context& context, SemIR::InstId inst_id)
+    -> SemIR::TypeInstId {
+  if (inst_id == SemIR::ErrorInst::InstId) {
+    return SemIR::ErrorInst::TypeInstId;
+  }
+
+  inst_id = GetCanonicalizedFacetOrTypeValue(context, inst_id);
+  auto type_id = context.insts().Get(inst_id).type_id();
+  if (context.types().Is<SemIR::TypeType>(type_id)) {
+    return context.types().GetAsTypeInstId(inst_id);
+  } else {
+    CARBON_CHECK(context.types().Is<SemIR::FacetType>(type_id));
+    return context.types().GetInstId(type_id);
+  }
+}


I'm having trouble understanding what this function is doing. It looks like:

Given inst_id which is a facet value, perform some canonicalization step. Then:
If the type of inst_id is the type type, then return inst_id.
If the type of inst_id is a facet type other than type, then return the type of inst_id.

I find that behavior surprising -- that it sometimes returns the value of inst_id, and sometimes returns the type of inst_id. Is that the intent here?

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

toolchain/check/type.h

+// If `preserve_facet_value` is false, the `FacetValue` instruction is unwrapped
+// to get to an underlying canonical type instruction. Otherwise, the output is
+// either the original instruction or a facet value instruction.


Maybe I'm misunderstanding something, but it looks to me like this comment doesn't match the implementation. Specifically, I think if we're given a SymbolicBindingType, we'll always produce a facet value regardless of preserve_facet_value, and won't produce a canoncial type instruction (which would be the SymbolicBindingType).

zygoloid · 2025-09-27T00:20:53Z

toolchain/check/testdata/facet/convert_facet_type_to_facet_value.carbon

  Feed(Goat as (Animal & Climbs));

-  // CHECK:STDERR: fail_convert_multi_interface_facet_value_to_facet_value.carbon:[[@LINE+7]]:3: error: cannot convert type `Animal & Climbs` into type implementing `Eats` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR: fail_convert_multi_interface_facet_value_to_facet_value.carbon:[[@LINE+7]]:3: error: cannot convert type `Animal & Climbs` that implements `Animal & Climbs` into type implementing `Eats` [ConversionFailureFacetToFacet]


This diagnostic doesn't look right to me.

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_)

Co-authored-by: Richard Smith <[email protected]>

facetaccesstype-roundtrip

66a28e9

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 added 5 commits September 23, 2025 09:43

canonicalize-facet-value-of-binding

b127990

rephrase comment as shortcut again

f74e5da

rephrase

8bb4261

limit-semir

47813ad

convert-type

1a25bdc

danakj commented Sep 23, 2025

View reviewed changes

toolchain/sem_ir/typed_insts.h Show resolved Hide resolved

danakj added 2 commits September 23, 2025 11:11

symbolic-binding-type

c4c8032

move-to-facet-valuetype

d7e37c3

danakj force-pushed the symbolic-binding-type branch from d1f58ab to 0d4947f Compare September 23, 2025 15:14

comment

80f3f92

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

danakj commented Sep 23, 2025

View reviewed changes

combining-operations

0961607

zygoloid reviewed Sep 27, 2025

View reviewed changes

danakj and others added 2 commits September 29, 2025 16:51

wording

6e41730

Co-authored-by: Richard Smith <[email protected]>

wrapping

df76e20

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

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

Uh oh!

danakj commented Sep 22, 2025

Uh oh!

danakj commented Sep 22, 2025

Uh oh!

Uh oh!

danakj Sep 23, 2025

Uh oh!

danakj Sep 23, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zygoloid Sep 26, 2025

Uh oh!

zygoloid Sep 26, 2025

Uh oh!

zygoloid Sep 27, 2025

Uh oh!

zygoloid Sep 27, 2025

Uh oh!

zygoloid Sep 27, 2025

Uh oh!

zygoloid Sep 27, 2025

Uh oh!

zygoloid Sep 27, 2025

Uh oh!

Uh oh!

		// TODO: This is to be removed, at which point replace NewSamePhase with
		// NewAnyPhase.

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

Are you sure you want to change the base?

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

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!

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!

Choose a reason for hiding this comment

Uh oh!

Uh oh!