Commit 5c0c751a authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Zonk before calling splitDepVarsOfType.

It was Utterly Wrong before.

Note to self: Never, ever take the free vars of an unzonked type.
parent 35e93797
......@@ -1442,7 +1442,7 @@ kindGeneralize :: TcType -> TcM [KindVar]
kindGeneralize ty
= do { gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
; kvs <- zonkTcTypeAndFV ty
; quantifyTyVars gbl_tvs (Pair kvs emptyVarSet) }
; quantifyZonkedTyVars gbl_tvs (Pair kvs emptyVarSet) }
{-
Note [Kind generalisation]
......@@ -1746,6 +1746,7 @@ tcTyClTyVars :: Name -> LHsQTyVars Name -- LHS of the type or class decl
-- ^ Used for the type variables of a type or class decl
-- on the second full pass (type-checking/desugaring) in TcTyClDecls.
-- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
-- Accordingly, everything passed to the continuation is fully zonked.
--
-- (tcTyClTyVars T [a,b] thing_inside)
-- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
......
......@@ -68,7 +68,9 @@ module TcMType (
tidyEvVar, tidyCt, tidySkolemInfo,
skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV,
zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType, quantifyTyVars,
zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType,
quantifyTyVars, quantifyZonkedTyVars,
defaultKindVar,
zonkTcTyCoVarBndr, zonkTcTyBinder, zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind, zonkTcTypeMapper,
......@@ -827,22 +829,27 @@ Note that this function can accept covars, but will never return them.
This is because we never want to infer a quantified covar!
-}
quantifyTyVars :: TcTyCoVarSet -- global tvs
-> Pair TcTyCoVarSet -- dependent tvs We only distinguish
-- nondependent tvs between these for
-- -XNoPolyKinds
-> TcM [TcTyVar]
quantifyTyVars, quantifyZonkedTyVars
:: TcTyCoVarSet -- global tvs
-> Pair TcTyCoVarSet -- dependent tvs We only distinguish
-- nondependent tvs between these for
-- -XNoPolyKinds
-> TcM [TcTyVar]
-- See Note [quantifyTyVars]
-- Can be given a mixture of TcTyVars and TyVars, in the case of
-- associated type declarations. Also accepts covars, but *never* returns any.
-- The zonked variant assumes everything is already zonked.
quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
= do { dep_tkvs <- zonkTyCoVarsAndFV dep_tkvs
; nondep_tkvs <- (`minusVarSet` dep_tkvs) <$>
zonkTyCoVarsAndFV nondep_tkvs
; gbl_tvs <- zonkTyCoVarsAndFV gbl_tvs
; quantifyZonkedTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs) }
; let all_cvs = filterVarSet isCoVar $
quantifyZonkedTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
= do { let all_cvs = filterVarSet isCoVar $
dep_tkvs `unionVarSet` nondep_tkvs `minusVarSet` gbl_tvs
dep_kvs = varSetElemsWellScoped $
dep_tkvs `minusVarSet` gbl_tvs
......@@ -1137,6 +1144,11 @@ tcGetGlobalTyCoVars
; writeMutVar gtv_var gbl_tvs'
; return gbl_tvs' }
-- | Zonk a type without using the smart constructors; the result type
-- is available for inspection within the type-checking knot.
zonkTcTypeInKnot :: TcType -> TcM TcType
zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
-- Zonk a type and take its free variables
-- With kind polymorphism it can be essential to zonk *first*
......@@ -1147,7 +1159,17 @@ zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
-- NB: This might be called from within the knot, so don't use
-- smart constructors. See Note [Zonking within the knot] in TcHsType
zonkTcTypeAndFV ty
= tyCoVarsOfType <$> mapType (zonkTcTypeMapper { tcm_smart = False }) () ty
= tyCoVarsOfType <$> zonkTcTypeInKnot ty
-- | Zonk a type and call 'splitDepVarsOfType' on it.
-- Works within the knot.
zonkTcTypeAndSplitDepVars :: TcType -> TcM (Pair TyCoVarSet)
zonkTcTypeAndSplitDepVars ty
= splitDepVarsOfType <$> zonkTcTypeInKnot ty
zonkTcTypesAndSplitDepVars :: [TcType] -> TcM (Pair TyCoVarSet)
zonkTcTypesAndSplitDepVars tys
= splitDepVarsOfTypes <$> mapM zonkTcTypeInKnot tys
zonkTyCoVar :: TyCoVar -> TcM TcType
-- Works on TyVars and TcTyVars
......
......@@ -121,10 +121,15 @@ tcPatSynSig name sig_ty
, bound_tvs) }
-- Kind generalisation; c.f. kindGeneralise
; let free_kvs = tyCoVarsOfTelescope (implicit_tvs ++ univ_tvs ++ ex_tvs) $
tyCoVarsOfTypes (body_ty : req ++ prov ++ arg_tys)
; kvs <- quantifyTyVars emptyVarSet (Pair free_kvs emptyVarSet)
; free_kvs <- zonkTcTypeAndFV $
mkSpecForAllTys (implicit_tvs ++ univ_tvs) $
mkFunTys req $
mkSpecForAllTys ex_tvs $
mkFunTys prov $
mkFunTys arg_tys $
body_ty
; kvs <- quantifyZonkedTyVars emptyVarSet (Pair free_kvs emptyVarSet)
-- These are /signatures/ so we zonk to squeeze out any kind
-- unification variables. Do this after quantifyTyVars which may
......
......@@ -101,11 +101,11 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
-- during zonking (see TcHsSyn.zonkRule)
; let tpl_ids = lhs_evs ++ id_bndrs
forall_tkvs = splitDepVarsOfTypes $
rule_ty : map idType tpl_ids
; forall_tkvs <- zonkTcTypesAndSplitDepVars $
rule_ty : map idType tpl_ids
; gbls <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level
-- monomorphic bindings from the MR; test tc111
; qtkvs <- quantifyTyVars gbls forall_tkvs
; qtkvs <- quantifyZonkedTyVars gbls forall_tkvs
; traceTc "tcRule" (vcat [ pprFullRuleName name
, ppr forall_tkvs
, ppr qtkvs
......
......@@ -517,8 +517,8 @@ simplifyInfer :: TcLevel -- Used when generating the constraints
simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
| isEmptyWC wanteds
= do { gbl_tvs <- tcGetGlobalTyCoVars
; qtkvs <- quantify_tvs sigs gbl_tvs $
splitDepVarsOfTypes (map snd name_taus)
; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
; qtkvs <- quantify_tvs sigs gbl_tvs dep_vars
; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
; return (qtkvs, [], emptyTcEvBinds) }
......@@ -796,6 +796,8 @@ quantify_tvs :: [TcIdSigInfo]
-> TcM [TcTyVar]
-- See Note [Which type variables to quantify]
quantify_tvs sigs mono_tvs (Pair tau_kvs tau_tvs)
-- NB: don't use quantifyZonkedTyVars because the sig stuff might
-- be unzonked
= quantifyTyVars (mono_tvs `delVarSetList` sig_qtvs)
(Pair tau_kvs
(tau_tvs `extendVarSetList` sig_qtvs
......
......@@ -1244,8 +1244,8 @@ tcFamTyPats fam_shape@(name,_,_,_) mb_clsinfo pats kind_checker thing_inside
-- them into skolems, so that we don't subsequently
-- replace a meta kind var with (Any *)
-- Very like kindGeneralize
; qtkvs <- quantifyTyVars emptyVarSet $
splitDepVarsOfTypes typats
; vars <- zonkTcTypesAndSplitDepVars typats
; qtkvs <- quantifyZonkedTyVars emptyVarSet vars
; MASSERT( isEmptyVarSet $ coVarsOfTypes typats )
-- This should be the case, because otherwise the solveEqualities
......@@ -1437,11 +1437,10 @@ tcConDecl new_or_data rep_tycon tmpl_tvs tmpl_bndrs res_tmpl
-- Kind generalisation
; let all_user_tvs = imp_tvs ++ exp_tvs
; kvs <- quantifyTyVars (mkVarSet tmpl_tvs)
(splitDepVarsOfType (mkSpecForAllTys all_user_tvs $
mkFunTys ctxt $
mkFunTys arg_tys $
unitTy))
; vars <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys all_user_tvs $
mkFunTys ctxt $
mkFunTys arg_tys $
unitTy)
-- 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,
......@@ -1449,6 +1448,8 @@ tcConDecl new_or_data rep_tycon tmpl_tvs tmpl_bndrs res_tmpl
-- we're doing this to get the right behavior around removing
-- any vars bound in exp_binders.
; kvs <- quantifyZonkedTyVars (mkVarSet tmpl_tvs) vars
-- Zonk to Types
; (ze, qkvs) <- zonkTyBndrsX emptyZonkEnv kvs
; (ze, user_qtvs) <- zonkTyBndrsX ze all_user_tvs
......@@ -1487,11 +1488,12 @@ tcConDecl _new_or_data rep_tycon tmpl_tvs _tmpl_bndrs res_tmpl
do { traceTc "tcConDecl 1" (ppr names)
; (user_tvs, ctxt, stricts, field_lbls, arg_tys, res_ty,hs_details)
<- tcGadtSigType (ppr names) (unLoc $ head names) ty
; tkvs <- quantifyTyVars emptyVarSet
(splitDepVarsOfType (mkSpecForAllTys user_tvs $
mkFunTys ctxt $
mkFunTys arg_tys $
res_ty))
; vars <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys user_tvs $
mkFunTys ctxt $
mkFunTys arg_tys $
res_ty)
; tkvs <- quantifyZonkedTyVars emptyVarSet vars
-- Zonk to Types
; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (tkvs ++ user_tvs)
......@@ -2160,11 +2162,13 @@ checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
-- produces the appropriate error message.
checkValidTyConTyVars :: TyCon -> TcM ()
checkValidTyConTyVars tc
= when duplicate_vars $
do { -- strip off the duplicates and look for ill-scoped things
= do { -- strip off the duplicates and look for ill-scoped things
-- but keep the *last* occurrence of each variable, as it's
-- most likely the one the user wrote
let stripped_tvs = reverse $ nub $ reverse tvs
let stripped_tvs | duplicate_vars
= reverse $ nub $ reverse tvs
| otherwise
= tvs
vis_tvs = filterOutInvisibleTyVars tc tvs
extra | not (vis_tvs `equalLength` stripped_tvs)
= text "NB: Implicitly declared kind variables are put first."
......@@ -2174,11 +2178,12 @@ checkValidTyConTyVars tc
`and_if_that_doesn't_error`
-- This triggers on test case dependent/should_fail/InferDependency
-- It reports errors around Note [Dependent LHsQTyVars] in TcHsType
addErr (vcat [ text "Invalid declaration for" <+>
quotes (ppr tc) <> semi <+> text "you must explicitly"
, text "declare which variables are dependent on which others."
, hang (text "Inferred variable kinds:")
2 (vcat (map pp_tv stripped_tvs)) ]) }
when duplicate_vars (
addErr (vcat [ text "Invalid declaration for" <+>
quotes (ppr tc) <> semi <+> text "you must explicitly"
, text "declare which variables are dependent on which others."
, hang (text "Inferred variable kinds:")
2 (vcat (map pp_tv stripped_tvs)) ])) }
where
tvs = tyConTyVars tc
duplicate_vars = sizeVarSet (mkVarSet tvs) < length tvs
......
......@@ -2302,13 +2302,27 @@ synTyConResKind :: TyCon -> Kind
synTyConResKind tycon = piResultTys (tyConKind tycon) (mkTyVarTys (tyConTyVars tycon))
-- | Retrieve the free variables in this type, splitting them based
-- on whether the variable was used in a dependent context. It's possible
-- for a variable to be reported twice, if it's used both dependently
-- and non-dependently. (This isn't the most precise analysis, because
-- on whether the variable was used in a dependent context.
-- (This isn't the most precise analysis, because
-- it's used in the typechecking knot. It might list some dependent
-- variables as also non-dependent.)
splitDepVarsOfType :: Type -> Pair TyCoVarSet
splitDepVarsOfType = go
splitDepVarsOfType ty = Pair dep_vars final_nondep_vars
where
Pair dep_vars nondep_vars = split_dep_vars ty
final_nondep_vars = nondep_vars `minusVarSet` dep_vars
-- | Like 'splitDepVarsOfType', but over a list of types
splitDepVarsOfTypes :: [Type] -> Pair TyCoVarSet
splitDepVarsOfTypes tys = Pair dep_vars final_nondep_vars
where
Pair dep_vars nondep_vars = foldMap split_dep_vars tys
final_nondep_vars = nondep_vars `minusVarSet` dep_vars
-- | Worker for 'splitDepVarsOfType'. This might output the same var
-- in both sets, if it's used in both a type and a kind.
split_dep_vars :: Type -> Pair TyCoVarSet
split_dep_vars = go
where
go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv)
(unitVarSet tv)
......@@ -2328,10 +2342,6 @@ splitDepVarsOfType = go
go ty1 `mappend` go ty2 -- NB: the Pairs separate along different
-- dimensions here. Be careful!
-- | Like 'splitDepVarsOfType', but over a list of types
splitDepVarsOfTypes :: [Type] -> Pair TyCoVarSet
splitDepVarsOfTypes = foldMap splitDepVarsOfType
-- | Retrieve the free variables in this type, splitting them based
-- on whether they are used visibly or invisibly. Invisible ones come
-- first.
......
data D2 where
MkD2 :: (forall (p :: k -> *) (a :: k). p a -> Int) -> D2
-- Defined at <interactive>:3:1
data D3 where
MkD3 :: (forall k1 (p :: k1 -> *) (a :: k1). p a -> Int) -> D3
data D3 = MkD3 (forall k (p :: k -> *) (a :: k). p a -> Int)
-- Defined at <interactive>:4:1
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