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

(Another) minor refactoring of substitutions

No change in functionality here, but greater clarity:

* In FamInstEnv.FlattenEnv, kill off the fi_in_scope field
  We are already maintaining an in-scope set in the fe_subst field,
  so it's silly do to it twice.

  (This isn't strictly connected to the rest of this patch, but
  the nomenclature changes below affect the same code, so I put
  them together.)

* TyCoRep.extendTCVSubst used to take a TyVar or a CoVar and work
  out what to do, but in fact we almost always know which of the
  two we are doing.  So:
    - define extendTvSubst, extendCvSubst
    - and use them

* Similar renamings in TyCoRep:
   - extendTCvSubstList        -->   extendTvSubstList
   - extendTCvSubstBinder      -->   extendTvSubstBinder
   - extendTCvSubstAndInScope  --> extendTvSubstAndInScope

* Add Type.extendTvSubstWithClone, extendCvSubstWithClone

* Similar nomenclature changes in Subst, SimplEnv, Specialise

* Kill off TyCoRep.substTelescope (never used)
parent 01449eb5
......@@ -564,8 +564,8 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
mk_boxer boxers = DCB (\ ty_args src_vars ->
do { let (ex_vars, term_vars) = splitAtList ex_tvs src_vars
subst1 = zipTvSubst univ_tvs ty_args
subst2 = extendTCvSubstList subst1 ex_tvs
(mkTyVarTys ex_vars)
subst2 = extendTvSubstList subst1 ex_tvs
(mkTyVarTys ex_vars)
; (rep_ids, binds) <- go subst2 boxers term_vars
; return (ex_vars ++ rep_ids, binds) } )
......
......@@ -1688,7 +1688,7 @@ addInScopeVar var m
extendSubstL :: TyVar -> Type -> LintM a -> LintM a
extendSubstL tv ty m
= LintM $ \ env errs ->
unLintM m (env { le_subst = Type.extendTCvSubst (le_subst env) tv ty }) errs
unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
updateTCvSubst :: TCvSubst -> LintM a -> LintM a
updateTCvSubst subst' m
......
......@@ -21,7 +21,7 @@ module CoreSubst (
-- ** Operations on substitutions
emptySubst, mkEmptySubst, mkSubst, mkOpenSubst, substInScope, isEmptySubst,
extendIdSubst, extendIdSubstList, extendTCvSubst, extendTCvSubstList,
extendIdSubst, extendIdSubstList, extendTCvSubst, extendTvSubstList,
extendSubst, extendSubstList, extendSubstWithVar, zapSubstEnv,
addInScopeSet, extendInScope, extendInScopeList, extendInScopeIds,
isInScope, setInScope,
......@@ -50,7 +50,7 @@ import qualified Type
import qualified Coercion
-- We are defining local versions
import Type hiding ( substTy, extendTCvSubst, extendTCvSubstList
import Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList
, isInScope, substTyVarBndr, cloneTyVarBndr )
import Coercion hiding ( substCo, substCoVarBndr )
......@@ -215,48 +215,43 @@ extendIdSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope (extendVarEnv id
extendIdSubstList :: Subst -> [(Id, CoreExpr)] -> Subst
extendIdSubstList (Subst in_scope ids tvs cvs) prs = Subst in_scope (extendVarEnvList ids prs) tvs cvs
-- | Add a substitution for a 'TyVar' to the 'Subst': the 'TyVar' *must*
-- be a real TyVar, and not a CoVar
extend_tv_subst :: Subst -> TyVar -> Type -> Subst
extend_tv_subst (Subst in_scope ids tvs cvs) tv ty
-- | Add a substitution for a 'TyVar' to the 'Subst'
-- The 'TyVar' *must* be a real TyVar, and not a CoVar
-- You must ensure that the in-scope set is such that
-- the "CoreSubst#in_scope_invariant" is true after extending
-- the substitution like this.
extendTvSubst :: Subst -> TyVar -> Type -> Subst
extendTvSubst (Subst in_scope ids tvs cvs) tv ty
= ASSERT( isTyVar tv )
Subst in_scope ids (extendVarEnv tvs tv ty) cvs
-- | Add a substitution for a 'TyVar' to the 'Subst': you must ensure that the in-scope set is
-- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this
extendTCvSubst :: Subst -> TyVar -> Type -> Subst
extendTCvSubst subst v r
| isTyVar v
= extend_tv_subst subst v r
| Just co <- isCoercionTy_maybe r
= extendCvSubst subst v co
| otherwise
= pprPanic "CoreSubst.extendTCvSubst" (ppr v <+> text "|->" <+> ppr r)
-- | Adds multiple 'TyVar' substitutions to the 'Subst': see also 'extendTCvSubst'
extendTCvSubstList :: Subst -> [(TyVar,Type)] -> Subst
extendTCvSubstList subst vrs
-- | Adds multiple 'TyVar' substitutions to the 'Subst': see also 'extendTvSubst'
extendTvSubstList :: Subst -> [(TyVar,Type)] -> Subst
extendTvSubstList subst vrs
= foldl' extend subst vrs
where extend subst (v, r) = extendTCvSubst subst v r
where
extend subst (v, r) = extendTvSubst subst v r
-- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst': you must ensure that the in-scope set is
-- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this
extendCvSubst :: Subst -> CoVar -> Coercion -> Subst
extendCvSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope ids tvs (extendVarEnv cvs v r)
extendCvSubst (Subst in_scope ids tvs cvs) v r
= ASSERT( isCoVar v )
Subst in_scope ids tvs (extendVarEnv cvs v r)
-- | Add a substitution appropriate to the thing being substituted
-- (whether an expression, type, or coercion). See also
-- 'extendIdSubst', 'extendTCvSubst'
-- 'extendIdSubst', 'extendTvSubst', 'extendCvSubst'
extendSubst :: Subst -> Var -> CoreArg -> Subst
extendSubst subst var arg
= case arg of
Type ty -> ASSERT( isTyVar var ) extend_tv_subst subst var ty
Type ty -> ASSERT( isTyVar var ) extendTvSubst subst var ty
Coercion co -> ASSERT( isCoVar var ) extendCvSubst subst var co
_ -> ASSERT( isId var ) extendIdSubst subst var arg
extendSubstWithVar :: Subst -> Var -> Var -> Subst
extendSubstWithVar subst v1 v2
| isTyVar v1 = ASSERT( isTyVar v2 ) extend_tv_subst subst v1 (mkTyVarTy v2)
| isTyVar v1 = ASSERT( isTyVar v2 ) extendTvSubst subst v1 (mkTyVarTy v2)
| isCoVar v1 = ASSERT( isCoVar v2 ) extendCvSubst subst v1 (mkCoVarCo v2)
| otherwise = ASSERT( isId v2 ) extendIdSubst subst v1 (Var v2)
......@@ -1050,7 +1045,7 @@ maybe_substitute :: Subst -> InVar -> OutExpr -> Maybe Subst
maybe_substitute subst b r
| Type ty <- r -- let a::* = TYPE ty in <body>
= ASSERT( isTyVar b )
Just (extendTCvSubst subst b ty)
Just (extendTvSubst subst b ty)
| Coercion co <- r
= ASSERT( isCoVar b )
......
......@@ -1564,7 +1564,7 @@ dataConInstPat fss uniqs con inst_tys
(zip3 ex_tvs ex_fss ex_uniqs)
mk_ex_var :: TCvSubst -> (TyVar, FastString, Unique) -> (TCvSubst, TyVar)
mk_ex_var subst (tv, fs, uniq) = (Type.extendTCvSubst subst tv
mk_ex_var subst (tv, fs, uniq) = (Type.extendTvSubst subst tv
(mkTyVarTy new_tv)
, new_tv)
where
......
......@@ -505,7 +505,7 @@ toIfaceTcArgs tc ty_args
| otherwise = ITC_Invis t' ts'
where
t' = toIfaceType t
ts' = go (extendTCvSubstBinder env bndr t) res ts
ts' = go (extendTvSubstBinder env bndr t) res ts
go env (TyVarTy tv) ts
| Just ki <- lookupTyVar env tv = go env ki ts
......
......@@ -54,7 +54,7 @@ import Packages
-- Important GHC types
import Module
import Type hiding {- conflict with CoreSubst -}
( substTy, extendTCvSubst, extendTCvSubstList, isInScope )
( substTy, extendTvSubst, extendTvSubstList, isInScope )
import Coercion hiding {- conflict with CoreSubst -}
( substCo )
import TyCon
......
......@@ -16,7 +16,8 @@ module SimplEnv (
-- Environments
SimplEnv(..), StaticEnv, pprSimplEnv, -- Temp not abstract
mkSimplEnv, extendIdSubst, SimplEnv.extendTCvSubst,
mkSimplEnv, extendIdSubst,
SimplEnv.extendTvSubst, SimplEnv.extendCvSubst,
zapSubstEnv, setSubstEnv,
getInScope, setInScope, setInScopeSet, modifyInScope, addNewInScopeIds,
getSimplRules,
......@@ -271,14 +272,15 @@ extendIdSubst env@(SimplEnv {seIdSubst = subst}) var res
= ASSERT2( isId var && not (isCoVar var), ppr var )
env {seIdSubst = extendVarEnv subst var res}
extendTCvSubst :: SimplEnv -> TyVar -> Type -> SimplEnv
extendTCvSubst env@(SimplEnv {seTvSubst = tsubst, seCvSubst = csubst}) var res
| isTyVar var
= env {seTvSubst = extendVarEnv tsubst var res}
| Just co <- isCoercionTy_maybe res
= env {seCvSubst = extendVarEnv csubst var co}
| otherwise
= pprPanic "SimplEnv.extendTCvSubst" (ppr res)
extendTvSubst :: SimplEnv -> TyVar -> Type -> SimplEnv
extendTvSubst env@(SimplEnv {seTvSubst = tsubst}) var res
= ASSERT( isTyVar var )
env {seTvSubst = extendVarEnv tsubst var res}
extendCvSubst :: SimplEnv -> CoVar -> Coercion -> SimplEnv
extendCvSubst env@(SimplEnv {seCvSubst = csubst}) var co
= ASSERT( isCoVar var )
env {seCvSubst = extendVarEnv csubst var co}
---------------------
getInScope :: SimplEnv -> InScopeSet
......
......@@ -12,7 +12,7 @@ module Simplify ( simplTopBinds, simplExpr, simplRules ) where
import DynFlags
import SimplMonad
import Type hiding ( substTy, substTyVar, extendTCvSubst )
import Type hiding ( substTy, substTyVar, extendTvSubst, extendCvSubst )
import SimplEnv
import SimplUtils
import FamInstEnv ( FamInstEnv )
......@@ -385,7 +385,7 @@ simplNonRecX env bndr new_rhs
-- the binding c = (a,b)
| Coercion co <- new_rhs
= return (extendTCvSubst env bndr (mkCoercionTy co))
= return (extendCvSubst env bndr co)
| otherwise
= do { (env', bndr') <- simplBinder env bndr
......@@ -665,7 +665,7 @@ completeBind :: SimplEnv
completeBind env top_lvl old_bndr new_bndr new_rhs
| isCoVar old_bndr
= case new_rhs of
Coercion co -> return (extendTCvSubst env old_bndr (mkCoercionTy co))
Coercion co -> return (extendCvSubst env old_bndr co)
_ -> return (addNonRec env new_bndr new_rhs)
| otherwise
......@@ -1237,7 +1237,7 @@ simplLam env [] body cont = simplExprF env body cont
simplLam env (bndr:bndrs) body (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = cont })
= do { tick (BetaReduction bndr)
; simplLam (extendTCvSubst env bndr arg_ty) bndrs body cont }
; simplLam (extendTvSubst env bndr arg_ty) bndrs body cont }
simplLam env (bndr:bndrs) body (ApplyToVal { sc_arg = arg, sc_env = arg_se
, sc_cont = cont })
......@@ -1245,7 +1245,7 @@ simplLam env (bndr:bndrs) body (ApplyToVal { sc_arg = arg, sc_env = arg_se
; simplNonRecE env' (zap_unfolding bndr) (arg, arg_se) (bndrs, body) cont }
where
env' | Coercion co <- arg
= extendTCvSubst env bndr (mkCoercionTy co)
= extendCvSubst env bndr co
| otherwise
= env
......@@ -1321,7 +1321,7 @@ simplNonRecE :: SimplEnv
simplNonRecE env bndr (Type ty_arg, rhs_se) (bndrs, body) cont
= ASSERT( isTyVar bndr )
do { ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
; simplLam (extendTCvSubst env bndr ty_arg') bndrs body cont }
; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
= do dflags <- getDynFlags
......@@ -2260,11 +2260,11 @@ knownCon env scrut dc dc_ty_args dc_args bndr bs rhs cont
bind_args env' (b:bs') (Type ty : args)
= ASSERT( isTyVar b )
bind_args (extendTCvSubst env' b ty) bs' args
bind_args (extendTvSubst env' b ty) bs' args
bind_args env' (b:bs') (Coercion co : args)
= ASSERT( isCoVar b )
bind_args (extendTCvSubst env' b (mkCoercionTy co)) bs' args
bind_args (extendCvSubst env' b co) bs' args
bind_args env' (b:bs') (arg : args)
= ASSERT( isId b )
......
......@@ -10,8 +10,8 @@ module Specialise ( specProgram, specUnfolding ) where
#include "HsVersions.h"
import Id
import TcType hiding( substTy, extendTCvSubstList )
import Type hiding( substTy, extendTCvSubstList )
import TcType hiding( substTy )
import Type hiding( substTy, extendTvSubstList )
import Coercion( Coercion )
import Module( Module, HasModule(..) )
import CoreMonad
......@@ -1241,7 +1241,7 @@ specCalls mb_mod env rules_for_me calls_for_me fn rhs
-- spec_tyvars = [a,c]
-- ty_args = [t1,b,t3]
spec_tv_binds = [(tv,ty) | (tv, Just ty) <- rhs_tyvars `zip` call_ts]
env1 = extendTCvSubstList env spec_tv_binds
env1 = extendTvSubstList env spec_tv_binds
(rhs_env, poly_tyvars) = substBndrs env1
[tv | (tv, Nothing) <- rhs_tyvars `zip` call_ts]
......@@ -2133,9 +2133,9 @@ mapAndCombineSM f (x:xs) = do (y, uds1) <- f x
(ys, uds2) <- mapAndCombineSM f xs
return (y:ys, uds1 `plusUDs` uds2)
extendTCvSubstList :: SpecEnv -> [(TyVar,Type)] -> SpecEnv
extendTCvSubstList env tv_binds
= env { se_subst = CoreSubst.extendTCvSubstList (se_subst env) tv_binds }
extendTvSubstList :: SpecEnv -> [(TyVar,Type)] -> SpecEnv
extendTvSubstList env tv_binds
= env { se_subst = CoreSubst.extendTvSubstList (se_subst env) tv_binds }
substTy :: SpecEnv -> Type -> Type
substTy env ty = CoreSubst.substTy (se_subst env) ty
......
......@@ -228,7 +228,8 @@ deeplyInstantiate orig ty
, text "type" <+> ppr ty
, text "with" <+> ppr tvs'
, text "args:" <+> ppr ids1
, text "theta:" <+> ppr theta' ])
, text "theta:" <+> ppr theta'
, text "subst:" <+> ppr subst ])
; (wrap2, rho2) <- deeplyInstantiate orig (substTyUnchecked subst rho)
; return (mkWpLams ids1
<.> wrap2
......@@ -309,7 +310,7 @@ instDFunType dfun_id dfun_inst_tys
go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
go subst [] [] = return (subst, [])
go subst (tv:tvs) (Just ty : mb_tys)
= do { (subst', tys) <- go (extendTCvSubst subst tv ty) tvs mb_tys
= do { (subst', tys) <- go (extendTvSubst subst tv ty) tvs mb_tys
; return (subst', ty : tys) }
go subst (tv:tvs) (Nothing : mb_tys)
= do { (subst', tv') <- newMetaTyVarX subst tv
......
......@@ -479,7 +479,7 @@ tcATDefault emit_warn loc inst_subst defined_ats (ATI fam_tc defs)
| Just ty <- lookupVarEnv (getTvSubstEnv subst) tc_tv
= (subst, ty)
| otherwise
= (extendTCvSubst subst tc_tv ty', ty')
= (extendTvSubst subst tc_tv ty', ty')
where
ty' = mkTyVarTy (updateTyVarKind (substTyUnchecked subst) tc_tv)
......
......@@ -860,7 +860,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
-- c.f. TcMType.newMetaTyVars
mk_inst_ty subst (tv, result_inst_ty)
| is_fixed_tv tv -- Same as result type
= return (extendTCvSubst subst tv result_inst_ty, result_inst_ty)
= return (extendTvSubst subst tv result_inst_ty, result_inst_ty)
| otherwise -- Fresh type, of correct kind
= do { (subst', new_tv) <- newMetaTyVarX subst tv
; return (subst', mkTyVarTy new_tv) }
......
......@@ -769,7 +769,7 @@ tc_infer_args mode orig_ty ki mb_kind_info orig_args n0
; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
tc_lhs_type mode' arg (substTyUnchecked subst $ binderType bndr)
; let subst' = case binderVar_maybe bndr of
Just tv -> extendTCvSubst subst tv arg'
Just tv -> extendTvSubst subst tv arg'
Nothing -> subst
; go subst' res_k args (n+1) (arg' : acc) }
......@@ -830,7 +830,7 @@ tcInstBinderX :: Maybe (VarEnv Kind)
tcInstBinderX mb_kind_info subst binder
| Just tv <- binderVar_maybe binder
= case lookup_tv tv of
Just ki -> return (extendTCvSubstAndInScope subst tv ki, ki)
Just ki -> return (extendTvSubstAndInScope subst tv ki, ki)
Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv
; return (subst', mkTyVarTy tv') }
......
......@@ -81,7 +81,7 @@ module TcMType (
#include "HsVersions.h"
-- friends:
import TyCoRep ( CoercionHole(..) )
import TyCoRep
import TcType
import Type
import Coercion
......@@ -453,8 +453,7 @@ tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
tcSuperSkolTyVar subst tv
= (extendTCvSubst (extendTCvInScope subst new_tv) tv (mkTyVarTy new_tv)
, new_tv)
= (extendTvSubstWithClone subst tv new_tv, new_tv)
where
kind = substTyUnchecked subst (tyVarKind tv)
new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
......@@ -535,19 +534,16 @@ instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
instSkolTyCoVarX mk_tcv subst tycovar
= do { uniq <- newUnique -- using a new unique is critical. See
-- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
; let new_tv = mk_tcv uniq old_name kind
; return (extendTCvSubst (extendTCvInScope subst new_tv) tycovar
(mk_ty_co new_tv)
, new_tv)
}
; let new_tcv = mk_tcv uniq old_name kind
subst1 | isTyVar new_tcv
= extendTvSubstWithClone subst tycovar new_tcv
| otherwise
= extendCvSubstWithClone subst tycovar new_tcv
; return (subst1, new_tcv) }
where
old_name = tyVarName tycovar
kind = substTyUnchecked subst (tyVarKind tycovar)
mk_ty_co v
| isTyVar v = mkTyVarTy v
| otherwise = mkCoercionTy $ mkCoVarCo v
newFskTyVar :: TcType -> TcM TcTyVar
newFskTyVar fam_ty
= do { uniq <- newUnique
......@@ -777,29 +773,22 @@ newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
newMetaTyVarX subst tyvar
= do { uniq <- newUnique
; details <- newMetaDetails TauTv
; let name = mkSystemName uniq (getOccName tyvar)
-- See Note [Name of an instantiated type variable]
kind = substTyUnchecked subst (tyVarKind tyvar)
new_tv = mkTcTyVar name kind details
; return (extendTCvSubstAndInScope subst tyvar
(mkTyVarTy new_tv)
, new_tv)
}
newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a SigTv
newMetaSigTyVarX subst tyvar
newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
new_meta_tv_x info subst tyvar
= do { uniq <- newUnique
; details <- newMetaDetails SigTv
; details <- newMetaDetails info
; let name = mkSystemName uniq (getOccName tyvar)
kind = substTy subst (tyVarKind tyvar)
-- See Note [Name of an instantiated type variable]
kind = substTyUnchecked subst (tyVarKind tyvar)
new_tv = mkTcTyVar name kind details
; return (extendTCvSubst (extendTCvInScope subst new_tv) tyvar
(mkTyVarTy new_tv)
, new_tv) }
subst1 = extendTvSubstWithClone subst tyvar new_tv
; return (subst1, new_tv) }
{- Note [Name of an instantiated type variable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -2891,7 +2891,7 @@ instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTCvSubst tvs)
inst_one subst tv
= do { ty' <- instFlexiTcSHelper (tyVarName tv)
(substTyUnchecked subst (tyVarKind tv))
; return (extendTCvSubst subst tv ty', ty') }
; return (extendTvSubst subst tv ty', ty') }
instFlexiTcSHelper :: Name -> Kind -> TcM TcType
instFlexiTcSHelper tvname kind
......
......@@ -1815,8 +1815,8 @@ mkGADTVars tmpl_tvs dc_tvs subst
, tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv))
-> -- simple, well-kinded variable substitution.
choose (r_tv:univs) eqs
(extendTCvSubst t_sub t_tv r_ty)
(extendTCvSubst r_sub r_tv r_ty)
(extendTvSubst t_sub t_tv r_ty)
(extendTvSubst r_sub r_tv r_ty)
t_tvs
where
r_tv1 = setTyVarName r_tv (choose_tv_name r_tv t_tv)
......
......@@ -149,9 +149,10 @@ module TcType (
zipTvSubst,
mkTvSubstPrs, notElemTCvSubst, unionTCvSubst,
getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
extendTCvInScopeList, extendTCvInScopeSet, extendTCvSubstAndInScope,
extendTCvInScopeList, extendTCvInScopeSet, extendTvSubstAndInScope,
Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
extendTCvSubstList, isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
Type.extendTvSubst,
isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
Type.substTy, substTys, substTyWith, substTyWithCoVars,
substTyAddInScope,
substTyUnchecked, substTysUnchecked, substThetaUnchecked,
......
......@@ -73,7 +73,7 @@ module Coercion (
lookupCoVar,
substCo, substCos, substCoVar, substCoVars, substCoWith,
substCoVarBndr,
extendTCvSubstAndInScope, getCvSubstEnv,
extendTvSubstAndInScope, getCvSubstEnv,
-- ** Lifting
liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
......
......@@ -1427,13 +1427,11 @@ flattenTys is defined here because of module dependencies.
-}
data FlattenEnv = FlattenEnv { fe_type_map :: TypeMap TyVar
, fe_in_scope :: InScopeSet
, fe_subst :: TCvSubst }
emptyFlattenEnv :: InScopeSet -> FlattenEnv
emptyFlattenEnv in_scope
= FlattenEnv { fe_type_map = emptyTypeMap
, fe_in_scope = in_scope
, fe_subst = mkEmptyTCvSubst in_scope }
-- See Note [Flattening]
......@@ -1502,28 +1500,27 @@ coreFlattenCo env co
where
(env1, kind') = coreFlattenTy env (coercionType co)
fresh_name = mkFlattenFreshCoName
in_scope = fe_in_scope env1
covar = uniqAway in_scope $ mkCoVar fresh_name kind'
env2 = env1 { fe_in_scope = in_scope `extendInScopeSet` covar }
subst1 = fe_subst env1
in_scope = getTCvInScope subst1
covar = uniqAway in_scope (mkCoVar fresh_name kind')
env2 = env1 { fe_subst = subst1 `extendTCvInScope` covar }
coreFlattenVarBndr :: FlattenEnv -> TyVar -> (FlattenEnv, TyVar)
coreFlattenVarBndr env tv
| kind' `eqType` kind
= ( env { fe_subst = extendTCvSubst old_subst tv (mkTyVarTy tv) }
= ( env { fe_subst = extendTvSubst old_subst tv (mkTyVarTy tv) }
-- override any previous binding for tv
, tv)
| otherwise
= let new_tv = uniqAway (fe_in_scope env) (setTyVarKind tv kind')
new_subst = extendTCvSubst old_subst tv (mkTyVarTy new_tv)
new_is = extendInScopeSet old_in_scope new_tv
= let new_tv = uniqAway (getTCvInScope old_subst) (setTyVarKind tv kind')
new_subst = extendTvSubstWithClone old_subst tv new_tv
in
(env' { fe_in_scope = new_is
, fe_subst = new_subst }, new_tv)
(env' { fe_subst = new_subst }, new_tv)
where
kind = tyVarKind tv
(env', kind') = coreFlattenTy env kind
old_subst = fe_subst env
old_in_scope = fe_in_scope env
coreFlattenTyFamApp :: FlattenEnv
-> TyCon -- type family tycon
......@@ -1538,14 +1535,14 @@ coreFlattenTyFamApp env fam_tc fam_args
-- contains *all* tyvars, even locally bound ones elsewhere in the
-- overall type, so this really is fresh.
Nothing -> let tyvar_name = mkFlattenFreshTyName fam_tc
tv = uniqAway in_scope $ mkTyVar tyvar_name
(typeKind fam_ty)
tv = uniqAway (getTCvInScope subst) $
mkTyVar tyvar_name (typeKind fam_ty)
env' = env { fe_type_map = extendTypeMap type_map fam_ty tv
, fe_in_scope = extendInScopeSet in_scope tv }
, fe_subst = extendTCvInScope subst tv }
in (env', tv)
where fam_ty = mkTyConApp fam_tc fam_args
FlattenEnv { fe_type_map = type_map
, fe_in_scope = in_scope } = env
, fe_subst = subst } = env
-- | Get the set of all type variables mentioned anywhere in the list
-- of types. These variables are not necessarily free.
......
......@@ -10,7 +10,7 @@ module OptCoercion ( optCoercion, checkAxInstCo ) where
import TyCoRep
import Coercion
import Type hiding( substTyVarBndr, substTy, extendTCvSubst )
import Type hiding( substTyVarBndr, substTy )
import TcType ( exactTyCoVarsOfType )
import TyCon
import CoAxiom
......
......@@ -83,14 +83,16 @@ module TyCoRep (
getCvSubstEnv, getTCvInScope, isInScope, notElemTCvSubst,
setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
extendTCvSubst, extendTCvSubstAndInScope, extendTCvSubstList,
extendTCvSubstBinder,
extendTCvSubst,
extendCvSubst, extendCvSubstWithClone,
extendTvSubst, extendTvSubstWithClone,
extendTvSubstList, extendTvSubstAndInScope,
extendTvSubstBinder,
unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
zipTvSubst, zipCvSubst,
zipTyBinderSubst,
mkTvSubstPrs,
substTelescope,
substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
substCoWith,
substTy, substTyAddInScope,
......@@ -239,8 +241,8 @@ data TyLit
-- ('Named') or nondependent ('Anon'). They may also be visible or not.
-- See also Note [TyBinder]
data TyBinder
= Named TyVar VisibilityFlag
| Anon Type -- visibility is determined by the type (Constraint vs. *)
= Named TyVar VisibilityFlag -- Always a TyVar (not CoVar or Id)
| Anon Type -- Visibility is determined by the type (Constraint vs. *)
deriving (Data.Typeable, Data.Data)
-- | Is something required to appear in source Haskell ('Visible'),
......@@ -1517,7 +1519,7 @@ CoercionTy.
Note [The substitution invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When calling substTy subst ty it should be the case that
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
......@@ -1624,39 +1626,50 @@ extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
extendTCvInScopeSet (TCvSubst in_scope tenv cenv) vars
= TCvSubst (extendInScopeSetSet in_scope vars) tenv cenv
extendSubstEnvs :: (TvSubstEnv, CvSubstEnv) -> Var -> Type
-> (TvSubstEnv, CvSubstEnv)
extendSubstEnvs (tenv, cenv) v ty
extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst
extendTCvSubst subst v ty
| isTyVar v
= ASSERT( not $ isCoercionTy ty )
(extendVarEnv tenv v ty, cenv)
-- NB: v might *not* be a proper covar, because it might be lifted.
-- This happens in tcCoercionToCoercion
= extendTvSubst subst v ty
| CoercionTy co <- ty
= (tenv, extendVarEnv cenv v co)
= extendCvSubst subst v co
| otherwise
= pprPanic "extendSubstEnvs" (ppr v <+> text "|->" <+> ppr ty)
extendTCvSubst :: TCvSubst -> Var -> Type -> TCvSubst
extendTCvSubst (TCvSubst in_scope tenv cenv) tv ty
= TCvSubst in_scope tenv' cenv'
where (tenv', cenv') = extendSubstEnvs (tenv, cenv) tv ty
extendTCvSubstAndInScope :: TCvSubst -> TyCoVar -> Type -> TCvSubst
= pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty)
extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst
extendTvSubst (TCvSubst in_scope tenv cenv) tv ty
= TCvSubst in_scope (extendVarEnv tenv tv ty) cenv
extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst
-- Adds a new tv -> tv mapping, /and/ extends the in-scope set
extendTvSubstWithClone (TCvSubst in_scope tenv cenv) tv tv'
= TCvSubst (extendInScopeSet in_scope tv')
(extendVarEnv tenv tv (mkTyVarTy tv'))
cenv
extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst
extendCvSubst (TCvSubst in_scope tenv cenv) v co
= TCvSubst in_scope tenv (extendVarEnv cenv v co)
extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst
extendCvSubstWithClone (TCvSubst in_scope tenv cenv) cv cv'
= TCvSubst (extendInScopeSet in_scope cv')
tenv
(extendVarEnv cenv cv (mkCoVarCo cv'))
extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
-- Also extends the in-scope set
extendTCvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty
extendTvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty
= TCvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfType ty)
tenv' cenv'
where (tenv', cenv') = extendSubstEnvs (tenv, cenv) tv ty
(extendVarEnv tenv tv ty)
cenv
extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
extendTCvSubstList subst tvs tys
= foldl2 extendTCvSubst subst tvs tys
extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
extendTvSubstList subst tvs tys
= foldl2 extendTvSubst subst tvs tys
extendTCvSubstBinder :: TCvSubst -> TyBinder -> Type -> TCvSubst
extendTCvSubstBinder env (Anon {}) _ = env
extendTCvSubstBinder env (Named tv _) ty = extendTCvSubst env tv ty
extendTvSubstBinder :: TCvSubst -> TyBinder -> Type -> TCvSubst
extendTvSubstBinder env (Anon {}) _ = env
extendTvSubstBinder env (Named tv _) ty = extendTvSubst env tv ty
unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
-- Works when the ranges are disjoint
......@@ -1798,19 +1811,6 @@ ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h])
-}
-- | Create a substitution from tyvars to types, but later types may depend
-- on earlier ones. Return the substed types and the built substitution.
substTelescope :: [TyCoVar] -> [Type] -> ([Type], TCvSubst)
substTelescope = go_subst emptyTCvSubst
where
go_subst :: TCvSubst -> [TyCoVar] -> [Type] -> ([Type], TCvSubst)
go_subst subst [] [] = ([], subst)
go_subst subst (tv:tvs) (k:ks)
= let k' = substTy subst k in
liftFst (k' :) $ go_subst (extendTCvSubst subst tv k') tvs ks
go_subst _ _ _ = panic "substTelescope"
-- | Type substitution, see 'zipTvSubst'
substTyWith ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
......@@ -1818,6 +1818,8 @@ substTyWith ::
(?callStack :: CallStack) =>
#endif
[TyVar] -> [Type] -> Type -> Type
-- Works only if the domain of the substitution is a
-- superset of the type being substituted into
substTyWith tvs tys = ASSERT( length tvs == length tys )
substTy (zipTvSubst tvs tys)
......
......@@ -157,7 +157,8 @@ module Type (
getTvSubstEnv, setTvSubstEnv,
zapTCvSubst, getTCvInScope,
extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
extendTCvSubst, extendTCvSubstList, extendTCvSubstAndInScope,
extendTCvSubst, extendCvSubst,
extendTvSubst, extendTvSubstList, extendTvSubstAndInScope,
isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
isEmptyTCvSubst, unionTCvSubst,
......@@ -168,7 +169,7 @@ module Type (