[doc] Tweak recent Lexicon additions based on feedback.

Author: jrose-apple

docs/Lexicon.rst

@@ -20,7 +20,9 @@ source code, tests, and commit messages. See also the `LLVM lexicon`_.
 
   archetype
     A placeholder for a generic parameter or an associated type within a
-    generic context.
+    generic context. Sometimes known as a "rigid type variable" in formal
+    CS literature. Directly stores its conforming protocols and nested 
+    archetypes, if any.
 
   canonical SIL
     SIL after the
@@ -38,9 +40,12 @@ source code, tests, and commit messages. See also the `LLVM lexicon`_.
     the AST level. See also `witness table`.
 
   contextual type
-    The type of a value or declaration from inside a generic context. This type
-    may contain `archetypes <archetype>` and cannot be used directly from
-    outside the context. Compare with `interface type`.
+    1. The expected type for a Swift sub-expression based on the rest of the 
+       statement. For example, in the statement ``print(6 * 9)``, the contextual
+       type of the expression ``6 * 9`` is ``Any``.
+    2. The type of a value or declaration from inside a potentially generic
+       context. This type may contain `archetypes <archetype>` and cannot be 
+       used directly from outside the context. Compare with `interface type`.
 
   DI (definite initialization / definitive initialization)
     The feature that no uninitialized variables, constants, or properties will
@@ -58,12 +63,18 @@ source code, tests, and commit messages. See also the `LLVM lexicon`_.
     compatibility. See :doc:`LibraryEvolution.rst <LibraryEvolution>`.
 
   iff
-    "if and only if". This term comes from mathematics.
+    "`if and only if`__". This term comes from mathematics.
+    
+    __ https://en.wikipedia.org/wiki/If_and_only_if
 
   interface type
     The type of a value or declaration outside its generic context. These types
-    can be compared across declarations but cannot be used directly from within
-    the context. Compare with `contextual type`.
+    are written using "formal" generic types, which only have meaning when
+    combined with a particular generic declaration's "generic signature".
+    Unlike `contextual types <contextual type>`, interface types store
+    conformances and requirements in the generic signature and not in the types
+    themselves. They can be compared across declarations but cannot be used
+    directly from within the context.
 
   IUO (implicitly unwrapped optional)
     A type like Optional, but it implicitly converts to its wrapped type. If