Commit f594a68a authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Use level numbers for generalisation

This fixes #15809, and is covered in
Note [Use level numbers for quantification] in TcMType.

This patch removes the "global tyvars" from the
environment, a nice little win.
parent d9c6b86e
......@@ -56,9 +56,6 @@ module TcEnv(
-- Defaults
tcGetDefaultTys,
-- Global type variables
tcGetGlobalTyCoVars,
-- Template Haskell stuff
checkWellStaged, tcMetaTy, thLevel,
topIdLvl, isBrackStage,
......@@ -84,7 +81,6 @@ import PrelNames
import TysWiredIn
import Id
import Var
import VarSet
import RdrName
import InstEnv
import DataCon ( DataCon )
......@@ -108,7 +104,6 @@ import Encoding
import FastString
import ListSetOps
import ErrUtils
import Util
import Maybes( MaybeErr(..), orElse )
import qualified GHC.LanguageExtensions as LangExt
......@@ -576,7 +571,7 @@ tc_extend_local_env top_lvl extra_env thing_inside
-- as free in the types of extra_env.
= do { traceTc "tc_extend_local_env" (ppr extra_env)
; env0 <- getLclEnv
; env1 <- tcExtendLocalTypeEnv env0 extra_env
; let env1 = tcExtendLocalTypeEnv env0 extra_env
; stage <- getStage
; let env2 = extend_local_env (top_lvl, thLevel stage) extra_env env1
; setLclEnv env2 thing_inside }
......@@ -594,52 +589,9 @@ tc_extend_local_env top_lvl extra_env thing_inside
, tcl_th_bndrs = extendNameEnvList th_bndrs -- We only track Ids in tcl_th_bndrs
[(n, thlvl) | (n, ATcId {}) <- pairs] }
tcExtendLocalTypeEnv :: TcLclEnv -> [(Name, TcTyThing)] -> TcM TcLclEnv
tcExtendLocalTypeEnv :: TcLclEnv -> [(Name, TcTyThing)] -> TcLclEnv
tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things
| isEmptyVarSet extra_tvs
= return (lcl_env { tcl_env = extendNameEnvList lcl_type_env tc_ty_things })
| otherwise
= do { global_tvs <- readMutVar (tcl_tyvars lcl_env)
; new_g_var <- newMutVar (global_tvs `unionVarSet` extra_tvs)
; return (lcl_env { tcl_tyvars = new_g_var
, tcl_env = extendNameEnvList lcl_type_env tc_ty_things } ) }
where
extra_tvs = foldr get_tvs emptyVarSet tc_ty_things
get_tvs (_, ATcId { tct_id = id, tct_info = closed }) tvs
= case closed of
ClosedLet -> ASSERT2( is_closed_type, ppr id $$ ppr (idType id) )
tvs
_other -> tvs `unionVarSet` id_tvs
where
id_ty = idType id
id_tvs = tyCoVarsOfType id_ty
id_co_tvs = closeOverKinds (coVarsOfType id_ty)
is_closed_type = not (anyVarSet isTyVar (id_tvs `minusVarSet` id_co_tvs))
-- We only care about being closed wrt /type/ variables
-- E.g. a top-level binding might have a type like
-- foo :: t |> co
-- where co :: * ~ *
-- or some other as-yet-unsolved kind coercion
get_tvs (_, ATyVar _ tv) tvs -- See Note [Global TyVars]
= tvs `unionVarSet` tyCoVarsOfType (tyVarKind tv) `extendVarSet` tv
get_tvs (_, ATcTyCon tc) tvs = tvs `unionVarSet` tyCoVarsOfType (tyConKind tc)
get_tvs (_, AGlobal {}) tvs = tvs
get_tvs (_, APromotionErr {}) tvs = tvs
-- Note [Global TyVars]
-- It's important to add the in-scope tyvars to the global tyvar set
-- as well. Consider
-- f (_::r) = let g y = y::r in ...
-- Here, g mustn't be generalised. This is also important during
-- class and instance decls, when we mustn't generalise the class tyvars
-- when typechecking the methods.
--
-- Nor must we generalise g over any kind variables free in r's kind
= lcl_env { tcl_env = extendNameEnvList lcl_type_env tc_ty_things }
{- *********************************************************************
* *
......
......@@ -1849,7 +1849,7 @@ kcLHsQTyVars_Cusk name flav
; let inf_candidates = candidates `delCandidates` spec_req_tkvs
; inferred <- quantifyTyVars emptyVarSet inf_candidates
; inferred <- quantifyTyVars inf_candidates
-- NB: 'inferred' comes back sorted in dependency order
; scoped_kvs <- mapM zonkTyCoVarKind scoped_kvs
......@@ -2289,26 +2289,24 @@ kindGeneralizeSome should_gen kind_or_type
-- use the "Kind" variant here, as any types we see
-- here will already have all type variables quantified;
-- thus, every free variable is really a kv, never a tv.
; dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) <- candidateQTyVarsOfKind kind_or_type
; dvs <- candidateQTyVarsOfKind kind_or_type
; let promote_kvs = filterVarSet (not . should_gen) $ dVarSetToVarSet kvs
promote_tvs = filterVarSet (not . should_gen) $ dVarSetToVarSet tvs
-- So 'dvs' are the variables free in kind_or_type, with a level greater
-- than the ambient level, hence candidates for quantification
-- Next: filter out the ones we don't want to generalize (specified by should_gen)
-- and promote them instead
; (_, promoted) <- promoteTyVarSet (promote_kvs `unionVarSet` promote_tvs)
; let (to_promote, dvs') = partitionCandidates dvs (not . should_gen)
; gbl_tvs <- tcGetGlobalTyCoVars -- already zonked
; let dvs' = dvs { dv_kvs = kvs `dVarSetMinusVarSet` promote_kvs
, dv_tvs = tvs `dVarSetMinusVarSet` promote_tvs }
; qkvs <- quantifyTyVars gbl_tvs dvs'
; (_, promoted) <- promoteTyVarSet (dVarSetToVarSet to_promote)
; qkvs <- quantifyTyVars dvs'
; traceTc "kindGeneralizeSome }" $
vcat [ text "Kind or type:" <+> ppr kind_or_type
, text "dvs:" <+> ppr dvs
, text "dvs':" <+> ppr dvs'
, text "promote_kvs:" <+> pprTyVars (nonDetEltsUniqSet promote_kvs)
, text "promote_tvs:" <+> pprTyVars (nonDetEltsUniqSet promote_tvs)
, text "to_promote:" <+> pprTyVars (dVarSetElems to_promote)
, text "promoted:" <+> pprTyVars (nonDetEltsUniqSet promoted)
, text "gbl_tvs:" <+> pprTyVars (nonDetEltsUniqSet gbl_tvs)
, text "qkvs:" <+> pprTyVars qkvs ]
; return qkvs }
......
......@@ -820,7 +820,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
-- check there too!
; let scoped_tvs = imp_tvs ++ exp_tvs
; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
; qtvs <- quantifyTyVars emptyVarSet dvs
; qtvs <- quantifyTyVars dvs
-- Zonk the patterns etc into the Type world
; (ze, qtvs) <- zonkTyBndrs qtvs
......
This diff is collapsed.
......@@ -1888,7 +1888,8 @@ runTcInteractive hsc_env thing_inside
, tcg_imports = imports
}
; lcl_env' <- tcExtendLocalTypeEnv lcl_env lcl_ids
lcl_env' = tcExtendLocalTypeEnv lcl_env lcl_ids
; setEnvs (gbl_env', lcl_env') thing_inside }
where
(home_insts, home_fam_insts) = hptInstances hsc_env (\_ -> True)
......@@ -1930,9 +1931,8 @@ types have free RuntimeUnk skolem variables, standing for unknown
types. If we don't register these free TyVars as global TyVars then
the typechecker will try to quantify over them and fall over in
skolemiseQuantifiedTyVar. so we must add any free TyVars to the
typechecker's global TyVar set. That is most conveniently by using
tcExtendLocalTypeEnv, which automatically extends the global TyVar
set.
typechecker's global TyVar set. That is done by using
tcExtendLocalTypeEnv.
We do this by splitting out the Ids with open types, using 'is_closed'
to do the partition. The top-level things go in the global TypeEnv;
......
......@@ -331,8 +331,7 @@ initTcWithGbl :: HscEnv
-> TcM r
-> IO (Messages, Maybe r)
initTcWithGbl hsc_env gbl_env loc do_this
= do { tvs_var <- newIORef emptyVarSet
; lie_var <- newIORef emptyWC
= do { lie_var <- newIORef emptyWC
; errs_var <- newIORef (emptyBag, emptyBag)
; let lcl_env = TcLclEnv {
tcl_errs = errs_var,
......@@ -344,7 +343,6 @@ initTcWithGbl hsc_env gbl_env loc do_this
tcl_arrow_ctxt = NoArrowCtxt,
tcl_env = emptyNameEnv,
tcl_bndrs = [],
tcl_tyvars = tvs_var,
tcl_lie = lie_var,
tcl_tclvl = topTcLevel
}
......@@ -1667,8 +1665,7 @@ setLclTypeEnv :: TcLclEnv -> TcM a -> TcM a
setLclTypeEnv lcl_env thing_inside
= updLclEnv upd thing_inside
where
upd env = env { tcl_env = tcl_env lcl_env,
tcl_tyvars = tcl_tyvars lcl_env }
upd env = env { tcl_env = tcl_env lcl_env }
traceTcConstraints :: String -> TcM ()
traceTcConstraints msg
......
......@@ -833,12 +833,6 @@ data TcLclEnv -- Changes as we move inside an expression
tcl_bndrs :: TcBinderStack, -- Used for reporting relevant bindings,
-- and for tidying types
tcl_tyvars :: TcRef TcTyVarSet, -- The "global tyvars"
-- Namely, the in-scope TyVars bound in tcl_env,
-- plus the tyvars mentioned in the types of Ids bound
-- in tcl_lenv.
-- Why mutable? see notes with tcGetGlobalTyCoVars
tcl_lie :: TcRef WantedConstraints, -- Place to accumulate type constraints
tcl_errs :: TcRef Messages -- Place to accumulate errors
}
......
......@@ -110,12 +110,10 @@ tcRule (HsRule { rd_ext = ext
-- during zonking (see TcHsSyn.zonkRule)
; let tpl_ids = lhs_evs ++ id_bndrs
; gbls <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level
-- monomorphic bindings from the MR; test tc111
; forall_tkvs <- candidateQTyVarsOfTypes $
map (mkSpecForAllTys tv_bndrs) $ -- don't quantify over lexical tyvars
rule_ty : map idType tpl_ids
; qtkvs <- quantifyTyVars gbls forall_tkvs
; qtkvs <- quantifyTyVars forall_tkvs
; traceTc "tcRule" (vcat [ pprFullRuleName rname
, ppr forall_tkvs
, ppr qtkvs
......
......@@ -764,9 +764,8 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
psig_theta = [ pred | sig <- partial_sigs
, pred <- sig_inst_theta sig ]
; gbl_tvs <- tcGetGlobalTyCoVars
; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus)
; qtkvs <- quantifyTyVars gbl_tvs dep_vars
; qtkvs <- quantifyTyVars dep_vars
; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) }
......@@ -1029,7 +1028,7 @@ decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
-- Step 3: decide which kind/type variables to quantify over
; qtvs <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
; qtvs <- decideQuantifiedTyVars name_taus psigs candidates
-- Step 4: choose which of the remaining candidate
-- predicates to actually quantify over
......@@ -1081,7 +1080,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
; taus <- mapM (TcM.zonkTcType . snd) name_taus
; mono_tvs0 <- tcGetGlobalTyCoVars
; tc_lvl <- TcM.getTcLevel
; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
co_vars = coVarsOfTypes (psig_tys ++ taus)
......@@ -1092,19 +1091,34 @@ decideMonoTyVars infer_mode name_taus psigs candidates
-- E.g. If we can't quantify over co :: k~Type, then we can't
-- quantify over k either! Hence closeOverKinds
mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
tyCoVarsOfTypes candidates
-- We need to grab all the non-quantifiable tyvars in the
-- candidates so that we can grow this set to find other
-- non-quantifiable tyvars. This can happen with something
-- like
-- f x y = ...
-- where z = x 3
-- The body of z tries to unify the type of x (call it alpha[1])
-- with (beta[2] -> gamma[2]). This unification fails because
-- alpha is untouchable. But we need to know not to quantify over
-- beta or gamma, because they are in the equality constraint with
-- alpha. Actual test case: typecheck/should_compile/tc213
mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
eq_constraints = filter isEqPrimPred candidates
mono_tvs2 = growThetaTyVars eq_constraints mono_tvs1
constrained_tvs = (growThetaTyVars eq_constraints
constrained_tvs = filterVarSet (isQuantifiableTv tc_lvl) $
(growThetaTyVars eq_constraints
(tyCoVarsOfTypes no_quant)
`minusVarSet` mono_tvs2)
`delVarSetList` psig_qtvs
-- constrained_tvs: the tyvars that we are not going to
-- quantify solely because of the moonomorphism restriction
-- quantify solely because of the monomorphism restriction
--
-- (`minusVarSet` mono_tvs1`): a type variable is only
-- (`minusVarSet` mono_tvs2`): a type variable is only
-- "constrained" (so that the MR bites) if it is not
-- free in the environment (#13785)
--
......@@ -1126,7 +1140,6 @@ decideMonoTyVars infer_mode name_taus psigs candidates
; traceTc "decideMonoTyVars" $ vcat
[ text "mono_tvs0 =" <+> ppr mono_tvs0
, text "mono_tvs1 =" <+> ppr mono_tvs1
, text "no_quant =" <+> ppr no_quant
, text "maybe_quant =" <+> ppr maybe_quant
, text "eq_constraints =" <+> ppr eq_constraints
......@@ -1215,13 +1228,12 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
------------------
decideQuantifiedTyVars
:: TyCoVarSet -- Monomorphic tyvars
-> [(Name,TcType)] -- Annotated theta and (name,tau) pairs
:: [(Name,TcType)] -- Annotated theta and (name,tau) pairs
-> [TcIdSigInst] -- Partial signatures
-> [PredType] -- Candidates, zonked
-> TcM [TyVar]
-- Fix what tyvars we are going to quantify over, and quantify them
decideQuantifiedTyVars mono_tvs name_taus psigs candidates
decideQuantifiedTyVars name_taus psigs candidates
= do { -- Why psig_tys? We try to quantify over everything free in here
-- See Note [Quantification and partial signatures]
-- Wrinkles 2 and 3
......@@ -1230,7 +1242,6 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates
; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
, pred <- sig_inst_theta sig ]
; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
; mono_tvs <- TcM.zonkTyCoVarsAndFV mono_tvs
; let -- Try to quantify over variables free in these types
psig_tys = psig_tv_tys ++ psig_theta
......@@ -1258,7 +1269,7 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates
, text "grown_tcvs =" <+> ppr grown_tcvs
, text "dvs =" <+> ppr dvs_plus])
; quantifyTyVars mono_tvs dvs_plus }
; quantifyTyVars dvs_plus }
------------------
growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
......
......@@ -604,7 +604,7 @@ generaliseTcTyCon tc
-- Step 2b: quantify, mainly meaning skolemise the free variables
-- Returned 'inferred' are scope-sorted and skolemised
; inferred <- quantifyTyVars emptyVarSet dvs2
; inferred <- quantifyTyVars dvs2
-- Step 3a: rename all the Specified and Required tyvars back to
-- TyVars with their oroginal user-specified name. Example
......@@ -2320,7 +2320,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
-- check there too!
; let scoped_tvs = imp_tvs ++ exp_tvs
; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
; qtvs <- quantifyTyVars emptyVarSet dvs
; qtvs <- quantifyTyVars dvs
; (ze, qtvs) <- zonkTyBndrs qtvs
; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
......
T14040a.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl0
-> (forall y. p0 _0 'WeirdNil)
• Cannot apply expression of type ‘Sing wl
-> (forall y. p _0 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
-> Sing xs
-> p0 GHC.Types.Any xs
-> p0 GHC.Types.Any ('WeirdCons x xs))
-> p0 GHC.Types.Any wl0
-> p GHC.Types.Any xs
-> p GHC.Types.Any ('WeirdCons x xs))
-> p _1 wl
to a visible type argument ‘(WeirdList z)’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
......
......@@ -34,8 +34,14 @@ instance Ix key => Mark (ST s) (STUArray s key Bool) key where
seen s = liftM (map fst . filter snd) (getAssocs s)
-- traversing the hull suc^*(start) with loop detection
-- trav :: forall f f2 m store key.
-- (Foldable f, Foldable f2, Mark m store key, Monad m)
-- => (key -> f key) -> f2 key -> (key, key) -> m store
trav suc start i = new i >>= \ c -> mapM_ (compo c) start >> return c
where compo c x = markQ c x >>= flip unless (visit c x)
where -- compo :: (Monad m, Mark m store' key) => store' -> key -> m ()
compo c x = markQ c x >>= flip unless (visit c x)
-- visit :: (Monad m, Mark m store' key) => store' -> key -> m ()
visit c x = mark c x >> mapM_ (compo c) (suc x)
-- sample graph
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment