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

Refactor kindGeneralize and friends

This commit should have no change in behavior.(*)

The observation was that Note [Recipe for checking a signature]
says that every metavariable in a type-checked type must either
  (A) be generalized
  (B) be promoted
  (C) be zapped.
Yet the code paths for doing these were all somewhat separate.
This led to some steps being skipped. This commit shores this
all up. The key innovation is TcHsType.kindGeneralizeSome, with
appropriate commentary.

This commit also sets the stage for #15809, by turning the
WARNing about bad level-numbers in generalisation into an
ASSERTion. The actual fix for #15809 will be in a separate

Other changes:
 * zonkPromoteType is now replaced by kindGeneralizeNone.
   This might have a small performance degradation, because
   zonkPromoteType zonked and promoted all at once. The new
   code path promotes first, and then zonks.

 * A call to kindGeneralizeNone was added in tcHsPartialSigType.
   I think this was a lurking bug, because it did not follow
   Note [Recipe for checking a signature]. I did not try to
   come up with an example showing the bug. This is the (*)

   Because of this change, there is an error message regression
   in partial-sigs/should_fail/T14040a. This problem isn't really
   a direct result of this refactoring, but is a symptom of
   something deeper. See #16775, which addresses the deeper

 * I added a short-cut to quantifyTyVars, in case there's
   nothing to quantify.

 * There was a horribly-outdated Note that wasn't referred
   to. Gone now.

 * While poking around with T14040a, I discovered a small
   mistake in the Coercion.simplifyArgsWorker. Easy to fix,

 * See new Note [Free vars in coercion hole] in TcMType.
   Previously, we were doing the wrong thing when looking
   at a coercion hole in the gather-candidates algorithm.
   Fixed now, with lengthy explanation.

Metric Decrease:
parent de1723b2
......@@ -1553,7 +1553,7 @@ flatten_tyvar1 tv
(ppr tv <+> equals <+> ppr ty)
; role <- getRole
; return (FTRFollowed ty (mkReflCo role ty)) } ;
Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv)
Nothing -> do { traceFlat "Unfilled tyvar" (pprTyVar tv)
; fr <- getFlavourRole
; flatten_tyvar2 tv fr } }
This diff is collapsed.
......@@ -65,7 +65,7 @@ module TcMType (
tidyEvVar, tidyCt, tidySkolemInfo,
zonkTcTyVar, zonkTcTyVars,
zonkTcTyVarToTyVar, zonkTyVarTyVarPairs,
zonkTyCoVarsAndFV, zonkTcTypeAndFV,
zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV,
candidateQTyVarsOfType, candidateQTyVarsOfKind,
candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
......@@ -759,7 +759,7 @@ cloneAnonMetaTyVar info tv kind
= do { details <- newMetaDetails info
; name <- cloneMetaTyVarName (tyVarName tv)
; let tyvar = mkTcTyVar name kind details
; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
; traceTc "cloneAnonMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar))
; return tyvar }
newFskTyVar :: TcType -> TcM TcTyVar
......@@ -1145,9 +1145,12 @@ data CandidatesQTvs
-- See Note [CandidatesQTvs determinism and order]
-- Invariants:
-- * All variables stored here are MetaTvs. No exceptions.
-- * All variables are fully zonked, including their kinds
-- This *can* contain skolems. For example, in `data X k :: k -> Type`
-- we need to know that the k is a dependent variable. This is done
-- by collecting the candidates in the kind.
= DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent)
, dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent)
-- A variable may appear in both sets
......@@ -1252,11 +1255,11 @@ collect_cand_qtvs is_dep bound dvs ty
go dv (CoercionTy co) = collect_cand_qtvs_co bound dv co
go dv (TyVarTy tv)
| is_bound tv = return dv
| otherwise = do { m_contents <- isFilledMetaTyVar_maybe tv
; case m_contents of
Just ind_ty -> go dv ind_ty
Nothing -> go_tv dv tv }
| is_bound tv = return dv
| otherwise = do { m_contents <- isFilledMetaTyVar_maybe tv
; case m_contents of
Just ind_ty -> go dv ind_ty
Nothing -> go_tv dv tv }
go dv (ForAllTy (Bndr tv _) ty)
= do { dv1 <- collect_cand_qtvs True bound dv (tyVarKind tv)
......@@ -1286,7 +1289,12 @@ collect_cand_qtvs is_dep bound dvs ty
intersectsVarSet bound (tyCoVarsOfType tv_kind)
then -- See Note [Naughty quantification candidates]
do { traceTc "Zapping naughty quantifier" (pprTyVar tv)
do { traceTc "Zapping naughty quantifier" $
vcat [ ppr tv <+> dcolon <+> ppr tv_kind
, text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound)
, text "fvs:" <+> pprTyVars (nonDetEltsUniqSet $
tyCoVarsOfType tv_kind) ]
; writeMetaTyVar tv (anyTypeOfKind tv_kind)
; collect_cand_qtvs True bound dv tv_kind }
......@@ -1295,6 +1303,7 @@ collect_cand_qtvs is_dep bound dvs ty
| otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' }
-- See Note [Order of accumulation]
; collect_cand_qtvs True emptyVarSet dv' tv_kind } }
-- Why emptyVarSet? See Note [Closing over free variable kinds] in TyCoRep
collect_cand_qtvs_co :: VarSet -- bound variables
-> CandidatesQTvs -> Coercion
......@@ -1320,10 +1329,19 @@ collect_cand_qtvs_co bound = go_co
go_co dv (KindCo co) = go_co dv co
go_co dv (SubCo co) = go_co dv co
go_co dv (HoleCo hole) = do m_co <- unpackCoercionHole_maybe hole
case m_co of
Just co -> go_co dv co
Nothing -> go_cv dv (coHoleCoVar hole)
go_co dv@(DV { dv_cvs = cvs }) (HoleCo hole)
= do m_co <- unpackCoercionHole_maybe hole
case m_co of
Just co -> go_co dv co
| cv `elemVarSet` cvs -> return dv
| otherwise
-> collect_cand_qtvs True bound (dv { dv_cvs = cvs `extendVarSet` cv })
-- See Note [Free vars in coercion hole]
where cv = coHoleCoVar hole
cv_type = varType cv
go_co dv (CoVarCo cv) = go_cv dv cv
......@@ -1343,6 +1361,8 @@ collect_cand_qtvs_co bound = go_co
go_cv dv@(DV { dv_cvs = cvs }) cv
| is_bound cv = return dv
| cv `elemVarSet` cvs = return dv
-- Why emptyVarSet below? See Note [Closing over free variable kinds] in TyCoRep
| otherwise = collect_cand_qtvs True emptyVarSet
(dv { dv_cvs = cvs `extendVarSet` cv })
(idType cv)
......@@ -1368,6 +1388,37 @@ element to the right.
Note that the unitDVarSet/mappend implementation would not be wrong
against any specification -- just suboptimal and confounding to users.
Note [Free vars in coercion hole]
First, read Note [Closing over free variable kinds] in TyCoRep, paying
attention to the end of the Note about using an empty bound set when
traversing a variable's kind.
We do not do this for coercion holes. (The other Note doesn't address coercion
holes, because that Note is about Core, where coercion holes do not exist.)
Coercion holes are *never* bound. Yet a coercion hole *can* mention a locally
bound type/coercion variable in its kind. This would happen if the constraint
associated with the coercion hole is inside an implication constraint, and the
bound variables in the hole's type are the skolems of the implication. We do
not want to collect *all* free variables in the coercion hole's kind, because
that list might contain skolems. (This actually happened in test case
dependent/should_fail/BadTelescope5.) Instead, we remember the bound variables
when traversing the coercion hole's kind so we can avoid visiting bound
variables there.
Example: forall k1 k2. .... |> (hole :: k1 ~# k2) ....
This is obviously bogus, but if we collect k1 and k2 into the candidates,
we'll have skolems in the CandidatesQTvs, directly contradicting that data
structure's invariant. See its definition.
Of course, Note [Closing over free variable kinds] observes that maintaining
a bound set while going into a kind is potentially wrong, if there is shadowing.
However, given that we are in the type-checker now, not in Core, shadowing cannot
happen: the renamer would have sorted it out. So the bug that Note is fixing
cannot occur here, and so we do not have to zap the bound set when looking at
{- *********************************************************************
......@@ -1426,6 +1477,13 @@ quantifyTyVars
-- associated type declarations. Also accepts covars, but *never* returns any.
quantifyTyVars gbl_tvs
dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs, dv_cvs = covars })
-- short-circuit common case
| isEmptyDVarSet dep_tkvs
, isEmptyDVarSet nondep_tkvs
= do { traceTc "quantifyTyVars has nothing to quantify" empty
; return [] }
| otherwise
= do { outer_tclvl <- getTcLevel
; traceTc "quantifyTyVars 1" (vcat [ppr outer_tclvl, ppr dvs, ppr gbl_tvs])
; let co_tvs = closeOverKinds covars
......@@ -1461,6 +1519,8 @@ quantifyTyVars gbl_tvs
all_ok = dep_kvs == dep_kvs2 && nondep_tvs == nondep_tvs2
bad_msg = hang (text "Quantification by level numbers would fail")
2 (vcat [ text "Outer level =" <+> ppr outer_tclvl
, text "gbl_tvs =" <+> ppr gbl_tvs
, text "mono_tvs =" <+> ppr mono_tvs
, text "dep_tkvs =" <+> ppr dep_tkvs
, text "co_vars =" <+> vcat [ ppr cv <+> dcolon <+> ppr (varType cv)
| cv <- nonDetEltsUniqSet covars ]
......@@ -1469,7 +1529,7 @@ quantifyTyVars gbl_tvs
, text "dep_kvs2 =" <+> ppr dep_kvs2
, text "nondep_tvs =" <+> ppr nondep_tvs
, text "nondep_tvs2 =" <+> ppr nondep_tvs2 ])
; WARN( not all_ok, bad_msg ) return ()
; MASSERT2( all_ok, bad_msg )
-- In the non-PolyKinds case, default the kind variables
-- to *, and zonk the tyvars as usual. Notice that this
......@@ -1843,6 +1903,10 @@ zonkTyCoVarsAndFV tycovars
-- the ordering by turning it into a nondeterministic set and the order
-- of zonking doesn't matter for determinism.
zonkDTyCoVarSetAndFV :: DTyCoVarSet -> TcM DTyCoVarSet
zonkDTyCoVarSetAndFV tycovars
= mkDVarSet <$> (zonkTyCoVarsAndFVList $ dVarSetElems tycovars)
-- Takes a list of TyCoVars, zonks them and returns a
-- deterministically ordered list of their free variables.
zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
......@@ -2432,6 +2432,8 @@ tcRnType hsc_env flexi normalise rdr_type
-- generalisation; e.g. :kind (T _)
; failIfErrsM
-- We follow Note [Recipe for checking a signature] in TcHsType here
-- Now kind-check the type
-- It can have any rank or kind
-- First bring into scope any wildcards
......@@ -2445,8 +2447,7 @@ tcRnType hsc_env flexi normalise rdr_type
; tcLHsTypeUnsaturated rn_type }
-- Do kind generalisation; see Note [Kind-generalise in tcRnType]
; kind <- zonkTcType kind
; kvs <- kindGeneralize kind
; kvs <- kindGeneralizeAll kind
; e <- mkEmptyZonkEnv flexi
; ty <- zonkTcTypeToTypeX e ty
......@@ -396,7 +396,7 @@ tcPatSynSig name sig_ty
req ex_tvs prov body_ty
-- Kind generalisation
; kvs <- kindGeneralize ungen_patsyn_ty
; kvs <- kindGeneralizeAll ungen_patsyn_ty
; traceTc "tcPatSynSig" (ppr ungen_patsyn_ty)
-- These are /signatures/ so we zonk to squeeze out any kind
......@@ -2444,30 +2444,6 @@ But it can deal with covars that are arguments to GADT data constructors.
So we somehow want to allow covars only in precisely those spots, then use
them as givens when checking the RHS. TODO (RAE): Implement plan.
Note [Quantifying over family patterns]
We need to quantify over two different lots of kind variables:
First, the ones that come from the kinds of the tyvar args of
tcTyVarBndrsKindGen, as usual
data family Dist a
-- Proxy :: forall k. k -> *
data instance Dist (Proxy a) = DP
-- Generates data DistProxy = DP
-- ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
-- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
Second, the ones that come from the kind argument of the type family
which we pick up using the (tyCoVarsOfTypes typats) in the result of
the thing_inside of tcHsTyvarBndrsGen.
-- Any :: forall k. k
data instance Dist Any = DA
-- Generates data DistAny k = DA
-- ax7 k :: Dist k (Any k) ~ DistAny k
-- The 'k' comes from kindGeneralizeKinds (Any k)
Note [Quantified kind variables of a family pattern]
Consider type family KindFam (p :: k1) (q :: k1)
......@@ -2586,11 +2562,11 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
-- the kvs below are those kind variables entirely unmentioned by the user
-- and discovered only by generalization
; kvs <- kindGeneralize (mkSpecForAllTys (binderVars tmpl_bndrs) $
mkSpecForAllTys exp_tvs $
mkPhiTy ctxt $
mkVisFunTys arg_tys $
; kvs <- kindGeneralizeAll (mkSpecForAllTys (binderVars tmpl_bndrs) $
mkSpecForAllTys exp_tvs $
mkPhiTy ctxt $
mkVisFunTys arg_tys $
-- That type is a lie, of course. (It shouldn't end in ()!)
-- And we could construct a proper result type from the info
-- at hand. But the result would mention only the tmpl_tvs,
......@@ -2670,10 +2646,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
; imp_tvs <- zonkAndScopedSort imp_tvs
; let user_tvs = imp_tvs ++ exp_tvs
; tkvs <- kindGeneralize (mkSpecForAllTys user_tvs $
mkPhiTy ctxt $
mkVisFunTys arg_tys $
; tkvs <- kindGeneralizeAll (mkSpecForAllTys user_tvs $
mkPhiTy ctxt $
mkVisFunTys arg_tys $
-- Zonk to Types
; (ze, tkvs) <- zonkTyBndrs tkvs
......@@ -2604,8 +2604,9 @@ Then we do the process described in Note [simplifyArgsWorker].
2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> sym co1).
This is not a dependent argument, so we don't extend the lifting context.
Now we need to deal with argument (3). After flattening, should we tack on a homogenizing
coercion? The way we normally tell is to lift the kind of the binder.
Now we need to deal with argument (3).
The way we normally proceed is to lift the kind of the binder, to see whether
it's dependent.
But here, the remainder of the kind of `a` that we're left with
after processing two arguments is just `k`.
......@@ -2712,6 +2713,19 @@ as desired.
Historical note: I (Richard E) once thought that the final part of the kind
had to be a variable k (as in the example above). But it might not be: it could
be an application of a variable. Here is the example:
let f :: forall (a :: Type) (b :: a -> Type). b (Any @a)
k :: Type
x :: k
flatten (f @Type @((->) k) x)
After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)`
is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.
......@@ -2786,9 +2800,8 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
-- See Note [Last case in simplifyArgsWorker]
go acc_xis acc_cos lc [] inner_ki roles args
| Just k <- getTyVar_maybe inner_ki
, Just co1 <- liftCoSubstTyVar lc Nominal k
= let co1_kind = coercionKind co1
= let co1 = liftCoSubst Nominal lc inner_ki
co1_kind = coercionKind co1
unflattened_tys = map (pSnd . coercionKind . snd) args
(arg_cos, res_co) = decomposePiCos co1 co1_kind unflattened_tys
casted_args = ASSERT2( equalLength args arg_cos
......@@ -162,8 +162,11 @@ ty_co_vars_of_type (TyVarTy v) is acc
| otherwise = ty_co_vars_of_type (tyVarKind v) emptyVarSet (extendVarSet acc v)
And that's it.
And that's it. This works because a variable is either bound or free. If it is bound,
then we won't look at it at all. If it is free, then all the variables free in its
kind are free -- regardless of whether some local variable has the same Unique.
So if we're looking at a variable occurrence at all, then all variables in its
kind are free.
tyCoVarsOfType :: Type -> TyCoVarSet
......@@ -816,4 +819,3 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
-- | Get the free vars of types in scoped order
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
T14040a.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
-> (forall y. p _2 'WeirdNil)
-> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
Sing x -> Sing xs -> p _0 xs -> p _1 ('WeirdCons x xs))
-> p _2 wl’
• Cannot apply expression of type ‘Sing wl0
-> (forall y. p0 _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’
to a visible type argument ‘(WeirdList z)’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment