[commit: ghc] master: Re-do the invariant for TcDepVars (0597493)
git at git.haskell.org
git at git.haskell.org
Tue May 10 08:31:32 UTC 2016
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/0597493293eeea9b966697471d443fb20025bbf9/ghc
>---------------------------------------------------------------
commit 0597493293eeea9b966697471d443fb20025bbf9
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Mon May 9 23:12:31 2016 +0100
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
>---------------------------------------------------------------
0597493293eeea9b966697471d443fb20025bbf9
compiler/typecheck/TcMType.hs | 21 ++++++++-----
compiler/typecheck/TcType.hs | 68 +++++++++++++++++++++++++------------------
2 files changed, 53 insertions(+), 36 deletions(-)
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 71bf861..8ad9aba 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -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
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index a373dc6..94ab0bc 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -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 }
{-
************************************************************************
More information about the ghc-commits
mailing list