Commit 447d1264 authored by Ryan Scott's avatar Ryan Scott
Browse files

Fix #14710 with more validity checks during renaming

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
parent 5d768464
......@@ -1929,7 +1929,7 @@ rnConDecl decl@(ConDeclGADT { con_names = names
mb_ctxt = Just (inHsDocContext ctxt)
; traceRn "rnConDecl" (ppr names $$ ppr free_tkvs $$ ppr explicit_forall )
; rnImplicitBndrs (not explicit_forall) ctxt free_tkvs $ \ implicit_tkvs ->
; rnImplicitBndrs (not explicit_forall) free_tkvs $ \ implicit_tkvs ->
bindLHsTyVarBndrs ctxt mb_ctxt Nothing explicit_tkvs $ \ explicit_tkvs ->
do { (new_cxt, fvs1) <- rnMbContext ctxt mcxt
; (new_args, fvs2) <- rnConDeclDetails (unLoc (head new_names)) ctxt args
......
......@@ -125,7 +125,7 @@ rn_hs_sig_wc_type always_bind_free_tvs ctxt
; (tv_rdrs, nwc_rdrs') <- partition_nwcs free_vars
; let nwc_rdrs = nubL nwc_rdrs'
bind_free_tvs = always_bind_free_tvs || not (isLHsForAllTy hs_ty)
; rnImplicitBndrs bind_free_tvs ctxt tv_rdrs $ \ vars ->
; rnImplicitBndrs bind_free_tvs tv_rdrs $ \ vars ->
do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
; let sig_ty' = HsWC { hswc_wcs = wcs, hswc_body = ib_ty' }
ib_ty' = mk_implicit_bndrs vars hs_ty' fvs1
......@@ -294,7 +294,7 @@ rnHsSigType :: HsDocContext -> LHsSigType GhcPs
rnHsSigType ctx (HsIB { hsib_body = hs_ty })
= do { traceRn "rnHsSigType" (ppr hs_ty)
; vars <- extractFilteredRdrTyVarsDups hs_ty
; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) ctx vars $ \ vars ->
; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) vars $ \ vars ->
do { (body', fvs) <- rnLHsType ctx hs_ty
; return ( mk_implicit_bndrs vars body' fvs, fvs ) } }
......@@ -303,14 +303,13 @@ rnImplicitBndrs :: Bool -- True <=> bring into scope any free type variables
-- we do not want to bring 'b' into scope, hence False
-- But f :: a -> b
-- we want to bring both 'a' and 'b' into scope
-> HsDocContext
-> FreeKiTyVarsWithDups
-- Free vars of hs_ty (excluding wildcards)
-- May have duplicates, which is
-- checked here
-> ([Name] -> RnM (a, FreeVars))
-> RnM (a, FreeVars)
rnImplicitBndrs bind_free_tvs doc
rnImplicitBndrs bind_free_tvs
fvs_with_dups@(FKTV { fktv_kis = kvs_with_dups
, fktv_tys = tvs_with_dups })
thing_inside
......@@ -333,8 +332,6 @@ rnImplicitBndrs bind_free_tvs doc
; loc <- getSrcSpanM
; vars <- mapM (newLocalBndrRn . L loc . unLoc) (kvs ++ real_tvs)
; checkBadKindBndrs doc kvs
; traceRn "checkMixedVars2" $
vcat [ text "kvs_with_dups" <+> ppr kvs_with_dups
, text "tvs_with_dups" <+> ppr tvs_with_dups ]
......@@ -538,7 +535,14 @@ rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau })
, fvs1 `plusFV` fvs2) }
rnHsTyKi env (HsTyVar _ ip (L loc rdr_name))
= do { name <- rnTyVar env rdr_name
= do { when (isRnKindLevel env && isRdrTyVar rdr_name) $
unlessXOptM LangExt.PolyKinds $ addErr $
withHsDocContext (rtke_ctxt env) $
vcat [ text "Unexpected kind variable" <+> quotes (ppr rdr_name)
, text "Perhaps you intended to use PolyKinds" ]
-- Any type variable at the kind level is illegal without the use
-- of PolyKinds (see #14710)
; name <- rnTyVar env rdr_name
; return (HsTyVar noExt ip (L loc name), unitFV name) }
rnHsTyKi env ty@(HsOpTy _ ty1 l_op ty2)
......@@ -936,7 +940,6 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
, text "bndr_kv_occs" <+> ppr bndr_kv_occs
, text "wubble" <+> ppr ((kv_occs \\ bndrs) \\ bndr_kv_occs)
]
; checkBadKindBndrs doc implicit_kvs
; checkMixedVars kv_occs bndrs
; implicit_kv_nms <- mapM (newTyVarNameRn mb_assoc) implicit_kvs
......@@ -1041,6 +1044,34 @@ In implementation terms
scope in the kind of 'a'.
* Similarly in extract_hs_tv_bndrs
Note [Variables used as both types and kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In (checkMixedVars kvs tvs), we bind the type variables tvs, and kvs is the
set of free variables of the kinds in the scope of the binding. Here is one
typical example:
forall a b. a -> (b::k) -> (c::a)
Here, tvs will be {a,b}, and kvs {k,a}.
Without -XTypeInType we want to complain that `a` is used both
as a type and a kind.
Specifically, check that there is no overlap between kvs and tvs
See typecheck/should_fail/T11963 for examples.
We must also make sure that kvs includes all of variables in the kinds of type
variable bindings. For instance:
forall k (a :: k). Proxy a
If we only look in the body of the `forall` type, we will mistakenly conclude
that kvs is {}. But in fact, the type variable `k` is also used as a kind
variable in (a :: k), later in the binding. (This mistake lead to #14710.)
So tvs is {k,a} and kvs is {k}, so we must also reject this without the use
of -XTypeInType.
NB: we do this only at the binding site of 'tvs'.
-}
bindLHsTyVarBndrs :: HsDocContext
......@@ -1515,15 +1546,6 @@ unexpectedTypeSigErr ty
= hang (text "Illegal type signature:" <+> quotes (ppr ty))
2 (text "Type signatures are only allowed in patterns with ScopedTypeVariables")
checkBadKindBndrs :: HsDocContext -> [Located RdrName] -> RnM ()
checkBadKindBndrs doc kvs
= unless (null kvs) $
unlessXOptM LangExt.PolyKinds $
addErr (withHsDocContext doc $
hang (text "Unexpected kind variable" <> plural kvs
<+> pprQuotedList kvs)
2 (text "Perhaps you intended to use PolyKinds"))
badKindSigErr :: HsDocContext -> LHsType GhcPs -> TcM ()
badKindSigErr doc (L loc ty)
= setSrcSpan loc $ addErr $
......@@ -1866,16 +1888,22 @@ extract_hs_tv_bndrs tv_bndrs
| otherwise
= do { bndr_kvs <- extract_hs_tv_bndrs_kvs tv_bndrs
; let tv_bndr_rdrs :: [Located RdrName]
; let tv_bndr_rdrs, all_kv_occs :: [Located RdrName]
tv_bndr_rdrs = map hsLTyVarLocName tv_bndrs
-- We must include both kind variables from the binding as well
-- as the body of the `forall` type.
-- See Note [Variables used as both types and kinds].
all_kv_occs = bndr_kvs ++ body_kvs
; traceRn "checkMixedVars1" $
vcat [ text "body_kvs" <+> ppr body_kvs
vcat [ text "bndr_kvs" <+> ppr bndr_kvs
, text "body_kvs" <+> ppr body_kvs
, text "all_kv_occs" <+> ppr all_kv_occs
, text "tv_bndr_rdrs" <+> ppr tv_bndr_rdrs ]
; checkMixedVars body_kvs tv_bndr_rdrs
; checkMixedVars all_kv_occs tv_bndr_rdrs
; return $
FKTV (filterOut (`elemRdr` tv_bndr_rdrs) (bndr_kvs ++ body_kvs)
FKTV (filterOut (`elemRdr` tv_bndr_rdrs) all_kv_occs
-- NB: delete all tv_bndr_rdrs from bndr_kvs as well
-- as body_kvs; see Note [Kind variable scoping]
++ acc_kvs)
......@@ -1907,19 +1935,9 @@ nubL = nubBy eqLocated
elemRdr :: Located RdrName -> [Located RdrName] -> Bool
elemRdr x = any (eqLocated x)
-- Check for type variables that are also used as kinds without the use of
-- -XTypeInType. See Note [Variables used as both types and kinds].
checkMixedVars :: [Located RdrName] -> [Located RdrName] -> RnM ()
-- In (checkMixedVars kvs tvs) we are about to bind the type
-- variables tvs, and kvs is the set of free variables of the kinds
-- in the scope of the binding. E.g.
-- forall a b. a -> (b::k) -> (c::a)
-- Here tv will be {a,b}, and kvs {k,a}.
-- Without -XTypeInType we want to complain that 'a' is used both
-- as a type and a kind.
--
-- Specifically, check that there is no overlap between kvs and tvs
-- See typecheck/should_fail/T11963 for examples
--
-- NB: we do this only at the binding site of 'tvs'.
checkMixedVars kvs tvs
= do { type_in_type <- xoptM LangExt.TypeInType
; unless type_in_type $
......
......@@ -70,6 +70,25 @@ Language
See :ref:`Numeric underscores <numeric-underscores>`
for the full details.
- GHC is now more diligent about catching illegal uses of kind polymorphism.
For instance, this used to be accepted without :extension:`PolyKinds`: ::
class C a where
c :: Proxy (x :: a)
Despite the fact that ``a`` is used as a kind variable in the type signature
for ``c``. This is now an error unless :extension:`PolyKinds` is explicitly
enabled.
Moreover, GHC 8.4 would accept the following without the use of
:extension:`TypeInType` (or even :extension:`PolyKinds`!): ::
f :: forall k (a :: k). Proxy a
f = Proxy
Despite the fact that ``k`` is used as both a type and kind variable. This is
now an error unless :extension:`TypeInType` is explicitly enabled.
Compiler
~~~~~~~~
......
......@@ -84,6 +84,7 @@ Other Prelude modules are much easier with fewer complex dependencies.
, ExistentialQuantification
, RankNTypes
, KindSignatures
, TypeInType
#-}
-- -Wno-orphans is needed for things like:
-- Orphan rule: "x# -# x#" ALWAYS forall x# :: Int# -# x# x# = 0
......
BadKindVar.hs:8:1: error:
Unexpected kind variable ‘k’ Perhaps you intended to use PolyKinds
BadKindVar.hs:8:19: error:
Unexpected kind variable ‘k’
Perhaps you intended to use PolyKinds
In the type signature for ‘f’
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
module T14710 where
import Data.Proxy
class C a b where
c1 :: Proxy (x :: a) -> b
c2 :: forall (x :: a). Proxy x -> b
f :: forall a. a -> a
f x = const x (const g1 g2)
where
g1 :: Proxy (x :: a)
g1 = Proxy
g2 :: forall (x :: a). Proxy x
g2 = Proxy
h1 :: forall k a. Proxy (a :: k)
h1 = Proxy
h2 :: forall k (a :: k). Proxy a
h2 = Proxy
T14710.hs:9:21: error:
Unexpected kind variable ‘a’
Perhaps you intended to use PolyKinds
In a class method signature for ‘c1’
T14710.hs:10:22: error:
Unexpected kind variable ‘a’
Perhaps you intended to use PolyKinds
In a class method signature for ‘c2’
T14710.hs:15:23: error:
Unexpected kind variable ‘a’
Perhaps you intended to use PolyKinds
In the type signature for ‘g1’
T14710.hs:18:24: error:
Unexpected kind variable ‘a’
Perhaps you intended to use PolyKinds
In the type signature for ‘g2’
T14710.hs:21:31: error:
Variable ‘k’ used as both a kind and a type
Did you intend to use TypeInType?
T14710.hs:21:31: error:
Unexpected kind variable ‘k’
Perhaps you intended to use PolyKinds
In the type signature for ‘h1’
T14710.hs:24:22: error:
Variable ‘k’ used as both a kind and a type
Did you intend to use TypeInType?
T14710.hs:24:22: error:
Unexpected kind variable ‘k’
Perhaps you intended to use PolyKinds
In the type signature for ‘h2’
......@@ -183,6 +183,7 @@ test('T14563', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
test('T14561', normal, compile_fail, [''])
test('T14580', normal, compile_fail, [''])
test('T14515', normal, compile, [''])
test('T14710', normal, compile_fail, [''])
test('T14723', normal, compile, [''])
test('T14846', normal, compile_fail, [''])
test('T14873', normal, compile, [''])
......
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