| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Implements GHC Proposal #24: .../ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst
Fixes Trac #16334, Trac #16315
With this patch, scoping rules for type and kind variables have been
unified: kind variables no longer receieve special treatment. This
simplifies both the language and the implementation.
User-facing changes
-------------------
* Kind variables are no longer implicitly quantified when an explicit
forall is used:
p :: Proxy (a :: k) -- still accepted
p :: forall k a. Proxy (a :: k) -- still accepted
p :: forall a. Proxy (a :: k) -- no longer accepted
In other words, now we adhere to the "forall-or-nothing" rule more
strictly.
Related function: RnTypes.rnImplicitBndrs
* The -Wimplicit-kind-vars warning has been deprecated.
* Kind variables are no longer implicitly quantified in constructor
declarations:
data T a = T1 (S (a :: k) | forall (b::k). T2 (S b) -- no longer accepted
data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b) -- still accepted
Related function: RnTypes.extractRdrKindSigVars
* Implicitly quantified kind variables are no longer put in front of
other variables:
f :: Proxy (a :: k) -> Proxy (b :: j)
f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b -- old order
f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b -- new order
This is a breaking change for users of TypeApplications. Note that
we still respect the dpendency order: 'k' before 'a', 'j' before 'b'.
See "Ordering of specified variables" in the User's Guide.
Related function: RnTypes.rnImplicitBndrs
* In type synonyms and type family equations, free variables on the RHS
are no longer implicitly quantified unless used in an outermost kind
annotation:
type T = Just (Nothing :: Maybe a) -- no longer accepted
type T = Just Nothing :: Maybe (Maybe a) -- still accepted
The latter form is a workaround due to temporary lack of an explicit
quantification method. Ideally, we would write something along these
lines:
type T @a = Just (Nothing :: Maybe a)
Related function: RnTypes.extractHsTyRdrTyVarsKindVars
* Named wildcards in kinds are fixed (Trac #16334):
x :: (Int :: _t) -- this compiles, infers (_t ~ Type)
Related function: RnTypes.partition_nwcs
Implementation notes
--------------------
* One of the key changes is the removal of FKTV in RnTypes:
- data FreeKiTyVars = FKTV { fktv_kis :: [Located RdrName]
- , fktv_tys :: [Located RdrName] }
+ type FreeKiTyVars = [Located RdrName]
We used to keep track of type and kind variables separately, but
now that they are on equal footing when it comes to scoping, we
can put them in the same list.
* extract_lty and family are no longer parametrized by TypeOrKind,
as we now do not distinguish kind variables from type variables.
* PatSynExPE and the related Note [Pattern synonym existentials do not scope]
have been removed (Trac #16315). With no implicit kind quantification,
we can no longer trigger the error.
* reportFloatingKvs and the related Note [Free-floating kind vars]
have been removed. With no implicit kind quantification,
we can no longer trigger the error.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Summary:
#14710 revealed two unfortunate regressions related to kind
polymorphism that had crept in in recent GHC releases:
1. While GHC was able to catch illegal uses of kind polymorphism
(i.e., if `PolyKinds` wasn't enabled) in limited situations, it
wasn't able to catch kind polymorphism of the following form:
```lang=haskell
f :: forall a. a -> a
f x = const x g
where
g :: Proxy (x :: a)
g = Proxy
```
Note that the variable `a` is being used as a kind variable in the
type signature of `g`, but GHC happily accepts it, even without
the use of `PolyKinds`.
2. If you have `PolyKinds` (but not `TypeInType`) enabled, then GHC
incorrectly accepts the following definition:
```lang=haskell
f :: forall k (a :: k). Proxy a
f = Proxy
```
Even though `k` is explicitly bound and then later used as a kind
variable within the same telescope.
This patch fixes these two bugs as follows:
1. Whenever we rename any `HsTyVar`, we check if the following three
criteria are met:
(a) It's a type variable
(b) It's used at the kind level
(c) `PolyKinds` is not enabled
If so, then we have found an illegal use of kind polymorphism, so
throw an error.
This check replaces the `checkBadKindBndrs` function, which could
only catch illegal uses of kind polymorphism in very limited
situations (when the bad kind variable happened to be implicitly
quantified in the same type signature).
2. In `extract_hs_tv_bndrs`, we must error if `TypeInType` is not
enabled and either of the following criteria are met:
(a) An explicitly bound type variable is used in kind position
in the body of a `forall` type.
(b) An explicitly bound type variable is used in kind position
in the kind of a bound type variable in a `forall` type.
`extract_hs_tv_bndrs` was checking (a), but not (b). Easily fixed.
Test Plan: ./validate
Reviewers: goldfire, simonpj, bgamari, hvr
Reviewed By: simonpj
Subscribers: thomie, carter
GHC Trac Issues: #14710
Differential Revision: https://phabricator.haskell.org/D4554
|
|
|
This work was triggered by Trac #13738, which revealed to me that
the code RnTypes.bindHsQTyVars and bindLHsTyVarBndrs was a huge
tangled mess -- and outright wrong on occasion as the ticket showed.
The big problem was that bindLHsTyVarBndrs (which is invoked at every
HsForAll, including nested higher rank ones) was attempting to bind
implicit kind variables, which it has absolutely no busineess doing.
Imlicit kind quantification is done at the outside only, in fact
precisely where we have HsImplicitBndrs or LHsQTyVars (which also
has implicit binders).
Achieving this move was surprisingly hard, because more and more
barnacles had accreted aroud the original mistake. It's much
much better now.
Summary of changes. Almost all the action is in RnTypes.
* Implicit kind variables are bound only by
- By bindHsQTyVars, which deals with LHsQTyVars
- By rnImplicitBndrs, which deals with HsImplicitBndrs
* bindLHsTyVarBndrs, and bindLHsTyVarBndr are radically simplified.
They simply does far less, and have lots their forest of
incomprehensible accumulating parameters. (To be fair, some of
the code in bindLHsTyVarBndrs just moved to bindHsQTyVars, but
in much more perspicuous form.)
* The code that checks if a variable appears in both a kind and
a type (triggering RnTypes.mixedVarsErr) was bizarre. E.g.
we had this in RnTypes.extract_hs_tv_bndrs
; check_for_mixed_vars bndr_kvs acc_tvs
; check_for_mixed_vars bndr_kvs body_tvs
; check_for_mixed_vars body_tvs acc_kvs
; check_for_mixed_vars body_kvs acc_tvs
; check_for_mixed_vars locals body_kvs
I cleaned all this up; now we check for mixed use at binding
sites only.
* Checks for "Variable used as a kind before being bound", like
data T (a :: k) k = rhs
now just show up straightforwardly as "k is not in scope".
See Note [Kind variable ordering]
* There are some knock-on simplifications in RnSource.
|
