Refactor computing dependent type vars
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 18 Apr 2016 14:01:13 +0000 (15:01 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 19 Apr 2016 07:38:47 +0000 (08:38 +0100)
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

compiler/typecheck/TcHsType.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcType.hs
compiler/types/Type.hs

index 4b61501..58f9ccc 100644 (file)
@@ -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]
index 3a03e4d..0ccb909 100644 (file)
@@ -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
 
index 2accd24..0983be5 100644 (file)
@@ -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
index db48bc1..16fe22e 100644 (file)
@@ -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 ]
index 3f637c8..f44cca0 100644 (file)
@@ -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
index 6910fe8..7ad2013 100644 (file)
@@ -2307,47 +2307,6 @@ 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.
 splitVisVarsOfType :: Type -> Pair TyCoVarSet