diff options
author | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-07-14 16:02:13 -0400 |
---|---|---|
committer | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-08-02 16:38:28 -0400 |
commit | c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (patch) | |
tree | 138432de269b813e605fad0e870e9bc205a20c18 /docs | |
parent | c50574a8e006ff26911f6762187d01210a1dda0f (diff) | |
download | haskell-c955a514f033a12f6d0ab0fbacec3e18a5757ab5.tar.gz |
Remove decideKindGeneralisationPlan
TypeInType came with a new function: decideKindGeneralisationPlan.
This type-level counterpart to the term-level decideGeneralisationPlan
chose whether or not a kind should be generalized. The thinking was
that if `let` should not be generalized, then kinds shouldn't either
(under the same circumstances around -XMonoLocalBinds).
However, this is too conservative -- the situation described in the
motivation for "let should be be generalized" does not occur in types.
This commit thus removes decideKindGeneralisationPlan, always
generalizing.
One consequence is that tc_hs_sig_type_and_gen no longer calls
solveEqualities, which reports all unsolved constraints, instead
relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect
of this is that reporing kind errors gets delayed more frequently.
This seems to be a net benefit in error reporting; often, alongside
a kind error, the type error is now reported (and users might find
type errors easier to understand).
Some of these errors ended up at the top level, where it was
discovered that the GlobalRdrEnv containing the definitions in the
local module was not in the TcGblEnv, and thus errors were reported
with qualified names unnecessarily. This commit rejiggers some of
the logic around captureTopConstraints accordingly.
One error message (typecheck/should_fail/T1633)
is a regression, mentioning the name of a default method. However,
that problem is already reported as #10087, its solution is far from
clear, and so I'm not addressing it here.
This commit fixes #15141. As it's an internal refactor, there is
no concrete test case for it.
Along the way, we no longer need the hsib_closed field of
HsImplicitBndrs (it was used only in decideKindGeneralisationPlan)
and so it's been removed, simplifying the datatype structure.
Along the way, I removed code in the validity checker that looks
at coercions. This isn't related to this patch, really (though
it was, at one point), but it's an improvement, so I kept it.
This updates the haddock submodule.
Diffstat (limited to 'docs')
-rw-r--r-- | docs/users_guide/glasgow_exts.rst | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 5d1c0b30cb..d5cdf71ed0 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -10559,49 +10559,6 @@ and :extension:`GADTs`. You can switch it off again with :extension:`NoMonoLocalBinds <-XMonoLocalBinds>` but type inference becomes less predictable if you do so. (Read the papers!) -.. _kind-generalisation: - -Kind generalisation -------------------- - -Just as :extension:`MonoLocalBinds` 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 :extension:`MonoLocalBinds` 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 |