Updates to generics design details, part 2

docs/design/generics/details.md

@@ -2592,19 +2592,25 @@ this interface while `.Self` refers to the associated facet currently being
 defined.
 
 ```carbon
+interface Container;
+constraint SliceConstraint(E:! type, S:! Container);
+
 interface Container {
   let ElementType:! type;
   let IteratorType:! Iterator where .ElementType = ElementType;
 
-  let SliceType:! Container
-      where .ElementType = ElementType and
-            // `.Self` means `SliceType`.
-            .SliceType = .Self;
+  // `.Self` means `SliceType`.
+  let SliceType:! SliceConstraint(ElementType, .Self);
 
   // `Self` means the type implementing `Container`.
   fn GetSlice[addr self: Self*]
       (start: IteratorType, end: IteratorType) -> SliceType;
 }
+
+constraint SliceConstraint(E:! type, S:! Container) {
+  extend Container where .ElementType = E and
+                         .SliceType = S;
+}
 ```
 
 Note that [naming](#named-constraint-constants) a recursive constraint using the
@@ -2898,9 +2904,9 @@ interface Edge {
 }
 interface Node {
   let E:! EdgeFor(Self);
-  fn GetE[self: Self]() -> EdgeT;
-  fn AddE[addr self: Self*](e: EdgeT);
-  fn NearN[self: Self](n: N) -> bool;
+  fn GetE[self: Self]() -> E;
+  fn AddE[addr self: Self*](e: E);
+  fn NearN[self: Self](n: Self) -> bool;
 }
 
 constraint EdgeFor(NodeT:! Node) {
@@ -3022,8 +3028,8 @@ fn J[G: Graph](g: G) {
 ```
 
 the expression `G.E.N.E.N` is one equality away from `G.N.E.N` and so it is
-allowed. This is even though `G.N.E.N` isn't the type expression immediately
-prior to `G.E.N.E.N`.
+allowed. This is true even though `G.N.E.N` isn't the type expression
+immediately prior to `G.E.N.E.N`.
 
 After an `observe` declaration, all of the listed type expressions are
 considered equal to each other using a single `where` equality. In this example,
@@ -3148,6 +3154,11 @@ the above example, `Container` defines `ElementType` as having type `type`, but
 need to be a bit careful when talking about the type of `ContainerType` when
 there is a `where` clause modifying it.
 
+> **Future work:** We may want to use a different operator in this case, such as
+> `&=`, in place of `impls`, to reflect the change in the type. This is
+> analogous to rewrite constraints using `=` instead of `==` to visibly reflect
+> the different impact on the type.
+
 An implements constraint can be applied to [`.Self`](#recursive-constraints), as
 in `I where .Self impls C`. This has the same requirements as `I & C`, but that
 `where` clause does not affect the API. This means that a