Commit 18c3a7ea authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

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
parent 9eea43f9
......@@ -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
~~~~
......
......@@ -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
......
{-# 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
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)’
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment