docs: add a section about formal vs lowered types in the SIL documentation

docs/SIL/SIL.md

@@ -108,6 +108,56 @@ largely according to Swift's type grammar.
 sil-type ::= '$' '*'? generic-parameter-list? type
 ```
 
+## Formal vs. Lowered Types
+
+A formal type corresponds to a Swift type as it is defined in the source code.
+The AST and the type checker work with formal types. Formal types can be
+canonicalized which resolves type aliases and removes sugar. Later stages of
+the compiler, like the SIL optimizer, only deal with canonical formal types.
+Therefore, if we speak about formal types in the following sections, we always
+refer to _canonical_ formal types.
+
+Each formal type has a corresponding lowered type. However, most lowered types
+are identical to their original formal type, for example all nominal types,
+like classes, structs or enums (except `Optional`). Only a few kind of types
+are lowered to a different lowered type. The most prominent example is function
+types: a lowered function type adds information about the calling convention and 
+it lowers tuple arguments to individual arguments.
+
+For example, the formal type of
+
+```
+  func foo(a: (Int, String), b: any P) { }
+```
+
+is `((Int, String), any P) -> ()` whereas its lowered type is
+`(Int, @guaranteed String, @in_guaranteed any P) -> ()`.
+
+Deriving a lowered type from a formal type is called _type lowering_ which is
+described in detail in the [Types](Types.md#Type-Lowering) document.
+
+SIL types are always lowered types. The soundness of the SIL type system
+depends on lowered types and the SIL optimizer needs lowered types to perform
+correct optimizations.
+
+However, there are a few places where SIL needs to refer to formal types. These
+are operations on types which are "user visible", for example cast
+instructions.
+
+For example, a cast from `((Int, Bool)) -> ()` to `(Int, Bool) -> ()` fails
+because the two formal function types differ. If a SIL cast instruction would
+operate on SIL types, the cast would incorrectly succeed because the formal
+types of those functions types are equivalent.
+
+To summarize:
+
+|                    | Definition                                   | Example                             |
+| ------------------ | -------------------------------------------- | ----------------------------------- |
+| **Formal type**    | original type from the source code           | `typealias C = ((Int, Bool)) -> ()` |
+| **Canonical type** | formal type minus sugar, aliases resolved    | `((Int, Bool)) -> ()`               |
+| **SIL type**       | lowered canonical type, plus is-address flag | `$*(Int, Bool) -> ()`               |
+
+
 ## Loadable vs. Address-only Types
 
 Most SIL types are _loadable_. That means that a value of such a type can be