User's Guide: extensions compatibility

Adds the mention that extensions "AllowAmbiguousTypes" and "RankNTypes"
are not always compatible with each other.
Specifies the conditions and causes of failing in resolving
of ambiguity.

1 files changed, 18 insertions, 0 deletions

diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 5a86e877c4..ccb3afb7ed 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -10358,6 +10358,24 @@ function that can *never* be called, such as this one: ::
 
       f :: (Int ~ Bool) => a -> a
 
+Sometimes :extension:`AllowAmbiguousTypes` does not mix well with :extension:`RankNTypes`.
+For example: :: 
+      foo :: forall r. (forall i. (KnownNat i) => r) -> r
+      foo f = f @1
+
+      boo :: forall j. (KnownNat j) => Int
+      boo = ....
+          
+      h :: Int
+      h = foo boo
+
+This program will be rejected as ambiguous because GHC will not unify
+the type variables `j` and `i`.
+
+Unlike the previous examples, it is not currently possible
+to resolve the ambiguity manually by using :extension:`TypeApplications`.
+
+       
 .. note::
     *A historical note.* GHC used to impose some more restrictive and less
     principled conditions on type signatures. For type