Which contexts support implied constraints?

[zygoloid]

Summary of issue:

Currently, the only place the design says we support implied constraints is in generic function signatures:

interface Hashable { ... }
class HashSet(T:! Hashable);

// `F` has an implied constraint: `T impls Hashable`
fn F[T:! type](x: HashSet(T));

But there are other places where allowing implied constraints would make sense and would improve expressivity and/or reduce redundancy. Do we want implied constraints to be limited to function signatures or to be more general?

Details:

For any kind of parameterized entity, implied constraints could make sense as constraints on the parameters:

// Should each of these be invalid, or should they have an implied constraint
// of `T impls Hashable`?
class C(T:! type, U:! ImplicitAs(HashSet(T)));
interface I(T:! type, U:! ImplicitAs(HashSet(T)));

For a parameterized impl, implied constraints could make sense, as constraints on the deduced parameters:

// Invalid, or implied constraint?
impl forall [T:! type] T as ImplicitAs(HashSet(T));

Within an interface definition, implied constraints could make sense as require clause constraining implementations:

interface X {
  let T:! type;
  // invalid, or implies `require T as Hashable`?
  let U:! ImplicitAs(HashSet(T));
}

Any other information that you want to share?

This review comment shows a case where we may gain some expressivity if we use implied constraints within an interface:

interface Container;
constraint SliceConstraint(E:! type, S:! Container);
interface Container {
  let ElementType:! type;
  // For this to type-check, need to know that `.Self impls Container`.
  // We could imply that constraint, or we could require the developer
  // to write `Container where .Self impls SliceConstraint(ElementType, .Self)`
  // ... but that doesn't give `SliceType` the right API.
  let SliceType:! SliceConstraint(ElementType, .Self);
}

[josh11b]

Within an interface definition, implied constraints could make sense as require clause constraining implementations:

interface X {
  let T:! type;
  // invalid, or implies `require T as Hashable`?
  let U:! ImplicitAs(HashSet(T));
}

I don't think we want this. require T as Hashable; is not a valid declaration in an interface since it doesn't involve Self itself. The previous guidance, which I think had a solid reason behind it, was that implied constraints were local to a single declaration. A good counter-argument would be that implied constraints solve this expressivity problem, which leads to the question: do we only need extra constraints in the cases where implied constraints would solve the problem (and other cases where we need extra constraints are fully handled by forward-declaring a named constraint), or is there a broader expressivity gap? I'm in particular worried about cases where we want to access members of an associated facet.

[zygoloid]

require T as Hashable; is not a valid declaration in an interface since it doesn't involve Self itself.

It'd be equivalent to require Self.T impls Hashable;, which does involve Self. Is that sufficient?

[josh11b]

require T as Hashable; is not a valid declaration in an interface since it doesn't involve Self itself.

It'd be equivalent to require Self.T impls Hashable;, which does involve Self. Is that sufficient?

Here is the relevant section: https://github.com/carbon-language/carbon-lang/blob/trunk/docs/design/generics/details.md#interface-requiring-other-interfaces-revisited . That section doesn't seem to have examples using associated facets directly. It definitely seems possible to support require T as..., unlike the coherence problems it is specifically trying to exclude, but it gets at the question of "when is a type finished being modified" and "where does the compiler have to look for facts about a type." I guess this might fall into the category of acceptable places to learn a fact as long as it doesn't affect the API of the type.

I should probably add a clarification to the document about whether associated facets count as Self, whichever way we decide.