From 9efa9f13466dc73ac9152ab44ffeeebd930030fb Mon Sep 17 00:00:00 2001
From: Oliver Schneider <github35764891676564198441@oli-obk.de>
Date: Fri, 6 Jul 2018 14:53:53 +0200
Subject: [PATCH] Explain existential types

---
 src/SUMMARY.md           |  1 +
 src/existential-types.md | 48 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+)
 create mode 100644 src/existential-types.md

diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index ca3b4c02..981da5c1 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -45,6 +45,7 @@
 - [Type checking](./type-checking.md)
     - [Method Lookup](./method-lookup.md)
     - [Variance](./variance.md)
+    - [Existential Types](./existential-types.md)
 - [The MIR (Mid-level IR)](./mir/index.md)
     - [MIR construction](./mir/construction.md)
     - [MIR visitor and traversal](./mir/visitor.md)
diff --git a/src/existential-types.md b/src/existential-types.md
new file mode 100644
index 00000000..4c5ebb75
--- /dev/null
+++ b/src/existential-types.md
@@ -0,0 +1,48 @@
+# Existential Types
+
+Existential types are essentially strong type aliases which only expose
+a specific set of traits as their interface and the concrete type in the
+background is inferred from a certain set of use sites of the existential
+type.
+
+In the language they are expressed via
+
+```rust
+existential type Foo: Bar;
+```
+
+This is in existential type named `Foo` which can be interacted with via
+the `Bar` trait's interface.
+
+Since there needs to be a concrete background type, you can currently
+express that type by using the existential type in a "defining use site".
+
+```rust
+struct Struct;
+impl Bar for Struct { /* stuff */ }
+fn foo() -> Foo {
+    Struct
+}
+```
+
+Any other "defining use site" needs to produce the exact same type.
+
+## Defining use site(s)
+
+Currently only the return value of a function inside can
+be a defining use site of an existential type (and only if the return
+type of that function contains the existential type).
+
+The defining use of an existential type can be any code *within* the parent
+of the existential type definition. This includes any siblings of the
+existential type and all children of the siblings.
+
+The initiative for *"not causing fatal brain damage to developers due to
+accidentally running infinite loops in their brain while trying to
+comprehend what the type system is doing"* has decided to disallow children
+of existential types to be defining use sites.
+
+### Associated existential types
+
+Associated existential types can be defined by any other associated item
+on the same trait `impl` or a child of these associated items.
\ No newline at end of file