Commit 80dfcee6 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

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.
parent e6ce1743
Pipeline #3105 passed with stages
in 317 minutes and 17 seconds
......@@ -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)
......
......@@ -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"
......
......@@ -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')
......
......@@ -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
......
......@@ -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"
......
......@@ -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")