Commit 05974932 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Re-do the invariant for TcDepVars

Previously I had it so that dv_kvs and dv_tvs didn't
overlap.  Now they can, and quantifyZonkedTyVars
removes the former from the latter.  This is more
economical, and in fact there was a bug where the
invariant wasn't re-established.

It's much easier to allow dv_kvs and dv_kvs to overlap,
and to eliminate the overlap in TcMType.quantifyZonkedTyVars
parent bb296bf1
......@@ -866,13 +866,13 @@ quantifyTyVars, quantifyZonkedTyVars
quantifyTyVars gbl_tvs (DV { dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
= do { dep_tkvs <- zonkTyCoVarsAndFVDSet dep_tkvs
; nondep_tkvs <- (`minusDVarSet` dep_tkvs) <$>
zonkTyCoVarsAndFVDSet nondep_tkvs
; nondep_tkvs <- zonkTyCoVarsAndFVDSet nondep_tkvs
; gbl_tvs <- zonkTyCoVarsAndFV gbl_tvs
; quantifyZonkedTyVars gbl_tvs (DV { dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) }
quantifyZonkedTyVars gbl_tvs (DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
= do { let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
quantifyZonkedTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
= do { traceTc "quantifyZonkedTyVars" (vcat [ppr dvs, ppr gbl_tvs])
; let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
dep_kvs = dVarSetElemsWellScoped $
dep_tkvs `dVarSetMinusVarSet` gbl_tvs
`dVarSetMinusVarSet` closeOverKinds all_cvs
......@@ -883,12 +883,17 @@ quantifyZonkedTyVars gbl_tvs (DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
-- variables, or any any tvs that a covar depends on
nondep_tvs = dVarSetElems $
nondep_tkvs `dVarSetMinusVarSet` gbl_tvs
-- No worry about dependent covars here; they are
-- all in dep_tkvs
(nondep_tkvs `minusDVarSet` dep_tkvs)
`dVarSetMinusVarSet` gbl_tvs
-- See Note [Dependent type variables] in TcType
-- The `minus` dep_tkvs removes any kind-level vars
-- e.g. T k (a::k) Since k appear in a kind it'll
-- be in dv_kvs, and is dependent. So remove it from
-- dv_tvs which will also contain k
-- No worry about dependent covars here;
-- they are all in dep_tkvs
-- No worry about scoping, becuase these are all
-- type variables
-- See Note [Dependent type variables] in TcType
-- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
-- In the non-PolyKinds case, default the kind variables
......
......@@ -214,7 +214,7 @@ import BasicTypes
import Util
import Bag
import Maybes
import Pair
import Pair( pFst )
import Outputable
import FastString
import ErrUtils( Validity(..), MsgDoc, isValid )
......@@ -855,12 +855,22 @@ data TcDepVars -- See Note [Dependent type variables]
-- See Note [TcDepVars determinism]
= DV { dv_kvs :: DTyCoVarSet -- "kind" variables (dependent)
, dv_tvs :: DTyVarSet -- "type" variables (non-dependent)
-- The two are disjoint sets
-- A variable may appear in both sets
-- E.g. T k (x::k) The first occurence of k makes it
-- show up in dv_tvs, the second in dv_kvs
-- See Note [Dependent type variables]
}
depVarsTyVars :: TcDepVars -> DTyVarSet
depVarsTyVars = dv_tvs
instance Monoid TcDepVars where
mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet }
mappend (DV { dv_kvs = kv1, dv_tvs = tv1 })
(DV { dv_kvs = kv2, dv_tvs = tv2 })
= DV { dv_kvs = kv1 `unionDVarSet` kv2
, dv_tvs = tv1 `unionDVarSet` tv2}
instance Outputable TcDepVars where
ppr (DV {dv_kvs = kvs, dv_tvs = tvs })
= text "DV" <+> braces (sep [ text "dv_kvs =" <+> ppr kvs
......@@ -885,8 +895,20 @@ E.g. In the type T k (a::k)
even though it also appears at "top level" of the type
'a' is a type variable, becuase it doesn't
We gather these variables using a TcDepVars record:
DV { dv_kvs: Variables free in the kind of a free type variable
or of a forall-bound type variable
, dv_tvs: Variables sytactically free in the type }
So: dv_kvs are the kind variables of the type
(dv_tvs - dv_kvs) are the type variable of the type
Note that
* A variable can occur in both.
T k (x::k) The first occurence of k makes it
show up in dv_tvs, the second in dv_kvs
* We include any coercion variables in the "dependent",
"kind-variable" set because we never quantify over them.
......@@ -911,43 +933,33 @@ For more information about deterministic sets see
Note [Deterministic UniqFM] in UniqDFM.
-}
splitDepVarsOfType :: Type -> TcDepVars
-- See Note [Dependent type variables]
splitDepVarsOfType ty
= DV { dv_kvs = dep_vars
, dv_tvs = nondep_vars `minusDVarSet` dep_vars }
where
Pair dep_vars nondep_vars = split_dep_vars ty
-- | Like 'splitDepVarsOfType', but over a list of types
splitDepVarsOfTypes :: [Type] -> TcDepVars
-- See Note [Dependent type variables]
splitDepVarsOfTypes tys
= DV { dv_kvs = dep_vars
, dv_tvs = nondep_vars `minusDVarSet` dep_vars }
where
Pair dep_vars nondep_vars = foldMap split_dep_vars tys
splitDepVarsOfTypes = foldMap splitDepVarsOfType
-- | Worker for 'splitDepVarsOfType'. This might output the same var
-- in both sets, if it's used in both a type and a kind.
-- See Note [TcDepVars determinism]
split_dep_vars :: Type -> Pair DTyCoVarSet -- Pair kvs tvs
split_dep_vars = go
-- See Note [Dependent type variables]
splitDepVarsOfType :: Type -> TcDepVars
splitDepVarsOfType = go
where
go (TyVarTy tv) = Pair (tyCoVarsOfTypeDSet $ tyVarKind tv)
(unitDVarSet tv)
go (TyVarTy tv) = DV { dv_kvs =tyCoVarsOfTypeDSet $ tyVarKind tv
, dv_tvs = unitDVarSet tv }
go (AppTy t1 t2) = go t1 `mappend` go t2
go (TyConApp _ tys) = foldMap go tys
go (ForAllTy (Anon arg) res) = go arg `mappend` go res
go (ForAllTy (Named tv _) ty)
= let Pair kvs tvs = go ty in
Pair (kvs `delDVarSet` tv
`extendDVarSetList` tyCoVarsOfTypeList (tyVarKind tv))
(tvs `delDVarSet` tv)
go (LitTy {}) = mempty
go (CastTy ty co) = go ty `mappend` Pair (tyCoVarsOfCoDSet co)
emptyDVarSet
go (CoercionTy co) = Pair (tyCoVarsOfCoDSet co) emptyDVarSet
go (CastTy ty co) = go ty `mappend` go_co co
go (CoercionTy co) = go_co co
go (ForAllTy (Named tv _) ty)
= let DV { dv_kvs = kvs, dv_tvs = tvs } = go ty in
DV { dv_kvs = (kvs `delDVarSet` tv)
`extendDVarSetList` tyCoVarsOfTypeList (tyVarKind tv)
, dv_tvs = tvs `delDVarSet` tv }
go_co co = DV { dv_kvs = tyCoVarsOfCoDSet co
, dv_tvs = emptyDVarSet }
{-
************************************************************************
......
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