Deduce through FacetValue should not consider witnesses

[danakj]

So I understand the failure in deduce from the symbolic witness PR. When we deduce on FacetValue it is now deduce_through, which makes it look at its args. There are two args:

• type_inst_id

This is the instruction "wrapped" by the FacetValue. It's often a FacetAccessType, in generic code. And it's a concrete type implementing the required interfaces in non-generic code.

The deduce look-through is about this instruction.

For example here:

class DD(E:! type) {}
impl forall [E:! type] DD(E) as Z {}

class CC(D:! Z) {}
impl forall [E:! type] CC(DD(E)) as Z {}

In the second impl decl, we get a deduction parameter of:

• ClassType "CC"
  • Specific: FacetValue
    • ClassType "DD"
      • Specific: BindSymbolicName "E"

Which is itself symbolic due to the BindSymbolicName.

And we have an argument of:

• ClassType "CC"
  • Specific: FacetValue
    • ClassType "DD"
      • Specific: ClassType "EE"

These FacetValues are not the same constant value, since they differ in the specific of the nested DD class. So we deduce-through and compare the instructions inside, which are ClassType. The parameter's type is not symbolic so we compare the values as-is. They also don't have the same constant value so we deduce-through them, which makes use deduce on the values in the specific when AddInstArg() is called on the ClassType::arg1 values: BindSymbolicName, and ClassType "EE".

Here the parameter type is now the BindSymbolicName from the generic bindings. The argument ClassType "EE" has the same type type as the parameter, so it is stored as the deduced argument value for it.

• witnesses_block_id

This is the found witnesses for the FacetValue. When we deduce through the FacetValue we now also compare these for equality.

Before specialization and symbolic witnesses, we were counting on these witnesses to always be the same constant values for compatible FacetValues.

Specialization and Symbolic witnesses break deduction

When impl lookup finds a symbolic witness, which is placed in the InstBlock of the FacetValue, the above deduction process breaks. Before we compare the type_inst_id, we first compare the witnesses, since AddInstArg() on the FacetValue::witnesses_block_id will add them all (from both param and arg) to the deduction. Now we get two different kinds of witnesses, with different constant values.

(gdb) call Dump(context(), param_id)
inst74: {kind: ImplSymbolicWitness, arg0: inst41, arg1: specific_interface0, type: type(inst(WitnessSymbolicType))}
  - type type(inst(WitnessSymbolicType)): <symbolic witness>; {kind: WitnessSymbolicType, type: type(TypeType)}
  - value symbolic_constant16
  - LocId(<none>)
(gdb) call Dump(context(), arg_id)
inst99: {kind: ImplWitness, arg0: inst_block_empty, arg1: specific11, type: type(inst(WitnessType))}
  - type type(inst(WitnessType)): <witness>; {kind: WitnessType, type: type(TypeType)}
  - value concrete_constant(inst99)
  - LocId(<none>)

The parameter's type is the concrete WitnessSymbolicType, so their values are compared for deduction. ImplWitness has a different type, WitnessType so we try to convert them for which there is no conversion defined. This results in an ErrorInst from conversion and we abort deduction since the arguments can't be substituted into the parameters.

What do?

I posit that it was never correct to compare the witnesses of a FacetValue. That deduce should deduce-through the FacetValue to the type_inst_id only.

Why is this correct? The exact value of the witnesses do not matter for deduction. All witnesses share the fact that they prove an impl declaration does exist for the query. Symbolic witnesses for a given query are all the same. A concrete witness only adds more information to the symbolic one, so it's always safe to use a concrete witness in the place of a symbolic one. Meaning it's fine to use the argument FacetValue when the parameter is a FacetValue in all cases:

• The parameter has a concrete witness - the argument will be the same, since it has strictly more information available to it. The only case it can be different is when we change the result of a concrete impl lookup result, but this (in the future) results in poisoning the query and a diagnostic.
• The parameter has a symbolic witness - if the argument is symbolic they are the same.
• The parameter has a symbolic witness - if the argument is concrete it provides more information.

What about converting?

We should thus allow argument FacetValue (of any witnesses) to convert to parameter FacetValue (of any witnesses). Convert itself has no problem with this as long as deduce asks for it.

We don't want to convert ImplWitness to ImplSymbolicWitness in deduction. The types are different and converting a concrete witness to a symbolic one loses information. Whereas converting the FacetValue containing a concrete witness to a FacetValue containing a symbolic witness will retain the concrete witnesses after conversion, since it is the FacetValue's type that is changing not the witnesses'.

Deduce through FacetValue (sort-of)

There's a couple ways to approach deducing through FacetValue for its type_inst_id but not its witnesses:

1. Change deduce_through in typed_inst.h from a bool to an enum:

enum DeduceThrough {
  NoArgs,
  Arg1Only
  Arg2Only,
  AllArgs
};

2. Hardcode FacetValue behaviour into the deduce_through() branch in deduce.cpp:

if (arg_inst.kind() != SemIR::InstKind::FacetValue) {
  worklist_.AddInstArg(kind1, param_inst.arg1(), arg_inst.arg1(),
                       needs_substitution);
}

3. Skip instructions with type_id() of WitnessType and WitnessSymbolicType (or instructions that are ImplWitness and ImplSymbolicWitness) in the deduce loop, or when adding insts to the worklist.
4. Disable deduce_through for FacetValue and handle it explicitly in the deduce for loop, comparing that the argument is also a FacetValue and then adding both type_inst_ids.

[danakj]

I am going to throw up a PR that does the 2nd one for now, but open to any of these or other ideas - or let me know if I am wrong in here somewhere.

[danakj]

Added a fourth possible option, which hardcodes FacetValue differently - avoiding deduce_through() for it.

[danakj]

Here's the full example/test:

interface Z {}

class EE {}
impl EE as Z {}

class DD(E:! type) {}
impl forall [E:! type] DD(E) as Z {}

class CC(D:! Z) {}
impl forall [E:! type] CC(DD(E)) as Z {}

fn F() {
  CC(DD(EE)) as Z;
}

[zygoloid]

From open discussion 2025-03-25: we like option 4.

[danakj]

We talked more and determined that the type of ImplSymbolicWitness should actually be WitnessType, the same type as ImplWitness. I thought originally they should not be as they are different builtin instructions, but @zygoloid pointed out that since the former will be changed to the latter as the constant value in some generic instructions, the process of changing the value should not change the type of the constant value.

Once that change is done, deduce is fine with the different instructions since they have the same types, so no change is needed to accomodate things here.

[danakj]

This will be done as part of #5169, then, by simply sharing the type. No particular work item for this issue, so I will close it.