further detail in example

proposals/p3833.md

@@ -115,6 +115,10 @@ result in sunk cost.
 
 ### Example: overloaded operators
 
+> Note: this example isn't trying to capture all the nuance of the current
+> design or suggest any change to the design. It is merely trying to provide an
+> illustration of how we might follow the proposal in practice.
+
 As an example to help illustrate this, how should the toolchain model overloaded
 operators? This proposal suggests that _initially_, the implementation should
 aim to fully model the rewrite-based dispatch through interfaces in the prelude.
@@ -123,9 +127,30 @@ be used to model the rewritten semantics of `x.(Core.AddWith(typeof(y)).Op)(y)`.
 This in turn would dispatch to an exact-type implementation which would provide
 any implicit conversions, and so-on.
 
-> Note: this example isn't trying to capture all the nuance of the current
-> design or suggest any change to the design. It is merely trying to provide an
-> illustration of how we might follow the proposal in practice.
+To be precise, the expectation is that the SemIR for `x + y` should as a
+consequence model all of:
+
+- Looking up the `Core.AddWith` interface.
+- Passing the type of `y` as a parameter to the interface (but likely using
+ that type directly rather than forming a literal `typeof(y)` kind of
+ expression, see below).
+- Looking up the `Op` method.
+- Calling that `Op` method on `x` with `y` as its parameter just as we would
+ model any call to `object.(Interface.Method)(y)`.
+
+However, specific things that would still be reasonable without deviating from
+the full semantic modeling here:
+
+- Not representing a user-written `typeof` style expression to compute the
+ type, or duplicating the `y` expression.
+- Caching and re-using SemIR for immutable things like successfully resolved
+ name lookup. Concretely, re-using a single cached lookup of `Core.AddWith`
+ would still provide the full model. And similarly, re-using an already
+ computed parameterization such as `Core.AddWith(i32)` repeatedly, and the
+ lookup of `Op` within that parameterization.
+
+The reason is that these don't change the semantics in any way -- they are
+constructively the same results.
 
 This should be the initial implementation _goal_, not a requirement for any
 incremental progress on implementation. Short-circuiting or other approximations