Check InScopeSet in substTy and provide substTyUnchecked
authorBartosz Nitka <niteria@gmail.com>
Tue, 19 Jan 2016 11:25:39 +0000 (03:25 -0800)
committerBartosz Nitka <niteria@gmail.com>
Tue, 19 Jan 2016 11:26:02 +0000 (03:26 -0800)
This adds sanity checks to `substTy` that implement:

> when calling substTy subst ty it should be the case that the in-scope
> set in the substitution is a superset of
> * The free vars of the range of the substitution
> * The free vars of ty minus the domain of the substitution

and replaces violators with unchecked version. The violators were found
by running the GHC test suite.

This ensures that I can work on this incrementally and that what I fix won't
be undone by some other change.

It also includes a couple of fixes that I've already done.

Test Plan: ./validate

Reviewers: simonmar, goldfire, simonpj, austin, bgamari

Reviewed By: simonpj, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1792

GHC Trac Issues: #11371

20 files changed:
compiler/basicTypes/MkId.hs
compiler/basicTypes/VarEnv.hs
compiler/coreSyn/CoreSubst.hs
compiler/coreSyn/CoreUtils.hs
compiler/iface/BuildTyCl.hs
compiler/typecheck/Inst.hs
compiler/typecheck/TcClassDcl.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/types/FamInstEnv.hs
compiler/types/TyCoRep.hs
compiler/types/Type.hs
compiler/utils/UniqFM.hs

index 27e9dc1..6876956 100644 (file)
@@ -730,7 +730,7 @@ dataConArgUnpack arg_ty
                          [(DataAlt con, rep_ids, body)]
           ; return (rep_ids, unbox_fn) }
      , Boxer $ \ subst ->
-       do { rep_ids <- mapM (newLocal . TcType.substTy subst) rep_tys
+       do { rep_ids <- mapM (newLocal . TcType.substTyUnchecked subst) rep_tys
           ; return (rep_ids, Var (dataConWorkId con)
                              `mkTyApps` (substTys subst tc_args)
                              `mkVarApps` rep_ids ) } ) )
index 0fa0f57..08eabee 100644 (file)
@@ -40,6 +40,7 @@ module VarEnv (
         extendInScopeSet, extendInScopeSetList, extendInScopeSetSet,
         getInScopeVars, lookupInScope, lookupInScope_Directly,
         unionInScope, elemInScopeSet, uniqAway,
+        varSetInScope,
 
         -- * The RnEnv2 type
         RnEnv2,
@@ -140,6 +141,9 @@ unionInScope :: InScopeSet -> InScopeSet -> InScopeSet
 unionInScope (InScope s1 _) (InScope s2 n2)
   = InScope (s1 `plusVarEnv` s2) n2
 
+varSetInScope :: VarSet -> InScopeSet -> Bool
+varSetInScope vars (InScope s1 _) = vars `subVarSet` s1
+
 -- | @uniqAway in_scope v@ finds a unique that is not used in the
 -- in-scope set, and gives that to v.
 uniqAway :: InScopeSet -> Var -> Var
index 8cc609d..a3ab970 100644 (file)
@@ -600,7 +600,7 @@ substCoVarBndr (Subst in_scope id_env tv_env cv_env) cv
 
 -- | See 'Type.substTy'
 substTy :: Subst -> Type -> Type
-substTy subst ty = Type.substTy (getTCvSubst subst) ty
+substTy subst ty = Type.substTyUnchecked (getTCvSubst subst) ty
 
 getTCvSubst :: Subst -> TCvSubst
 getTCvSubst (Subst in_scope _ tenv cenv) = TCvSubst in_scope tenv cenv
index 9c2f16c..59f1d4f 100644 (file)
@@ -1533,12 +1533,12 @@ dataConInstPat fss uniqs con inst_tys
                                      , new_tv)
       where
         new_tv = mkTyVar (mkSysTvName uniq fs) kind
-        kind   = Type.substTy subst (tyVarKind tv)
+        kind   = Type.substTyUnchecked subst (tyVarKind tv)
 
       -- Make value vars, instantiating types
     arg_ids = zipWith4 mk_id_var id_uniqs id_fss arg_tys arg_strs
     mk_id_var uniq fs ty str
-      = mkLocalIdOrCoVarWithInfo name (Type.substTy full_subst ty) info
+      = mkLocalIdOrCoVarWithInfo name (Type.substTyUnchecked full_subst ty) info
       where
         name = mkInternalName uniq (mkVarOccFS fs) noSrcSpan
         info | isMarkedStrict str = vanillaIdInfo `setUnfoldingInfo` evaldUnfolding
index 0015e01..75e8875 100644 (file)
@@ -184,7 +184,7 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
     -- compatible with the pattern synonym
     ASSERT2((and [ univ_tvs `equalLength` univ_tvs1
                  , ex_tvs `equalLength` ex_tvs1
-                 , pat_ty `eqType` substTy subst pat_ty1
+                 , pat_ty `eqType` substTyUnchecked subst pat_ty1
                  , prov_theta `eqTypes` substTys subst prov_theta1
                  , req_theta `eqTypes` substTys subst req_theta1
                  , arg_tys `eqTypes` substTys subst arg_tys1
index 43f7f1e..43cbb48 100644 (file)
@@ -137,7 +137,8 @@ deeplySkolemise ty
   = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
        ; (subst, tvs1) <- tcInstSkolTyVars tvs
        ; ev_vars1 <- newEvVars (substTheta subst theta)
-       ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty')
+       ; (wrap, tvs2, ev_vars2, rho) <-
+           deeplySkolemise (substTyAddInScope subst ty')
        ; return ( mkWpLams ids1
                    <.> mkWpTyLams tvs1
                    <.> mkWpLams ev_vars1
@@ -178,8 +179,8 @@ top_instantiate inst_all orig ty
                | otherwise        = ([], theta)
        ; (subst, inst_tvs') <- newMetaTyVars (map (binderVar "top_inst") inst_bndrs)
        ; let inst_theta' = substTheta subst inst_theta
-             sigma'      = substTy    subst (mkForAllTys leave_bndrs $
-                                             mkFunTys leave_theta rho)
+             sigma'      = substTyAddInScope subst (mkForAllTys leave_bndrs $
+                                                    mkFunTys leave_theta rho)
 
        ; wrap1 <- instCall orig (mkTyVarTys inst_tvs') inst_theta'
        ; traceTc "Instantiating"
@@ -227,7 +228,7 @@ deeplyInstantiate orig ty
                                                 , text "with" <+> ppr tvs'
                                                 , text "args:" <+> ppr ids1
                                                 , text "theta:" <+>  ppr theta' ])
-       ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
+       ; (wrap2, rho2) <- deeplyInstantiate orig (substTyUnchecked subst rho)
        ; return (mkWpLams ids1
                     <.> wrap2
                     <.> wrap1
index 4fe42b0..6ffe902 100644 (file)
@@ -456,7 +456,7 @@ tcATDefault emit_warn loc inst_subst defined_ats (ATI fam_tc defs)
   | Just (rhs_ty, _loc) <- defs
   = do { let (subst', pat_tys') = mapAccumL subst_tv inst_subst
                                             (tyConTyVars fam_tc)
-             rhs'     = substTy subst' rhs_ty
+             rhs'     = substTyUnchecked subst' rhs_ty
              tcv_set' = tyCoVarsOfTypes pat_tys'
              (tv_set', cv_set') = partitionVarSet isTyVar tcv_set'
              tvs'     = varSetElemsWellScoped tv_set'
@@ -486,7 +486,7 @@ tcATDefault emit_warn loc inst_subst defined_ats (ATI fam_tc defs)
       | otherwise
       = (extendTCvSubst subst tc_tv ty', ty')
       where
-        ty' = mkTyVarTy (updateTyVarKind (substTy subst) tc_tv)
+        ty' = mkTyVarTy (updateTyVarKind (substTyUnchecked subst) tc_tv)
 
 warnMissingAT :: Name -> TcM ()
 warnMissingAT name
index 125d455..ad49631 100644 (file)
@@ -872,7 +872,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
                                                       (con1_tvs `zip` result_inst_tys)
 
         ; let rec_res_ty    = TcType.substTy result_subst con1_res_ty
-              scrut_ty      = TcType.substTy scrut_subst  con1_res_ty
+              scrut_ty      = TcType.substTyUnchecked scrut_subst con1_res_ty
               con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys
 
         ; wrap_res <- tcSubTypeHR (exprCtOrigin expr)
index f87a302..612f8a6 100644 (file)
@@ -956,7 +956,7 @@ flatten_one (TyConApp tc tys)
   -- Expand type synonyms that mention type families
   -- on the RHS; see Note [Flattening synonyms]
   | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
-  , let expanded_ty = mkAppTys (substTy (mkTopTCvSubst tenv) rhs) tys'
+  , let expanded_ty = mkAppTys (substTyUnchecked (mkTopTCvSubst tenv) rhs) tys'
   = do { mode <- getMode
        ; let used_tcs = tyConsOfType rhs
        ; case mode of
index b301149..76c2977 100644 (file)
@@ -760,7 +760,7 @@ tc_infer_args mode orig_ty ki mb_kind_info orig_args n0
        ; go emptyTCvSubst ki orig_args n0 [] }
   where
     go subst fun_kind []   n acc
-      = return ( substTy subst fun_kind, reverse acc, [], n )
+      = return ( substTyUnchecked subst fun_kind, reverse acc, [], n )
     -- when we call this when checking type family patterns, we really
     -- do want to instantiate all invisible arguments. During other
     -- typechecking, we don't.
@@ -784,7 +784,7 @@ tc_infer_args mode orig_ty ki mb_kind_info orig_args n0
         do { let mode' | isNamedBinder bndr = kindLevel mode
                        | otherwise          = mode
            ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
-                     tc_lhs_type mode' arg (substTy subst $ binderType bndr)
+                     tc_lhs_type mode' arg (substTyUnchecked subst $ binderType bndr)
            ; let subst' = case binderVar_maybe bndr of
                    Just tv -> extendTCvSubst subst tv arg'
                    Nothing -> subst
index 8582c72..1853cb3 100644 (file)
@@ -1257,7 +1257,7 @@ emitFunDepDeriveds fd_eqns
 
     do_one_eq loc subst (Pair ty1 ty2)
        = unifyDerived loc Nominal $
-         Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
+         Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
 
 {-
 **********************************************************************
@@ -1513,7 +1513,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
       injImproveEqns inj_args (ax_args, theta, unsubstTvs, cabr) = do
         (theta', _) <- instFlexiTcS (varSetElems unsubstTvs)
         let subst = theta `unionTCvSubst` theta'
-        return [ Pair arg (substTy subst ax_arg)
+        return [ Pair arg (substTyUnchecked subst ax_arg)
                | case cabr of
                   Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
                   _          -> True
index 7ab59be..bb31005 100644 (file)
@@ -294,7 +294,7 @@ tcInstType inst_tyvars ty
                             return ([], theta, tau)
 
         (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
-                            ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
+                            ; let (theta, tau) = tcSplitPhiTy (substTyUnchecked subst rho)
                             ; return (tyvars', theta, tau) }
 
 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
@@ -311,9 +311,10 @@ tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTCvSubst [])
 
 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
 tcSuperSkolTyVar subst tv
-  = (extendTCvSubst subst tv (mkTyVarTy new_tv), new_tv)
+  = (extendTCvSubst (extendTCvInScope subst new_tv) tv (mkTyVarTy new_tv)
+    , new_tv)
   where
-    kind   = substTy subst (tyVarKind tv)
+    kind   = substTyUnchecked subst (tyVarKind tv)
     new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
 
 -- Wrappers
@@ -392,10 +393,13 @@ instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
 instSkolTyCoVarX mk_tcv subst tycovar
   = do  { uniq <- newUnique
         ; let new_tv = mk_tcv uniq old_name kind
-        ; return (extendTCvSubst subst tycovar (mk_ty_co new_tv), new_tv) }
+        ; return (extendTCvSubst (extendTCvInScope subst new_tv) tycovar
+                   (mk_ty_co new_tv)
+                 , new_tv)
+        }
   where
     old_name = tyVarName tycovar
-    kind     = substTy subst (tyVarKind tycovar)
+    kind     = substTyUnchecked subst (tyVarKind tycovar)
 
     mk_ty_co v
       | isTyVar v = mkTyVarTy v
@@ -687,9 +691,12 @@ newMetaTyVarX subst tyvar
         ; details <- newMetaDetails info
         ; let name   = mkSystemName uniq (getOccName tyvar)
                        -- See Note [Name of an instantiated type variable]
-              kind   = substTy subst (tyVarKind tyvar)
+              kind   = substTyUnchecked subst (tyVarKind tyvar)
               new_tv = mkTcTyVar name kind details
-        ; return (extendTCvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
+        ; return (extendTCvSubst (extendTCvInScope subst new_tv) tyvar
+                   (mkTyVarTy new_tv)
+                 , new_tv)
+        }
 
 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 -- Just like newMetaTyVarX, but make a SigTv
@@ -699,7 +706,9 @@ newMetaSigTyVarX subst tyvar
         ; let name   = mkSystemName uniq (getOccName tyvar)
               kind   = substTy subst (tyVarKind tyvar)
               new_tv = mkTcTyVar name kind details
-        ; return (extendTCvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
+        ; return (extendTCvSubst (extendTCvInScope subst new_tv) tyvar
+                   (mkTyVarTy new_tv)
+                 , new_tv) }
 
 {- Note [Name of an instantiated type variable]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
index c12ca6c..0c6d713 100644 (file)
@@ -278,7 +278,7 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
              arg_id <- tcLookupId arg_name
            ; coi <- unifyType (Just arg_id)
                               (idType arg_id)
-                              (substTy subst arg_ty)
+                              (substTyUnchecked subst arg_ty)
            ; return (mkLHsWrapCo coi $ nlHsVar arg_id) }
 
 {- Note [Checking against a pattern signature]
index 0214f13..44e9a03 100644 (file)
@@ -2857,7 +2857,7 @@ instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTCvSubst tvs)
   where
      inst_one subst tv
          = do { ty' <- instFlexiTcSHelper (tyVarName tv)
-                                          (substTy subst (tyVarKind tv))
+                                          (substTyUnchecked subst (tyVarKind tv))
               ; return (extendTCvSubst subst tv ty', ty') }
 
 instFlexiTcSHelper :: Name -> Kind -> TcM TcType
@@ -3065,8 +3065,8 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
                        mkCastTy (mkTyVarTys tvs1) kind_cos
             body2' = substTyWith tvs2 tvs1' body2
       ; (subst, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
-      ; let phi1  = Type.substTy subst body1
-            phi2  = Type.substTy subst body2'
+      ; let phi1  = Type.substTyUnchecked subst body1
+            phi2  = Type.substTyUnchecked subst body2'
             skol_info = UnifyForAllSkol phi1
 
       ; (ctev, hole_co) <- newWantedEq loc role phi1 phi2
index 2d2c5bb..95f773e 100644 (file)
@@ -999,7 +999,7 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
 
          -- See Note [Type-checking default assoc decls]
        ; case tcMatchTys pats' (mkTyVarTys (tyConTyVars fam_tc)) of
-           Just subst -> return ( Just (substTy subst rhs_ty, loc) )
+           Just subst -> return ( Just (substTyUnchecked subst rhs_ty, loc) )
            Nothing    -> failWithTc (defaultAssocKindErr fam_tc)
            -- We check for well-formedness and validity later,
            -- in checkValidClass
index 2f00be2..1b9ae29 100644 (file)
@@ -149,6 +149,7 @@ module TcType (
   Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
   extendTCvSubstList, isInScope, mkTCvSubst, zipTyEnv, zipCoEnv,
   Type.substTy, substTys, substTyWith, substTyWithCoVars,
+  substTyAddInScope, substTyUnchecked,
   substTheta,
 
   isUnLiftedType,       -- Source types are always lifted
index 4b4cc5d..1167ac2 100644 (file)
@@ -1237,7 +1237,7 @@ normalise_tc_app tc tys
        ; case expandSynTyCon_maybe tc ntys of
          { Just (tenv, rhs, ntys') ->
            do { (co2, ninst_rhs)
-                  <- normalise_type (substTy (mkTopTCvSubst tenv) rhs)
+                  <- normalise_type (substTyUnchecked (mkTopTCvSubst tenv) rhs)
               ; return $
                 if isReflCo co2
                 then (args_co,                 mkTyConApp tc ntys)
index c0fc5fe..bd5745a 100644 (file)
@@ -19,6 +19,7 @@ Note [The Type-related module hierarchy]
 {-# OPTIONS_HADDOCK hide #-}
 {-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
              DeriveTraversable, MultiWayIf #-}
+{-# LANGUAGE ImplicitParams #-}
 
 module TyCoRep (
         TyThing(..),
@@ -88,7 +89,7 @@ module TyCoRep (
         substTelescope,
         substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
         substCoWith,
-        substTy,
+        substTy, substTyAddInScope, substTyUnchecked,
         substTyWithBinders,
         substTys, substTheta,
         lookupTyVar, substTyVarBndr,
@@ -144,11 +145,13 @@ import Pair
 import UniqSupply
 import ListSetOps
 import Util
+import UniqFM
 
 -- libraries
 import qualified Data.Data as Data hiding ( TyCon )
 import Data.List
 import Data.IORef ( IORef )   -- for CoercionHole
+import GHC.Stack (CallStack)
 
 {-
 %************************************************************************
@@ -1383,6 +1386,7 @@ data TCvSubst
         -- See Note [Apply Once]
         -- and Note [Extending the TvSubstEnv]
         -- and Note [Substituting types and coercions]
+        -- and Note [Generating the in-scope set for a substitution]
 
 -- | A substitution of 'Type's for 'TyVar's
 --                 and 'Kind's for 'KindVar's
@@ -1454,6 +1458,25 @@ Note that the TvSubstEnv should *never* map a CoVar (built with the Id
 constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore,
 the range of the TvSubstEnv should *never* include a type headed with
 CoercionTy.
+
+Note [Generating the in-scope set for a substitution]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When calling substTy subst ty it should be the case that
+the in-scope set in the substitution is a superset of both:
+
+  * The free vars of the range of the substitution
+  * The free vars of ty minus the domain of the substitution
+
+If we want to substitute [a -> ty1, b -> ty2] I used to
+think it was enough to generate an in-scope set that includes
+fv(ty1,ty2).  But that's not enough; we really should also take the
+free vars of the type we are substituting into!  Example:
+     (forall b. (a,b,x)) [a -> List b]
+Then if we use the in-scope set {b}, there is a danger we will rename
+the forall'd variable to 'x' by mistake, getting this:
+     (forall x. (List b, x, x))
+
+Breaking this invariant caused the bug from #11371.
 -}
 
 emptyTvSubstEnv :: TvSubstEnv
@@ -1588,19 +1611,6 @@ unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2)
 -- the types given; but it's just a thunk so with a bit of luck
 -- it'll never be evaluated
 
--- Note [Generating the in-scope set for a substitution]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- If we want to substitute [a -> ty1, b -> ty2] I used to
--- think it was enough to generate an in-scope set that includes
--- fv(ty1,ty2).  But that's not enough; we really should also take the
--- free vars of the type we are substituting into!  Example:
---      (forall b. (a,b,x)) [a -> List b]
--- Then if we use the in-scope set {b}, there is a danger we will rename
--- the forall'd variable to 'x' by mistake, getting this:
---      (forall x. (List b, x, x))
--- Urk!  This means looking at all the calls to mkOpenTCvSubst....
-
-
 -- | Generates an in-scope set from the free variables in a list of types
 -- and a list of coercions
 mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
@@ -1753,7 +1763,7 @@ substTelescope = go_subst emptyTCvSubst
 -- is assumed to be open, see 'zipOpenTCvSubst'
 substTyWith :: [TyVar] -> [Type] -> Type -> Type
 substTyWith tvs tys = ASSERT( length tvs == length tys )
-                      substTy (zipOpenTCvSubst tvs tys)
+                      substTyUnchecked (zipOpenTCvSubst tvs tys)
 
 -- | Coercion substitution making use of an 'TCvSubst' that
 -- is assumed to be open, see 'zipOpenTCvSubst'
@@ -1781,11 +1791,59 @@ substTysWithCoVars cvs cos = ASSERT( length cvs == length cos )
 -- simply ignore their matching type.
 substTyWithBinders :: [TyBinder] -> [Type] -> Type -> Type
 substTyWithBinders bndrs tys = ASSERT( length bndrs == length tys )
-                               substTy (zipOpenTCvSubstBinders bndrs tys)
+                               substTyUnchecked (zipOpenTCvSubstBinders bndrs tys)
+
+-- | Substitute within a 'Type' after adding the free variables of the type
+-- to the in-scope set. This is useful for the case when the free variables
+-- aren't already in the in-scope set or easily available.
+-- See also Note [Generating the in-scope set for a substitution].
+substTyAddInScope :: TCvSubst -> Type -> Type
+substTyAddInScope subst ty =
+  substTy (extendTCvInScopeSet subst $ tyCoVarsOfType ty) ty
+
+-- | When calling `substTy` it should be the case that the in-scope set in
+-- the substitution is a superset of the free vars of the range of the
+-- substitution.
+-- See also Note [Generating the in-scope set for a substitution].
+isValidTCvSubst :: TCvSubst -> Bool
+isValidTCvSubst (TCvSubst in_scope tenv cenv) =
+  (tenvFVs `varSetInScope` in_scope) &&
+  (cenvFVs `varSetInScope` in_scope)
+  where
+  tenvFVs = tyCoVarsOfTypes $ varEnvElts tenv
+  cenvFVs = tyCoVarsOfCos $ varEnvElts cenv
 
 -- | Substitute within a 'Type'
-substTy :: TCvSubst -> Type  -> Type
-substTy subst ty | isEmptyTCvSubst subst = ty
+-- The substitution has to satisfy the invariants described in
+-- Note [Generating the in-scope set for a substitution].
+substTy :: (?callStack :: CallStack) => TCvSubst -> Type  -> Type
+substTy subst@(TCvSubst in_scope tenv cenv) ty
+  | isEmptyTCvSubst subst = ty
+  | otherwise = ASSERT2( isValidTCvSubst subst,
+                         text "in_scope" <+> ppr in_scope $$
+                         text "tenv" <+> ppr tenv $$
+                         text "cenv" <+> ppr cenv $$
+                         text "ty" <+> ppr ty )
+                ASSERT2( typeFVsInScope,
+                         text "in_scope" <+> ppr in_scope $$
+                         text "tenv" <+> ppr tenv $$
+                         text "cenv" <+> ppr cenv $$
+                         text "ty" <+> ppr ty $$
+                         text "needInScope" <+> ppr needInScope )
+                subst_ty subst ty
+  where
+  substDomain = varEnvKeys tenv ++ varEnvKeys cenv
+  needInScope = tyCoVarsOfType ty `delListFromUFM_Directly` substDomain
+  typeFVsInScope = needInScope `varSetInScope` in_scope
+
+-- | Substitute within a 'Type' disabling the sanity checks.
+-- The problems that the sanity checks in substTy catch are described in
+-- Note [Generating the in-scope set for a substitution].
+-- The goal of #11371 is to migrate all the calls of substTyUnchecked to
+-- substTy and remove this function. Please don't use in new code.
+substTyUnchecked :: TCvSubst -> Type  -> Type
+substTyUnchecked subst ty
+                 | isEmptyTCvSubst subst = ty
                  | otherwise             = subst_ty subst ty
 
 -- | Substitute within several 'Type's
@@ -1931,7 +1989,7 @@ lookupCoVar :: TCvSubst -> Var  -> Maybe Coercion
 lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
 
 substTyVarBndr :: TCvSubst -> TyVar -> (TCvSubst, TyVar)
-substTyVarBndr = substTyVarBndrCallback substTy
+substTyVarBndr = substTyVarBndrCallback substTyUnchecked
 
 -- | Substitute a tyvar in a binding position, returning an
 -- extended subst and a new tyvar.
index 94da5f1..4e67db8 100644 (file)
@@ -161,6 +161,7 @@ module Type (
 
         -- ** Performing substitution on types and kinds
         substTy, substTys, substTyWith, substTysWith, substTheta,
+        substTyAddInScope, substTyUnchecked,
         substTyVarBndr, substTyVar, substTyVars,
         cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar, substTelescope,
 
@@ -293,7 +294,7 @@ coreView :: Type -> Maybe Type
 -- By being non-recursive and inlined, this case analysis gets efficiently
 -- joined onto the case analysis that the caller is already doing
 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
-              = Just (mkAppTys (substTy (mkTopTCvSubst tenv) rhs) tys')
+              = Just (mkAppTys (substTyUnchecked (mkTopTCvSubst tenv) rhs) tys')
                -- Its important to use mkAppTys, rather than (foldl AppTy),
                -- because the function part might well return a
                -- partially-applied type constructor; indeed, usually will!
index 9d8669b..969e1dc 100644 (file)
@@ -48,6 +48,7 @@ module UniqFM (
         delFromUFM,
         delFromUFM_Directly,
         delListFromUFM,
+        delListFromUFM_Directly,
         plusUFM,
         plusUFM_C,
         plusUFM_CD,
@@ -138,6 +139,7 @@ adjustUFM_Directly :: (elt -> elt) -> UniqFM elt -> Unique -> UniqFM elt
 
 delFromUFM      :: Uniquable key => UniqFM elt -> key    -> UniqFM elt
 delListFromUFM  :: Uniquable key => UniqFM elt -> [key] -> UniqFM elt
+delListFromUFM_Directly :: UniqFM elt -> [Unique] -> UniqFM elt
 delFromUFM_Directly :: UniqFM elt -> Unique -> UniqFM elt
 
 -- Bindings in right argument shadow those in the left
@@ -252,6 +254,7 @@ adjustUFM_Directly f (UFM m) u = UFM (M.adjust f (getKey u) m)
 delFromUFM (UFM m) k = UFM (M.delete (getKey $ getUnique k) m)
 delListFromUFM = foldl delFromUFM
 delFromUFM_Directly (UFM m) u = UFM (M.delete (getKey u) m)
+delListFromUFM_Directly = foldl delFromUFM_Directly
 
 -- M.union is left-biased, plusUFM should be right-biased.
 plusUFM (UFM x) (UFM y) = UFM (M.union y x)