[commit: ghc] master: Document the kind generalization behavior observed in #13555 (18c3a7e)
git at git.haskell.org
git at git.haskell.org
Sun Apr 23 15:06:13 UTC 2017
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/18c3a7ea0f7577514721feadefd9a62c228edb60/ghc
>---------------------------------------------------------------
commit 18c3a7ea0f7577514721feadefd9a62c228edb60
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date: Sun Apr 23 10:02:45 2017 -0400
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
>---------------------------------------------------------------
18c3a7ea0f7577514721feadefd9a62c228edb60
docs/users_guide/8.2.1-notes.rst | 5 ++++
docs/users_guide/glasgow_exts.rst | 43 +++++++++++++++++++++++++++++++++
testsuite/tests/polykinds/T13555.hs | 26 ++++++++++++++++++++
testsuite/tests/polykinds/T13555.stderr | 40 ++++++++++++++++++++++++++++++
testsuite/tests/polykinds/all.T | 1 +
5 files changed, 115 insertions(+)
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, [''])
More information about the ghc-commits
mailing list