summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2019-02-25 08:31:33 +0000
committerMarge Bot <ben+marge-bot@smart-cactus.org>2019-03-05 03:09:41 -0500
commit80dfcee61e3bfb67f131cd674f96467e16c0f9d8 (patch)
tree3b486a446fa687097b66b99dc22424ec929e2aaf /compiler
parente6ce17433b75c6c985bffaf1f6fc18d299666ccb (diff)
downloadhaskell-80dfcee61e3bfb67f131cd674f96467e16c0f9d8.tar.gz
Be more careful when naming TyCon binders
This patch fixes two rather gnarly test cases: * Trac #16342 (mutual recursion) See Note [Tricky scoping in generaliseTcTyCon] * Trac #16221 (shadowing) See Note [Unification variables need fresh Names] The main changes are: * Substantial reworking of TcTyClsDecls.generaliseTcTyCon This is the big change, and involves the rather tricky function TcHsSyn.zonkRecTyVarBndrs. See Note [Inferring kinds for type declarations] and Note [Tricky scoping in generaliseTcTyCon] for the details. * bindExplicitTKBndrs_Tv and bindImplicitTKBndrs_Tv both now allocate /freshly-named/ unification variables. Indeed, more generally, unification variables are always fresh; see Note [Unification variables need fresh Names] in TcMType * Clarify the role of tcTyConScopedTyVars. See Note [Scoped tyvars in a TcTyCon] in TyCon As usual, this dragged in some more refactoring: * Renamed TcMType.zonkTyCoVarBndr to zonkAndSkolemise * I renamed checkValidTelescope to checkTyConTelescope; it's only used on TyCons, and indeed takes a TyCon as argument. * I folded the slightly-mysterious reportFloatingKvs into checkTyConTelescope. (Previously all its calls immediately followed a call to checkTyConTelescope.) It makes much more sense there. * I inlined some called-once functions to simplify checkValidTyFamEqn. It's less spaghetti-like now. * This patch also fixes Trac #16251. I'm not quite sure why #16251 went wrong in the first place, nor how this patch fixes it, but hey, it's good, and life is short.
Diffstat (limited to 'compiler')
-rw-r--r--compiler/deSugar/DsMeta.hs4
-rw-r--r--compiler/hsSyn/HsTypes.hs13
-rw-r--r--compiler/rename/RnSource.hs5
-rw-r--r--compiler/typecheck/TcHsSyn.hs56
-rw-r--r--compiler/typecheck/TcHsType.hs103
-rw-r--r--compiler/typecheck/TcMType.hs240
-rw-r--r--compiler/typecheck/TcSigs.hs4
-rw-r--r--compiler/typecheck/TcTyClsDecls.hs237
-rw-r--r--compiler/typecheck/TcValidity.hs249
-rw-r--r--compiler/types/TyCon.hs40
10 files changed, 595 insertions, 356 deletions
diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index 5e0976d1a2..67a05d647d 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -208,7 +208,7 @@ get_scoped_tvs (dL->L _ signature)
| HsIB { hsib_ext = implicit_vars
, hsib_body = hs_ty } <- sig
, (explicit_vars, _) <- splitLHsForAllTy hs_ty
- = implicit_vars ++ map hsLTyVarName explicit_vars
+ = implicit_vars ++ hsLTyVarNames explicit_vars
get_scoped_tvs_from_sig (XHsImplicitBndrs _)
= panic "get_scoped_tvs_from_sig"
@@ -1037,7 +1037,7 @@ addHsTyVarBinds :: [LHsTyVarBndr GhcRn] -- the binders to be added
-> (Core [TH.TyVarBndrQ] -> DsM (Core (TH.Q a))) -- action in the ext env
-> DsM (Core (TH.Q a))
addHsTyVarBinds exp_tvs thing_inside
- = do { fresh_exp_names <- mkGenSyms (map hsLTyVarName exp_tvs)
+ = do { fresh_exp_names <- mkGenSyms (hsLTyVarNames exp_tvs)
; term <- addBinds fresh_exp_names $
do { kbs <- repList tyVarBndrQTyConName mk_tv_bndr
(exp_tvs `zip` fresh_exp_names)
diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index aabe9f4597..85715a9282 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -53,7 +53,7 @@ module HsTypes (
isHsKindedTyVar, hsTvbAllKinded, isLHsForAllTy,
hsScopedTvs, hsWcScopedTvs, dropWildCards,
hsTyVarName, hsAllLTyVarNames, hsLTyVarLocNames,
- hsLTyVarName, hsLTyVarLocName, hsExplicitLTyVarNames,
+ hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsExplicitLTyVarNames,
splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
splitLHsPatSynTy,
splitLHsForAllTy, splitLHsForAllTyInvis,
@@ -949,7 +949,7 @@ hsWcScopedTvs sig_ty
, hsib_body = sig_ty2 } <- sig_ty1
= case sig_ty2 of
L _ (HsForAllTy { hst_bndrs = tvs }) -> vars ++ nwcs ++
- map hsLTyVarName tvs
+ hsLTyVarNames tvs
-- include kind variables only if the type is headed by forall
-- (this is consistent with GHC 7 behaviour)
_ -> nwcs
@@ -962,7 +962,7 @@ hsScopedTvs sig_ty
| HsIB { hsib_ext = vars
, hsib_body = sig_ty2 } <- sig_ty
, L _ (HsForAllTy { hst_bndrs = tvs }) <- sig_ty2
- = vars ++ map hsLTyVarName tvs
+ = vars ++ hsLTyVarNames tvs
| otherwise
= []
@@ -988,6 +988,9 @@ hsTyVarName (XTyVarBndr{}) = panic "hsTyVarName"
hsLTyVarName :: LHsTyVarBndr pass -> IdP pass
hsLTyVarName = hsTyVarName . unLoc
+hsLTyVarNames :: [LHsTyVarBndr pass] -> [IdP pass]
+hsLTyVarNames = map hsLTyVarName
+
hsExplicitLTyVarNames :: LHsQTyVars pass -> [IdP pass]
-- Explicit variables only
hsExplicitLTyVarNames qtvs = map hsLTyVarName (hsQTvExplicit qtvs)
@@ -996,7 +999,7 @@ hsAllLTyVarNames :: LHsQTyVars GhcRn -> [Name]
-- All variables
hsAllLTyVarNames (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kvs }
, hsq_explicit = tvs })
- = kvs ++ map hsLTyVarName tvs
+ = kvs ++ hsLTyVarNames tvs
hsAllLTyVarNames (XLHsQTyVars _) = panic "hsAllLTyVarNames"
hsLTyVarLocName :: LHsTyVarBndr pass -> Located (IdP pass)
@@ -1255,7 +1258,7 @@ splitLHsInstDeclTy :: LHsSigType GhcRn
splitLHsInstDeclTy (HsIB { hsib_ext = itkvs
, hsib_body = inst_ty })
| (tvs, cxt, body_ty) <- splitLHsSigmaTyInvis inst_ty
- = (itkvs ++ map hsLTyVarName tvs, cxt, body_ty)
+ = (itkvs ++ hsLTyVarNames tvs, cxt, body_ty)
-- Return implicitly bound type and kind vars
-- For an instance decl, all of them are in scope
splitLHsInstDeclTy (XHsImplicitBndrs _) = panic "splitLHsInstDeclTy"
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index 5155f3ab84..f902b0ef07 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -776,8 +776,7 @@ rnFamInstEqn doc mb_cls rhs_kvars
inst_tvs = case mb_cls of
Nothing -> []
Just (_, inst_tvs) -> inst_tvs
- all_nms = all_imp_var_names
- ++ map hsLTyVarName bndrs'
+ all_nms = all_imp_var_names ++ hsLTyVarNames bndrs'
; warnUnusedTypePatterns all_nms nms_used
; return ((bndrs', pats', payload'), rhs_fvs `plusFV` pat_fvs) }
@@ -1809,7 +1808,7 @@ rnLDerivStrategy doc mds thing_inside
let HsIB { hsib_ext = via_imp_tvs
, hsib_body = via_body } = via_ty'
(via_exp_tv_bndrs, _, _) = splitLHsSigmaTy via_body
- via_exp_tvs = map hsLTyVarName via_exp_tv_bndrs
+ via_exp_tvs = hsLTyVarNames via_exp_tv_bndrs
via_tvs = via_imp_tvs ++ via_exp_tvs
(thing, fvs2) <- extendTyVarEnvFVRn via_tvs $
thing_inside via_tvs (ppr via_ty')
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 8b815bb0e7..7755daf44b 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -34,7 +34,7 @@ module TcHsSyn (
zonkTopBndrs,
ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv,
zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX,
- zonkTyBndrs, zonkTyBndrsX,
+ zonkTyBndrs, zonkTyBndrsX, zonkRecTyVarBndrs,
zonkTcTypeToType, zonkTcTypeToTypeX,
zonkTcTypesToTypes, zonkTcTypesToTypesX,
zonkTyVarOcc,
@@ -278,7 +278,11 @@ data ZonkFlexi -- See Note [Un-unified unification variables]
| RuntimeUnkFlexi -- Used in the GHCi debugger
instance Outputable ZonkEnv where
- ppr (ZonkEnv { ze_id_env = var_env}) = pprUFM var_env (vcat . map ppr)
+ ppr (ZonkEnv { ze_tv_env = tv_env
+ , ze_id_env = id_env })
+ = text "ZE" <+> braces (vcat
+ [ text "ze_tv_env =" <+> ppr tv_env
+ , text "ze_id_env =" <+> ppr id_env ])
-- The EvBinds have to already be zonked, but that's usually the case.
emptyZonkEnv :: TcM ZonkEnv
@@ -292,9 +296,9 @@ mkEmptyZonkEnv flexi
, ze_id_env = emptyVarEnv
, ze_meta_tv_env = mtv_env_ref }) }
-initZonkEnv :: (ZonkEnv -> a -> TcM b) -> a -> TcM b
-initZonkEnv do_it x = do { ze <- mkEmptyZonkEnv DefaultFlexi
- ; do_it ze x }
+initZonkEnv :: (ZonkEnv -> TcM b) -> TcM b
+initZonkEnv thing_inside = do { ze <- mkEmptyZonkEnv DefaultFlexi
+ ; thing_inside ze }
-- | Extend the knot-tied environment.
extendIdZonkEnvRec :: ZonkEnv -> [Var] -> ZonkEnv
@@ -324,6 +328,12 @@ extendTyZonkEnv1 :: ZonkEnv -> TyVar -> ZonkEnv
extendTyZonkEnv1 ze@(ZonkEnv { ze_tv_env = ty_env }) tv
= ze { ze_tv_env = extendVarEnv ty_env tv tv }
+extendTyZonkEnvN :: ZonkEnv -> [(Name,TyVar)] -> ZonkEnv
+extendTyZonkEnvN ze@(ZonkEnv { ze_tv_env = ty_env }) pairs
+ = ze { ze_tv_env = foldl add ty_env pairs }
+ where
+ add env (name, tv) = extendVarEnv_Directly env (getUnique name) tv
+
setZonkType :: ZonkEnv -> ZonkFlexi -> ZonkEnv
setZonkType ze flexi = ze { ze_flexi = flexi }
@@ -374,7 +384,7 @@ zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
zonkIdBndrs env ids = mapM (zonkIdBndr env) ids
zonkTopBndrs :: [TcId] -> TcM [Id]
-zonkTopBndrs ids = initZonkEnv zonkIdBndrs ids
+zonkTopBndrs ids = initZonkEnv $ \ ze -> zonkIdBndrs ze ids
zonkFieldOcc :: ZonkEnv -> FieldOcc GhcTcId -> TcM (FieldOcc GhcTc)
zonkFieldOcc env (FieldOcc sel lbl)
@@ -419,7 +429,7 @@ zonkCoreBndrsX :: ZonkEnv -> [Var] -> TcM (ZonkEnv, [Var])
zonkCoreBndrsX = mapAccumLM zonkCoreBndrX
zonkTyBndrs :: [TcTyVar] -> TcM (ZonkEnv, [TyVar])
-zonkTyBndrs = initZonkEnv zonkTyBndrsX
+zonkTyBndrs tvs = initZonkEnv $ \ze -> zonkTyBndrsX ze tvs
zonkTyBndrsX :: ZonkEnv -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
zonkTyBndrsX = mapAccumLM zonkTyBndrX
@@ -436,7 +446,7 @@ zonkTyBndrX env tv
zonkTyVarBinders :: [VarBndr TcTyVar vis]
-> TcM (ZonkEnv, [VarBndr TyVar vis])
-zonkTyVarBinders = initZonkEnv zonkTyVarBindersX
+zonkTyVarBinders tvbs = initZonkEnv $ \ ze -> zonkTyVarBindersX ze tvbs
zonkTyVarBindersX :: ZonkEnv -> [VarBndr TcTyVar vis]
-> TcM (ZonkEnv, [VarBndr TyVar vis])
@@ -449,11 +459,27 @@ zonkTyVarBinderX env (Bndr tv vis)
= do { (env', tv') <- zonkTyBndrX env tv
; return (env', Bndr tv' vis) }
+zonkRecTyVarBndrs :: [Name] -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
+-- This rather specialised function is used in exactly one place.
+-- See Note [Tricky scoping in generaliseTcTyCon] in TcTyClsDecls.
+zonkRecTyVarBndrs names tc_tvs
+ = initZonkEnv $ \ ze ->
+ fixM $ \ ~(_, rec_new_tvs) ->
+ do { let ze' = extendTyZonkEnvN ze $
+ zipWithLazy (\ tc_tv new_tv -> (getName tc_tv, new_tv))
+ tc_tvs rec_new_tvs
+ ; new_tvs <- zipWithM (zonk_one ze') names tc_tvs
+ ; return (ze', new_tvs) }
+ where
+ zonk_one ze name tc_tv
+ = do { ki <- zonkTcTypeToTypeX ze (tyVarKind tc_tv)
+ ; return (mkTyVar name ki) }
+
zonkTopExpr :: HsExpr GhcTcId -> TcM (HsExpr GhcTc)
-zonkTopExpr e = initZonkEnv zonkExpr e
+zonkTopExpr e = initZonkEnv $ \ ze -> zonkExpr ze e
zonkTopLExpr :: LHsExpr GhcTcId -> TcM (LHsExpr GhcTc)
-zonkTopLExpr e = initZonkEnv zonkLExpr e
+zonkTopLExpr e = initZonkEnv $ \ ze -> zonkLExpr ze e
zonkTopDecls :: Bag EvBind
-> LHsBinds GhcTcId
@@ -466,7 +492,7 @@ zonkTopDecls :: Bag EvBind
[LTcSpecPrag],
[LRuleDecl GhcTc])
zonkTopDecls ev_binds binds rules imp_specs fords
- = do { (env1, ev_binds') <- initZonkEnv zonkEvBinds ev_binds
+ = do { (env1, ev_binds') <- initZonkEnv $ \ ze -> zonkEvBinds ze ev_binds
; (env2, binds') <- zonkRecMonoBinds env1 binds
-- Top level is implicitly recursive
; rules' <- zonkRules env2 rules
@@ -1744,9 +1770,9 @@ Solution: (see Trac #15552 for other variants)
* The map is of course stateful, held in a TcRef. (That is unlike
the treatment of lexically-scoped variables in ze_tv_env and
- ze_id_env.
+ ze_id_env.)
- Is the extra work worth it. Some non-sytematic perf measurements
+ Is the extra work worth it? Some non-sytematic perf measurements
suggest that compiler allocation is reduced overall (by 0.5% or so)
but compile time really doesn't change.
-}
@@ -1865,13 +1891,13 @@ zonkTcTyConToTyCon tc
-- Confused by zonking? See Note [What is zonking?] in TcMType.
zonkTcTypeToType :: TcType -> TcM Type
-zonkTcTypeToType = initZonkEnv zonkTcTypeToTypeX
+zonkTcTypeToType ty = initZonkEnv $ \ ze -> zonkTcTypeToTypeX ze ty
zonkTcTypeToTypeX :: ZonkEnv -> TcType -> TcM Type
zonkTcTypeToTypeX = mapType zonk_tycomapper
zonkTcTypesToTypes :: [TcType] -> TcM [Type]
-zonkTcTypesToTypes = initZonkEnv zonkTcTypesToTypesX
+zonkTcTypesToTypes tys = initZonkEnv $ \ ze -> zonkTcTypesToTypesX ze tys
zonkTcTypesToTypesX :: ZonkEnv -> [TcType] -> TcM [Type]
zonkTcTypesToTypesX env tys = mapM (zonkTcTypeToTypeX env) tys
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 24b416c6e8..b3c40274c4 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -190,9 +190,9 @@ tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
kcHsSigType :: [Located Name] -> LHsSigType GhcRn -> TcM ()
kcHsSigType names (HsIB { hsib_body = hs_ty
, hsib_ext = sig_vars })
- = addSigCtxt (funsSigCtxt names) hs_ty $
- discardResult $
- bindImplicitTKBndrs_Skol sig_vars $
+ = discardResult $
+ addSigCtxt (funsSigCtxt names) hs_ty $
+ bindImplicitTKBndrs_Skol sig_vars $
tc_lhs_type typeLevelMode hs_ty liftedTypeKind
kcHsSigType _ (XHsImplicitBndrs _) = panic "kcHsSigType"
@@ -238,7 +238,6 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
solveLocalEqualitiesX "tc_hs_sig_type" $
bindImplicitTKBndrs_Skol sig_vars $
do { kind <- newExpectedKind ctxt_kind
-
; tc_lhs_type typeLevelMode hs_ty kind }
-- Any remaining variables (unsolved in the solveLocalEqualities)
-- should be in the global tyvars, and therefore won't be quantified
@@ -1864,15 +1863,12 @@ kcLHsQTyVars_Cusk name flav
++ map (mkRequiredTyConBinder mentioned_kv_set) tc_tvs
all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
- tycon = mkTcTyCon name
- final_tc_binders
- res_kind
- all_tv_prs
+ tycon = mkTcTyCon name final_tc_binders res_kind all_tv_prs
True {- it is generalised -} flav
-- If the ordering from
-- Note [Required, Specified, and Inferred for types] in TcTyClsDecls
-- doesn't work, we catch it here, before an error cascade
- ; checkValidTelescope tycon
+ ; checkTyConTelescope tycon
; traceTc "kcLHsQTyVars: cusk" $
vcat [ text "name" <+> ppr name
@@ -1921,8 +1917,13 @@ kcLHsQTyVars_NonCusk name flav
-- Also, note that tc_binders has the tyvars from only the
-- user-written tyvarbinders. See S1 in Note [How TcTyCons work]
-- in TcTyClsDecls
- tycon = mkTcTyCon name tc_binders res_kind
- (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
+
+ all_tv_prs = (kv_ns `zip` scoped_kvs) ++
+ (hsLTyVarNames hs_tvs `zip` tc_tvs)
+ -- NB: bindIplicitTKBndrs_Q_Tv makes /freshly-named/ unification
+ -- variables, hence the need to zip here. Ditto bindExplicit..
+ -- See TcMType Note [Unification variables need fresh Names]
+ tycon = mkTcTyCon name tc_binders res_kind all_tv_prs
False -- not yet generalised
flav
@@ -2046,32 +2047,24 @@ expectedKindInCtxt _ = OpenKind
bindImplicitTKBndrs_Skol, bindImplicitTKBndrs_Tv,
bindImplicitTKBndrs_Q_Skol, bindImplicitTKBndrs_Q_Tv
- :: [Name]
- -> TcM a
- -> TcM ([TcTyVar], a)
+ :: [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Skol = bindImplicitTKBndrsX newFlexiKindedSkolemTyVar
bindImplicitTKBndrs_Tv = bindImplicitTKBndrsX newFlexiKindedTyVarTyVar
bindImplicitTKBndrs_Q_Skol = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedSkolemTyVar)
bindImplicitTKBndrs_Q_Tv = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedTyVarTyVar)
-bindImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function
- -> [Name]
- -> TcM a
- -> TcM ([TcTyVar], a) -- these tyvars are dependency-ordered
--- * Guarantees to call solveLocalEqualities to unify
--- all constraints from thing_inside.
---
--- * Returned TcTyVars have the supplied HsTyVarBndrs,
--- but may be in different order to the original [Name]
--- (because of sorting to respect dependency)
---
--- * Returned TcTyVars have zonked kinds
--- See Note [Keeping scoped variables in order: Implicit]
+bindImplicitTKBndrsX
+ :: (Name -> TcM TcTyVar) -- new_tv function
+ -> [Name]
+ -> TcM a
+ -> TcM ([TcTyVar], a) -- Returned [TcTyVar] are in 1-1 correspondence
+ -- with the passed in [Name]
bindImplicitTKBndrsX new_tv tv_names thing_inside
= do { tkvs <- mapM new_tv tv_names
- ; result <- tcExtendTyVarEnv tkvs thing_inside
; traceTc "bindImplicitTKBndrs" (ppr tv_names $$ ppr tkvs)
- ; return (tkvs, result) }
+ ; res <- tcExtendNameTyVarEnv (tv_names `zip` tkvs)
+ thing_inside
+ ; return (tkvs, res) }
newImplicitTyVarQ :: (Name -> TcM TcTyVar) -> Name -> TcM TcTyVar
-- Behave like new_tv, except that if the tyvar is in scope, use it
@@ -2091,6 +2084,7 @@ newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar
+ -- See Note [Unification variables need fresh Names] in TcMType
--------------------------------------
-- Explicit binders
@@ -2119,7 +2113,8 @@ bindExplicitTKBndrsX
:: (HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn]
-> TcM a
- -> TcM ([TcTyVar], a)
+ -> TcM ([TcTyVar], a) -- Returned [TcTyVar] are in 1-1 correspondence
+ -- with the passed-in [LHsTyVarBndr]
bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
= do { traceTc "bindExplicTKBndrs" (ppr hs_tvs)
; go hs_tvs }
@@ -2128,7 +2123,13 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
; return ([], res) }
go (L _ hs_tv : hs_tvs)
= do { tv <- tc_tv hs_tv
- ; (tvs, res) <- tcExtendTyVarEnv [tv] (go hs_tvs)
+ -- Extend the environment as we go, in case a binder
+ -- is mentioned in the kind of a later binder
+ -- e.g. forall k (a::k). blah
+ -- NB: tv's Name may differ from hs_tv's
+ -- See TcMType Note [Unification variables need fresh Names]
+ ; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $
+ go hs_tvs
; return (tv:tvs, res) }
-----------------
@@ -2192,7 +2193,7 @@ bindTyClTyVars tycon_name thing_inside
; let scoped_prs = tcTyConScopedTyVars tycon
res_kind = tyConResKind tycon
binders = tyConBinders tycon
- ; traceTc "bindTyClTyVars" (ppr tycon_name <+> ppr binders)
+ ; traceTc "bindTyClTyVars" (ppr tycon_name <+> ppr binders $$ ppr scoped_prs)
; tcExtendNameTyVarEnv scoped_prs $
thing_inside binders res_kind }
@@ -2215,8 +2216,8 @@ kcLookupTcTyCon nm
zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort spec_tkvs
- = do { spec_tkvs <- mapM zonkTcTyCoVarBndr spec_tkvs
- -- Use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv
+ = do { spec_tkvs <- mapM zonkAndSkolemise spec_tkvs
+ -- Use zonkAndSkolemise because a skol_tv might be a TyVarTv
-- Do a stable topological sort, following
-- Note [Ordering of implicit variables] in RnTypes
@@ -2503,7 +2504,7 @@ tcHsPartialSigType ctxt sig_ty
-- 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
- ; let tv_names = map tyVarName (implicit_tvs ++ explicit_tvs)
+ ; let tv_names = implicit_hs_tvs ++ hsLTyVarNames explicit_hs_tvs
-- Spit out the wildcards (including the extra-constraints one)
-- as "hole" constraints, so that they'll be reported if necessary
@@ -2520,7 +2521,7 @@ tcHsPartialSigType ctxt sig_ty
-- we need to promote the TyVarTvs so we don't violate the TcLevel
-- invariant
; implicit_tvs <- zonkAndScopedSort implicit_tvs
- ; explicit_tvs <- mapM zonkTcTyCoVarBndr explicit_tvs
+ ; explicit_tvs <- mapM zonkAndSkolemise explicit_tvs
; theta <- mapM zonkTcType theta
; tau <- zonkTcType tau
@@ -2605,17 +2606,17 @@ tcHsPatSigType :: UserTypeCtxt
-- See Note [Recipe for checking a signature]
tcHsPatSigType ctxt sig_ty
| HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
- , HsIB { hsib_ext = sig_vars
+ , HsIB { hsib_ext = sig_ns
, hsib_body = hs_ty } <- ib_ty
= addSigCtxt ctxt hs_ty $
- do { sig_tkvs <- mapM new_implicit_tv sig_vars
+ do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
; (wcs, sig_ty)
<- solveLocalEqualities "tcHsPatSigType" $
-- Always solve local equalities if possible,
-- else casts get in the way of deep skolemisation
-- (Trac #16033)
- tcWildCardBinders sig_wcs $ \ wcs ->
- tcExtendTyVarEnv sig_tkvs $
+ tcWildCardBinders sig_wcs $ \ wcs ->
+ tcExtendNameTyVarEnv sig_tkv_prs $
do { sig_ty <- tcHsOpenType hs_ty
; return (wcs, sig_ty) }
@@ -2629,19 +2630,17 @@ tcHsPatSigType ctxt sig_ty
; sig_ty <- zonkPromoteType sig_ty
; checkValidType ctxt sig_ty
- ; let tv_pairs = mkTyVarNamePairs sig_tkvs
-
- ; traceTc "tcHsPatSigType" (ppr sig_vars)
- ; return (wcs, tv_pairs, sig_ty) }
+ ; traceTc "tcHsPatSigType" (ppr sig_tkv_prs)
+ ; return (wcs, sig_tkv_prs, sig_ty) }
where
- new_implicit_tv name = do { kind <- newMetaKindVar
- ; new_tv name kind }
-
- new_tv = case ctxt of
- RuleSigCtxt {} -> newSkolemTyVar
- _ -> newTauTyVar
- -- See Note [Pattern signature binders]
-
+ new_implicit_tv name
+ = do { kind <- newMetaKindVar
+ ; tv <- case ctxt of
+ RuleSigCtxt {} -> newSkolemTyVar name kind
+ _ -> newPatSigTyVar name kind
+ -- See Note [Pattern signature binders]
+ -- NB: tv's Name may be fresh (in the case of newPatSigTyVar)
+ ; return (name, tv) }
tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType"
tcHsPatSigType _ (XHsWildCardBndrs _) = panic "tcHsPatSigType"
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 19fbadeacf..0c9e0e223e 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -52,7 +52,7 @@ module TcMType (
-- Instantiation
newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
newMetaTyVarTyVars, newMetaTyVarTyVarX,
- newTyVarTyVar, newTauTyVar, newSkolemTyVar, newWildCardX,
+ newTyVarTyVar, newPatSigTyVar, newSkolemTyVar, newWildCardX,
tcInstType,
tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
@@ -70,9 +70,8 @@ module TcMType (
candidateQTyVarsOfType, candidateQTyVarsOfKind,
candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
CandidatesQTvs(..), delCandidates, candidateKindVars,
- skolemiseQuantifiedTyVar, defaultTyVar,
- quantifyTyVars,
- zonkTcTyCoVarBndr, zonkTyConBinders,
+ zonkAndSkolemise, skolemiseQuantifiedTyVar,
+ defaultTyVar, quantifyTyVars,
zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind,
@@ -141,11 +140,12 @@ kind_var_occ :: OccName -- Just one for all MetaKindVars
kind_var_occ = mkOccName tvName "k"
newMetaKindVar :: TcM TcKind
-newMetaKindVar = do { uniq <- newUnique
- ; details <- newMetaDetails TauTv
- ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
- ; traceTc "newMetaKindVar" (ppr kv)
- ; return (mkTyVarTy kv) }
+newMetaKindVar
+ = do { details <- newMetaDetails TauTv
+ ; uniq <- newUnique
+ ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
+ ; traceTc "newMetaKindVar" (ppr kv)
+ ; return (mkTyVarTy kv) }
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
@@ -661,42 +661,118 @@ The remaining uses of newTyVarTyVars are
* In partial type signatures, see Note [Quantified variables in partial type signatures]
-}
--- see Note [TyVarTv]
+newMetaTyVarName :: FastString -> TcM Name
+-- Makes a /System/ Name, which is eagerly eliminated by
+-- the unifier; see TcUnify.nicer_to_update_tv1, and
+-- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
+newMetaTyVarName str
+ = do { uniq <- newUnique
+ ; return (mkSystemName uniq (mkTyVarOccFS str)) }
+
+cloneMetaTyVarName :: Name -> TcM Name
+cloneMetaTyVarName name
+ = do { uniq <- newUnique
+ ; return (mkSystemName uniq (nameOccName name)) }
+ -- See Note [Name of an instantiated type variable]
+
+{- Note [Name of an instantiated type variable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+At the moment we give a unification variable a System Name, which
+influences the way it is tidied; see TypeRep.tidyTyVarBndr.
+
+Note [Unification variables need fresh Names]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Whenever we allocate a unification variable (MetaTyVar) we give
+it a fresh name. Trac #16221 is a very tricky case that illustrates
+why this is important:
+
+ data SameKind :: k -> k -> *
+ data T0 a = forall k2 (b :: k2). MkT0 (SameKind a b) !Int
+
+When kind-checking T0, we give (a :: kappa1). Then, in kcConDecl
+we allocate a unification variable kappa2 for k2, and then we
+end up unifying kappa1 := kappa2 (because of the (SameKind a b).
+
+Now we generalise over kappa2; but if kappa2's Name is k2,
+we'll end up giving T0 the kind forall k2. k2 -> *. Nothing
+directly wrong with that but when we typecheck the data constrautor
+we end up giving it the type
+ MkT0 :: forall k1 (a :: k1) k2 (b :: k2).
+ SameKind @k2 a b -> Int -> T0 @{k2} a
+which is bogus. The result type should be T0 @{k1} a.
+
+And there no reason /not/ to clone the Name when making a
+unification variable. So that's what we do.
+-}
+
+newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
+-- Make a new meta tyvar out of thin air
+newAnonMetaTyVar meta_info kind
+ = do { let s = case meta_info of
+ TauTv -> fsLit "t"
+ FlatMetaTv -> fsLit "fmv"
+ FlatSkolTv -> fsLit "fsk"
+ TyVarTv -> fsLit "a"
+ ; name <- newMetaTyVarName s
+ ; details <- newMetaDetails meta_info
+ ; let tyvar = mkTcTyVar name kind details
+ ; traceTc "newAnonMetaTyVar" (ppr tyvar)
+ ; return tyvar }
+
+-- makes a new skolem tv
+newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
+newSkolemTyVar name kind
+ = do { lvl <- getTcLevel
+ ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
+
newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
+-- See Note [TyVarTv]
+-- See Note [Unification variables need fresh Names]
newTyVarTyVar name kind
= do { details <- newMetaDetails TyVarTv
- ; let tyvar = mkTcTyVar name kind details
+ ; uniq <- newUnique
+ ; let name' = name `setNameUnique` uniq
+ tyvar = mkTcTyVar name' kind details
+ -- Don't use cloneMetaTyVar, which makes a SystemName
+ -- We want to keep the original more user-friendly Name
+ -- In practical terms that means that in error messages,
+ -- when the Name is tidied we get 'a' rather than 'a0'
; traceTc "newTyVarTyVar" (ppr tyvar)
; return tyvar }
+newPatSigTyVar :: Name -> Kind -> TcM TcTyVar
+newPatSigTyVar name kind
+ = do { details <- newMetaDetails TauTv
+ ; uniq <- newUnique
+ ; let name' = name `setNameUnique` uniq
+ tyvar = mkTcTyVar name' kind details
+ -- Don't use cloneMetaTyVar;
+ -- same reasoning as in newTyVarTyVar
+ ; traceTc "newPatSigTyVar" (ppr tyvar)
+ ; return tyvar }
--- makes a new skolem tv
-newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
-newSkolemTyVar name kind = do { lvl <- getTcLevel
- ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
+cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
+-- Make a fresh MetaTyVar, basing the name
+-- on that of the supplied TyVar
+cloneAnonMetaTyVar info tv kind
+ = do { details <- newMetaDetails info
+ ; name <- cloneMetaTyVarName (tyVarName tv)
+ ; let tyvar = mkTcTyVar name kind details
+ ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
+ ; return tyvar }
newFskTyVar :: TcType -> TcM TcTyVar
newFskTyVar fam_ty
- = do { uniq <- newUnique
- ; ref <- newMutVar Flexi
- ; tclvl <- getTcLevel
- ; let details = MetaTv { mtv_info = FlatSkolTv
- , mtv_ref = ref
- , mtv_tclvl = tclvl }
- name = mkMetaTyVarName uniq (fsLit "fsk")
+ = do { details <- newMetaDetails FlatSkolTv
+ ; name <- newMetaTyVarName (fsLit "fsk")
; return (mkTcTyVar name (tcTypeKind fam_ty) details) }
newFmvTyVar :: TcType -> TcM TcTyVar
-- Very like newMetaTyVar, except sets mtv_tclvl to one less
-- so that the fmv is untouchable.
newFmvTyVar fam_ty
- = do { uniq <- newUnique
- ; ref <- newMutVar Flexi
- ; tclvl <- getTcLevel
- ; let details = MetaTv { mtv_info = FlatMetaTv
- , mtv_ref = ref
- , mtv_tclvl = tclvl }
- name = mkMetaTyVarName uniq (fsLit "s")
+ = do { details <- newMetaDetails FlatMetaTv
+ ; name <- newMetaTyVarName (fsLit "s")
; return (mkTcTyVar name (tcTypeKind fam_ty) details) }
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
@@ -710,10 +786,9 @@ newMetaDetails info
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
= ASSERT( isTcTyVar tv )
- do { uniq <- newUnique
- ; ref <- newMutVar Flexi
- ; let name' = setNameUnique (tyVarName tv) uniq
- details' = case tcTyVarDetails tv of
+ do { ref <- newMutVar Flexi
+ ; name' <- cloneMetaTyVarName (tyVarName tv)
+ ; let details' = case tcTyVarDetails tv of
details@(MetaTv {}) -> details { mtv_ref = ref }
_ -> pprPanic "cloneMetaTyVar" (ppr tv)
tyvar = mkTcTyVar name' (tyVarKind tv) details'
@@ -859,51 +934,6 @@ coercion variables, except for the special case of the promoted Eq#. But,
that can't ever appear in user code, so we're safe!
-}
-newTauTyVar :: Name -> Kind -> TcM TcTyVar
-newTauTyVar name kind
- = do { details <- newMetaDetails TauTv
- ; let tyvar = mkTcTyVar name kind details
- ; traceTc "newTauTyVar" (ppr tyvar)
- ; return tyvar }
-
-
-mkMetaTyVarName :: Unique -> FastString -> Name
--- Makes a /System/ Name, which is eagerly eliminated by
--- the unifier; see TcUnify.nicer_to_update_tv1, and
--- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
-mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
-
-newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
--- Make a new meta tyvar out of thin air
-newAnonMetaTyVar meta_info kind
- = do { uniq <- newUnique
- ; let name = mkMetaTyVarName uniq s
- s = case meta_info of
- TauTv -> fsLit "t"
- FlatMetaTv -> fsLit "fmv"
- FlatSkolTv -> fsLit "fsk"
- TyVarTv -> fsLit "a"
- ; details <- newMetaDetails meta_info
- ; let tyvar = mkTcTyVar name kind details
- ; traceTc "newAnonMetaTyVar" (ppr tyvar)
- ; return tyvar }
-
-cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
--- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
-cloneAnonMetaTyVar info tv kind
- = do { uniq <- newUnique
- ; details <- newMetaDetails info
- ; let name = mkSystemName uniq (getOccName tv)
- -- See Note [Name of an instantiated type variable]
- tyvar = mkTcTyVar name kind details
- ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
- ; return tyvar }
-
-{- Note [Name of an instantiated type variable]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-At the moment we give a unification variable a System Name, which
-influences the way it is tidied; see TypeRep.tidyTyVarBndr.
--}
newFlexiTyVar :: Kind -> TcM TcTyVar
newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
@@ -978,10 +1008,9 @@ new_meta_tv_x info subst tv
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
newMetaTyVarTyAtLevel tc_lvl kind
- = do { uniq <- newUnique
- ; ref <- newMutVar Flexi
- ; let name = mkMetaTyVarName uniq (fsLit "p")
- details = MetaTv { mtv_info = TauTv
+ = do { ref <- newMutVar Flexi
+ ; name <- newMetaTyVarName (fsLit "p")
+ ; let details = MetaTv { mtv_info = TauTv
, mtv_ref = ref
, mtv_tclvl = tc_lvl }
; return (mkTyVarTy (mkTcTyVar name kind details)) }
@@ -1472,6 +1501,24 @@ quantifiableTv outer_tclvl tcv
| otherwise
= False
+zonkAndSkolemise :: TcTyCoVar -> TcM TcTyCoVar
+-- A tyvar binder is never a unification variable (TauTv),
+-- 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.
+zonkAndSkolemise tyvar
+ | isTyVarTyVar tyvar
+ -- We want to preserve the binding location of the original TyVarTv.
+ -- This is important for error messages. If we don't do this, then
+ -- we get bad locations in, e.g., typecheck/should_fail/T2688
+ = do { zonked_tyvar <- zonkTcTyVarToTyVar tyvar
+ ; skolemiseQuantifiedTyVar zonked_tyvar }
+
+ | otherwise
+ = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar )
+ zonkTyCoVarKind tyvar
+
skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
-- The quantified type variables often include meta type variables
-- we want to freeze them into ordinary type variables
@@ -1973,35 +2020,6 @@ zonkTcType = mapType zonkTcTypeMapper ()
zonkCo :: Coercion -> TcM Coercion
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 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
- | isTyVarTyVar tyvar
- -- We want to preserve the binding location of the original TyVarTv.
- -- This is important for error messages. If we don't do this, then
- -- we get bad locations in, e.g., typecheck/should_fail/T2688
- = do { zonked_ty <- zonkTcTyVar tyvar
- ; let zonked_tyvar = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" zonked_ty
- zonked_name = getName zonked_tyvar
- reloc'd_name = setNameLoc zonked_name (getSrcSpan tyvar)
- ; return (setTyVarName zonked_tyvar reloc'd_name) }
-
- | otherwise
- = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar )
- zonkTyCoVarKind tyvar
-
-zonkTyConBinders :: [TyConBinder] -> TcM [TyConBinder]
-zonkTyConBinders = mapM zonk1
- where
- zonk1 (Bndr tv vis)
- = do { tv' <- zonkTcTyCoVarBndr tv
- ; return (Bndr tv' vis) }
-
zonkTcTyVar :: TcTyVar -> TcM TcType
-- Simply look through all Flexis
zonkTcTyVar tv
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 17e3f54893..9146b10fe2 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -382,8 +382,8 @@ tcPatSynSig name sig_ty
-- e.g. pattern Zero <- 0# (Trac #12094)
; return (req, prov, body_ty) }
- ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvs req
- ex_tvs prov body_ty
+ ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvs
+ req ex_tvs prov body_ty
-- Kind generalisation
; kvs <- kindGeneralize ungen_patsyn_ty
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index eb8a066529..8d413139ba 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -536,94 +536,121 @@ generaliseTcTyCon tc
-- See Note [Required, Specified, and Inferred for types]
= setSrcSpan (getSrcSpan tc) $
addTyConCtxt tc $
- do { let tc_name = tyConName tc
- tc_res_kind = tyConResKind tc
- tc_tvs = tyConTyVars tc
-
- (scoped_tv_names, scoped_tvs) = unzip (tcTyConScopedTyVars tc)
- -- NB: scoped_tvs includes both specified and required (tc_tvs)
- -- ToDo: Is this a good idea?
-
- -- Step 1: find all the variables we want to quantify over,
- -- including Inferred, Specfied, and Required
- ; dvs <- candidateQTyVarsOfKinds $
- (tc_res_kind : map tyVarKind scoped_tvs)
- ; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs
- ; let full_dvs = dvs { dv_tvs = mkDVarSet tc_tvs }
-
- -- Step 2: quantify, mainly meaning skolemise the free variables
- ; qtkvs <- quantifyTyVars emptyVarSet full_dvs
- -- Returned 'qtkvs' are scope-sorted and skolemised
-
- -- Step 3: find the final identity of the Specified and Required tc_tvs
+ do { let tc_name = tyConName tc
+ tc_res_kind = tyConResKind tc
+ spec_req_prs = tcTyConScopedTyVars tc
+
+ (spec_req_names, spec_req_tvs) = unzip spec_req_prs
+ -- NB: spec_req_tvs includes both Specified and Required
+ -- Running example in Note [Inferring kinds for type declarations]
+ -- spec_req_prs = [ ("k1",kk1), ("a", (aa::kk1))
+ -- , ("k2",kk2), ("x", (xx::kk2))]
+ -- where "k1" dnotes the Name k1, and kk1, aa, etc are MetaTyVarss,
+ -- specifically TyVarTvs
+
+ -- Step 0: zonk and skolemise the Specified and Required binders
+ -- It's essential that they are skolems, not MetaTyVars,
+ -- for Step 3 to work right
+ ; spec_req_tvs <- mapM zonkAndSkolemise spec_req_tvs
+ -- Running example, where kk1 := kk2, so we get
+ -- [kk2,kk2]
+
+ -- Step 1: Check for duplicates
+ -- E.g. data SameKind (a::k) (b::k)
+ -- data T (a::k1) (b::k2) = MkT (SameKind a b)
+ -- Here k1 and k2 start as TyVarTvs, and get unified with each other
+ -- If this happens, things get very confused later, so fail fast
+ ; checkDuplicateTyConBinders spec_req_names spec_req_tvs
+
+ -- Step 2a: find all the Inferred variables we want to quantify over
+ -- NB: candidateQTyVarsOfKinds zonks as it goes
+ ; dvs1 <- candidateQTyVarsOfKinds $
+ (tc_res_kind : map tyVarKind spec_req_tvs)
+ ; let dvs2 = dvs1 `delCandidates` spec_req_tvs
+
+ -- Step 2b: quantify, mainly meaning skolemise the free variables
+ -- Returned 'inferred' are scope-sorted and skolemised
+ ; inferred <- quantifyTyVars emptyVarSet dvs2
+
+ -- Step 3a: rename all the Specified and Required tyvars back to
+ -- TyVars with their oroginal user-specified name. Example
+ -- class C a_r23 where ....
+ -- By this point we have scoped_prs = [(a_r23, a_r89[TyVarTv])]
+ -- We return with the TyVar a_r23[TyVar],
+ -- and ze mapping a_r89 :-> a_r23[TyVar]
+ ; traceTc "generaliseTcTyCon: before zonkRec"
+ (vcat [ text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
+ , text "inferred =" <+> pprTyVars inferred ])
+ ; (ze, final_spec_req_tvs) <- zonkRecTyVarBndrs spec_req_names spec_req_tvs
+ -- So ze maps from the tyvars that have ended up
+
+ -- Step 3b: Apply that mapping to the other variables
-- (remember they all started as TyVarTvs).
-- They have been skolemised by quantifyTyVars.
- ; scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs
- ; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs
- ; tc_res_kind <- zonkTcType tc_res_kind
+ ; (ze, inferred) <- zonkTyBndrsX ze inferred
+ ; tc_res_kind <- zonkTcTypeToTypeX ze tc_res_kind
- ; traceTc "Generalise kind pre" $
+ ; traceTc "generaliseTcTyCon: post zonk" $
vcat [ text "tycon =" <+> ppr tc
- , text "tc_tvs =" <+> pprTyVars tc_tvs
- , text "scoped_tvs =" <+> pprTyVars scoped_tvs ]
+ , text "inferred =" <+> pprTyVars inferred
+ , text "ze =" <+> ppr ze
+ , text "spec_req_prs =" <+> ppr spec_req_prs
+ , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
+ , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs ]
-- Step 4: Find the Specified and Inferred variables
- -- First, delete the Required tc_tvs from qtkvs; then
- -- partition by whether they are scoped (if so, Specified)
- ; let qtkv_set = mkVarSet qtkvs
- tc_tv_set = mkVarSet tc_tvs
- specified = scopedSort $
- [ tv | tv <- scoped_tvs
- , not (tv `elemVarSet` tc_tv_set)
- , tv `elemVarSet` qtkv_set ]
+ -- NB: spec_req_tvs = spec_tvs ++ req_tvs
+ -- And req_tvs is 1-1 with tyConTyVars
+ -- See Note [Scoped tyvars in a TcTyCon] in TyCon
+ ; let n_spec = length final_spec_req_tvs - tyConArity tc
+ (spec_tvs, req_tvs) = splitAt n_spec final_spec_req_tvs
+ specified = scopedSort spec_tvs
-- NB: maintain the L-R order of scoped_tvs
- spec_req_set = mkVarSet specified `unionVarSet` tc_tv_set
- inferred = filterOut (`elemVarSet` spec_req_set) qtkvs
-- Step 5: Make the TyConBinders.
- dep_fv_set = candidateKindVars dvs
+ to_user tv = lookupTyVarOcc ze tv `orElse` tv
+ dep_fv_set = mapVarSet to_user (candidateKindVars dvs1)
inferred_tcbs = mkNamedTyConBinders Inferred inferred
specified_tcbs = mkNamedTyConBinders Specified specified
- required_tcbs = map (mkRequiredTyConBinder dep_fv_set) tc_tvs
+ required_tcbs = map (mkRequiredTyConBinder dep_fv_set) req_tvs
-- Step 6: Assemble the final list.
final_tcbs = concat [ inferred_tcbs
, specified_tcbs
, required_tcbs ]
- scoped_tv_pairs = scoped_tv_names `zip` scoped_tvs
-
-- Step 7: Make the result TcTyCon
tycon = mkTcTyCon tc_name final_tcbs tc_res_kind
- scoped_tv_pairs
+ (mkTyVarNamePairs final_spec_req_tvs)
True {- it's generalised now -}
(tyConFlavour tc)
- ; traceTc "Generalise kind" $
+ ; traceTc "generaliseTcTyCon done" $
vcat [ text "tycon =" <+> ppr tc
- , text "tc_tvs =" <+> pprTyVars tc_tvs
, text "tc_res_kind =" <+> ppr tc_res_kind
- , text "scoped_tvs =" <+> pprTyVars scoped_tvs
+ , text "dep_fv_set =" <+> ppr dep_fv_set
+ , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs
, text "inferred =" <+> pprTyVars inferred
, text "specified =" <+> pprTyVars specified
, text "required_tcbs =" <+> ppr required_tcbs
, text "final_tcbs =" <+> ppr final_tcbs ]
- -- Step 8: Check for duplicates
- -- E.g. data SameKind (a::k) (b::k)
- -- data T (a::k1) (b::k2) = MkT (SameKind a b)
- -- Here k1 and k2 start as TyVarTvs, and get unified with each other
- ; mapM_ report_sig_tv_err (findDupTyVarTvs scoped_tv_pairs)
-
- -- Step 9: Check for validity.
- -- We do this here because we're about to put the tycon into
- -- the environment, and we don't want anything malformed in the
- -- environment.
- ; checkValidTelescope tycon
+ -- Step 8: Check for validity.
+ -- We do this here because we're about to put the tycon into the
+ -- the environment, and we don't want anything malformed there
+ ; checkTyConTelescope tycon
; return tycon }
+
+checkDuplicateTyConBinders :: [Name] -> [TcTyVar] -> TcM ()
+checkDuplicateTyConBinders spec_req_names spec_req_tvs
+ | null dups = return ()
+ | otherwise = mapM_ report_dup dups >> failM
where
- report_sig_tv_err (n1, n2)
+ dups :: [(Name,Name)]
+ dups = findDupTyVarTvs $ spec_req_names `zip` spec_req_tvs
+
+ report_dup (n1, n2)
= setSrcSpan (getSrcSpan n2) $
addErrTc (text "Couldn't match" <+> quotes (ppr n1)
<+> text "with" <+> quotes (ppr n2))
@@ -669,7 +696,7 @@ Example:
data SameKind :: k -> k -> *
data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
-For X:
+For Bad:
- a, c, d, x are Required; they are explicitly listed by the user
as the positional arguments of Bad
- b is Specified; it appears explicitly in a kind signature
@@ -711,7 +738,7 @@ How it works
These design choices are implemented by two completely different code
paths for
- * Declarations with a compulete user-specified kind signature (CUSK)
+ * Declarations with a complete user-specified kind signature (CUSK)
Handed by the CUSK case of kcLHsQTyVars.
* Declarations without a CUSK are handled by kcTyClDecl; see
@@ -726,7 +753,6 @@ tyvars; Specified are always included there.
Design alternatives
~~~~~~~~~~~~~~~~~~~
-
* For associated types we considered putting the class variables
before the local variables, in a nod to the treatment for class
methods. But it got too compilicated; see Trac #15592, comment:21ff.
@@ -761,41 +787,62 @@ that do not have a CUSK. Consider
We do kind inference as follows:
-* Step 1: Assign initial monomorophic kinds to S, T
+* Step 1: getInitialKinds, and in particular kcLHsQTyVars_NonCusk.
+ Make a unification variable for each of the Required and Specified
+ type varialbes in the header.
+
+ Record the connection between the Names the user wrote and the
+ fresh unification variables in the tcTyConScopedTyVars field
+ of the TcTyCon we are making
+ [ (a, aa)
+ , (k1, kk1)
+ , (k2, kk2)
+ , (x, xx) ]
+ (I'm using the convention that double letter like 'aa' or 'kk'
+ mean a unification variable.)
+
+ These unification variables
+ - Are TyVarTvs: that is, unification variables that can
+ unify only with other type variables.
+ See Note [Signature skolems] in TcType
+
+ - Have complete fresh Names; see TcMType
+ Note [Unification variables need fresh Names]
+
+ Assign initial monomorophic kinds to S, T
S :: kk1 -> * -> kk2 -> *
T :: kk3 -> * -> kk4 -> *
- Here kk1 etc are TyVarTvs: that is, unification variables that
- are allowed to unify only with other type variables. See
- Note [Signature skolems] in TcType
-* Step 2: Extend the environment with a TcTyCon for S and T, with
- these monomophic kinds. Now kind-check the declarations, and solve
- the resulting equalities. The goal here is to discover constraints
- on all these unification variables.
+* Step 2: kcTyClDecl. Extend the environment with a TcTyCon for S and
+ T, with these monomophic kinds. Now kind-check the declarations,
+ and solve the resulting equalities. The goal here is to discover
+ constraints on all these unification variables.
Here we find that kk1 := kk3, and kk2 := kk4.
This is why we can't use skolems for kk1 etc; they have to
unify with each other.
-* Step 3. Generalise each TyCon in turn (generaliseTcTyCon).
+* Step 3: generaliseTcTyCon. Generalise each TyCon in turn.
We find the free variables of the kind, skolemise them,
sort them out into Inferred/Required/Specified (see the above
Note [Required, Specified, and Inferred for types]),
and perform some validity checks.
- This makes the utterly-final TyConBinders for the TyCon
+ This makes the utterly-final TyConBinders for the TyCon.
All this is very similar at the level of terms: see TcBinds
Note [Quantified variables in partial type signatures]
+ But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon]
+
* Step 4. Extend the type environment with a TcTyCon for S and T, now
with their utterly-final polymorphic kinds (needed for recursive
occurrences of S, T). Now typecheck the declarations, and build the
final AlgTyCOn for S and T resp.
-The first three steps are in kcTyClGroup;
-the fourth is in tcTyClDecls.
+The first three steps are in kcTyClGroup; the fourth is in
+tcTyClDecls.
There are some wrinkles
@@ -834,7 +881,51 @@ There are some wrinkles
a) when collecting quantification candidates, in
candidateQTyVarsOfKind, we must collect skolems
b) quantifyTyVars should be a no-op on such a skolem
--}
+
+Note [Tricky scoping in generaliseTcTyCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider Trac #16342
+ class C (a::ka) x where
+ cop :: D a x => x -> Proxy a -> Proxy a
+ cop _ x = x :: Proxy (a::ka)
+
+ class D (b::kb) y where
+ dop :: C b y => y -> Proxy b -> Proxy b
+ dop _ x = x :: Proxy (b::kb)
+
+C and D are mutually recursive, by the time we get to
+generaliseTcTyCon we'll have unified kka := kkb.
+
+But when typechecking the default declarations for 'cop' and 'dop' in
+tcDlassDecl2 we need {a, ka} and {b, kb} respectively to be in scope.
+But at that point all we have is the utterly-final Class itself.
+
+Conclusion: the classTyVars of a class must have the same Mame as
+that originally assigned by the user. In our example, C must have
+classTyVars {a, ka, x} while D has classTyVars {a, kb, y}. Despite
+the fact that kka and kkb got unified!
+
+We achieve this sleight of hand in generaliseTcTyCon, using
+the specialised function zonkRecTyVarBndrs. We make the call
+ zonkRecTyVarBndrs [ka,a,x] [kkb,aa,xxx]
+where the [ka,a,x] are the Names originally assigned by the user, and
+[kkb,aa,xx] are the corresponding (post-zonking, skolemised) TcTyVars.
+zonkRecTyVarBndrs builds a recursive ZonkEnv that binds
+ kkb :-> (ka :: <zonked kind of kkb>)
+ aa :-> (a :: <konked kind of aa>)
+ etc
+That is, it maps each skolemised TcTyVars to the utterly-final
+TyVar to put in the class, with its correct user-specified name.
+When generalising D we'll do the same thing, but the ZonkEnv will map
+ kkb :-> (kb :: <zonked kind of kkb>)
+ bb :-> (b :: <konked kind of bb>)
+ etc
+Note that 'kkb' again appears in the domain of the mapping, but this
+time mapped to 'kb'. That's how C and D end up with differently-named
+final TyVars despite the fact that we unified kka:=kkb
+
+zonkRecTyVarBndrs we need to do knot-tying because of the need to
+apply this same substitution to the kind of each. -}
--------------
tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
@@ -1051,7 +1142,7 @@ kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
, con_mb_cxt = ex_ctxt, con_args = args })
= addErrCtxt (dataConCtxtName [name]) $
discardResult $
- bindExplicitTKBndrs_Skol ex_tvs $
+ bindExplicitTKBndrs_Tv ex_tvs $
do { _ <- tcHsMbContext ex_ctxt
; traceTc "kcConDecl {" (ppr name $$ ppr args)
; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index d17ac0f567..90c2b5a4a7 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -13,7 +13,7 @@ module TcValidity (
checkValidCoAxiom, checkValidCoAxBranch,
checkValidTyFamEqn, checkConsistentFamInst,
badATErr, arityErr,
- checkValidTelescope,
+ checkTyConTelescope,
allDistinctTyVars
) where
@@ -40,7 +40,7 @@ import TyCon
-- others:
import IfaceType( pprIfaceType, pprIfaceTypeApp )
-import ToIface( toIfaceType, toIfaceTyCon, toIfaceTcArgs )
+import ToIface ( toIfaceTyCon, toIfaceTcArgs, toIfaceType )
import HsSyn -- HsType
import TcRnMonad -- TcType, amongst others
import TcEnv ( tcInitTidyEnv, tcInitOpenTidyEnv )
@@ -2033,7 +2033,20 @@ checkValidTyFamEqn :: TyCon -- ^ of the type family
-> Type -- ^ Rhs
-> TcM ()
checkValidTyFamEqn fam_tc qvs typats rhs
- = do { checkValidFamPats fam_tc qvs typats rhs
+ = do { checkValidTypePats fam_tc typats
+
+ -- Check for things used on the right but not bound on the left
+ ; checkFamPatBinders fam_tc qvs typats rhs
+
+ -- Check for oversaturated visible kind arguments in a type family
+ -- equation.
+ -- See Note [Oversaturated type family equations]
+ ; when (isTypeFamilyTyCon fam_tc) $
+ case drop (tyConArity fam_tc) typats of
+ [] -> pure ()
+ spec_arg:_ ->
+ addErr $ text "Illegal oversaturated visible kind argument:"
+ <+> quotes (char '@' <> pprParendType spec_arg)
-- The argument patterns, and RHS, are all boxed tau types
-- E.g Reject type family F (a :: k1) :: k2
@@ -2078,23 +2091,6 @@ checkFamInstRhs lhs_tc lhs_tys famInsts
-- [a,b,a,a] \\ [a,a] = [b,a]
-- So we are counting repetitions
-checkValidFamPats :: TyCon -> [Var]
- -> [Type] -- ^ patterns
- -> Type -- ^ RHS
- -> TcM ()
--- Patterns in a 'type instance' or 'data instance' decl should
--- a) Shoule contain no type family applications
--- (vanilla synonyms are fine, though)
--- b) For associated types, are consistently instantiated
-checkValidFamPats fam_tc qvs pats rhs
- = do { checkValidTypePats fam_tc pats
-
- -- Check for things used on the right but not bound on the left
- ; checkFamPatBinders fam_tc qvs pats rhs
-
- ; traceTc "checkValidFamPats" (ppr fam_tc <+> ppr pats)
- }
-
-----------------
checkFamPatBinders :: TyCon
-> [TcTyVar] -- Bound on LHS of family instance
@@ -2122,24 +2118,17 @@ checkFamPatBinders fam_tc qtvs pats rhs
-- data family D Int = MkD (forall (a::k). blah)
-- In both cases, 'k' is not bound on the LHS, but is used on the RHS
-- We catch the former in kcLHsQTyVars, and the latter right here
+ -- See Note [Check type-family instance binders]
; check_tvs bad_rhs_tvs (text "mentioned in the RHS")
(text "bound on the LHS of")
-- Check for explicitly forall'd variable that is not bound on LHS
-- data instance forall a. T Int = MkT Int
-- See Note [Unused explicitly bound variables in a family pattern]
+ -- See Note [Check type-family instance binders]
; check_tvs bad_qtvs (text "bound by a forall")
(text "used in")
-
- -- Check for oversaturated visible kind arguments in a type family
- -- equation.
- -- See Note [Oversaturated type family equations]
- ; when (isTypeFamilyTyCon fam_tc) $
- case drop (tyConArity fam_tc) pats of
- [] -> pure ()
- spec_arg:_ ->
- addErr $ text "Illegal oversaturated visible kind argument:"
- <+> quotes (char '@' <> pprParendType spec_arg) }
+ }
where
pat_tvs = tyCoVarsOfTypes pats
exact_pat_tvs = exactTyCoVarsOfTypes pats
@@ -2166,21 +2155,26 @@ checkFamPatBinders fam_tc qtvs pats rhs
2 (pprTypeApp fam_tc (map expandTypeSynonyms pats))
--- | Checks for occurrences of type families in class instances and type/data
--- family instances.
+-- | Checks that a list of type patterns is valid in a matching (LHS)
+-- position of a class instances or type/data family instance.
+--
+-- Specifically:
+-- * All monotypes
+-- * No type-family applications
checkValidTypePats :: TyCon -> [Type] -> TcM ()
-checkValidTypePats tc pat_ty_args = do
- -- Check that each of pat_ty_args is a monotype.
- -- One could imagine generalising to allow
- -- instance C (forall a. a->a)
- -- but we don't know what all the consequences might be.
- traverse_ checkValidMonoType pat_ty_args
-
- -- Ensure that no type family instances occur a type pattern
- case tcTyConAppTyFamInstsAndVis tc pat_ty_args of
- [] -> pure ()
- ((tf_is_invis_arg, tf_tc, tf_args):_) -> failWithTc $
- ty_fam_inst_illegal_err tf_is_invis_arg (mkTyConApp tf_tc tf_args)
+checkValidTypePats tc pat_ty_args
+ = do { -- Check that each of pat_ty_args is a monotype.
+ -- One could imagine generalising to allow
+ -- instance C (forall a. a->a)
+ -- but we don't know what all the consequences might be.
+ traverse_ checkValidMonoType pat_ty_args
+
+ -- Ensure that no type family applications occur a type pattern
+ ; case tcTyConAppTyFamInstsAndVis tc pat_ty_args of
+ [] -> pure ()
+ ((tf_is_invis_arg, tf_tc, tf_args):_) -> failWithTc $
+ ty_fam_inst_illegal_err tf_is_invis_arg
+ (mkTyConApp tf_tc tf_args) }
where
inst_ty = mkTyConApp tc pat_ty_args
@@ -2294,8 +2288,52 @@ checkConsistentFamInst (InClsInst { ai_class = clas
| otherwise = BindMe
-{- Note [Matching in the consistent-instantation check]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Check type-family instance binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In a type family instance, we require (of course), type variables
+used on the RHS are matched on the LHS. This is checked by
+checkFamPatBinders. 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 unbound. Contrast that with this example (Trac #13985)
+
+ 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 -> *)
+
+
+Note [Matching in the consistent-instantation check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Matching the class-instance header to family-instance tyvars is
tricker than it sounds. Consider (Trac #13972)
class C (a :: k) where
@@ -2547,8 +2585,8 @@ family instance equations: see Note [Arity of data families] in FamInstEnv.
* *
************************************************************************
-Note [Bad telescopes]
-~~~~~~~~~~~~~~~~~~~~~
+Note [Bad TyCon telescopes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
Now that we can mix type and kind variables, there are an awful lot of
ways to shoot yourself in the foot. Here are some.
@@ -2566,54 +2604,93 @@ Note that b is not bound. Yet its kind mentions a. Because we have
a nice rule that all implicitly bound variables come before others,
this is bogus.
-To catch these errors, we call checkValidTelescope during kind-checking
-datatype declarations. See also
-Note [Required, Specified, and Inferred for types] in TcTyClsDecls.
+To catch these errors, we call checkTyConTelescope during kind-checking
+datatype declarations. This checks for
+
+* Ill-scoped binders. From (1) and (2) above we can get putative
+ kinds like
+ T1 :: forall (a:k) (k:*) (b:k). SameKind a b -> *
+ where 'k' is mentioned a's kind before k is bound
+
+ This is easy to check for: just look for
+ out-of-scope variables in the kind
-Note [Keeping scoped variables in order: Explicit] discusses how this
-check works for `forall x y z.` written in a type.
+* We should arguably also check for ambiguous binders
+ but we don't. See Note [Ambiguous kind vars].
+See also
+ * Note [Required, Specified, and Inferred for types] in TcTyClsDecls.
+ * Note [Keeping scoped variables in order: Explicit] discusses how
+ this check works for `forall x y z.` written in a type.
+
+Note [Ambiguous kind vars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+We used to be concerned about ambiguous binders. Suppose we have the kind
+ S1 :: forall k -> * -> *
+ S2 :: forall k. * -> *
+Here S1 is OK, because k is Required, and at a use of S1 we will
+see (S1 *) or (S1 (*->*)) or whatever.
+
+But S2 is /not/ OK because 'k' is Specfied (and hence invisible) and
+we have no way (ever) to figure out how 'k' should be instantiated.
+For example if we see (S2 Int), that tells us nothing about k's
+instantiation. (In this case we'll instantiate it to Any, but that
+seems wrong.) This is really the same test as we make for ambiguous
+type in term type signatures.
+
+Now, it's impossible for a Specified variable not to occur
+at all in the kind -- after all, it is Specified so it must have
+occurred. (It /used/ to be possible; see tests T13983 and T7873. But
+with the advent of the forall-or-nothing rule for kind variables,
+those strange cases went away.)
+
+But one might worry about
+ type v k = *
+ S3 :: forall k. V k -> *
+which appears to mention 'k' but doesn't really. Or
+ S4 :: forall k. F k -> *
+where F is a type function. But we simply don't check for
+those cases of ambiguity, yet anyway. The worst that can happen
+is ambiguity at the call sites.
+
+Historical note: this test used to be called reportFloatingKvs.
-}
-- | Check a list of binders to see if they make a valid telescope.
--- The key property we're checking for is scoping. For example:
--- > data SameKind :: k -> k -> *
--- > data X a k (b :: k) (c :: SameKind a b)
--- Kind inference says that a's kind should be k. But that's impossible,
--- because k isn't in scope when a is bound. This check has to come before
--- general validity checking, because once we kind-generalise, this sort
--- of problem is harder to spot (as we'll generalise over the unbound
--- k in a's type.)
---
--- See Note [Generalisation for type constructors] in TcTyClsDecls for
--- data type declarations
--- and Note [Keeping scoped variables in order: Explicit] in TcHsType
--- for foralls
-checkValidTelescope :: TyCon -> TcM ()
-checkValidTelescope tc
- = unless (null bad_tcbs) $ addErr $
+-- See Note [Bad TyCon telescopes]
+type TelescopeAcc
+ = ( TyVarSet -- Bound earlier in the telescope
+ , Bool -- At least one binder occurred (in a kind) before
+ -- it was bound in the telescope. E.g.
+ ) -- T :: forall (a::k) k. blah
+
+checkTyConTelescope :: TyCon -> TcM ()
+checkTyConTelescope tc
+ | bad_scope
+ = -- See "Ill-scoped binders" in Note [Bad TyCon telescopes]
+ addErr $
vcat [ hang (text "The kind of" <+> quotes (ppr tc) <+> text "is ill-scoped")
- 2 (text "Inferred kind:" <+> ppr tc <+> dcolon <+> ppr_untidy (tyConKind tc))
+ 2 pp_tc_kind
, extra
, hang (text "Perhaps try this order instead:")
- 2 (pprTyVars sorted_tidied_tvs) ]
+ 2 (pprTyVars sorted_tvs) ]
+
+ | otherwise
+ = return ()
where
- ppr_untidy ty = pprIfaceType (toIfaceType ty)
tcbs = tyConBinders tc
- tvs = binderVars tcbs
- (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv (scopedSort tvs)
+ tvs = binderVars tcbs
+ sorted_tvs = scopedSort tvs
- (_, bad_tcbs) = foldl add_one (mkVarSet tvs, []) tcbs
+ (_, bad_scope) = foldl add_one (emptyVarSet, False) tcbs
- add_one :: (TyVarSet, [TyConBinder])
- -> TyConBinder -> (TyVarSet, [TyConBinder])
- add_one (bad_bndrs, acc) tvb
- | fkvs `intersectsVarSet` bad_bndrs = (bad', tvb : acc)
- | otherwise = (bad', acc)
+ add_one :: TelescopeAcc -> TyConBinder -> TelescopeAcc
+ add_one (bound, bad_scope) tcb
+ = ( bound `extendVarSet` tv
+ , bad_scope || not (isEmptyVarSet (fkvs `minusVarSet` bound)) )
where
- tv = binderVar tvb
+ tv = binderVar tcb
fkvs = tyCoVarsOfType (tyVarKind tv)
- bad' = bad_bndrs `delVarSet` tv
inferred_tvs = [ binderVar tcb
| tcb <- tcbs, Inferred == tyConBinderArgFlag tcb ]
@@ -2623,6 +2700,14 @@ checkValidTelescope tc
pp_inf = parens (text "namely:" <+> pprTyVars inferred_tvs)
pp_spec = parens (text "namely:" <+> pprTyVars specified_tvs)
+ pp_tc_kind = text "Inferred kind:" <+> ppr tc <+> dcolon <+> ppr_untidy (tyConKind tc)
+ ppr_untidy ty = pprIfaceType (toIfaceType ty)
+ -- We need ppr_untidy here because pprType will tidy the type, which
+ -- will turn the bogus kind we are trying to report
+ -- T :: forall (a::k) k (b::k) -> blah
+ -- into a misleadingly sanitised version
+ -- T :: forall (a::k) k1 (b::k1) -> blah
+
extra
| null inferred_tvs && null specified_tvs
= empty
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 4557ad6388..ce40d74278 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -871,24 +871,42 @@ data TyCon
-- See Note [The binders/kind/arity fields of a TyCon]
tyConBinders :: [TyConBinder], -- ^ Full binders
- tyConTyVars :: [TyVar], -- ^ TyVar binders
- tyConResKind :: Kind, -- ^ Result kind
- tyConKind :: Kind, -- ^ Kind of this TyCon
- tyConArity :: Arity, -- ^ Arity
+ tyConTyVars :: [TyVar], -- ^ TyVar binders
+ tyConResKind :: Kind, -- ^ Result kind
+ tyConKind :: Kind, -- ^ Kind of this TyCon
+ tyConArity :: Arity, -- ^ Arity
+
+ -- NB: the TyConArity of a TcTyCon must match
+ -- the number of Required (positional, user-specified)
+ -- arguments to the type constructor; see the use
+ -- of tyConArity in generaliseTcTyCon
tcTyConScopedTyVars :: [(Name,TyVar)],
- -- ^ Scoped tyvars over the tycon's body
- -- See Note [How TcTyCons work] in TcTyClsDecls
- -- Order *does* matter: for TcTyCons with a CUSK,
- -- it's the correct dependency order. For TcTyCons
- -- without a CUSK, it's the original left-to-right
- -- that the user wrote. Nec'y for getting Specified
- -- variables in the right order.
+ -- ^ Scoped tyvars over the tycon's body
+ -- See Note [Scoped tyvars in a TcTyCon]
+
tcTyConIsPoly :: Bool, -- ^ Is this TcTyCon already generalized?
tcTyConFlavour :: TyConFlavour
-- ^ What sort of 'TyCon' this represents.
}
+{- Note [Scoped tyvars in a TcTyCon]
+
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The tcTyConScopedTyVars field records the lexicial-binding connection
+between the original, user-specified Name (i.e. thing in scope) and
+the TcTyVar that the Name is bound to.
+
+Order *does* matter; the tcTyConScopedTyvars list consists of
+ specified_tvs ++ required_tvs
+
+where
+ * specified ones first
+ * required_tvs the same as tyConTyVars
+ * tyConArity = length required_tvs
+
+See also Note [How TcTyCons work] in TcTyClsDecls
+-}
-- | Represents right-hand-sides of 'TyCon's for algebraic types
data AlgTyConRhs