diff --git a/docs/docs/reference/changed/implicit-resolution.md b/docs/docs/reference/changed/implicit-resolution.md
index 8fa6eca24709..a30e166e15e6 100644
--- a/docs/docs/reference/changed/implicit-resolution.md
+++ b/docs/docs/reference/changed/implicit-resolution.md
@@ -29,7 +29,7 @@ affect implicits on the language level.
         /*!*/ def f(implicit x: y.type) // error `y.type` not allowed as type of implicit
 
  3. Nesting is now taken into account for selecting an implicit.
-    Consider for instance the following scenario
+    Consider for instance the following scenario:
 
         def f(implicit i: C) = {
           def g(implicit j: C) = {
@@ -41,4 +41,40 @@ affect implicits on the language level.
     more deeply than `i`. Previously, this would have resulted in an
     ambiguity error.
 
+ 4. The treatment of ambiguity errors has changed. If an ambiguity is encountered
+    in some recursive step of an implicit search, the ambiguity is propagated to the caller.
+    Example: Say you have the following definitions:
+
+        class A
+        class B extends C
+        class C
+        implicit def a1: A
+        implicit def a2: A
+        implicit def b(implicit a: A): B
+        implicit def c: C
+
+    and the query `implicitly[C]`.
+
+    This query would now be classified as ambiguous. This makes sense, after all
+    there are two possible solutions, `b(a1)` and `b(a2)`, neither of which is better
+    than the other and both of which are better than the third solution, `c`.
+    By contrast, Scala 2 would have rejected the search for `A` as
+    ambiguous, and subsequently have classified the query `b(implicitly[A])` as a normal fail,
+    which means that the alternative `c` would be chosen as solution!
+
+    Scala 2's somewhat puzzling behavior with respect to ambiguity has been exploited to implement
+    the analogue of a "negated" search in implicit resolution, where a query `Q1` fails if some
+    other query `Q2` succeeds and `Q1` succeeds if `Q2` fails. With the new cleaned up behavior
+    these techniques no longer work. But there is now a new special type `scala.implicits.Not`
+    which implements negation directly. For any query type `Q`: `Not[Q]` succeeds if and only if
+    the implicit search for `Q` fails.
+
+ 5. The treatment of divergence errors has also changed. A divergent implicit is
+    treated as a normal failure, after which alternatives are still tried. This also makes
+    sense: Encountering a divergent implicit means that we assume that no finite
+    solution can be found on the given path, but another path can still be tried. By contrast
+    most (but not all) divergence errors in Scala 2 would terminate the implicit
+    search as a whole.
+
+
 [//]: # todo: expand with precise rules
diff --git a/docs/docs/reference/dependent-function-types.md b/docs/docs/reference/dependent-function-types.md
new file mode 100644
index 000000000000..e32885773019
--- /dev/null
+++ b/docs/docs/reference/dependent-function-types.md
@@ -0,0 +1,50 @@
+---
+layout: doc-page
+title: "Dependent Function Types"
+---
+
+A dependent function type describes functions where the result type may depend
+on the function's parameter values. Example:
+
+    class Entry { type Key; key: Key }
+
+    def extractKey(e: Entry): e.Key = e.key          // a dependent method
+    val extractor: (e: Entry) => e.Key = extractKey  // a dependent function value
+
+Scala already has _dependent methods_, i.e. methods where the result
+type refers to some of the parameters of the method. Method
+`extractKey` is an example. Its result type, `e.key` refers its
+parameter `e` (we also say, `e.Key` _depends_ on `e`). But so far it
+was not possible to turn such methods into function values, so that
+they can be passed as parameters to other functions, or returned as
+results. Dependent methods could not be turned into functions simply
+because there was no type that could describe them.
+
+In Dotty this is now possible. The type of the `extractor` value above is
+
+    (e: Entry) => e.Key
+
+This type describes function values that take any argument `x` of type
+`Entry` and return a result of type `x.Key`.
+
+Recall that a normal function type `A => B` is represented as an
+instance of the `Function1` trait (i.e. `Function1[A, B]`) and
+analogously for functions with more parameters. Dependent functions
+are also represented as instances of these traits, but they get an additional
+refinement. In fact, the dependent function type above is just syntactic sugar for
+
+    Function1[Entry, Entry#Key] {
+      def apply(e: Entry): e.Key
+    }
+
+In general, a dependent functon type `(x1: K1, ..., xN: KN) => R` of arity `N`
+translates to
+
+    FunctionN[K1, ..., Kn, R'] {
+      def apply(x1: K1, ..., xN: KN): R
+    }
+
+where the result type parameter `R'` is an upper approximation of the
+true result type `R` that does not mention any of the parameters `e1, ..., eN`.
+
+
diff --git a/docs/sidebar.yml b/docs/sidebar.yml
index 35a807c25705..09228fc8d360 100644
--- a/docs/sidebar.yml
+++ b/docs/sidebar.yml
@@ -25,6 +25,8 @@ sidebar:
               url: docs/reference/type-lambdas.html
             - title: Implicit Function Types
               url: docs/reference/implicit-function-types.html
+            - title: Dependent Function Types
+              url: docs/reference/dependent-function-types.html
             - title: Phantom Types
               url: docs/reference/phantom-types.html
             - title: Literal Singleton Types