[SIL.rst] Add docs explaining how Move Only Types can be copied in Raw SIL, but not in later SIL stages.

Since I am going to start enforcing this invariant more broadly, I want to
document it in SIL.rst. I also included a discussion explaining why we maintain
this invariant: it enables SILGen to use a simple algorithm to insert copies/us
to clean that up using a diagnostic guaranteed optimization pass which runs on
Raw SIL.

Author: gottesmm

docs/SIL.rst

@@ -2762,6 +2762,32 @@ sil-opt, one will see that we actually have an ownership violation due to the
 two uses of "value", one for initializing value2 and the other for the return
 value.
 
+Move Only Types
+---------------
+
+NOTE: This is experimental and is just an attempt to describe where the design
+is currently for others reading SIL today. It should not be interpreted as
+final.
+
+Currently there are two kinds of "move only types" in SIL: pure move only types
+that are always move only and move only wrapped types that are move only
+versions of copyable types. The invariant that values of Move Only type obey is
+that they can only be copied (e.x.: operand to a `copy_value`_, ``copy_addr [init]``) during the
+guaranteed passes when we are in Raw SIL. Once we are in non-Raw SIL though
+(i.e. Canonical and later SIL stages), a program is ill formed if one copies a
+move only type.
+
+The reason why we have this special rule for move only types is that this allows
+for SIL code generators to insert copies and then have a later guaranteed
+checker optimization pass recover the underlying move only semantics by
+reconstructing needed copies and removing unneeded copies using Ownership
+SSA. If any such copies are actually needed according to Ownership SSA, the
+checker pass emits a diagnostic stating that move semantics have been
+violated. If such a diagnostic is emitted then the checker pass transforms all
+copies on move only types to their explicit copy forms to ensure that once we
+leave the diagnostic passes and enter canonical SIL, our "copy" invariant is
+maintained.
+
 Runtime Failure
 ---------------