Commit 5bc195b1 authored by Vladislav Zavialov's avatar Vladislav Zavialov Committed by Marge Bot
Browse files

Treat kind/type variables identically, demolish FKTV

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.
parent 4dbacba5
Pipeline #2825 passed with stages
in 268 minutes and 34 seconds
...@@ -3992,7 +3992,8 @@ wWarningFlagsDeps = [ ...@@ -3992,7 +3992,8 @@ wWarningFlagsDeps = [
flagSpec "hi-shadowing" Opt_WarnHiShadows, flagSpec "hi-shadowing" Opt_WarnHiShadows,
flagSpec "inaccessible-code" Opt_WarnInaccessibleCode, flagSpec "inaccessible-code" Opt_WarnInaccessibleCode,
flagSpec "implicit-prelude" Opt_WarnImplicitPrelude, flagSpec "implicit-prelude" Opt_WarnImplicitPrelude,
flagSpec "implicit-kind-vars" Opt_WarnImplicitKindVars, depFlagSpec "implicit-kind-vars" Opt_WarnImplicitKindVars
"it is now an error",
flagSpec "incomplete-patterns" Opt_WarnIncompletePatterns, flagSpec "incomplete-patterns" Opt_WarnIncompletePatterns,
flagSpec "incomplete-record-updates" Opt_WarnIncompletePatternsRecUpd, flagSpec "incomplete-record-updates" Opt_WarnIncompletePatternsRecUpd,
flagSpec "incomplete-uni-patterns" Opt_WarnIncompleteUniPatterns, flagSpec "incomplete-uni-patterns" Opt_WarnIncompleteUniPatterns,
...@@ -4830,7 +4831,6 @@ minusWcompatOpts ...@@ -4830,7 +4831,6 @@ minusWcompatOpts
= [ Opt_WarnMissingMonadFailInstances = [ Opt_WarnMissingMonadFailInstances
, Opt_WarnSemigroup , Opt_WarnSemigroup
, Opt_WarnNonCanonicalMonoidInstances , Opt_WarnNonCanonicalMonoidInstances
, Opt_WarnImplicitKindVars
, Opt_WarnStarIsType , Opt_WarnStarIsType
] ]
......
...@@ -727,15 +727,11 @@ rnFamInstEqn doc mb_cls rhs_kvars ...@@ -727,15 +727,11 @@ rnFamInstEqn doc mb_cls rhs_kvars
; let pat_kity_vars_with_dups = extractHsTyArgRdrKiTyVarsDup pats ; let pat_kity_vars_with_dups = extractHsTyArgRdrKiTyVarsDup pats
-- Use the "...Dups" form because it's needed -- Use the "...Dups" form because it's needed
-- below to report unsed binder on the LHS -- below to report unsed binder on the LHS
; let pat_kity_vars = rmDupsInRdrTyVars pat_kity_vars_with_dups
-- Implicitly bound variables, empty if we have an explicit 'forall' according
-- all pat vars not explicitly bound (see extractHsTvBndrs) -- to the "forall-or-nothing" rule.
; let mb_imp_kity_vars = extractHsTvBndrs <$> mb_bndrs <*> pure pat_kity_vars ; let imp_vars | isNothing mb_bndrs = nubL pat_kity_vars_with_dups
imp_vars = case mb_imp_kity_vars of | otherwise = []
-- kind vars are the only ones free if we have an explicit forall
Just nbnd_kity_vars -> freeKiTyVarsKindVars nbnd_kity_vars
-- all pattern vars are free otherwise
Nothing -> freeKiTyVarsAllVars pat_kity_vars
; imp_var_names <- mapM (newTyVarNameRn mb_cls) imp_vars ; imp_var_names <- mapM (newTyVarNameRn mb_cls) imp_vars
; let bndrs = fromMaybe [] mb_bndrs ; let bndrs = fromMaybe [] mb_bndrs
...@@ -766,7 +762,7 @@ rnFamInstEqn doc mb_cls rhs_kvars ...@@ -766,7 +762,7 @@ rnFamInstEqn doc mb_cls rhs_kvars
-- See Note [Unused type variables in family instances] -- See Note [Unused type variables in family instances]
; let groups :: [NonEmpty (Located RdrName)] ; let groups :: [NonEmpty (Located RdrName)]
groups = equivClasses cmpLocated $ groups = equivClasses cmpLocated $
freeKiTyVarsAllVars pat_kity_vars_with_dups pat_kity_vars_with_dups
; nms_dups <- mapM (lookupOccRn . unLoc) $ ; nms_dups <- mapM (lookupOccRn . unLoc) $
[ tv | (tv :| (_:_)) <- groups ] [ tv | (tv :| (_:_)) <- groups ]
-- Add to the used variables -- Add to the used variables
......
This diff is collapsed.
...@@ -47,7 +47,6 @@ module TcHsType ( ...@@ -47,7 +47,6 @@ module TcHsType (
typeLevelMode, kindLevelMode, typeLevelMode, kindLevelMode,
kindGeneralize, checkExpectedKind_pp, kindGeneralize, checkExpectedKind_pp,
reportFloatingKvs,
-- Sort-checking kinds -- Sort-checking kinds
tcLHsKindSig, badKindSig, tcLHsKindSig, badKindSig,
...@@ -1871,13 +1870,6 @@ kcLHsQTyVars_Cusk name flav ...@@ -1871,13 +1870,6 @@ kcLHsQTyVars_Cusk name flav
-- doesn't work, we catch it here, before an error cascade -- doesn't work, we catch it here, before an error cascade
; checkValidTelescope tycon ; checkValidTelescope tycon
-- If any of the specified tyvars aren't actually mentioned in a binder's
-- kind (or the return kind), then we're in the CUSK case from
-- Note [Free-floating kind vars]
; let unmentioned_kvs = filterOut (`elemVarSet` mentioned_kv_set) specified
; reportFloatingKvs name flav (map binderVar final_tc_binders) unmentioned_kvs
; traceTc "kcLHsQTyVars: cusk" $ ; traceTc "kcLHsQTyVars: cusk" $
vcat [ text "name" <+> ppr name vcat [ text "name" <+> ppr name
, text "kv_ns" <+> ppr kv_ns , text "kv_ns" <+> ppr kv_ns
...@@ -2889,8 +2881,6 @@ promotionErr name err ...@@ -2889,8 +2881,6 @@ promotionErr name err
NoDataKindsTC -> text "perhaps you intended to use DataKinds" NoDataKindsTC -> text "perhaps you intended to use DataKinds"
NoDataKindsDC -> text "perhaps you intended to use DataKinds" NoDataKindsDC -> text "perhaps you intended to use DataKinds"
PatSynPE -> text "pattern synonyms cannot be promoted" PatSynPE -> text "pattern synonyms cannot be promoted"
PatSynExPE -> sep [ text "the existential variables of a pattern synonym"
, text "signature do not scope over the pattern" ]
_ -> text "it is defined and used in the same recursive group" _ -> text "it is defined and used in the same recursive group"
{- {-
...@@ -2919,112 +2909,6 @@ badPatTyVarTvs sig_ty bad_tvs ...@@ -2919,112 +2909,6 @@ badPatTyVarTvs sig_ty bad_tvs
-} -}
{- Note [Free-floating kind vars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data S a = MkS (Proxy (a :: k))
According to the rules around implicitly-bound kind variables,
that k scopes over the whole declaration. The renamer grabs
it and adds it to the hsq_implicits field of the HsQTyVars of the
tycon. So we get
S :: forall {k}. k -> Type
That's fine. But consider this variant:
data T = MkT (forall (a :: k). Proxy a)
-- from test ghci/scripts/T7873
This is not an existential datatype, but a higher-rank one (the forall
to the right of MkT). Again, 'k' scopes over the whole declaration,
but we do not want to get
T :: forall {k}. Type
Why not? Because the kind variable isn't fixed by anything. For
a variable like k to be implicit, it needs to be mentioned in the kind
of a tycon tyvar. But it isn't.
Rejecting T depends on whether or not the datatype has a CUSK.
Non-CUSK (handled in TcTyClsDecls.kcTyClGroup (generalise)):
When generalising the TyCon we check that every Specified 'k'
appears free in the kind of the TyCon; that is, in the kind of
one of its Required arguments, or the result kind.
CUSK (handled in TcHsType.kcLHsQTyVars, the CUSK case):
When we determine the tycon's final, never-to-be-changed kind
in kcLHsQTyVars, we check to make sure all implicitly-bound kind
vars are indeed mentioned in a kind somewhere. If not, error.
We also perform free-floating kind var analysis for type family instances
(see #13985). Here is an interesting example:
type family T :: k
type instance T = (Nothing :: Maybe a)
Upon a cursory glance, it may appear that the kind variable `a` is
free-floating above, since there are no (visible) LHS patterns in `T`. However,
there is an *invisible* pattern due to the return kind, so inside of GHC, the
instance looks closer to this:
type family T @k :: k
type instance T @(Maybe a) = (Nothing :: Maybe a)
Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
fact not free-floating. Contrast that with this example:
type instance T = Proxy (Nothing :: Maybe a)
This would looks like this inside of GHC:
type instance T @(*) = Proxy (Nothing :: Maybe a)
So this time, `a` is neither bound by a visible nor invisible type pattern on
the LHS, so it would be reported as free-floating.
Finally, here's one more brain-teaser (from #9574). In the example below:
class Funct f where
type Codomain f :: *
instance Funct ('KProxy :: KProxy o) where
type Codomain 'KProxy = NatTr (Proxy :: o -> *)
As it turns out, `o` is not free-floating in this example. That is because `o`
bound by the kind signature of the LHS type pattern 'KProxy. To make this more
obvious, one can also write the instance like so:
instance Funct ('KProxy :: KProxy o) where
type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
-}
-- See Note [Free-floating kind vars]
reportFloatingKvs :: Name -- of the tycon
-> TyConFlavour -- What sort of TyCon it is
-> [TcTyVar] -- all tyvars, not necessarily zonked
-> [TcTyVar] -- floating tyvars
-> TcM ()
reportFloatingKvs tycon_name flav all_tvs bad_tvs
= unless (null bad_tvs) $ -- don't bother zonking if there's no error
do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs
; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs
; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
tidy_bad_tvs = map (tidyTyCoVarOcc tidy_env) bad_tvs
; mapM_ (report tidy_all_tvs) tidy_bad_tvs }
where
report tidy_all_tvs tidy_bad_tv
= addErr $
vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+>
text "is implicitly bound in" <+> ppr flav
, quotes (ppr tycon_name) <> comma <+>
text "but does not appear as the kind of any"
, text "of its type variables. Perhaps you meant"
, text "to bind it explicitly somewhere?"
, ppWhen (not (null tidy_all_tvs)) $
hang (text "Type variables with inferred kinds:")
2 (ppr_tv_bndrs tidy_all_tvs) ]
ppr_tv_bndrs tvs = sep (map pp_tv tvs)
pp_tv tv = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv))
-- | If the inner action emits constraints, report them as errors and fail; -- | If the inner action emits constraints, report them as errors and fail;
-- otherwise, propagates the return value. Useful as a wrapper around -- otherwise, propagates the return value. Useful as a wrapper around
-- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be -- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be
......
...@@ -384,9 +384,6 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(dL->L _ name), psb_args = details ...@@ -384,9 +384,6 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(dL->L _ name), psb_args = details
ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys ) ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
pushLevelAndCaptureConstraints $ pushLevelAndCaptureConstraints $
tcExtendTyVarEnv univ_tvs $ tcExtendTyVarEnv univ_tvs $
tcExtendKindEnvList [(getName (binderVar ex_tv), APromotionErr PatSynExPE)
| ex_tv <- extra_ex] $
-- See Note [Pattern synonym existentials do not scope]
tcPat PatSyn lpat (mkCheckExpType pat_ty) $ tcPat PatSyn lpat (mkCheckExpType pat_ty) $
do { let in_scope = mkInScopeSet (mkVarSet univ_tvs) do { let in_scope = mkInScopeSet (mkVarSet univ_tvs)
empty_subst = mkEmptyTCvSubst in_scope empty_subst = mkEmptyTCvSubst in_scope
...@@ -451,54 +448,6 @@ This should work. But in the matcher we must match against MkT, and then ...@@ -451,54 +448,6 @@ This should work. But in the matcher we must match against MkT, and then
instantiate its argument 'x', to get a function of type (Int -> Int). instantiate its argument 'x', to get a function of type (Int -> Int).
Equality is not enough! Trac #13752 was an example. Equality is not enough! Trac #13752 was an example.
Note [Pattern synonym existentials do not scope]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (Trac #14498):
pattern SS :: forall (t :: k). () =>
=> forall (a :: kk -> k) (n :: kk).
=> TypeRep n -> TypeRep t
pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k)) n)
Here 'k' is implicitly bound in the signature, but (with
-XScopedTypeVariables) it does still scope over the pattern-synonym
definition. But what about 'kk', which is oexistential? It too is
implicitly bound in the signature; should it too scope? And if so,
what type variable is it bound to?
The trouble is that the type variable to which it is bound is itself
only brought into scope in part the pattern, so it makes no sense for
'kk' to scope over the whole pattern. See the discussion on
Trac #14498, esp comment:16ff. Here is a simpler example:
data T where { MkT :: x -> (x->Int) -> T }
pattern P :: () => forall x. x -> (x->Int) -> T
pattern P a b = (MkT a b, True)
Here it would make no sense to mention 'x' in the True pattern,
like this:
pattern P a b = (MkT a b, True :: x)
The 'x' only makes sense "under" the MkT pattern. Conclusion: the
existential type variables of a pattern-synonym signature should not
scope.
But it's not that easy to implement, because we don't know
exactly what the existentials /are/ until we get to type checking.
(See Note [The pattern-synonym signature splitting rule], and
the partition of implicit_tvs in tcCheckPatSynDecl.)
So we do this:
- The reaner brings all the implicitly-bound kind variables into
scope, without trying to distinguish universal from existential
- tcCheckPatSynDecl uses tcExtendKindEnvList to bind the
implicitly-bound existentials to
APromotionErr PatSynExPE
It's not really a promotion error, but it's a way to bind the Name
(which the renamer has not complained about) to something that, when
looked up, will cause a complaint (in this case
TcHsType.promotionErr)
Note [The pattern-synonym signature splitting rule] Note [The pattern-synonym signature splitting rule]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
...@@ -1107,9 +1107,6 @@ data PromotionErr ...@@ -1107,9 +1107,6 @@ data PromotionErr
| PatSynPE -- Pattern synonyms | PatSynPE -- Pattern synonyms
-- See Note [Don't promote pattern synonyms] in TcEnv -- See Note [Don't promote pattern synonyms] in TcEnv
| PatSynExPE -- Pattern synonym existential type variable
-- See Note [Pattern synonym existentials do not scope] in TcPatSyn
| RecDataConPE -- Data constructor in a recursive loop | RecDataConPE -- Data constructor in a recursive loop
-- See Note [Recursion and promoting data constructors] in TcTyClsDecls -- See Note [Recursion and promoting data constructors] in TcTyClsDecls
| NoDataKindsTC -- -XDataKinds not enabled (for a tycon) | NoDataKindsTC -- -XDataKinds not enabled (for a tycon)
...@@ -1303,7 +1300,6 @@ instance Outputable PromotionErr where ...@@ -1303,7 +1300,6 @@ instance Outputable PromotionErr where
ppr ClassPE = text "ClassPE" ppr ClassPE = text "ClassPE"
ppr TyConPE = text "TyConPE" ppr TyConPE = text "TyConPE"
ppr PatSynPE = text "PatSynPE" ppr PatSynPE = text "PatSynPE"
ppr PatSynExPE = text "PatSynExPE"
ppr FamDataConPE = text "FamDataConPE" ppr FamDataConPE = text "FamDataConPE"
ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE" ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE"
<+> parens (ppr pred) <+> parens (ppr pred)
...@@ -1322,7 +1318,6 @@ pprPECategory :: PromotionErr -> SDoc ...@@ -1322,7 +1318,6 @@ pprPECategory :: PromotionErr -> SDoc
pprPECategory ClassPE = text "Class" pprPECategory ClassPE = text "Class"
pprPECategory TyConPE = text "Type constructor" pprPECategory TyConPE = text "Type constructor"
pprPECategory PatSynPE = text "Pattern synonym" pprPECategory PatSynPE = text "Pattern synonym"
pprPECategory PatSynExPE = text "Pattern synonym existential"
pprPECategory FamDataConPE = text "Data constructor" pprPECategory FamDataConPE = text "Data constructor"
pprPECategory ConstrainedDataConPE{} = text "Data constructor" pprPECategory ConstrainedDataConPE{} = text "Data constructor"
pprPECategory RecDataConPE = text "Data constructor" pprPECategory RecDataConPE = text "Data constructor"
......
...@@ -1252,7 +1252,7 @@ reifyInstances th_nm th_tys ...@@ -1252,7 +1252,7 @@ reifyInstances th_nm th_tys
; rdr_ty <- cvt loc (mkThAppTs (TH.ConT th_nm) th_tys) ; rdr_ty <- cvt loc (mkThAppTs (TH.ConT th_nm) th_tys)
-- #9262 says to bring vars into scope, like in HsForAllTy case -- #9262 says to bring vars into scope, like in HsForAllTy case
-- of rnHsTyKi -- of rnHsTyKi
; let tv_rdrs = freeKiTyVarsAllVars (extractHsTyRdrTyVars rdr_ty) ; let tv_rdrs = extractHsTyRdrTyVars rdr_ty
-- Rename to HsType Name -- Rename to HsType Name
; ((tv_names, rn_ty), _fvs) ; ((tv_names, rn_ty), _fvs)
<- checkNoErrs $ -- If there are out-of-scope Names here, then we <- checkNoErrs $ -- If there are out-of-scope Names here, then we
......
...@@ -537,7 +537,6 @@ generaliseTcTyCon tc ...@@ -537,7 +537,6 @@ generaliseTcTyCon tc
= setSrcSpan (getSrcSpan tc) $ = setSrcSpan (getSrcSpan tc) $
addTyConCtxt tc $ addTyConCtxt tc $
do { let tc_name = tyConName tc do { let tc_name = tyConName tc
tc_flav = tyConFlavour tc
tc_res_kind = tyConResKind tc tc_res_kind = tyConResKind tc
tc_tvs = tyConTyVars tc tc_tvs = tyConTyVars tc
...@@ -610,21 +609,13 @@ generaliseTcTyCon tc ...@@ -610,21 +609,13 @@ generaliseTcTyCon tc
, text "required_tcbs =" <+> ppr required_tcbs , text "required_tcbs =" <+> ppr required_tcbs
, text "final_tcbs =" <+> ppr final_tcbs ] , text "final_tcbs =" <+> ppr final_tcbs ]
-- Step 8: check for floating kind vars -- Step 8: Check for duplicates
-- See Note [Free-floating kind vars]
-- They are easily identified by the fact that they
-- have not been skolemised by quantifyTyVars
; let floating_specified = filter isTyVarTyVar scoped_tvs
; reportFloatingKvs tc_name tc_flav
scoped_tvs floating_specified
-- Step 9: Check for duplicates
-- E.g. data SameKind (a::k) (b::k) -- E.g. data SameKind (a::k) (b::k)
-- data T (a::k1) (b::k2) = MkT (SameKind a b) -- data T (a::k1) (b::k2) = MkT (SameKind a b)
-- Here k1 and k2 start as TyVarTvs, and get unified with each other -- Here k1 and k2 start as TyVarTvs, and get unified with each other
; mapM_ report_sig_tv_err (findDupTyVarTvs scoped_tv_pairs) ; mapM_ report_sig_tv_err (findDupTyVarTvs scoped_tv_pairs)
-- Step 10: Check for validity. -- Step 9: Check for validity.
-- We do this here because we're about to put the tycon into -- We do this here because we're about to put the tycon into
-- the environment, and we don't want anything malformed in the -- the environment, and we don't want anything malformed in the
-- environment. -- environment.
......
...@@ -16,6 +16,34 @@ Full details ...@@ -16,6 +16,34 @@ Full details
Language Language
~~~~~~~~ ~~~~~~~~
- Kind variables are no longer implicitly quantified when an explicit ``forall`` is used, see
`GHC proposal #24
<https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst>`__.
:ghc-flag:`-Wimplicit-kind-vars` is now obsolete.
- 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
- Implicitly quantified kind variables are no longer put in front of other variables: ::
f :: Proxy (a :: k) -> Proxy (b :: j)
ghci> :t +v f -- old order:
f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b
ghci> :t +v f -- new order:
f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b
This is a breaking change for users of :extension:`TypeApplications`.
- 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
Compiler Compiler
~~~~~~~~ ~~~~~~~~
......
...@@ -7574,16 +7574,16 @@ instance for ``GMap`` is :: ...@@ -7574,16 +7574,16 @@ instance for ``GMap`` is ::
In this example, the declaration has only one variant. In general, it In this example, the declaration has only one variant. In general, it
can be any number. can be any number.
   
When :extension:`ExplicitForAll` is enabled, type or kind variables used on When :extension:`ExplicitForAll` is enabled, type and kind variables used on
the left hand side can be explicitly bound. For example: :: the left hand side can be explicitly bound. For example: ::
   
data instance forall a (b :: Proxy a). F (Proxy b) = FProxy Bool data instance forall a (b :: Proxy a). F (Proxy b) = FProxy Bool
   
When an explicit ``forall`` is present, all *type* variables mentioned which When an explicit ``forall`` is present, *all* type and kind variables mentioned
are not already in scope must be bound by the ``forall``. Kind variables will which are not already in scope must be bound by the ``forall``:
be implicitly bound if necessary, for example: ::
   
data instance forall (a :: k). F a = FOtherwise data instance forall (a :: k). F a = FOtherwise -- rejected: k not in scope
data instance forall k (a :: k). F a = FOtherwise -- accepted
   
When the flag :ghc-flag:`-Wunused-type-patterns` is enabled, type When the flag :ghc-flag:`-Wunused-type-patterns` is enabled, type
variables that are mentioned in the patterns on the left hand side, but not variables that are mentioned in the patterns on the left hand side, but not
...@@ -9184,17 +9184,74 @@ a type variable ``a`` of kind ``k``. In general, there is no limit to how ...@@ -9184,17 +9184,74 @@ a type variable ``a`` of kind ``k``. In general, there is no limit to how
deeply nested this sort of dependency can work. However, the dependency must deeply nested this sort of dependency can work. However, the dependency must
be well-scoped: ``forall (a :: k) k. ...`` is an error. be well-scoped: ``forall (a :: k) k. ...`` is an error.
   
For backward compatibility, kind variables *do not* need to be bound explicitly, Implicit quantification in type synonyms and type family instances
even if the type starts with ``forall``. ------------------------------------------------------------------
   
Accordingly, the rule for kind quantification in higher-rank contexts has Consider the scoping rules for type synonyms and type family instances, such as
changed slightly. In GHC 7, if a kind variable was mentioned for the first these::
time in the kind of a variable bound in a non-top-level ``forall``, the kind
variable was bound there, too. type TS a (b :: k) = <rhs>
That is, in ``f :: (forall (a :: k). ...) -> ...``, the ``k`` was bound type instance TF a (b :: k) = <rhs>
by the same ``forall`` as the ``a``. In GHC 8, however, all kind variables
mentioned in a type are bound at the outermost level. If you want one bound The basic principle is that all variables mentioned on the right hand side
in a higher-rank ``forall``, include it explicitly. ``<rhs>`` must be bound on the left hand side::
type TS a (b :: k) = (k, a, Proxy b) -- accepted
type TS a (b :: k) = (k, a, Proxy b, z) -- rejected: z not in scope
But there is one exception: free variables mentioned in the outermost kind
signature on the right hand side are quantified implicitly. Thus, in the
following example the variables ``a``, ``b``, and ``k`` are all in scope on the
right hand side of ``S``::
type S a b = <rhs> :: k -> k
The reason for this exception is that there may be no other way to bind ``k``.
For example, suppose we wanted ``S`` to have the the following kind with an
*invisible* parameter ``k``::
S :: forall k. Type -> Type -> k -> k
In this case, we could not simply bind ``k`` on the left-hand side, as ``k``
would become a *visible* parameter::
type S k a b = <rhs> :: k -> k
S :: forall k -> Type -> Type -> k -> k
Note that we only look at the *outermost* kind signature to decide which
variables to quantify implicitly. As a counter-example, consider ``M1``: ::
type M1 = 'Just ('Nothing :: Maybe k) -- rejected: k not in scope
Here, the kind signature is hidden inside ``'Just``, and there is no outermost
kind signature. We can fix this example by providing an outermost kind signature: ::
type M2 = 'Just ('Nothing :: Maybe k) :: Maybe (Maybe k)
Here, ``k`` is brought into scope by ``:: Maybe (Maybe k)``.
A kind signature is considered to be outermost regardless of redundant
parentheses: ::
type P = 'Nothing :: Maybe a -- accepted
type P = ((('Nothing :: Maybe a))) -- accepted
Closed type family instances are subject to the same rules: ::
type family F where
F = 'Nothing :: Maybe k -- accepted
type family F where
F = 'Just ('Nothing :: Maybe k) -- rejected: k not in scope
type family F where
F = 'Just ('Nothing :: Maybe k) :: Maybe (Maybe k) -- accepted
type family F :: Maybe (Maybe k) where
F = 'Just ('Nothing :: Maybe k) -- rejected: k not in scope
type family F :: Maybe (Maybe k) where
F @k = 'Just ('Nothing :: Maybe k) -- accepted
   
Kind-indexed GADTs Kind-indexed GADTs
------------------ ------------------
...@@ -10832,19 +10889,6 @@ the rules in the subtler cases: ...@@ -10832,19 +10889,6 @@ the rules in the subtler cases:
- If an identifier's type has a ``forall``, then the order of type variables - If an identifier's type has a ``forall``, then the order of type variables
as written in the ``forall`` is retained. as written in the ``forall`` is retained.
   
- If the type signature includes any kind annotations (either on variable
binders or as annotations on types), any variables used in kind
annotations come before any variables never used in kind annotations.
This rule is not recursive: if there is an annotation within an annotation,
then the variables used therein are on equal footing. Examples::
f :: Proxy (a :: k) -> Proxy (b :: j) -> ()
-- as if f :: forall k j a b. ...
g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> ()
-- as if g :: forall j k b a. ...
-- NB: k is in a kind annotation within a kind annotation
- If any of the variables depend on other variables (that is, if some - If any of the variables depend on other variables (that is, if some
of the variables are *kind* variables), the variables are reordered of the variables are *kind* variables), the variables are reordered
so that kind variables come before type variables, preserving the so that kind variables come before type variables, preserving the
...@@ -10854,13 +10898,11 @@ the rules in the subtler cases: ...@@ -10854,13 +10898,11 @@ the rules in the subtler cases:
h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> () h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> ()
-- as if h :: forall j k a b. ... -- as if h :: forall j k a b. ...
   
In this example, all of ``a``, ``j``, and ``k`` are considered kind In this example, ``a`` depends on ``j`` and ``k``, and ``b`` depends on ``a``.
variables and will always be placed before ``b``, a lowly type variable. Even though ``a`` appears lexically before ``j`` and ``k``, ``j`` and ``k``
(Note that ``a`` is used in ``b``\'s kind.) Yet, even though ``a`` appears are quantified first, because ``a`` depends on ``j`` and ``k``. Note further
lexically before ``j`` and ``k``, ``j`` and ``k`` are quantified first, that ``j`` and ``k`` are not reordered with respect to each other, even
because ``a`` depends on ``j`` and ``k``. Note further that ``j`` and ``k`` though doing so would not violate dependency conditions.
are not reordered with respect to each other, even though doing so would
not violate dependency conditions.
   
A "stable topological sort" here, we mean that we perform this algorithm A "stable topological sort" here, we mean that we perform this algorithm
(which we call *ScopedSort*): (which we call *ScopedSort*):
......