Commit 17eb2419 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Refactor computing dependent type vars

There should be no change in behaviour here

* Move splitDepVarsOfType(s) from Type to TcType

* Define data type TcType.TcDepVars, document what it means,
  and use it where appropriate, notably in splitDepVarsOfType(s)

* Use it in TcMType.quantifyTyVars and friends
parent d59939a4
......@@ -80,7 +80,6 @@ import UniqSupply
import Outputable
import FastString
import PrelNames hiding ( wildCardName )
import Pair
import qualified GHC.LanguageExtensions as LangExt
import Maybes
......@@ -192,8 +191,13 @@ tcHsSigType ctxt sig_ty
-- of kind * in a Template Haskell quote eg [t| Maybe |]
; ty <- tc_hs_sig_type sig_ty kind
-- Generalise here: see Note [Kind generalisation]
; ty <- maybeKindGeneralizeType ty -- also zonks
; do_kind_gen <- decideKindGeneralisationPlan ty
; ty <- if do_kind_gen
then kindGeneralizeType ty
else zonkTcType ty
; checkValidType ctxt ty
; return ty }
......@@ -318,7 +322,7 @@ tcLHsType :: LHsType Name -> TcM (TcType, TcKind)
tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
---------------------------
-- | Should we generalise the kind of this type?
-- | Should we generalise the kind of this type signature?
-- We *should* generalise if the type is mentions no scoped type variables
-- or if NoMonoLocalBinds is set. Otherwise, nope.
decideKindGeneralisationPlan :: Type -> TcM Bool
......@@ -333,13 +337,6 @@ decideKindGeneralisationPlan ty
, text "should gen?" <+> ppr should_gen ])
; return should_gen }
maybeKindGeneralizeType :: TcType -> TcM Type
maybeKindGeneralizeType ty
= do { should_gen <- decideKindGeneralisationPlan ty
; if should_gen
then kindGeneralizeType ty
else zonkTcType ty }
{-
************************************************************************
* *
......@@ -1439,10 +1436,14 @@ kindGeneralizeType ty
; zonkTcType (mkInvForAllTys kvs ty) }
kindGeneralize :: TcType -> TcM [KindVar]
kindGeneralize ty
= do { gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
; kvs <- zonkTcTypeAndFV ty
; quantifyZonkedTyVars gbl_tvs (Pair kvs emptyVarSet) }
-- Quantify the free kind variables of a kind or type
-- In the latter case the type is closed, so it has no free
-- type variables. So in both cases, all the free vars are kind vars
kindGeneralize kind_or_type
= do { kvs <- zonkTcTypeAndFV kind_or_type
; let dvs = DV { dv_kvs = kvs, dv_tvs = emptyVarSet }
; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
; quantifyZonkedTyVars gbl_tvs dvs }
{-
Note [Kind generalisation]
......
......@@ -825,19 +825,18 @@ has free vars {k,a}. But the type (see Trac #7916)
(f::k->*) (a::k)
has free vars {f,a}, but we must add 'k' as well! Hence step (3).
This function bothers to distinguish between dependent and non-dependent
variables only to keep correct defaulting behavior with -XNoPolyKinds.
With -XPolyKinds, it treats both classes of variables identically.
* This function distinguishes between dependent and non-dependent
variables only to keep correct defaulting behavior with -XNoPolyKinds.
With -XPolyKinds, it treats both classes of variables identically.
Note that this function can accept covars, but will never return them.
This is because we never want to infer a quantified covar!
* quantifyTyVars never quantifies over
- a coercion variable
- a runtime-rep variable
-}
quantifyTyVars, quantifyZonkedTyVars
:: TcTyCoVarSet -- global tvs
-> Pair TcTyCoVarSet -- dependent tvs We only distinguish
-- nondependent tvs between these for
-- -XNoPolyKinds
-> TcDepVars -- See Note [Dependent type variables] in TcType
-> TcM [TcTyVar]
-- See Note [quantifyTyVars]
-- Can be given a mixture of TcTyVars and TyVars, in the case of
......@@ -845,27 +844,32 @@ quantifyTyVars, quantifyZonkedTyVars
-- The zonked variant assumes everything is already zonked.
quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
quantifyTyVars gbl_tvs (DV { dv_kvs = dep_tkvs, dv_tvs = 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) }
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
`minusVarSet` (closeOverKinds all_cvs)
-- remove any tvs that a covar depends on
nondep_tvs = varSetElemsWellScoped $
; 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 dep_tkvs
dep_kvs = varSetElemsWellScoped $
dep_tkvs `minusVarSet` gbl_tvs
`minusVarSet` closeOverKinds all_cvs
-- varSetElemsWellScoped: put the kind variables into
-- well-scoped order.
-- E.g. [k, (a::k)] not the other way roud
-- closeOverKinds all_cvs: do not quantify over coercion
-- variables, or any any tvs that a covar depends on
nondep_tvs = varSetElems $
nondep_tkvs `minusVarSet` gbl_tvs
-- no worry about dependent cvs here, as these vars
-- are non-dependent
-- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
-- 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
-- to *, and zonk the tyvars as usual. Notice that this
......@@ -1167,11 +1171,11 @@ zonkTcTypeAndFV ty
-- | Zonk a type and call 'splitDepVarsOfType' on it.
-- Works within the knot.
zonkTcTypeAndSplitDepVars :: TcType -> TcM (Pair TyCoVarSet)
zonkTcTypeAndSplitDepVars :: TcType -> TcM TcDepVars
zonkTcTypeAndSplitDepVars ty
= splitDepVarsOfType <$> zonkTcTypeInKnot ty
zonkTcTypesAndSplitDepVars :: [TcType] -> TcM (Pair TyCoVarSet)
zonkTcTypesAndSplitDepVars :: [TcType] -> TcM TcDepVars
zonkTcTypesAndSplitDepVars tys
= splitDepVarsOfTypes <$> mapM zonkTcTypeInKnot tys
......
......@@ -14,7 +14,7 @@ module TcPatSyn ( tcPatSynSig, tcInferPatSynDecl, tcCheckPatSynDecl
import HsSyn
import TcPat
import TcHsType( tcImplicitTKBndrs, tcExplicitTKBndrs
, tcHsContext, tcHsLiftedType, tcHsOpenType )
, tcHsContext, tcHsLiftedType, tcHsOpenType, kindGeneralize )
import TcRnMonad
import TcEnv
import TcMType
......@@ -29,7 +29,6 @@ import Outputable
import FastString
import Var
import VarEnv( emptyTidyEnv )
import Type( tidyTyCoVarBndrs, tidyTypes, tidyType )
import Id
import IdInfo( RecSelParent(..))
import TcBinds
......@@ -50,7 +49,6 @@ import Util
import ErrUtils
import Control.Monad ( unless, zipWithM )
import Data.List( partition )
import Pair( Pair(..) )
#include "HsVersions.h"
......@@ -122,16 +120,14 @@ tcPatSynSig name sig_ty
; return ( (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty)
, bound_tvs) }
-- Kind generalisation; c.f. kindGeneralise
; 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)
-- Kind generalisation
; kvs <- kindGeneralize $
mkSpecForAllTys (implicit_tvs ++ univ_tvs) $
mkFunTys req $
mkSpecForAllTys ex_tvs $
mkFunTys prov $
mkFunTys arg_tys $
body_ty
-- These are /signatures/ so we zonk to squeeze out any kind
-- unification variables. Do this after quantifyTyVars which may
......
......@@ -25,7 +25,6 @@ import ListSetOps
import Maybes
import Name
import Outputable
import Pair
import PrelInfo
import PrelNames
import TcErrors
......@@ -49,7 +48,6 @@ import qualified GHC.LanguageExtensions as LangExt
import Control.Monad ( when, unless )
import Data.List ( partition )
import Data.Foldable ( fold )
{-
*********************************************************************************
......@@ -613,14 +611,12 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
-- we don't quantify over beta (since it is fixed by envt)
-- so we must promote it! The inferred type is just
-- f :: beta -> beta
; outer_tclvl <- TcM.getTcLevel
; zonked_tau_tvs <- fold <$>
traverse TcM.zonkTyCoVarsAndFV zonked_tau_tkvs
; zonked_tau_tvs <- TcM.zonkTyCoVarsAndFV (dv_tvs zonked_tau_tkvs)
-- decideQuantification turned some meta tyvars into
-- quantified skolems, so we have to zonk again
; let phi_tvs = tyCoVarsOfTypes bound_theta
`unionVarSet` zonked_tau_tvs
; let phi_tvs = tyCoVarsOfTypes bound_theta
`unionVarSet` zonked_tau_tvs
promote_tvs = closeOverKinds phi_tvs `delVarSetList` qtvs
; MASSERT2( closeOverKinds promote_tvs `subVarSet` promote_tvs
......@@ -631,6 +627,7 @@ simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
-- we really don't want a type to be promoted when its kind isn't!
-- promoteTyVar ignores coercion variables
; outer_tclvl <- TcM.getTcLevel
; mapM_ (promoteTyVar outer_tclvl) (varSetElems promote_tvs)
-- Emit an implication constraint for the
......@@ -729,18 +726,19 @@ decideQuantification
-> [TcIdSigInfo]
-> [(Name, TcTauType)] -- variables to be generalised (for errors only)
-> [PredType] -- candidate theta
-> Pair TcTyCoVarSet -- dependent (kind) variables & type variables
-> TcDepVars
-> TcM ( [TcTyVar] -- Quantify over these (skolems)
, [PredType] ) -- and this context (fully zonked)
-- See Note [Deciding quantification]
decideQuantification apply_mr sigs name_taus constraints
zonked_pair@(Pair zonked_tau_kvs zonked_tau_tvs)
zonked_dvs@(DV { dv_kvs = zonked_tau_kvs, dv_tvs = zonked_tau_tvs })
| apply_mr -- Apply the Monomorphism restriction
= do { gbl_tvs <- tcGetGlobalTyCoVars
; let constrained_tvs = tyCoVarsOfTypes constraints `unionVarSet`
; let zonked_tkvs = zonked_tau_kvs `unionVarSet` zonked_tau_tvs
constrained_tvs = tyCoVarsOfTypes constraints `unionVarSet`
filterVarSet isCoVar zonked_tkvs
mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
; qtvs <- quantify_tvs sigs mono_tvs zonked_pair
; qtvs <- quantify_tvs sigs mono_tvs zonked_dvs
-- Warn about the monomorphism restriction
; warn_mono <- woptM Opt_WarnMonomorphism
......@@ -761,7 +759,8 @@ decideQuantification apply_mr sigs name_taus constraints
= do { gbl_tvs <- tcGetGlobalTyCoVars
; let mono_tvs = growThetaTyVars equality_constraints gbl_tvs
tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs
; qtvs <- quantify_tvs sigs mono_tvs (Pair zonked_tau_kvs tau_tvs_plus)
dvs_plus = DV { dv_kvs = zonked_tau_kvs, dv_tvs = tau_tvs_plus }
; qtvs <- quantify_tvs sigs mono_tvs dvs_plus
-- We don't grow the kvs, as there's no real need to. Recall
-- that quantifyTyVars uses the separation between kvs and tvs
-- only for defaulting, and we don't want (ever) to default a tv
......@@ -786,23 +785,21 @@ decideQuantification apply_mr sigs name_taus constraints
, text "min_theta:" <+> ppr min_theta ])
; return (qtvs, min_theta) }
where
zonked_tkvs = zonked_tau_kvs `unionVarSet` zonked_tau_tvs
bndrs = map fst name_taus
pp_bndrs = pprWithCommas (quotes . ppr) bndrs
equality_constraints = filter isEqPred constraints
quantify_tvs :: [TcIdSigInfo]
-> TcTyVarSet -- the monomorphic tvs
-> Pair TcTyVarSet -- kvs, tvs to quantify
-> TcDepVars
-> TcM [TcTyVar]
-- See Note [Which type variables to quantify]
quantify_tvs sigs mono_tvs (Pair tau_kvs tau_tvs)
quantify_tvs sigs mono_tvs dep_tvs@(DV { dv_tvs = 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
`extendVarSetList` sig_wcs))
(dep_tvs { dv_tvs = tau_tvs `extendVarSetList` sig_qtvs
`extendVarSetList` sig_wcs })
-- NB: quantifyTyVars zonks its arguments
where
sig_qtvs = [ skol | sig <- sigs, (_, skol) <- sig_skols sig ]
......
......@@ -100,6 +100,7 @@ module TcType (
-- * Finding "exact" (non-dead) type variables
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
splitDepVarsOfType, splitDepVarsOfTypes, TcDepVars(..), depVarsTyVars,
-- * Extracting bound variables
allBoundVariables, allBoundVariabless,
......@@ -845,6 +846,99 @@ allBoundVariabless = mapUnionVarSet allBoundVariables
-}
isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
{- *********************************************************************
* *
Type and kind variables in a type
* *
********************************************************************* -}
data TcDepVars -- See note [Dependent type variables]
= DV { dv_kvs :: TyCoVarSet -- "kind" variables (dependent)
, dv_tvs :: TyVarSet -- "type" variables (non-dependent)
-- The two are disjoint sets
}
depVarsTyVars :: TcDepVars -> TyVarSet
depVarsTyVars = dv_tvs
instance Outputable TcDepVars where
ppr (DV {dv_kvs = kvs, dv_tvs = tvs })
= text "DV" <+> braces (sep [ text "dv_kvs =" <+> ppr kvs
, text "dv_tvs =" <+> ppr tvs ])
{- Note [Dependent type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In Haskell type inference we quantify over type variables; but we only
quantify over /kind/ variables when -XPolyKinds is on. So when
collecting the free vars of a type, prior to quantifying, we must keep
the type and kind veraibles separate. But what does that mean in a
system where kind variables /are/ type variables? It's a fairly
arbitrary distinction based on how the variables appear:
- "Kind variables" appear in the kind of some other free variable
PLUS any free coercion variables
- "Type variables" are all free vars that are not kind variables
E.g. In the type T k (a::k)
'k' is a kind variable, because it occurs in the kind of 'a',
even though it also appears at "top level" of the type
'a' is a type variable, becuase it doesn't
Note that
* We include any coercion variables in the "dependent",
"kind-variable" set because we never quantify over them.
* Both sets are un-ordered, of course.
* The "kind variables" might depend on each other; e.g
(k1 :: k2), (k2 :: *)
The "type variables" do not depend on each other; if
one did, it'd be classified as a kind variable!
-}
splitDepVarsOfType :: Type -> TcDepVars
-- See Note [Dependent type variables]
splitDepVarsOfType ty
= DV { dv_kvs = dep_vars
, dv_tvs = nondep_vars `minusVarSet` 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 `minusVarSet` dep_vars }
where
Pair dep_vars nondep_vars = foldMap split_dep_vars tys
-- | 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 -- Pair kvs tvs
split_dep_vars = go
where
go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv)
(unitVarSet 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 `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv))
(tvs `delVarSet` tv)
go (LitTy {}) = mempty
go (CastTy ty co) = go ty `mappend` Pair (tyCoVarsOfCo co)
emptyVarSet
go (CoercionTy co) = go_co co
go_co co = let Pair ty1 ty2 = coercionKind co in
-- co :: ty1 ~ ty2
go ty1 `mappend` go ty2
isTouchableOrFmv ctxt_tclvl tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
......
......@@ -2306,47 +2306,6 @@ tyConsOfType ty
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.
-- (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 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)
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 `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv))
(tvs `delVarSet` tv)
go (LitTy {}) = mempty
go (CastTy ty co) = go ty `mappend` Pair (tyCoVarsOfCo co)
emptyVarSet
go (CoercionTy co) = go_co co
go_co co = let Pair ty1 ty2 = coercionKind co in
go ty1 `mappend` go ty2 -- NB: the Pairs separate along different
-- dimensions here. Be careful!
-- | Retrieve the free variables in this type, splitting them based
-- on whether they are used visibly or invisibly. Invisible ones come
-- first.
......
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