Document the kind generalization behavior observed in #13555

The conclusion of #13555 was that a program which began to fail to
typecheck (starting in GHC 8.2) was never correct to begin with. Let's
document why this is the case with respect to `MonoLocalBinds`'
interaction with kind generalization. Also adds the reported program as
a `compile_fail` testcase.

Test Plan: make test TEST=T13555 # Also, read the docs

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: goldfire, simonpj, bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13555

Differential Revision: https://phabricator.haskell.org/D3472

5 files changed, 115 insertions, 0 deletions

diff --git a/docs/users_guide/8.2.1-notes.rst b/docs/users_guide/8.2.1-notes.rst
index 37fdabb..3b1a1f1 100644
--- a/docs/users_guide/8.2.1-notes.rst
+++ b/docs/users_guide/8.2.1-notes.rst
@@ -196,6 +196,11 @@ Compiler
   See the section on `associated type family instances <assoc-data-inst>` for
   more information.
 
+- A bug involving the interaction between :ghc-flag:`-XMonoLocalBinds` and
+  :ghc-flag:`-XPolyKinds` has been fixed. This can cause some programs to fail
+  to typecheck in case explicit kind signatures are not provided. See
+  :ref:`kind-generalisation` for an example.
+
 GHCi
 ~~~~
 
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 40e3f82..c45fbec 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -9332,6 +9332,49 @@ and :ghc-flag:`-XGADTs`. You can switch it off again with
 :ghc-flag:`-XNoMonoLocalBinds <-XMonoLocalBinds>` but type inference becomes
 less predicatable if you do so. (Read the papers!)
 
+.. _kind-generalisation:
+
+Kind generalisation
+-------------------
+
+Just as :ghc-flag:`-XMonoLocalBinds` places limitations on when the *type* of a
+*term* is generalised (see :ref:`mono-local-binds`), it also limits when the
+*kind* of a *type signature* is generalised. Here is an example involving
+:ref:`type signatures on instance declarations <instance-sigs>`: ::
+
+    data Proxy a = Proxy
+    newtype Tagged s b = Tagged b
+
+    class C b where
+      c :: forall (s :: k). Tagged s b
+
+    instance C (Proxy a) where
+      c :: forall s. Tagged s (Proxy a)
+      c = Tagged Proxy
+
+With :ghc-flag:`-XMonoLocalBinds` enabled, this ``C (Proxy a)`` instance will
+fail to typecheck. The reason is that the type signature for ``c`` captures
+``a``, an outer-scoped type variable, which means the type signature is not
+closed. Therefore, the inferred kind for ``s`` will *not* be generalised, and
+as a result, it will fail to unify with the kind variable ``k`` which is
+specified in the declaration of ``c``. This can be worked around by specifying
+an explicit kind variable for ``s``, e.g., ::
+
+    instance C (Proxy a) where
+      c :: forall (s :: k). Tagged s (Proxy a)
+      c = Tagged Proxy
+
+or, alternatively: ::
+
+    instance C (Proxy a) where
+      c :: forall k (s :: k). Tagged s (Proxy a)
+      c = Tagged Proxy
+
+This declarations are equivalent using Haskell's implicit "add implicit
+foralls" rules (see :ref:`implicit-quantification`). The implicit foralls rules
+are purely syntactic and are quite separate from the kind generalisation
+described here.
+
 .. _visible-type-application:
 
 Visible type application
diff --git a/testsuite/tests/polykinds/T13555.hs b/testsuite/tests/polykinds/T13555.hs
new file mode 100644
index 0000000..e71023e
--- /dev/null
+++ b/testsuite/tests/polykinds/T13555.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T13555 where
+
+import Data.Functor.Identity (Identity(..))
+
+data T a
+type Polynomial a = T a
+newtype GF fp d = GF (Polynomial fp)
+type CRTInfo r = (Int -> r, r)
+type Tagged s b = TaggedT s Identity b
+newtype TaggedT s m b = TagT { untagT :: m b }
+
+class Reflects a i where
+  value :: Tagged a i
+
+class CRTrans mon r where
+  crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)
+
+instance CRTrans Maybe (GF fp d) where
+  crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
+  crtInfo = undefined
diff --git a/testsuite/tests/polykinds/T13555.stderr b/testsuite/tests/polykinds/T13555.stderr
new file mode 100644
index 0000000..eaea033
--- /dev/null
+++ b/testsuite/tests/polykinds/T13555.stderr
@@ -0,0 +1,40 @@
+
+T13555.hs:25:14: error:
+    • Couldn't match type ‘k0’ with ‘k2’
+        because type variable ‘k2’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        the type signature for:
+          crtInfo :: forall k2 (m :: k2).
+                     Reflects m Int =>
+                     TaggedT m Maybe (CRTInfo (GF fp d))
+        at T13555.hs:25:14-79
+      Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
+        Actual type: TaggedT m Maybe (CRTInfo (GF fp d))
+    • When checking that instance signature for ‘crtInfo’
+        is more general than its signature in the class
+        Instance sig: forall (m :: k0).
+                      Reflects m Int =>
+                      TaggedT m Maybe (CRTInfo (GF fp d))
+           Class sig: forall k2 (m :: k2).
+                      Reflects m Int =>
+                      TaggedT m Maybe (CRTInfo (GF fp d))
+      In the instance declaration for ‘CRTrans Maybe (GF fp d)’
+
+T13555.hs:25:14: error:
+    • Could not deduce (Reflects m Int)
+      from the context: Reflects m Int
+        bound by the type signature for:
+                   crtInfo :: forall k2 (m :: k2).
+                              Reflects m Int =>
+                              TaggedT m Maybe (CRTInfo (GF fp d))
+        at T13555.hs:25:14-79
+      The type variable ‘k0’ is ambiguous
+    • When checking that instance signature for ‘crtInfo’
+        is more general than its signature in the class
+        Instance sig: forall (m :: k0).
+                      Reflects m Int =>
+                      TaggedT m Maybe (CRTInfo (GF fp d))
+           Class sig: forall k2 (m :: k2).
+                      Reflects m Int =>
+                      TaggedT m Maybe (CRTInfo (GF fp d))
+      In the instance declaration for ‘CRTrans Maybe (GF fp d)’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index eb5b09a..e534e08 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -159,3 +159,4 @@ test('T13394a', normal, compile, [''])
 test('T13394', normal, compile, [''])
 test('T13371', normal, compile, [''])
 test('T13393', normal, compile_fail, [''])
+test('T13555', normal, compile_fail, [''])