Commit 0257dacf authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Refactor bindHsQTyVars and friends

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.
parent 6f050d9c
......@@ -50,6 +50,7 @@ import Avail
import Outputable
import Bag
import BasicTypes ( DerivStrategy, RuleName, pprRuleName )
import Maybes ( orElse )
import FastString
import SrcLoc
import DynFlags
......@@ -140,7 +141,6 @@ rnSrcDecls group@(HsGroup { hs_valds = val_decls,
-- They are already in scope
traceRn "rnSrcDecls" (ppr id_bndrs) ;
tc_envs <- extendGlobalRdrEnvRn (map avail id_bndrs) local_fix_env ;
traceRn "D2" (ppr (tcg_rdr_env (fst tc_envs)));
setEnvs tc_envs $ do {
-- Now everything is in scope, as the remaining renaming assumes.
......@@ -226,7 +226,6 @@ rnSrcDecls group@(HsGroup { hs_valds = val_decls,
in -- we return the deprecs in the env, not in the HsGroup above
tcg_env' { tcg_warns = tcg_warns tcg_env' `plusWarns` rn_warns };
} ;
traceRn "last" (ppr (tcg_rdr_env final_tcg_env)) ;
traceRn "finish rnSrc" (ppr rn_group) ;
traceRn "finish Dus" (ppr src_dus ) ;
return (final_tcg_env, rn_group)
......@@ -467,7 +466,9 @@ rnSrcInstDecl (DataFamInstD { dfid_inst = dfi })
; return (DataFamInstD { dfid_inst = dfi' }, fvs) }
rnSrcInstDecl (ClsInstD { cid_inst = cid })
= do { (cid', fvs) <- rnClsInstDecl cid
= do { traceRn "rnSrcIstDecl {" (ppr cid)
; (cid', fvs) <- rnClsInstDecl cid
; traceRn "rnSrcIstDecl end }" empty
; return (ClsInstD { cid_inst = cid' }, fvs) }
-- | Warn about non-canonical typeclass instance declarations
......@@ -839,7 +840,7 @@ rnDataFamInstDecl mb_cls (DataFamInstDecl { dfid_tycon = tycon
, dfid_pats = pats
, dfid_fixity = fixity
, dfid_defn = defn })
= do { (tycon', pats', (defn', _), fvs) <-
= do { (tycon', pats', defn', fvs) <-
rnFamInstDecl (TyDataCtx tycon) mb_cls tycon pats defn rnDataDefn
; return (DataFamInstDecl { dfid_tycon = tycon'
, dfid_pats = pats'
......@@ -1656,13 +1657,11 @@ rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars,
; kvs <- freeKiTyVarsKindVars <$> extractHsTyRdrTyVars rhs
; let doc = TySynCtx tycon
; traceRn "rntycl-ty" (ppr tycon <+> ppr kvs)
; ((tyvars', rhs'), fvs) <- bindHsQTyVars doc Nothing Nothing kvs tyvars $
\ tyvars' _ ->
do { (rhs', fvs) <- rnTySyn doc rhs
; return ((tyvars', rhs'), fvs) }
; bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' _ ->
do { (rhs', fvs) <- rnTySyn doc rhs
; return (SynDecl { tcdLName = tycon', tcdTyVars = tyvars'
, tcdFixity = fixity
, tcdRhs = rhs', tcdFVs = fvs }, fvs) }
, tcdRhs = rhs', tcdFVs = fvs }, fvs) } }
-- "data", "newtype" declarations
-- both top level and (for an associated type) in an instance decl
......@@ -1672,20 +1671,16 @@ rnTyClDecl (DataDecl { tcdLName = tycon, tcdTyVars = tyvars,
; kvs <- extractDataDefnKindVars defn
; let doc = TyDataCtx tycon
; traceRn "rntycl-data" (ppr tycon <+> ppr kvs)
; ((tyvars', defn', no_kvs), fvs)
<- bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' dep_vars ->
do { ((defn', kind_sig_fvs), fvs) <- rnDataDefn doc defn
; let sig_tvs = filterNameSet isTyVarName kind_sig_fvs
unbound_sig_tvs = sig_tvs `minusNameSet` dep_vars
; return ((tyvars', defn', isEmptyNameSet unbound_sig_tvs), fvs) }
; bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' no_rhs_kvs ->
do { (defn', fvs) <- rnDataDefn doc defn
-- See Note [Complete user-supplied kind signatures] in HsDecls
; typeintype <- xoptM LangExt.TypeInType
; let cusk = hsTvbAllKinded tyvars' &&
(not typeintype || no_kvs)
(not typeintype || no_rhs_kvs)
; return (DataDecl { tcdLName = tycon', tcdTyVars = tyvars'
, tcdFixity = fixity
, tcdDataDefn = defn', tcdDataCusk = cusk
, tcdFVs = fvs }, fvs) }
, tcdFVs = fvs }, fvs) } }
rnTyClDecl (ClassDecl { tcdCtxt = context, tcdLName = lcls,
tcdTyVars = tyvars, tcdFixity = fixity,
......@@ -1756,9 +1751,7 @@ rnTySyn :: HsDocContext -> LHsType GhcPs -> RnM (LHsType GhcRn, FreeVars)
rnTySyn doc rhs = rnLHsType doc rhs
rnDataDefn :: HsDocContext -> HsDataDefn GhcPs
-> RnM ((HsDataDefn GhcRn, NameSet), FreeVars)
-- the NameSet includes all Names free in the kind signature
-- See Note [Complete user-supplied kind signatures]
-> RnM (HsDataDefn GhcRn, FreeVars)
rnDataDefn doc (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
, dd_ctxt = context, dd_cons = condecls
, dd_kindSig = m_sig, dd_derivs = derivs })
......@@ -1783,11 +1776,10 @@ rnDataDefn doc (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
; let all_fvs = fvs1 `plusFV` fvs3 `plusFV`
con_fvs `plusFV` sig_fvs
; return (( HsDataDefn { dd_ND = new_or_data, dd_cType = cType
, dd_ctxt = context', dd_kindSig = m_sig'
, dd_cons = condecls'
, dd_derivs = derivs' }
, sig_fvs )
; return ( HsDataDefn { dd_ND = new_or_data, dd_cType = cType
, dd_ctxt = context', dd_kindSig = m_sig'
, dd_cons = condecls'
, dd_derivs = derivs' }
, all_fvs )
}
where
......@@ -1841,9 +1833,8 @@ rnFamDecl mb_cls (FamilyDecl { fdLName = tycon, fdTyVars = tyvars
= do { tycon' <- lookupLocatedTopBndrRn tycon
; kvs <- extractRdrKindSigVars res_sig
; ((tyvars', res_sig', injectivity'), fv1) <-
bindHsQTyVars doc Nothing mb_cls kvs tyvars $
\ tyvars'@(HsQTvs { hsq_implicit = rn_kvs }) _ ->
do { let rn_sig = rnFamResultSig doc rn_kvs
bindHsQTyVars doc Nothing mb_cls kvs tyvars $ \ tyvars' _ ->
do { let rn_sig = rnFamResultSig doc
; (res_sig', fv_kind) <- wrapLocFstM rn_sig res_sig
; injectivity' <- traverse (rnInjectivityAnn tyvars' res_sig')
injectivity
......@@ -1868,15 +1859,14 @@ rnFamDecl mb_cls (FamilyDecl { fdLName = tycon, fdTyVars = tyvars
rn_info DataFamily = return (DataFamily, emptyFVs)
rnFamResultSig :: HsDocContext
-> [Name] -- kind variables already in scope
-> FamilyResultSig GhcPs
-> RnM (FamilyResultSig GhcRn, FreeVars)
rnFamResultSig _ _ NoSig
rnFamResultSig _ NoSig
= return (NoSig, emptyFVs)
rnFamResultSig doc _ (KindSig kind)
rnFamResultSig doc (KindSig kind)
= do { (rndKind, ftvs) <- rnLHsKind doc kind
; return (KindSig rndKind, ftvs) }
rnFamResultSig doc kv_names (TyVarSig tvbndr)
rnFamResultSig doc (TyVarSig tvbndr)
= do { -- `TyVarSig` tells us that user named the result of a type family by
-- writing `= tyvar` or `= (tyvar :: kind)`. In such case we want to
-- be sure that the supplied result name is not identical to an
......@@ -1894,12 +1884,9 @@ rnFamResultSig doc kv_names (TyVarSig tvbndr)
] $$
text "shadows an already bound type variable")
; bindLHsTyVarBndr doc Nothing -- this might be a lie, but it's used for
; bindLHsTyVarBndr doc Nothing -- This might be a lie, but it's used for
-- scoping checks that are irrelevant here
(mkNameSet kv_names) emptyNameSet
-- use of emptyNameSet here avoids
-- redundant duplicate errors
tvbndr $ \ _ _ tvbndr' ->
tvbndr $ \ tvbndr' ->
return (TyVarSig tvbndr', unitFV (hsLTyVarName tvbndr')) }
-- Note [Renaming injectivity annotation]
......@@ -2030,11 +2017,15 @@ rnConDecl decl@(ConDeclH98 { con_name = name, con_qvars = qtvs
, con_doc = mb_doc })
= do { _ <- addLocM checkConName name
; new_name <- lookupLocatedTopBndrRn name
; let doc = ConDeclCtx [new_name]
; mb_doc' <- rnMbLHsDoc mb_doc
; (kvs, qtvs') <- get_con_qtvs (hsConDeclArgTys details)
; bindHsQTyVars doc (Just $ inHsDocContext doc) Nothing kvs qtvs' $
; let doc = ConDeclCtx [new_name]
qtvs' = qtvs `orElse` mkHsQTvs []
body_kvs = [] -- Consider data T a = forall (b::k). MkT (...)
-- The 'k' will already be in scope from the
-- bindHsQTyVars for the entire DataDecl
-- So there can be no new body_kvs here
; bindHsQTyVars doc (Just $ inHsDocContext doc) Nothing body_kvs qtvs' $
\new_tyvars _ -> do
{ (new_context, fvs1) <- case mcxt of
Nothing -> return (Nothing,emptyFVs)
......@@ -2043,8 +2034,7 @@ rnConDecl decl@(ConDeclH98 { con_name = name, con_qvars = qtvs
; (new_details, fvs2) <- rnConDeclDetails (unLoc new_name) doc details
; let (new_details',fvs3) = (new_details,emptyFVs)
; traceRn "rnConDecl" (ppr name <+> vcat
[ text "free_kvs:" <+> ppr kvs
, text "qtvs:" <+> ppr qtvs
[ text "qtvs:" <+> ppr qtvs
, text "qtvs':" <+> ppr qtvs' ])
; let all_fvs = fvs1 `plusFV` fvs2 `plusFV` fvs3
new_tyvars' = case qtvs of
......@@ -2054,18 +2044,6 @@ rnConDecl decl@(ConDeclH98 { con_name = name, con_qvars = qtvs
, con_cxt = new_context, con_details = new_details'
, con_doc = mb_doc' },
all_fvs) }}
where
cxt = maybe [] unLoc mcxt
get_rdr_tvs tys = extractHsTysRdrTyVars (cxt ++ tys)
get_con_qtvs :: [LHsType GhcPs]
-> RnM ([Located RdrName], LHsQTyVars GhcPs)
get_con_qtvs arg_tys
| Just tvs <- qtvs -- data T = forall a. MkT (a -> a)
= do { free_vars <- get_rdr_tvs arg_tys
; return (freeKiTyVarsKindVars free_vars, tvs) }
| otherwise -- data T = MkT (a -> a)
= return ([], mkHsQTvs [])
rnConDecl decl@(ConDeclGADT { con_names = names, con_type = ty
, con_doc = mb_doc })
......
This diff is collapsed.
<interactive>:2:1: error:
Kind variable ‘k’ is implicitly bound in data type
‘D1’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it explicitly somewhere?
• Kind variable ‘k’ is implicitly bound in data type
‘D1’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it explicitly somewhere?
Type variables with inferred kinds: (k :: *)
• In the data declaration for ‘D1’
SimpleFail6.hs:6:10: error:
SimpleFail6.hs:7:11: error:
Conflicting definitions for ‘a’
Bound at: SimpleFail6.hs:6:10
Bound at: SimpleFail6.hs:7:11
SimpleFail6.hs:7:13
{-# LANGUAGE RankNTypes, KindSignatures #-}
module Foo where
import Data.Proxy
-- Should be illegal without PolyKinds
f :: forall (a :: k). Proxy a
f = f
BadKindVar.hs:8:1: error:
Unexpected kind variable ‘k’ Perhaps you intended to use PolyKinds
In the type signature for ‘f’
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module T13738 where
import Data.Coerce
import Data.Proxy
foo x = coerce @(forall (a :: k). Proxy a -> Int)
@(forall (a :: k). Proxy a -> Int)
x
T13738.hs:12:31: error: Not in scope: type variable ‘k’
T13738.hs:13:31: error: Not in scope: type variable ‘k’
T7404.hs:4:32: error:
Type variable ‘x’ used in a kind.
Did you mean to use TypeInType?
the declaration for type family ‘Foo’
Variable ‘x’ used as both a kind and a type
Did you intend to use TypeInType?
......@@ -164,3 +164,5 @@ test('T13555', normal, compile_fail, [''])
test('T13659', normal, compile_fail, [''])
test('T13625', normal, compile_fail, [''])
test('T14110', normal, compile_fail, [''])
test('BadKindVar', normal, compile_fail, [''])
test('T13738', normal, compile_fail, [''])
T11592.hs:5:9:
Variable ‘a’ is used in the kind signature of its
declaration as a type variable.
the data type declaration for ‘A’
T11592.hs:7:11:
Variable ‘a’ is used in the kind signature of its
declaration as a type variable.
the data type declaration for ‘B’
T11592.hs:5:14: error: Not in scope: type variable ‘a’
T11592.hs:8:11:
Variable ‘a’ is used in the kind signature of its
declaration as a type variable.
the data type declaration for ‘C’
T11592.hs:7:16: error: Not in scope: type variable ‘a’
T11592.hs:10:13:
Variable ‘a’ is used in the kind signature of its
declaration as a type variable.
the data type declaration for ‘D’
T11592.hs:8:18: error: Not in scope: type variable ‘a’
T11592.hs:10:20: error: Not in scope: type variable ‘a’
......@@ -7,7 +7,7 @@ T11963.hs:16:22: error:
Variable ‘k’ used as both a kind and a type
Did you intend to use TypeInType?
T11963.hs:20:15: error:
T11963.hs:20:31: error:
Variable ‘k’ used as both a kind and a type
Did you intend to use TypeInType?
......@@ -15,6 +15,6 @@ T11963.hs:24:32: error:
Variable ‘k’ used as both a kind and a type
Did you intend to use TypeInType?
T11963.hs:28:33: error:
T11963.hs:28:51: error:
Variable ‘k’ used as both a kind and a type
Did you intend to use TypeInType?
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