Documenting expected behaviour of intersection types

docs/types/intersection-types.md

@@ -209,6 +209,49 @@ In short: when a [conversion](../syntax/conversions.md) is needed to satisfy a
 type check a new value is created to satisfy just the types requested in the
 check.
 
+## Preserving identity of refined types
+
+Intersection types are often used to refine a value with additional
+functionality. For example, a value `table : Table & DB_Table` represents a
+table coming from a database that has both the base `Table` methods that all
+tables share but also database-specific methods from `DB_Table`. Either part of
+this compound type may get _hidden_ when passing around various methods (e.g.
+`table:Table` will hide the `DB_Table` part), but the value itself still retains
+its identity as a `Table & DB_Table` and can be uncovered via a cast or a case
+expression during runtime.
+
+To ensure intersection types properly propagate thru the Enso program the 
+basic language constructs are designed to handle them properly. Namely:
+
+- casting `x : A` will hide the `B` part, so the actual type is
+  `x : A & (hidden B)`.
+- inspecting the type via `case of`, e.g.
+  ```
+  case x of
+      a : A -> ...
+      _ -> ...
+  ```
+  in the first branch, the `a` has visible type `A` but the full type is still
+  `a : A & ~B` - the `B` part is hidden, but not removed.
+- dispatching a method on one of the types, e.g. calling `x.method_defined_on_A`
+  will pass the value `x` as `self` to the body of `method_defined_on_A`, the
+  `self` will have a visible type `A`, but the full type is still
+  `self : A & ~B` - so the `self` value can be cast if needed.
+- normally, calling conversions will 'start over' and the value returned from
+  one will not have an intersection type anymore. However, as long as possible,
+  even conversions should try to use existing (even if hidden) parts of the type
+  instead of calling into the conversion code; thus:
+  - calling `A.from x` will return a value of type `A & ~B` - the `B`
+    part is still there (only hidden), because no actual conversion code had to
+    be run - the type was simply extracted from the intersection type.
+  - similarly, calling `B.from x` will return a value of type `B & ~A` -
+    the `A` part is still there (only hidden), because no actual conversion code
+    had to be run.
+It is important to ensure these operations do not remove a part of the intersection type.
+Otherwise the value loses part of its functionality which would have a detrimental effect
+in the GUI, confusing users. 
+If the `DB_Table` part is not kept as hidden, but completely removed, the
+table can no longer be casted to `DB_Table` and used as such.
 ## Signature vs. Cast
 
 There are two slightly different places where _type checking_ occurs:
@@ -299,3 +342,10 @@ _has been cast to_. As a special case any value wrapped into an _intersection
 type_, but _cast down_ to the original type is `==` and has the same `hash` as
 the original value. E.g. `4.2 : Complex&Float : Float` is `==` and has the same
 `hash` as `4.2` (in spite it _can be cast to_ `Complex`).
+
+### TODO
+
+- self preserves intersection types, just hides them
+- case of also
+- T.from should preserve if no conversion was made (e.g. T was among visible or
+  hidden types)