Commit 7e19610c authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari
Browse files

Refactor the kind-checking of tyvar binders

The refactoring here is driven by the ghastly mess described in
comment:24 of Trac #1520.  The overall goal is to simplify the
kind-checking of typev-variable binders, and in particular to narrow
the use of the "in-scope tyvar binder" stuff,
which is needed only for associated types: see the new
Note [Kind-checking tyvar binders for associated types] in TcHsType.

Now

* The "in-scope tyvar binder" stuff is done only in
     - kcLHsQTyVars, which is used for the LHsQTyVars of a
       data/newtype, or type family declaration.

     - tcFamTyPats, which is used for associated family instances;
       it now calls tcImplicitQTKBndrs, which in turn usese
       newFlexiKindedQTyVar

* tcExpicitTKBndrs (which is used only for function signatures,
  data con signatures, pattern synonym signatures, and expression
  type signatures) now does not go via the "in-scope tyvar binder"
  stuff at all.

While I'm still not happy with all this code, the code is generally
simpler, and I think this is a useful step forward. It does cure
the problem too.

(It's hard to trigger the problem in vanilla Haskell code, because
the renamer would normally use different names for nested binders,
so I can't offer a test.)

(cherry picked from commit 9fc40c73)
parent 61adfbe6
......@@ -516,17 +516,11 @@ data TyClDecl pass
-- 'ApiAnnotation.AnnWhere',
-- For details on above see note [Api annotations] in ApiAnnotation
DataDecl { tcdDExt :: XDataDecl pass -- ^ Post renamer, CUSK flag, FVs
, tcdLName :: Located (IdP pass) -- ^ Type constructor
, tcdTyVars :: LHsQTyVars pass -- ^ Type variables; for an
-- associated type
-- these include outer binders
-- Eg class T a where
-- type F a :: *
-- type F a = a -> a
-- Here the type decl for 'f'
-- includes 'a' in its tcdTyVars
, tcdFixity :: LexicalFixity -- ^ Fixity used in the declaration
DataDecl { tcdDExt :: XDataDecl pass -- ^ Post renamer, CUSK flag, FVs
, tcdLName :: Located (IdP pass) -- ^ Type constructor
, tcdTyVars :: LHsQTyVars pass -- ^ Type variables
-- See Note [TyVar binders for associated declarations]
, tcdFixity :: LexicalFixity -- ^ Fixity used in the declaration
, tcdDataDefn :: HsDataDefn pass }
| ClassDecl { tcdCExt :: XClassDecl pass, -- ^ Post renamer, FVs
......@@ -539,8 +533,7 @@ data TyClDecl pass
tcdSigs :: [LSig pass], -- ^ Methods' signatures
tcdMeths :: LHsBinds pass, -- ^ Default methods
tcdATs :: [LFamilyDecl pass], -- ^ Associated types;
tcdATDefs :: [LTyFamDefltEqn pass],
-- ^ Associated type defaults
tcdATDefs :: [LTyFamDefltEqn pass], -- ^ Associated type defaults
tcdDocs :: [LDocDecl] -- ^ Haddock docs
}
-- ^ - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnClass',
......@@ -558,6 +551,27 @@ data DataDeclRn = DataDeclRn
, tcdFVs :: NameSet }
deriving Data
{- Note [TyVar binders for associated decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For an /associated/ data, newtype, or type-family decl, the LHsQTyVars
/includes/ outer binders. For example
class T a where
data D a c
type F a b :: *
type F a b = a -> a
Here the data decl for 'D', and type-family decl for 'F', both include 'a'
in their LHsQTyVars (tcdTyVars and fdTyVars resp).
Ditto any implicit binders in the hsq_implicit field of the LHSQTyVars.
The idea is that the associated type is really a top-level decl in its
own right. However we are careful to use the same name 'a', so that
we can match things up.
c.f. Note [Associated type tyvar names] in Class.hs
Note [Family instance declaration binders]
-}
type instance XFamDecl (GhcPass _) = NoExt
type instance XSynDecl GhcPs = NoExt
......@@ -966,6 +980,7 @@ data FamilyDecl pass = FamilyDecl
, fdInfo :: FamilyInfo pass -- type/data, closed/open
, fdLName :: Located (IdP pass) -- type constructor
, fdTyVars :: LHsQTyVars pass -- type variables
-- See Note [TyVar binders for associated declarations]
, fdFixity :: LexicalFixity -- Fixity used in the declaration
, fdResultSig :: LFamilyResultSig pass -- result signature
, fdInjectivityAnn :: Maybe (LInjectivityAnn pass) -- optional injectivity ann
......@@ -1490,6 +1505,8 @@ HsImplicitBndrs in FamInstEqn. Note in particular
For associated type family default instances (TyFamDefltEqn), instead of using
type patterns with binders in a surrounding HsImplicitBndrs, we use raw type
variables (LHsQTyVars) in the feqn_pats field of FamEqn.
c.f. Note [TyVar binders for associated declarations]
-}
-- | Type Family Instance Equation
......
......@@ -19,7 +19,7 @@ module TcHsType (
tcHsDeriv, tcDerivStrategy,
tcHsTypeApp,
UserTypeCtxt(..),
tcImplicitTKBndrs, tcImplicitTKBndrsX,
tcImplicitTKBndrs, tcImplicitQTKBndrs,
tcExplicitTKBndrs,
kcExplicitTKBndrs, kcImplicitTKBndrs,
......@@ -32,7 +32,7 @@ module TcHsType (
-- Kind-checking types
-- No kind generalisation, no checkValidType
kcLHsQTyVars, kcLHsTyVarBndrs,
kcLHsQTyVars,
tcWildCardBinders,
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
......@@ -1605,16 +1605,16 @@ kcLHsQTyVars name flav cusk
, hsq_explicit = hs_tvs }) thing_inside
| cusk
= do { (scoped_kvs, (tc_tvs, (res_kind, stuff)))
<- solveEqualities $
tcImplicitTKBndrsX newSkolemTyVar skol_info kv_ns $
kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
<- solveEqualities $
tcImplicitQTKBndrs skol_info kv_ns $
kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
-- Now, because we're in a CUSK, quantify over the mentioned
-- kind vars, in dependency order.
; let tc_binders_unzonked = zipWith mk_tc_binder hs_tvs tc_tvs
; dvs <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys scoped_kvs $
mkTyConKind tc_binders_unzonked res_kind)
; qkvs <- quantifyTyVars emptyVarSet dvs
; dvs <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys scoped_kvs $
mkTyConKind tc_binders_unzonked res_kind)
; qkvs <- quantifyTyVars emptyVarSet dvs
-- don't call tcGetGlobalTyCoVars. For associated types, it gets the
-- tyvars from the enclosing class -- but that's wrong. We *do* want
-- to quantify over those tyvars.
......@@ -1658,7 +1658,7 @@ kcLHsQTyVars name flav cusk
-- Why kcImplicitTKBndrs which uses newSigTyVar?
-- See Note [Kind generalisation and sigTvs]
<- kcImplicitTKBndrs kv_ns $
kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
; let -- NB: Don't add scoped_kvs to tyConTyVars, because they
-- must remain lined up with the binders
......@@ -1685,25 +1685,25 @@ kcLHsQTyVars name flav cusk
kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
kcLHsTyVarBndrs :: Bool -- True <=> bump the TcLevel when bringing vars into scope
-> Bool -- True <=> Default un-annotated tyvar
-- binders to kind *
-> SkolemInfo
-> [LHsTyVarBndr GhcRn]
-> TcM r
-> TcM ([TyVar], r)
kcLHsQTyVarBndrs :: Bool -- True <=> bump the TcLevel when bringing vars into scope
-> Bool -- True <=> Default un-annotated tyvar
-- binders to kind *
-> SkolemInfo
-> [LHsTyVarBndr GhcRn]
-> TcM r
-> TcM ([TyVar], r)
-- There may be dependency between the explicit "ty" vars.
-- So, we have to handle them one at a time.
kcLHsTyVarBndrs _ _ _ [] thing
kcLHsQTyVarBndrs _ _ _ [] thing
= do { stuff <- thing; return ([], stuff) }
kcLHsTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
kcLHsQTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
= do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
-- NB: Bring all tvs into scope, even non-dependent ones,
-- as they're needed in type synonyms, data constructors, etc.
; (tvs, stuff) <- bind_unless_scoped tv_pair $
kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs $
kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs $
thing
; return ( tv : tvs, stuff ) }
......@@ -1720,37 +1720,83 @@ kcLHsTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
-- `dependent` testsuite directory.
kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
kc_hs_tv (UserTyVar _ lname@(L _ name))
= do { tv_pair@(tv, in_scope) <- tcHsTyVarName newSkolemTyVar Nothing name
-- Special handling for the case where the binder is already in scope
-- See Note [Associated type tyvar names] in Class and
-- Note [TyVar binders for associated decls] in HsDecls
kc_hs_tv (UserTyVar _ (L _ name))
= do { mb_tv <- tcLookupLcl_maybe name
; case mb_tv of -- See Note [TyVar binders for associated decls]
Just (ATyVar _ tv) -> return (tv, True)
_ -> do { kind <- if open_fam
then return liftedTypeKind
else newMetaKindVar
-- Open type/data families default their variables
-- variables to kind *. But don't default in-scope
-- class tyvars, of course
; tv <- newSkolemTyVar name kind
; return (tv, False) } }
kc_hs_tv (KindedTyVar _ lname@(L _ name) lhs_kind)
= do { kind <- tcLHsKindSig (TyVarBndrKindCtxt name) lhs_kind
; mb_tv <- tcLookupLcl_maybe name
; case mb_tv of
Just (ATyVar _ tv)
-> do { discardResult $
unifyKind (Just (HsTyVar noExt NotPromoted lname))
kind (tyVarKind tv)
; return (tv, True) }
_ -> do { tv <- newSkolemTyVar name kind
; return (tv, False) } }
-- Open type/data families default their variables to kind *.
-- But don't default in-scope class tyvars, of course
; when (open_fam && not in_scope) $
discardResult $ unifyKind (Just (HsTyVar noExt NotPromoted lname))
liftedTypeKind (tyVarKind tv)
kc_hs_tv (XTyVarBndr{}) = panic "kc_hs_tv"
; return tv_pair }
{- Note [Kind-checking tyvar binders for associated types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When kind-checking the type-variable binders for associated
data/newtype decls
family decls
we behave specially for type variables that are already in scope;
that is, bound by the enclosing class decl. This is done in
kcLHsQTyVarBndrs:
* The use of tcImplicitQTKBndrs
* The tcLookupLocal_maybe code in kc_hs_tv
See Note [Associated type tyvar names] in Class and
Note [TyVar binders for associated decls] in HsDecls
We must do the same for family instance decls, where the in-scope
variables may be bound by the enclosing class instance decl.
Hence the use of tcImplicitQTKBndrs in tcFamTyPats.
-}
kc_hs_tv (KindedTyVar _ (L _ name) lhs_kind)
= do { kind <- tcLHsKindSig (TyVarBndrKindCtxt name) lhs_kind
; tcHsTyVarName newSkolemTyVar (Just kind) name }
kc_hs_tv (XTyVarBndr{}) = panic "kc_hs_tv"
--------------------------------------
-- Implicit binders
--------------------------------------
tcImplicitTKBndrs :: SkolemInfo
-> [Name]
-- | Bring implicitly quantified type/kind variables into scope during
-- kind checking. Uses SigTvs, as per Note [Use SigTvs in kind-checking pass]
-- in TcTyClsDecls.
kcImplicitTKBndrs :: [Name] -- of the vars
-> TcM a
-> TcM ([TcTyVar], a)
tcImplicitTKBndrs = tcImplicitTKBndrsX newSkolemTyVar
-> TcM ([TcTyVar], a) -- returns the tyvars created
-- these are *not* dependency ordered
kcImplicitTKBndrs var_ns thing_inside
= do { tkvs <- mapM newFlexiKindedSigTyVar var_ns
; result <- tcExtendTyVarEnv tkvs thing_inside
; return (tkvs, result) }
-- | Like 'tcImplicitTKBndrs', but uses 'newSigTyVar' to create tyvars
tcImplicitTKBndrsSig :: SkolemInfo
-> [Name]
-> TcM a
-> TcM ([TcTyVar], a)
tcImplicitTKBndrsSig = tcImplicitTKBndrsX newSigTyVar
tcImplicitTKBndrs, tcImplicitTKBndrsSig, tcImplicitQTKBndrs
:: SkolemInfo
-> [Name]
-> TcM a
-> TcM ([TcTyVar], a)
tcImplicitTKBndrs = tcImplicitTKBndrsX newFlexiKindedSkolemTyVar
tcImplicitTKBndrsSig = tcImplicitTKBndrsX newFlexiKindedSigTyVar
tcImplicitQTKBndrs = tcImplicitTKBndrsX newFlexiKindedQTyVar
tcImplicitTKBndrsX :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
tcImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function
-> SkolemInfo
-> [Name]
-> TcM a
......@@ -1774,12 +1820,9 @@ tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside
= do { (skol_tvs, result)
<- solveLocalEqualities $
checkTvConstraints skol_info Nothing $
do { tv_pairs <- mapM (tcHsTyVarName new_tv Nothing) tv_names
; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ]
; result <- tcExtendTyVarEnv must_scope_tvs $
thing_inside
; return (map fst tv_pairs, result) }
do { tkvs <- mapM new_tv tv_names
; result <- tcExtendTyVarEnv tkvs thing_inside
; return (tkvs, result) }
; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
-- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
......@@ -1788,26 +1831,59 @@ tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside
; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs)
; return (final_tvs, result) }
-- | Bring implicitly quantified type/kind variables into scope during
-- kind checking. Uses SigTvs, as per Note [Use SigTvs in kind-checking pass]
-- in TcTyClsDecls.
kcImplicitTKBndrs :: [Name] -- of the vars
newFlexiKindedQTyVar :: Name -> TcM TcTyVar
-- Make a new skolem for an implicit binder in a type/class/type
-- instance declaration, with a flexi-kind
-- But check for in-scope-ness, and if so return that instead
newFlexiKindedQTyVar name
= do { mb_tv <- tcLookupLcl_maybe name
; case mb_tv of
Just (ATyVar _ tv) -> return tv
_ -> newFlexiKindedSkolemTyVar name }
newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar
newFlexiKindedTyVar new_tv name
= do { kind <- newMetaKindVar
; new_tv name kind }
newFlexiKindedSkolemTyVar :: Name -> TcM TyVar
newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
newFlexiKindedSigTyVar :: Name -> TcM TyVar
newFlexiKindedSigTyVar = newFlexiKindedTyVar newSigTyVar
--------------------------------------
-- Explicit binders
--------------------------------------
-- | Used during the "kind-checking" pass in TcTyClsDecls only,
-- and even then only for data-con declarations.
-- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
kcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
-> TcM a
-> TcM ([TcTyVar], a) -- returns the tyvars created
-- these are *not* dependency ordered
kcImplicitTKBndrs var_ns thing_inside
= do { tkvs_pairs <- mapM (tcHsTyVarName newSigTyVar Nothing) var_ns
; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ]
; result <- tcExtendTyVarEnv must_scope_tkvs $
thing_inside
; return (map fst tkvs_pairs, result) }
-> TcM a
kcExplicitTKBndrs [] thing_inside = thing_inside
kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
= do { tv <- tcHsTyVarBndr newSigTyVar hs_tv
; tcExtendTyVarEnv [tv] $
kcExplicitTKBndrs hs_tvs thing_inside }
tcExplicitTKBndrs :: SkolemInfo
-> [LHsTyVarBndr GhcRn]
-> TcM a
-> TcM ([TcTyVar], a)
-- See also Note [Associated type tyvar names] in Class
tcExplicitTKBndrs skol_info hs_tvs thing_inside
-- Used for the forall'd binders in type signatures of various kinds:
-- - function signatures
-- - data con signatures in GADT-style decls
-- - pattern synonym signatures
-- - expression type signatures
--
-- Specifically NOT used for the binders of a data type
-- or type family decl. So the forall'd variables always /shadow/
-- anything already in scope, and the complications of
-- tcHsQTyVarName to not apply.
--
-- This function brings into scope a telescope of binders as written by
-- the user. At first blush, it would then seem that we should bring
-- them into scope one at a time, bumping the TcLevel each time.
......@@ -1839,46 +1915,29 @@ tcExplicitTKBndrs skol_info hs_tvs thing_inside
bind_tvbs [] = do { result <- thing_inside
; return ([], result) }
bind_tvbs (L _ tvb : tvbs)
= do { (tv, in_scope) <- tcHsTyVarBndr newSkolemTyVar tvb
; (if in_scope then id else tcExtendTyVarEnv [tv]) $
do { (tvs, result) <- bind_tvbs tvbs
; return (tv : tvs, result) }}
= do { tv <- tcHsTyVarBndr newSkolemTyVar tvb
; tcExtendTyVarEnv [tv] $
do { (tvs, result) <- bind_tvbs tvbs
; return (tv : tvs, result) }}
doc = sep (map ppr hs_tvs)
-- | Used during the "kind-checking" pass in TcTyClsDecls only.
-- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
kcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
-> TcM a
-> TcM a
kcExplicitTKBndrs [] thing_inside = thing_inside
kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
= do { (tv, _) <- tcHsTyVarBndr newSigTyVar hs_tv
; tcExtendTyVarEnv [tv] $
kcExplicitTKBndrs hs_tvs thing_inside }
-----------------
tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
-> HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
-> HsTyVarBndr GhcRn -> TcM TcTyVar
-- Return a TcTyVar, built using the provided function
-- Typically the Kind inside the HsTyVarBndr will be a tyvar
-- with a mutable kind in it.
--
-- These variables might be in scope already (with associated types, for example).
-- This function then checks that the kind annotation (if any) matches the
-- kind of the in-scope type variable.
--
-- Returned TcTyVar has the same name; no cloning
--
-- See also Note [Associated type tyvar names] in Class
--
-- Returns True iff the tyvar was already in scope
tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm))
= tcHsTyVarName new_tv Nothing tv_nm
= newFlexiKindedTyVar new_tv tv_nm
tcHsTyVarBndr new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
= do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
; tcHsTyVarName new_tv (Just kind) tv_nm }
; new_tv tv_nm kind }
tcHsTyVarBndr _ (XTyVarBndr _) = panic "tcHsTyVarBndr"
-----------------
newWildTyVar :: Name -> TcM TcTyVar
-- ^ New unification variable for a wildcard
newWildTyVar _name
......@@ -1890,31 +1949,6 @@ newWildTyVar _name
; traceTc "newWildTyVar" (ppr tyvar)
; return tyvar }
-- | Produce a tyvar of the given name (with the kind provided, or
-- otherwise a meta-var kind). If
-- the name is already in scope, return the scoped variable, checking
-- to make sure the known kind matches any kind provided. The
-- second return value says whether the variable is in scope (True)
-- or not (False). (Use this for associated types, for example.)
tcHsTyVarName :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
-> Maybe Kind -- Just k <=> use k as the variable's kind
-- Nothing <=> use a meta-tyvar
-> Name -> TcM (TcTyVar, Bool)
tcHsTyVarName new_tv m_kind name
= do { mb_tv <- tcLookupLcl_maybe name
; case mb_tv of
Just (ATyVar _ tv)
-> do { whenIsJust m_kind $ \ kind ->
discardResult $
unifyKind (Just (HsTyVar noExt NotPromoted (noLoc name)))
kind (tyVarKind tv)
; return (tv, True) }
_ -> do { kind <- case m_kind of
Just kind -> return kind
Nothing -> newMetaKindVar
; tv <- new_tv name kind
; return (tv, False) }}
--------------------------
-- Bringing tyvars into scope
--------------------------
......
......@@ -1615,7 +1615,8 @@ tcFamTyPats fam_tc mb_clsinfo
; (fam_used_tvs, (typats, (more_typats, res_kind)))
<- solveEqualities $ -- See Note [Constraints in patterns]
tcImplicitTKBndrs FamInstSkol tv_names $
tcImplicitQTKBndrs FamInstSkol tv_names $
-- See Note [Kind-checking tyvar binders for associated types]
do { let loc = nameSrcSpan fam_name
lhs_fun = L loc (HsTyVar noExt NotPromoted
(L loc fam_name))
......
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