Commit a50244c6 authored by Joachim Breitner's avatar Joachim Breitner

Rename SigTv to TyVarTv (#15480)

because since #15050, these are no longer used in pattern SIGnatures,
but still in other places where meta-variables should only be unified
with TYpe VARiables.

I also found mentions of `SigTv` in parts of the renamer and desugarer
that do not seem to directly relate to `SigTv` as used in the type
checker, but rather to uses of `forall a.` in type signatures. I renamed
these to `ScopedTv`.

Differential Revision: https://phabricator.haskell.org/D5074
parent 5238f204
......@@ -122,7 +122,7 @@ repTopDs group@(HsGroup { hs_valds = valds
, hs_annds = annds
, hs_ruleds = ruleds
, hs_docs = docs })
= do { let { bndrs = hsSigTvBinders valds
= do { let { bndrs = hsScopedTvBinders valds
++ hsGroupBinders group
++ hsPatSynSelectors valds
; instds = tyclds >>= group_instds } ;
......@@ -180,9 +180,9 @@ repTopDs group@(HsGroup { hs_valds = valds
= notHandledL loc "Haddock documentation" empty
repTopDs (XHsGroup _) = panic "repTopDs"
hsSigTvBinders :: HsValBinds GhcRn -> [Name]
hsScopedTvBinders :: HsValBinds GhcRn -> [Name]
-- See Note [Scoped type variables in bindings]
hsSigTvBinders binds
hsScopedTvBinders binds
= concatMap get_scoped_tvs sigs
where
sigs = case binds of
......@@ -222,7 +222,7 @@ Here the 'forall a' brings 'a' into scope over the binding group.
To achieve this we
a) Gensym a binding for 'a' at the same time as we do one for 'f'
collecting the relevant binders with hsSigTvBinders
collecting the relevant binders with hsScopedTvBinders
b) When processing the 'forall', don't gensym
......@@ -1484,12 +1484,12 @@ repBinds (EmptyLocalBinds _)
repBinds b@(HsIPBinds {}) = notHandled "Implicit parameters" (ppr b)
repBinds (HsValBinds _ decs)
= do { let { bndrs = hsSigTvBinders decs ++ collectHsValBinders decs }
= do { let { bndrs = hsScopedTvBinders decs ++ collectHsValBinders decs }
-- No need to worry about detailed scopes within
-- the binding group, because we are talking Names
-- here, so we can safely treat it as a mutually
-- recursive group
-- For hsSigTvBinders see Note [Scoped type variables in bindings]
-- For hsScopedTvBinders see Note [Scoped type variables in bindings]
; ss <- mkGenSyms bndrs
; prs <- addBinds ss (rep_val_binds decs)
; core_list <- coreList decQTyConName
......
......@@ -296,7 +296,7 @@ rnValBindsRHS :: HsSigCtxt
rnValBindsRHS ctxt (ValBinds _ mbinds sigs)
= do { (sigs', sig_fvs) <- renameSigs ctxt sigs
; binds_w_dus <- mapBagM (rnLBind (mkSigTvFn sigs')) mbinds
; binds_w_dus <- mapBagM (rnLBind (mkScopedTvFn sigs')) mbinds
; let !(anal_binds, anal_dus) = depAnalBinds binds_w_dus
; let patsyn_fvs = foldr (unionNameSet . psb_ext) emptyNameSet $
......@@ -581,21 +581,21 @@ depAnalBinds binds_w_dus
---------------------
-- Bind the top-level forall'd type variables in the sigs.
-- E.g f :: a -> a
-- E.g f :: forall a. a -> a
-- f = rhs
-- The 'a' scopes over the rhs
--
-- NB: there'll usually be just one (for a function binding)
-- but if there are many, one may shadow the rest; too bad!
-- e.g x :: [a] -> [a]
-- y :: [(a,a)] -> a
-- e.g x :: forall a. [a] -> [a]
-- y :: forall a. [(a,a)] -> a
-- (x,y) = e
-- In e, 'a' will be in scope, and it'll be the one from 'y'!
mkSigTvFn :: [LSig GhcRn] -> (Name -> [Name])
mkScopedTvFn :: [LSig GhcRn] -> (Name -> [Name])
-- Return a lookup function that maps an Id Name to the names
-- of the type variables that should scope over its body.
mkSigTvFn sigs = \n -> lookupNameEnv env n `orElse` []
mkScopedTvFn sigs = \n -> lookupNameEnv env n `orElse` []
where
env = mkHsSigEnv get_scoped_tvs sigs
......@@ -663,9 +663,9 @@ rnPatSynBind sig_fn bind@(PSB { psb_id = L l name
-- invariant: no free vars here when it's a FunBind
= do { pattern_synonym_ok <- xoptM LangExt.PatternSynonyms
; unless pattern_synonym_ok (addErr patternSynonymErr)
; let sig_tvs = sig_fn name
; let scoped_tvs = sig_fn name
; ((pat', details'), fvs1) <- bindSigTyVarsFV sig_tvs $
; ((pat', details'), fvs1) <- bindSigTyVarsFV scoped_tvs $
rnPat PatSyn pat $ \pat' ->
-- We check the 'RdrName's instead of the 'Name's
-- so that the binding locations are reported
......@@ -700,7 +700,7 @@ rnPatSynBind sig_fn bind@(PSB { psb_id = L l name
Unidirectional -> return (Unidirectional, emptyFVs)
ImplicitBidirectional -> return (ImplicitBidirectional, emptyFVs)
ExplicitBidirectional mg ->
do { (mg', fvs) <- bindSigTyVarsFV sig_tvs $
do { (mg', fvs) <- bindSigTyVarsFV scoped_tvs $
rnMatchGroup (mkPrefixFunRhs (L l name))
rnLExpr mg
; return (ExplicitBidirectional mg', fvs) }
......@@ -867,7 +867,7 @@ rnMethodBinds is_cls_decl cls ktv_names binds sigs
-- Answer no in Haskell 2010, but yes if you have -XScopedTypeVariables
; scoped_tvs <- xoptM LangExt.ScopedTypeVariables
; (binds'', bind_fvs) <- maybe_extend_tyvar_env scoped_tvs $
do { binds_w_dus <- mapBagM (rnLBind (mkSigTvFn other_sigs')) binds'
do { binds_w_dus <- mapBagM (rnLBind (mkScopedTvFn other_sigs')) binds'
; let bind_fvs = foldrBag (\(_,_,fv1) fv2 -> fv1 `plusFV` fv2)
emptyFVs binds_w_dus
; return (mapBag fstOf3 binds_w_dus, bind_fvs) }
......
......@@ -941,12 +941,12 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
, sig_inst_theta = annotated_theta
, sig_inst_skols = annotated_tvs }))
= -- Choose quantifiers for a partial type signature
do { psig_qtv_prs <- zonkSigTyVarPairs annotated_tvs
do { psig_qtv_prs <- zonkTyVarTyVarPairs annotated_tvs
-- Check whether the quantified variables of the
-- partial signature have been unified together
-- See Note [Quantified variables in partial type signatures]
; mapM_ report_dup_sig_tv_err (findDupSigTvs psig_qtv_prs)
; mapM_ report_dup_tyvar_tv_err (findDupTyVarTvs psig_qtv_prs)
-- Check whether a quantified variable of the partial type
-- signature is not actually quantified. How can that happen?
......@@ -969,7 +969,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
; return (final_qtvs, my_theta) }
where
report_dup_sig_tv_err (n1,n2)
report_dup_tyvar_tv_err (n1,n2)
| PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
= addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1)
<+> text "with" <+> quotes (ppr n2))
......@@ -977,7 +977,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
| otherwise -- Can't happen; by now we know it's a partial sig
= pprPanic "report_sig_tv_err" (ppr sig)
= pprPanic "report_tyvar_tv_err" (ppr sig)
report_mono_sig_tv_err n
| PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
......@@ -985,7 +985,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
2 (hang (text "bound by the partial type signature:")
2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
| otherwise -- Can't happen; by now we know it's a partial sig
= pprPanic "report_sig_tv_err" (ppr sig)
= pprPanic "report_mono_sig_tv_err" (ppr sig)
choose_psig_context :: VarSet -> TcThetaType -> Maybe TcType
-> TcM (VarSet, TcThetaType)
......@@ -1136,7 +1136,7 @@ Consider
g x y = [x, y]
Here, 'f' and 'g' are mutually recursive, and we end up unifying 'a' and 'b'
together, which is fine. So we bind 'a' and 'b' to SigTvs, which can then
together, which is fine. So we bind 'a' and 'b' to TyVarTvs, which can then
unify with each other.
But now consider:
......
......@@ -1993,10 +1993,10 @@ canEqTyVarTyVar, are these
number) on the left, so there is the best chance of unifying it
alpha[3] ~ beta[2]
* If both are meta-tyvars and both at the same level, put a SigTv
* If both are meta-tyvars and both at the same level, put a TyVarTv
on the right if possible
alpha[2] ~ beta[2](sig-tv)
That way, when we unify alpha := beta, we don't lose the SigTv flag.
That way, when we unify alpha := beta, we don't lose the TyVarTv flag.
* Put a meta-tv with a System Name on the left if possible so it
gets eliminated (improves error messages)
......
......@@ -635,8 +635,8 @@ isSkolemTy :: TcLevel -> Type -> Bool
isSkolemTy tc_lvl ty
| Just tv <- getTyVar_maybe ty
= isSkolemTyVar tv
|| (isSigTyVar tv && isTouchableMetaTyVar tc_lvl tv)
-- The last case is for touchable SigTvs
|| (isTyVarTyVar tv && isTouchableMetaTyVar tc_lvl tv)
-- The last case is for touchable TyVarTvs
-- we postpone untouchables to a latter test (too obscure)
| otherwise
......@@ -1606,7 +1606,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
, isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
-- be oriented the other way round;
-- see TcCanonical.canEqTyVarTyVar
|| isSigTyVar tv1 && not (isTyVarTy ty2)
|| isTyVarTyVar tv1 && not (isTyVarTy ty2)
|| ctEqRel ct == ReprEq
-- the cases below don't really apply to ReprEq (except occurs check)
= mkErrorMsgFromCt ctxt ct $ mconcat
......@@ -1669,7 +1669,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
-- If the immediately-enclosing implication has 'tv' a skolem, and
-- we know by now its an InferSkol kind of skolem, then presumably
-- it started life as a SigTv, else it'd have been unified, given
-- it started life as a TyVarTv, else it'd have been unified, given
-- that there's no occurs-check or forall problem
| (implic:_) <- cec_encl ctxt
, Implic { ic_skols = skols } <- implic
......@@ -1707,7 +1707,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
-- Nastiest case: attempt to unify an untouchable variable
-- So tv is a meta tyvar (or started that way before we
-- generalised it). So presumably it is an *untouchable*
-- meta tyvar or a SigTv, else it'd have been unified
-- meta tyvar or a TyVarTv, else it'd have been unified
-- See Note [Error messages for untouchables]
| (implic:_) <- cec_encl ctxt -- Get the innermost context
, Implic { ic_given = given, ic_tclvl = lvl, ic_info = skol_info } <- implic
......
......@@ -2075,9 +2075,9 @@ unflattenWanteds tv_eqs funeqs
| Just (rhs_tv, co) <- getCastedTyVar_maybe rhs
-- co :: kind(rhs_tv) ~ kind(lhs_tv)
, isFmvTyVar rhs_tv || (isTouchableMetaTyVar tclvl rhs_tv
&& not (isSigTyVar rhs_tv))
&& not (isTyVarTyVar rhs_tv))
-- LHS is a filled fmv, and so is a type
-- family application, which a SigTv should
-- family application, which a TyVarTv should
-- not unify with
= do { is_filled <- isFilledMetaTyVar rhs_tv
; if is_filled then return False
......
......@@ -1367,7 +1367,7 @@ Sidenote: It's quite possible that later, we'll consider (t -> s)
as a degenerate case of some (pi (x :: t) -> s) and then this will
all get more permissive.
Note [Kind generalisation and SigTvs]
Note [Kind generalisation and TyVarTvs]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data T (a :: k1) x = MkT (S a ())
......@@ -1375,14 +1375,14 @@ Consider
While we are doing kind inference for the mutually-recursive S,T,
we will end up unifying k1 and k2 together. So they can't be skolems.
We therefore make them SigTvs, which can unify with type variables,
We therefore make them TyVarTvs, which can unify with type variables,
but not with general types. All this is very similar at the level
of terms: see Note [Quantified variables in partial type signatures]
in TcBinds.
There are some wrinkles
* We always want to kind-generalise over SigTvs, and /not/ default
* We always want to kind-generalise over TyVarTvs, and /not/ default
them to Type. Another way to say this is: a SigTV should /never/
stand for a type, even via defaulting. Hence the check in
TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar. Here's
......@@ -1398,7 +1398,7 @@ There are some wrinkles
Here we will unify k1 with k2, but this time doing so is an error,
because k1 and k2 are bound in the same delcaration.
We sort this out using findDupSigTvs, in TcTyClTyVars; very much
We sort this out using findDupTyVarTvs, in TcTyClTyVars; very much
as we do with partial type signatures in mk_psig_qtvs in
TcBinds.chooseInferredQuantifiers
......@@ -1571,8 +1571,8 @@ kcLHsQTyVars name flav cusk
| otherwise
= do { (scoped_kvs, (tc_tvs, res_kind))
-- Why kcImplicitTKBndrs which uses newSigTyVar?
-- See Note [Kind generalisation and SigTvs]
-- Why kcImplicitTKBndrs which uses newTyVarTyVar?
-- See Note [Kind generalisation and TyVarTvs]
<- kcImplicitTKBndrs kv_ns $
kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
......@@ -1691,14 +1691,14 @@ Hence the use of tcImplicitQTKBndrs in tcFamTyPats.
--------------------------------------
-- | Bring implicitly quantified type/kind variables into scope during
-- kind checking. Uses SigTvs, as per Note [Use SigTvs in kind-checking pass]
-- kind checking. Uses TyVarTvs, as per Note [Use TyVarTvs in kind-checking pass]
-- in TcTyClsDecls.
kcImplicitTKBndrs :: [Name] -- of the vars
-> TcM a
-> TcM ([TcTyVar], a) -- returns the tyvars created
-- these are *not* dependency ordered
kcImplicitTKBndrs var_ns thing_inside
= do { tkvs <- mapM newFlexiKindedSigTyVar var_ns
= do { tkvs <- mapM newFlexiKindedTyVarTyVar var_ns
; result <- tcExtendTyVarEnv tkvs thing_inside
; return (tkvs, result) }
......@@ -1709,7 +1709,7 @@ tcImplicitTKBndrs, tcImplicitTKBndrsSig, tcImplicitQTKBndrs
-> TcM a
-> TcM ([TcTyVar], a)
tcImplicitTKBndrs = tcImplicitTKBndrsX newFlexiKindedSkolemTyVar
tcImplicitTKBndrsSig = tcImplicitTKBndrsX newFlexiKindedSigTyVar
tcImplicitTKBndrsSig = tcImplicitTKBndrsX newFlexiKindedTyVarTyVar
tcImplicitQTKBndrs = tcImplicitTKBndrsX newFlexiKindedQTyVar
tcImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function
......@@ -1741,7 +1741,7 @@ tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside
; return (tkvs, result) }
; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
-- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
-- use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv
-- do a stable topological sort, following
-- Note [Ordering of implicit variables] in HsTypes
......@@ -1767,8 +1767,8 @@ newFlexiKindedTyVar new_tv name
newFlexiKindedSkolemTyVar :: Name -> TcM TyVar
newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
newFlexiKindedSigTyVar :: Name -> TcM TyVar
newFlexiKindedSigTyVar = newFlexiKindedTyVar newSigTyVar
newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar
--------------------------------------
-- Explicit binders
......@@ -1776,13 +1776,13 @@ newFlexiKindedSigTyVar = newFlexiKindedTyVar newSigTyVar
-- | 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
-- See Note [Use TyVarTvs 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
= do { tv <- tcHsTyVarBndr newTyVarTyVar hs_tv
; tcExtendTyVarEnv [tv] $
kcExplicitTKBndrs hs_tvs thing_inside }
......@@ -2067,7 +2067,7 @@ kcLookupTcTyCon nm
-- Never emits constraints, though the thing_inside might.
kcTyClTyVars :: Name -> TcM a -> TcM a
kcTyClTyVars tycon_name thing_inside
-- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
-- See Note [Use TyVarTvs in kind-checking pass] in TcTyClsDecls
= do { tycon <- kcLookupTcTyCon tycon_name
; tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) $ thing_inside }
......@@ -2097,9 +2097,9 @@ tcTyClTyVars tycon_name thing_inside
; let flav = tyConFlavour tycon
scoped_prs = tcTyConScopedTyVars tycon
scoped_tvs = map snd scoped_prs
still_sig_tvs = filter isSigTyVar scoped_tvs
still_sig_tvs = filter isTyVarTyVar scoped_tvs
; mapM_ report_sig_tv_err (findDupSigTvs scoped_prs)
; mapM_ report_sig_tv_err (findDupTyVarTvs scoped_prs)
; checkNoErrs $ reportFloatingKvs tycon_name flav
scoped_tvs still_sig_tvs
......@@ -2284,7 +2284,7 @@ tcHsPartialSigType ctxt sig_ty
; return (wcs, wcx, theta, tau) }
-- We must return these separately, because all the zonking below
-- might change the name of a SigTv. This, in turn, causes trouble
-- might change the name of a TyVarTv. This, in turn, causes trouble
-- in partial type signatures that bind scoped type variables, as
-- we bring the wrong name into scope in the function body.
-- Test case: partial-sigs/should_compile/LocalDefinitionBug
......@@ -2295,17 +2295,17 @@ tcHsPartialSigType ctxt sig_ty
-- See Note [Extra-constraint holes in partial type signatures]
; emitWildCardHoleConstraints wcs
-- The SigTvs created above will sometimes have too high a TcLevel
-- The TyVarTvs created above will sometimes have too high a TcLevel
-- (note that they are generated *after* bumping the level in
-- the tc{Im,Ex}plicitTKBndrsSig functions. Bumping the level
-- is still important here, because the kinds of these variables
-- do indeed need to have the higher level, so they can unify
-- with other local type variables. But, now that we've type-checked
-- everything (and solved equalities in the tcImplicit call)
-- we need to promote the SigTvs so we don't violate the TcLevel
-- we need to promote the TyVarTvs so we don't violate the TcLevel
-- invariant
; all_tvs <- mapM zonkPromoteTyCoVarBndr (implicit_tvs ++ explicit_tvs)
-- zonkPromoteTyCoVarBndr deals well with SigTvs
-- zonkPromoteTyCoVarBndr deals well with TyVarTvs
; theta <- mapM zonkPromoteType theta
; tau <- zonkPromoteType tau
......@@ -2427,7 +2427,7 @@ tcHsPatSigType ctxt sig_ty
mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
; return (tyVarName tv, tv') }
-- The Name is one of sig_vars, the lexically scoped name
-- But if it's a SigTyVar, it might have been unified
-- But if it's a TyVarTv, it might have been unified
-- with an existing in-scope skolem, so we must zonk
-- here. See Note [Pattern signature binders]
tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType"
......@@ -2470,7 +2470,7 @@ tcPatSig in_pat_bind sig res_ty
-- Here 'a' doesn't get a binding. Sigh
; let bad_tvs = [ tv | (_,tv) <- sig_tvs
, not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
; checkTc (null bad_tvs) (badPatTyVarTvs sig_ty bad_tvs)
-- Now do a subsumption check of the pattern signature against res_ty
; wrap <- addErrCtxtM (mk_msg sig_ty) $
......@@ -2625,8 +2625,8 @@ zonkPromoteTyCoVarKind = updateTyVarKindM zonkPromoteType
zonkPromoteTyCoVarBndr :: TyCoVar -> TcM TyCoVar
zonkPromoteTyCoVarBndr tv
| isSigTyVar tv
= tcGetTyVar "zonkPromoteTyCoVarBndr SigTv" <$> zonkPromoteTcTyVar tv
| isTyVarTyVar tv
= tcGetTyVar "zonkPromoteTyCoVarBndr TyVarTv" <$> zonkPromoteTcTyVar tv
| isTcTyVar tv && isSkolemTyVar tv
= do { tc_lvl <- getTcLevel
......@@ -2699,8 +2699,8 @@ promotionErr name err
************************************************************************
-}
badPatSigTvs :: TcType -> [TyVar] -> SDoc
badPatSigTvs sig_ty bad_tvs
badPatTyVarTvs :: TcType -> [TyVar] -> SDoc
badPatTyVarTvs sig_ty bad_tvs
= vcat [ fsep [text "The type variable" <> plural bad_tvs,
quotes (pprWithCommas ppr bad_tvs),
text "should be bound by the pattern signature" <+> quotes (ppr sig_ty),
......
......@@ -50,8 +50,8 @@ module TcMType (
--------------------------------
-- Instantiation
newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
newMetaSigTyVars, newMetaSigTyVarX,
newSigTyVar, newTauTyVar, newSkolemTyVar, newWildCardX,
newMetaTyVarTyVars, newMetaTyVarTyVarX,
newTyVarTyVar, newTauTyVar, newSkolemTyVar, newWildCardX,
tcInstType,
tcInstSkolTyVars,tcInstSkolTyVarsX,
tcInstSuperSkolTyVarsX,
......@@ -65,7 +65,7 @@ module TcMType (
tidyEvVar, tidyCt, tidySkolemInfo,
skolemiseRuntimeUnk,
zonkTcTyVar, zonkTcTyVars,
zonkTcTyVarToTyVar, zonkSigTyVarPairs,
zonkTcTyVarToTyVar, zonkTyVarTyVarPairs,
zonkTyCoVarsAndFV, zonkTcTypeAndFV,
zonkTyCoVarsAndFVList,
zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
......@@ -621,32 +621,32 @@ instead of the buggous
-}
{-
Note [SigTv]
Note [TyVarTv]
~~~~~~~~~~~~
A SigTv can unify with type *variables* only, including other SigTvs and
A TyVarTv can unify with type *variables* only, including other TyVarTvs and
skolems. Sometimes, they can unify with type variables that the user would
rather keep distinct; see #11203 for an example. So, any client of this
function needs to either allow the SigTvs to unify with each other or check
that they don't (say, with a call to findDubSigTvs).
function needs to either allow the TyVarTvs to unify with each other or check
that they don't (say, with a call to findDubTyVarTvs).
Before #15050 this was used for ScopedTypeVariables in patterns, to make sure
these type variables only refer to other type variables, but this restriction
was dropped, and ScopedTypeVariables can now refer to full types (GHC Proposal
29).
Before #15050 this (under the name SigTv) was used for ScopedTypeVariables in
patterns, to make sure these type variables only refer to other type variables,
but this restriction was dropped, and ScopedTypeVariables can now refer to full
types (GHC Proposal 29).
The remaining uses of newSigTyVars are
* in kind signatures, see Note [Kind generalisation and SigTvs]
and Note [Use SigTvs in kind-checking pass]
The remaining uses of newTyVarTyVars are
* in kind signatures, see Note [Kind generalisation and TyVarTvs]
and Note [Use TyVarTvs in kind-checking pass]
* in partial type signatures, see Note [Quantified variables in partial type signatures]
-}
-- see Note [SigTv]
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
= do { details <- newMetaDetails SigTv
-- see Note [TyVarTv]
newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
newTyVarTyVar name kind
= do { details <- newMetaDetails TyVarTv
; let tyvar = mkTcTyVar name kind details
; traceTc "newSigTyVar" (ppr tyvar)
; traceTc "newTyVarTyVar" (ppr tyvar)
; return tyvar }
......@@ -846,7 +846,7 @@ newAnonMetaTyVar meta_info kind
TauTv -> fsLit "t"
FlatMetaTv -> fsLit "fmv"
FlatSkolTv -> fsLit "fsk"
SigTv -> fsLit "a"
TyVarTv -> fsLit "a"
; details <- newMetaDetails meta_info
; let tyvar = mkTcTyVar name kind details
; traceTc "newAnonMetaTyVar" (ppr tyvar)
......@@ -892,8 +892,8 @@ newOpenFlexiTyVarTy
= do { kind <- newOpenTypeKind
; newFlexiTyVarTy kind }
newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
newMetaTyVarTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst
newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- Instantiate with META type variables
......@@ -914,9 +914,9 @@ newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- Just like newMetaTyVars, but start with an existing substitution.
newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a SigTv
newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a TyVarTv
newMetaTyVarTyVarX subst tyvar = new_meta_tv_x TyVarTv subst tyvar
newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newWildCardX subst tv
......@@ -1102,16 +1102,16 @@ defaultTyVar default_kind tv
| not (isMetaTyVar tv)
= return False
| isSigTyVar tv
-- Do not default SigTvs. Doing so would violate the invariants
-- on SigTvs; see Note [Signature skolems] in TcType.
| isTyVarTyVar tv
-- Do not default TyVarTvs. Doing so would violate the invariants
-- on TyVarTvs; see Note [Signature skolems] in TcType.
-- Trac #13343 is an example; #14555 is another
-- See Note [Kind generalisation and SigTvs]
-- See Note [Kind generalisation and TyVarTvs]
= return False
| isRuntimeRepVar tv -- Do not quantify over a RuntimeRep var
-- unless it is a SigTv, handled earlier
-- unless it is a TyVarTv, handled earlier
= do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
; writeMetaTyVar tv liftedRepTy
; return True }
......@@ -1575,14 +1575,14 @@ zonkCo = mapCoercion zonkTcTypeMapper ()
zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
-- A tyvar binder is never a unification variable (TauTv),
-- rather it is always a skolem. It *might* be a SigTv.
-- (Because non-CUSK type declarations use SigTvs.)
-- rather it is always a skolem. It *might* be a TyVarTv.
-- (Because non-CUSK type declarations use TyVarTvs.)
-- Regardless, it may have a kind
-- that has not yet been zonked, and may include kind
-- unification variables.
zonkTcTyCoVarBndr tyvar
| isSigTyVar tyvar
= tcGetTyVar "zonkTcTyCoVarBndr SigTv" <$> zonkTcTyVar tyvar
| isTyVarTyVar tyvar
= tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" <$> zonkTcTyVar tyvar
| otherwise
-- can't use isCoVar, because it looks at a TyCon. Argh.
......@@ -1614,7 +1614,7 @@ zonkTcTyVar tv
; return (mkTyVarTy z_tv) }
-- Variant that assumes that any result of zonking is still a TyVar.
-- Should be used only on skolems and SigTvs
-- Should be used only on skolems and TyVarTvs
zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
zonkTcTyVarToTyVar tv
= do { ty <- zonkTcTyVar tv
......@@ -1624,8 +1624,8 @@ zonkTcTyVarToTyVar tv
(ppr tv $$ ppr ty)
; return tv' }
zonkSigTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
zonkSigTyVarPairs prs
zonkTyVarTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
zonkTyVarTyVarPairs prs
= mapM do_one prs
where
do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
......
......@@ -550,10 +550,10 @@ a pattern synonym. What about the /building/ side?
tcPatSynBuilderBind, by converting the pattern to an expression and
typechecking it.
At one point, for ImplicitBidirectional I used SigTvs (instead of
At one point, for ImplicitBidirectional I used TyVarTvs (instead of
TauTvs) in tcCheckPatSynDecl. But (a) strengthening the check here
is redundant since tcPatSynBuilderBind does the job, (b) it was
still incomplete (SigTvs can unify with each other), and (c) it
still incomplete (TyVarTvs can unify with each other), and (c) it
didn't even work (Trac #13441 was accepted with
ExplicitBidirectional, but rejected if expressed in
ImplicitBidirectional form. Conclusion: trying to be too clever is
......
......@@ -1500,7 +1500,7 @@ data TcIdSigInst
= TISI { sig_inst_sig :: TcIdSigInfo
, sig_inst_skols :: [(Name, TcTyVar)]
-- Instantiated type and kind variables, SigTvs
-- Instantiated type and kind variables, TyVarTvs
-- The Name is the Name that the renamer chose;
-- but the TcTyVar may come from instantiating
-- the type and hence have a different unique.
......
......@@ -401,7 +401,7 @@ tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
-- Instantiate a type signature; only used with plan InferGen
tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
= setSrcSpan loc $ -- Set the binding site of the tyvars
do { (tv_prs, theta, tau) <- tcInstType newMetaSigTyVars poly_id
do { (tv_prs, theta, tau) <- tcInstType newMetaTyVarTyVars poly_id
-- See Note [Pattern bindings and complete signatures]
; return (TISI { sig_inst_sig = sig
......@@ -446,8 +446,8 @@ tcInstSig sig@(PartialSig { psig_hs_ty = hs_ty
where
mk_sig_tv old_name kind
= do { uniq <- newUnique
; newSigTyVar (setNameUnique old_name uniq) kind }
-- Why newSigTyVar? See TcBinds
; newTyVarTyVar (setNameUnique old_name uniq) kind }
-- Why newTyVarTyVar? See TcBinds
-- Note [Quantified variables in partial type signatures]
......@@ -461,8 +461,8 @@ Consider
Here we'll infer a type from the pattern of 'T a', but if we feed in
the signature types for f and g, we'll end up unifying 'a' and 'b'
So we instantiate f and g's signature with SigTv skolems
(newMetaSigTyVars) that can unify with each other. If too much
So we instantiate f and g's signature with TyVarTv skolems
(newMetaTyVarTyVars) that can unify with each other. If too much
unification takes place, we'll find out when we do the final
impedance-matching check in TcBinds.mkExport
......
......@@ -932,7 +932,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
= do { (no_quant, maybe_quant) <- pick infer_mode candidates
-- If possible, we quantify over partial-sig qtvs, so they are
-- not mono. Need to zonk them because they are meta-tyvar SigTvs
-- not mono. Need to zonk them because they are meta-tyvar TyVarTvs
; psig_qtvs <- mapM zonkTcTyVarToTyVar $
concatMap (map snd . sig_inst_skols) psigs
......@@ -1165,7 +1165,7 @@ However, in the case of a partial type signature, be doing inference
or
g :: (Eq _a) => _b -> _b
In both cases we use plan InferGen, and hence call simplifyInfer. But
those 'a' variables are skolems (actually SigTvs), and we should be
those 'a' variables are skolems (actually TyVarTvs), and we should be
sure to quantify over them. This leads to several wrinkles:
* Wrinkle 1. In the case of a type error
......@@ -1953,9 +1953,9 @@ promoteTyVarTcS tv
defaultTyVarTcS :: TcTyVar -> TcS Bool
defaultTyVarTcS the_tv
| isRuntimeRepVar the_tv
, not (isSigTyVar the_tv) -- SigTvs should only be unified with a tyvar
, not (isTyVarTyVar the_tv) -- TyVarTvs should only be unified with a tyvar
-- never with a type; c.f. TcMType.defaultTyVar
-- See Note [Kind generalisation and SigTvs]
-- See Note [Kind generalisation and TyVarTvs]
= do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
; unifyTyVar the_tv liftedRepTy
; return True }
......@@ -2286,7 +2286,7 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
float_tv_eq_candidate tv1 ty2 -- See Note [Which equalities to float]
= isMetaTyVar tv1
&& (not (isSigTyVar tv1) || isTyVarTy ty2)
&& (not (isTyVarTyVar tv1) || isTyVarTy ty2)
{- Note [Float equalities from under a skolem binding]
......@@ -2320,7 +2320,7 @@ happen. In particular, float out equalities that are:
* Of form (alpha ~# ty) or (ty ~# alpha), where
* alpha is a meta-tyvar.
* And 'alpha' is not a SigTv with 'ty' being a non-tyvar. In that
* And 'alpha' is not a TyVarTv with 'ty' being a non-tyvar. In that
case, floating out won't help either, and it may affect grouping
of error messages.
......
......@@ -554,7 +554,7 @@ kcTyClGroup decls
; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
; tc_res_kind' <- zonkTcTypeToType env tc_res_kind
; scoped_tvs' <- zonkSigTyVarPairs scoped_tvs
; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs
-- See Note [Check telescope again during generalisation]
; let extra = text "NB: Implicitly declared variables come before others."
......@@ -775,7 +775,7 @@ kcConDecl :: ConDecl GhcRn -> TcM ()
kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
, con_mb_cxt = ex_ctxt, con_args = args })
= addErrCtxt (dataConCtxtName [name]) $
-- See Note [Use SigTvs in kind-checking pass]
-- See Note [Use TyVarTvs in kind-checking pass]
kcExplicitTKBndrs ex_tvs $
do { _ <- tcHsMbContext ex_ctxt
; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args) }
......@@ -822,8 +822,8 @@ mappings:
APromotionErr is only used for DataCons, and only used during type checking
in tcTyClGroup.
Note [Use SigTvs in kind-checking pass]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Use TyVarTvs in kind-checking pass]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data Proxy a where
......@@ -833,7 +833,7 @@ Consider
It seems reasonable that this should be accepted. But something very strange
is going on here: when we're kind-checking this declaration, we need to unify
the kind of `a` with k and j -- even though k and j's scopes are local to the type of
MkProxy{1,2}. The best approach we've come up with is to use SigTvs during
MkProxy{1,2}. The best approach we've come up with is to use TyVarTvs during
the kind-checking pass. First off, note that it's OK if the kind-checking pass
is too permissive: we'll snag the problems in the type-checking pass later.
(This extra permissiveness might happen with something like
......@@ -842,20 +842,20 @@ is too permissive: we'll snag the problems in the type-checking pass later.
data Bad a where
MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)
which would be accepted if k1 and k2 were SigTvs. This is correctly rejected
in the second pass, though. Test case: polykinds/SigTvKinds3)
which would be accepted if k1 and k2 were TyVarTvs. This is correctly rejected
in the second pass, though. Test case: polykinds/TyVarTvKinds3)
Recall that the kind-checking pass exists solely to collect constraints
on the kinds and to power unification.
To achieve the use of SigTvs, we must be careful to use specialized functions
that produce SigTvs, not ordinary skolems. This is why we need
To achieve the use of TyVarTvs, we must be careful to use specialized functions
that produce TyVarTvs, not ordinary skolems. This is why we need
kcExplicitTKBndrs and kcImplicitTKBndrs in TcHsType, separate from their
tc... variants.
</