{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1998
Type and Coercion - friends' interface
-}


{-# LANGUAGE BangPatterns #-}

-- | Substitution into types and coercions.
module GHC.Core.TyCo.Subst
  (
        -- * Substitutions
        Subst(..), TvSubstEnv, CvSubstEnv, IdSubstEnv,
        emptyIdSubstEnv, emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubst,
        emptySubst, mkEmptySubst, isEmptyTCvSubst, isEmptySubst,
        mkSubst, mkTvSubst, mkCvSubst, mkIdSubst,
        getTvSubstEnv, getIdSubstEnv,
        getCvSubstEnv, getSubstInScope, setInScope, getSubstRangeTyCoFVs,
        isInScope, elemSubst, notElemSubst, zapSubst,
        extendSubstInScope, extendSubstInScopeList, extendSubstInScopeSet,
        extendTCvSubst, extendTCvSubstWithClone,
        extendCvSubst, extendCvSubstWithClone,
        extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone,
        extendTvSubstList, extendTvSubstAndInScope,
        extendTCvSubstList,
        unionSubst, zipTyEnv, zipCoEnv,
        zipTvSubst, zipCvSubst,
        zipTCvSubst,
        mkTvSubstPrs,

        substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
        substCoWith,
        substTy, substTyAddInScope, substScaledTy,
        substTyUnchecked, substTysUnchecked, substScaledTysUnchecked, substThetaUnchecked,
        substTyWithUnchecked, substScaledTyUnchecked,
        substCoUnchecked, substCoWithUnchecked,
        substTyWithInScope,
        substTys, substScaledTys, substTheta,
        lookupTyVar,
        substCo, substCos, substCoVar, substCoVars, lookupCoVar,
        cloneTyVarBndr, cloneTyVarBndrs,
        substVarBndr, substVarBndrs,
        substTyVarBndr, substTyVarBndrs,
        substCoVarBndr,
        substTyVar, substTyVars, substTyVarToTyVar,
        substTyCoVars,
        substTyCoBndr, substForAllCoBndr,
        substVarBndrUsing, substForAllCoBndrUsing,
        checkValidSubst, isValidTCvSubst,
  ) where

import GHC.Prelude

import {-# SOURCE #-} GHC.Core.Type
   ( mkCastTy, mkAppTy, isCoercionTy, mkTyConApp, getTyVar_maybe )
import {-# SOURCE #-} GHC.Core.Coercion
   ( mkCoVarCo, mkKindCo, mkSelCo, mkTransCo
   , mkNomReflCo, mkSubCo, mkSymCo
   , mkFunCo2, mkForAllCo, mkUnivCo
   , mkAxiomInstCo, mkAppCo, mkGReflCo
   , mkInstCo, mkLRCo, mkTyConAppCo
   , mkCoercionType
   , coercionKind, coercionLKind, coVarKindsTypesRole )
import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprTyVar )
import {-# SOURCE #-} GHC.Core.Ppr ( )
import {-# SOURCE #-} GHC.Core ( CoreExpr )

import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs

import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env

import GHC.Data.Pair
import GHC.Utils.Constants (debugIsOn)
import GHC.Utils.Misc
import GHC.Types.Unique.Supply
import GHC.Types.Unique
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain

import Data.List (mapAccumL)

{-
%************************************************************************
%*                                                                      *
                        Substitutions
      Data type defined here to avoid unnecessary mutual recursion
%*                                                                      *
%************************************************************************
-}

-- | Type & coercion & id substitution
--
-- The "Subst" data type defined in this module contains substitution
-- for tyvar, covar and id. However, operations on IdSubstEnv (mapping
-- from "Id" to "CoreExpr") that require the definition of the "Expr"
-- data type are defined in GHC.Core.Subst to avoid circular module
-- dependency.
data Subst
  = Subst InScopeSet  -- Variables in scope (both Ids and TyVars) /after/
                      -- applying the substitution
          IdSubstEnv  -- Substitution from NcIds to CoreExprs
          TvSubstEnv  -- Substitution from TyVars to Types
          CvSubstEnv  -- Substitution from CoVars to Coercions

        -- INVARIANT 1: See Note [The substitution invariant]
        -- This is what lets us deal with name capture properly
        --
        -- INVARIANT 2: The substitution is apply-once;
        --              see Note [Substitutions apply only once]
        --
        -- INVARIANT 3: See Note [Extending the IdSubstEnv] in "GHC.Core.Subst"
        -- and Note [Extending the TvSubstEnv and CvSubstEnv]
        --
        -- INVARIANT 4: See Note [Substituting types, coercions, and expressions]

-- | A substitution of 'Expr's for non-coercion 'Id's
type IdSubstEnv = IdEnv CoreExpr   -- Domain is NonCoVarIds, i.e. not coercions

-- | A substitution of 'Type's for 'TyVar's
--                 and 'Kind's for 'KindVar's
type TvSubstEnv = TyVarEnv Type
  -- NB: A TvSubstEnv is used
  --   both inside a TCvSubst (with the apply-once invariant
  --        discussed in Note [Substitutions apply only once],
  --   and  also independently in the middle of matching,
  --        and unification (see Types.Unify).
  -- So you have to look at the context to know if it's idempotent or
  -- apply-once or whatever

-- | A substitution of 'Coercion's for 'CoVar's
type CvSubstEnv = CoVarEnv Coercion

{- Note [The substitution invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When calling (substTy subst ty) it should be the case that
the in-scope set in the substitution is a superset of both:

  (SIa) The free vars of the range of the substitution
  (SIb) The free vars of ty minus the domain of the substitution

* Reason for (SIa). Consider
      substTy [a :-> Maybe b] (forall b. b->a)
  we must rename the forall b, to get
      forall b2. b2 -> Maybe b
  Making 'b' part of the in-scope set forces this renaming to
  take place.

* Reason for (SIb). Consider
     substTy [a :-> Maybe b] (forall b. (a,b,x))
  Then if we use the in-scope set {b}, satisfying (SIa), there is
  a danger we will rename the forall'd variable to 'x' by mistake,
  getting this:
      forall x. (Maybe b, x, x)
  Breaking (SIb) caused the bug from #11371.

Note: if the free vars of the range of the substitution are freshly created,
then the problems of (SIa) can't happen, and so it would be sound to
ignore (SIa).

Note [Substitutions apply only once]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We use TCvSubsts to instantiate things, and we might instantiate
        forall a b. ty
with the types
        [a, b], or [b, a].
So the substitution might go [a->b, b->a].  A similar situation arises in Core
when we find a beta redex like
        (/\ a /\ b -> e) b a
Then we also end up with a substitution that permutes type variables. Other
variations happen to; for example [a -> (a, b)].

        ********************************************************
        *** So a substitution must be applied precisely once ***
        ********************************************************

A TCvSubst is not idempotent, but, unlike the non-idempotent substitution
we use during unifications, it must not be repeatedly applied.

Note [Extending the TvSubstEnv and CvSubstEnv]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See #tcvsubst_invariant# for the invariants that must hold.

This invariant allows a short-cut when the subst envs are empty:
if the TvSubstEnv and CvSubstEnv are empty --- i.e. (isEmptyTCvSubst subst)
holds --- then (substTy subst ty) does nothing.

For example, consider:
        (/\a. /\b:(a~Int). ...b..) Int
We substitute Int for 'a'.  The Unique of 'b' does not change, but
nevertheless we add 'b' to the TvSubstEnv, because b's kind does change

This invariant has several crucial consequences:

* In substVarBndr, we need extend the TvSubstEnv
        - if the unique has changed
        - or if the kind has changed

* In substTyVar, we do not need to consult the in-scope set;
  the TvSubstEnv is enough

* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty

Note [Substituting types, coercions, and expressions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Types and coercions are mutually recursive, and either may have variables
"belonging" to the other. Thus, every time we wish to substitute in a
type, we may also need to substitute in a coercion, and vice versa.
Likewise, expressions may contain type variables or coercion variables.
However, we use different constructors for constructing expression variables,
coercion variables, and type variables, so we carry three VarEnvs for each
variable type. Note that it would be possible to use the CoercionTy constructor
and the Type constructor to combine these environments, but that seems like a
false economy.

Note that the domain of the VarEnvs must be respected, despite the fact that
TyVar, Id, and CoVar are all type synonyms of the Var type. For example,
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.
-}

emptyIdSubstEnv :: IdSubstEnv
emptyIdSubstEnv :: IdSubstEnv
emptyIdSubstEnv = IdSubstEnv
forall a. VarEnv a
emptyVarEnv

emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv = TvSubstEnv
forall a. VarEnv a
emptyVarEnv

emptyCvSubstEnv :: CvSubstEnv
emptyCvSubstEnv :: CvSubstEnv
emptyCvSubstEnv = CvSubstEnv
forall a. VarEnv a
emptyVarEnv

-- | Composes two substitutions, applying the second one provided first,
-- like in function composition. This function leaves IdSubstEnv untouched
-- because IdSubstEnv is not used during substitution for types.
composeTCvSubst :: Subst -> Subst -> Subst
composeTCvSubst :: Subst -> Subst -> Subst
composeTCvSubst subst1 :: Subst
subst1@(Subst InScopeSet
is1 IdSubstEnv
ids1 TvSubstEnv
tenv1 CvSubstEnv
cenv1) (Subst InScopeSet
is2 IdSubstEnv
_ TvSubstEnv
tenv2 CvSubstEnv
cenv2)
  = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
is3 IdSubstEnv
ids1 TvSubstEnv
tenv3 CvSubstEnv
cenv3
  where
    is3 :: InScopeSet
is3 = InScopeSet
is1 InScopeSet -> InScopeSet -> InScopeSet
`unionInScope` InScopeSet
is2
    tenv3 :: TvSubstEnv
tenv3 = TvSubstEnv
tenv1 TvSubstEnv -> TvSubstEnv -> TvSubstEnv
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv` (Type -> Type) -> TvSubstEnv -> TvSubstEnv
forall a b. (a -> b) -> VarEnv a -> VarEnv b
mapVarEnv (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
extended_subst1) TvSubstEnv
tenv2
    cenv3 :: CvSubstEnv
cenv3 = CvSubstEnv
cenv1 CvSubstEnv -> CvSubstEnv -> CvSubstEnv
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv` (Coercion -> Coercion) -> CvSubstEnv -> CvSubstEnv
forall a b. (a -> b) -> VarEnv a -> VarEnv b
mapVarEnv (HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo Subst
extended_subst1) CvSubstEnv
cenv2

    -- Make sure the in-scope set in the first substitution is wide enough to
    -- cover the free variables in the range of the second substitution before
    -- applying it (#22235).
    extended_subst1 :: Subst
extended_subst1 = Subst
subst1 Subst -> InScopeSet -> Subst
`setInScope` InScopeSet
is3

emptySubst :: Subst
emptySubst :: Subst
emptySubst = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
emptyInScopeSet IdSubstEnv
forall a. VarEnv a
emptyVarEnv TvSubstEnv
forall a. VarEnv a
emptyVarEnv CvSubstEnv
forall a. VarEnv a
emptyVarEnv

mkEmptySubst :: InScopeSet -> Subst
mkEmptySubst :: InScopeSet -> Subst
mkEmptySubst InScopeSet
in_scope = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
forall a. VarEnv a
emptyVarEnv TvSubstEnv
forall a. VarEnv a
emptyVarEnv CvSubstEnv
forall a. VarEnv a
emptyVarEnv

isEmptySubst :: Subst -> Bool
isEmptySubst :: Subst -> Bool
isEmptySubst (Subst InScopeSet
_ IdSubstEnv
id_env TvSubstEnv
tv_env CvSubstEnv
cv_env)
  = IdSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv IdSubstEnv
id_env Bool -> Bool -> Bool
&& TvSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv TvSubstEnv
tv_env Bool -> Bool -> Bool
&& CvSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv CvSubstEnv
cv_env

-- | Checks whether the tyvar and covar environments are empty.
-- This function should be used over 'isEmptySubst' when substituting
-- for types, because types currently do not contain expressions; we can
-- safely disregard the expression environment when deciding whether
-- to skip a substitution. Using 'isEmptyTCvSubst' gives us a non-trivial
-- performance boost (up to 70% less allocation for T18223)
isEmptyTCvSubst :: Subst -> Bool
isEmptyTCvSubst :: Subst -> Bool
isEmptyTCvSubst (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tv_env CvSubstEnv
cv_env)
  = TvSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv TvSubstEnv
tv_env Bool -> Bool -> Bool
&& CvSubstEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv CvSubstEnv
cv_env

mkSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst
mkSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst
mkSubst InScopeSet
in_scope TvSubstEnv
tvs CvSubstEnv
cvs IdSubstEnv
ids = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs

mkIdSubst :: InScopeSet -> IdSubstEnv -> Subst
mkIdSubst :: InScopeSet -> IdSubstEnv -> Subst
mkIdSubst InScopeSet
in_scope IdSubstEnv
ids = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
emptyTvSubstEnv CvSubstEnv
emptyCvSubstEnv

mkTvSubst :: InScopeSet -> TvSubstEnv -> Subst
-- ^ Make a TCvSubst with specified tyvar subst and empty covar subst
mkTvSubst :: InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
in_scope TvSubstEnv
tenv = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
emptyIdSubstEnv TvSubstEnv
tenv CvSubstEnv
emptyCvSubstEnv

mkCvSubst :: InScopeSet -> CvSubstEnv -> Subst
-- ^ Make a TCvSubst with specified covar subst and empty tyvar subst
mkCvSubst :: InScopeSet -> CvSubstEnv -> Subst
mkCvSubst InScopeSet
in_scope CvSubstEnv
cenv = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
emptyIdSubstEnv TvSubstEnv
emptyTvSubstEnv CvSubstEnv
cenv

getIdSubstEnv :: Subst -> IdSubstEnv
getIdSubstEnv :: Subst -> IdSubstEnv
getIdSubstEnv (Subst InScopeSet
_ IdSubstEnv
ids TvSubstEnv
_ CvSubstEnv
_) = IdSubstEnv
ids

getTvSubstEnv :: Subst -> TvSubstEnv
getTvSubstEnv :: Subst -> TvSubstEnv
getTvSubstEnv (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
_) = TvSubstEnv
tenv

getCvSubstEnv :: Subst -> CvSubstEnv
getCvSubstEnv :: Subst -> CvSubstEnv
getCvSubstEnv (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
cenv) = CvSubstEnv
cenv

-- | Find the in-scope set: see Note [The substitution invariant]
getSubstInScope :: Subst -> InScopeSet
getSubstInScope :: Subst -> InScopeSet
getSubstInScope (Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
_) = InScopeSet
in_scope

setInScope :: Subst -> InScopeSet -> Subst
setInScope :: Subst -> InScopeSet -> Subst
setInScope (Subst InScopeSet
_ IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) InScopeSet
in_scope = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs

-- | Returns the free variables of the types in the range of a substitution as
-- a non-deterministic set.
getSubstRangeTyCoFVs :: Subst -> VarSet
getSubstRangeTyCoFVs :: Subst -> VarSet
getSubstRangeTyCoFVs (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
cenv)
  = VarSet
tenvFVs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
cenvFVs
  where
    tenvFVs :: VarSet
tenvFVs = TvSubstEnv -> VarSet
shallowTyCoVarsOfTyVarEnv TvSubstEnv
tenv
    cenvFVs :: VarSet
cenvFVs = CvSubstEnv -> VarSet
shallowTyCoVarsOfCoVarEnv CvSubstEnv
cenv

isInScope :: Var -> Subst -> Bool
isInScope :: Var -> Subst -> Bool
isInScope Var
v (Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
_) = Var
v Var -> InScopeSet -> Bool
`elemInScopeSet` InScopeSet
in_scope

elemSubst :: Var -> Subst -> Bool
elemSubst :: Var -> Subst -> Bool
elemSubst Var
v (Subst InScopeSet
_ IdSubstEnv
ids TvSubstEnv
tenv CvSubstEnv
cenv)
  | Var -> Bool
isTyVar Var
v
  = Var
v Var -> TvSubstEnv -> Bool
forall a. Var -> VarEnv a -> Bool
`elemVarEnv` TvSubstEnv
tenv
  | Var -> Bool
isCoVar Var
v
  = Var
v Var -> CvSubstEnv -> Bool
forall a. Var -> VarEnv a -> Bool
`elemVarEnv` CvSubstEnv
cenv
  | Bool
otherwise
  = Var
v Var -> IdSubstEnv -> Bool
forall a. Var -> VarEnv a -> Bool
`elemVarEnv` IdSubstEnv
ids

notElemSubst :: Var -> Subst -> Bool
notElemSubst :: Var -> Subst -> Bool
notElemSubst Var
v = Bool -> Bool
not (Bool -> Bool) -> (Subst -> Bool) -> Subst -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Subst -> Bool
elemSubst Var
v

-- | Remove all substitutions that might have been built up
-- while preserving the in-scope set
-- originally called zapSubstEnv
zapSubst :: Subst -> Subst
zapSubst :: Subst -> Subst
zapSubst (Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
_) = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
forall a. VarEnv a
emptyVarEnv TvSubstEnv
forall a. VarEnv a
emptyVarEnv CvSubstEnv
forall a. VarEnv a
emptyVarEnv

-- | Add the 'Var' to the in-scope set
extendSubstInScope :: Subst -> Var -> Subst
extendSubstInScope :: Subst -> Var -> Subst
extendSubstInScope (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) Var
v
  = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
v)
          IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs

-- | Add the 'Var's to the in-scope set: see also 'extendInScope'
extendSubstInScopeList :: Subst -> [Var] -> Subst
extendSubstInScopeList :: Subst -> [Var] -> Subst
extendSubstInScopeList (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) [Var]
vs
  = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> [Var] -> InScopeSet
`extendInScopeSetList` [Var]
vs)
          IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs

-- | Add the 'Var's to the in-scope set: see also 'extendInScope'
extendSubstInScopeSet :: Subst -> VarSet -> Subst
extendSubstInScopeSet :: Subst -> VarSet -> Subst
extendSubstInScopeSet (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) VarSet
vs
  = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> VarSet -> InScopeSet
`extendInScopeSetSet` VarSet
vs)
          IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs

extendTCvSubst :: Subst -> TyCoVar -> Type -> Subst
extendTCvSubst :: Subst -> Var -> Type -> Subst
extendTCvSubst Subst
subst Var
v Type
ty
  | Var -> Bool
isTyVar Var
v
  = Subst -> Var -> Type -> Subst
extendTvSubst Subst
subst Var
v Type
ty
  | CoercionTy Coercion
co <- Type
ty
  = Subst -> Var -> Coercion -> Subst
extendCvSubst Subst
subst Var
v Coercion
co
  | Bool
otherwise
  = String -> SDoc -> Subst
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendTCvSubst" (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"|->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)

extendTCvSubstWithClone :: Subst -> TyCoVar -> TyCoVar -> Subst
extendTCvSubstWithClone :: Subst -> Var -> Var -> Subst
extendTCvSubstWithClone Subst
subst Var
tcv
  | Var -> Bool
isTyVar Var
tcv = Subst -> Var -> Var -> Subst
extendTvSubstWithClone Subst
subst Var
tcv
  | Bool
otherwise   = Subst -> Var -> Var -> Subst
extendCvSubstWithClone Subst
subst Var
tcv

-- | 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
-- Note [The substitution invariant] holds
-- after extending the substitution like this.
extendTvSubst :: Subst -> TyVar -> Type -> Subst
extendTvSubst :: Subst -> Var -> Type -> Subst
extendTvSubst (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) Var
tv Type
ty
  = Bool -> Subst -> Subst
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
tv) (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$
    InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
ids (TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tvs Var
tv Type
ty) CvSubstEnv
cvs

extendTvSubstBinderAndInScope :: Subst -> PiTyBinder -> Type -> Subst
extendTvSubstBinderAndInScope :: Subst -> PiTyBinder -> Type -> Subst
extendTvSubstBinderAndInScope Subst
subst (Named (Bndr Var
v ForAllTyFlag
_)) Type
ty
  = Bool
-> (Subst -> Var -> Type -> Subst) -> Subst -> Var -> Type -> Subst
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
v )
    Subst -> Var -> Type -> Subst
extendTvSubstAndInScope Subst
subst Var
v Type
ty
extendTvSubstBinderAndInScope Subst
subst (Anon {}) Type
_
  = Subst
subst

extendTvSubstWithClone :: Subst -> TyVar -> TyVar -> Subst
-- Adds a new tv -> tv mapping, /and/ extends the in-scope set with the clone
-- Does not look in the kind of the new variable;
--   those variables should be in scope already
extendTvSubstWithClone :: Subst -> Var -> Var -> Subst
extendTvSubstWithClone (Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv) Var
tv Var
tv'
  = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet -> Var -> InScopeSet
extendInScopeSet InScopeSet
in_scope Var
tv')
          IdSubstEnv
idenv
          (TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tenv Var
tv (Var -> Type
mkTyVarTy Var
tv'))
          CvSubstEnv
cenv

-- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst':
-- you must ensure that the in-scope set satisfies
-- Note [The substitution invariant]
-- after extending the substitution like this
extendCvSubst :: Subst -> CoVar -> Coercion -> Subst
extendCvSubst :: Subst -> Var -> Coercion -> Subst
extendCvSubst (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs) Var
v Coercion
r
  = Bool -> Subst -> Subst
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isCoVar Var
v) (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$
    InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs (CvSubstEnv -> Var -> Coercion -> CvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv CvSubstEnv
cvs Var
v Coercion
r)

extendCvSubstWithClone :: Subst -> CoVar -> CoVar -> Subst
extendCvSubstWithClone :: Subst -> Var -> Var -> Subst
extendCvSubstWithClone (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tenv CvSubstEnv
cenv) Var
cv Var
cv'
  = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet -> VarSet -> InScopeSet
extendInScopeSetSet InScopeSet
in_scope VarSet
new_in_scope)
             IdSubstEnv
ids
             TvSubstEnv
tenv
             (CvSubstEnv -> Var -> Coercion -> CvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv CvSubstEnv
cenv Var
cv (Var -> Coercion
mkCoVarCo Var
cv'))
  where
    new_in_scope :: VarSet
new_in_scope = Type -> VarSet
tyCoVarsOfType (Var -> Type
varType Var
cv') VarSet -> Var -> VarSet
`extendVarSet` Var
cv'

extendTvSubstAndInScope :: Subst -> TyVar -> Type -> Subst
-- Also extends the in-scope set
extendTvSubstAndInScope :: Subst -> Var -> Type -> Subst
extendTvSubstAndInScope (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tenv CvSubstEnv
cenv) Var
tv Type
ty
  = InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> VarSet -> InScopeSet
`extendInScopeSetSet` Type -> VarSet
tyCoVarsOfType Type
ty)
             IdSubstEnv
ids
             (TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tenv Var
tv Type
ty)
             CvSubstEnv
cenv

-- | Adds multiple 'TyVar' substitutions to the 'Subst': see also 'extendTvSubst'
extendTvSubstList :: Subst -> [(TyVar,Type)] -> Subst
extendTvSubstList :: Subst -> [(Var, Type)] -> Subst
extendTvSubstList Subst
subst [(Var, Type)]
vrs
  = (Subst -> (Var, Type) -> Subst) -> Subst -> [(Var, Type)] -> Subst
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Subst -> (Var, Type) -> Subst
extend Subst
subst [(Var, Type)]
vrs
  where
    extend :: Subst -> (Var, Type) -> Subst
extend Subst
subst (Var
v, Type
r) = Subst -> Var -> Type -> Subst
extendTvSubst Subst
subst Var
v Type
r

extendTCvSubstList :: Subst -> [Var] -> [Type] -> Subst
extendTCvSubstList :: Subst -> [Var] -> [Type] -> Subst
extendTCvSubstList Subst
subst [Var]
tvs [Type]
tys
  = (Subst -> Var -> Type -> Subst)
-> Subst -> [Var] -> [Type] -> Subst
forall acc a b. (acc -> a -> b -> acc) -> acc -> [a] -> [b] -> acc
foldl2 Subst -> Var -> Type -> Subst
extendTCvSubst Subst
subst [Var]
tvs [Type]
tys

unionSubst :: Subst -> Subst -> Subst
-- Works when the ranges are disjoint
unionSubst :: Subst -> Subst -> Subst
unionSubst (Subst InScopeSet
in_scope1 IdSubstEnv
ids1 TvSubstEnv
tenv1 CvSubstEnv
cenv1) (Subst InScopeSet
in_scope2 IdSubstEnv
ids2 TvSubstEnv
tenv2 CvSubstEnv
cenv2)
  = Bool
-> (InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst)
-> InScopeSet
-> IdSubstEnv
-> TvSubstEnv
-> CvSubstEnv
-> Subst
forall a. HasCallStack => Bool -> a -> a
assert (IdSubstEnv
ids1  IdSubstEnv -> IdSubstEnv -> Bool
forall a. VarEnv a -> VarEnv a -> Bool
`disjointVarEnv` IdSubstEnv
ids2
         Bool -> Bool -> Bool
&& TvSubstEnv
tenv1 TvSubstEnv -> TvSubstEnv -> Bool
forall a. VarEnv a -> VarEnv a -> Bool
`disjointVarEnv` TvSubstEnv
tenv2
         Bool -> Bool -> Bool
&& CvSubstEnv
cenv1 CvSubstEnv -> CvSubstEnv -> Bool
forall a. VarEnv a -> VarEnv a -> Bool
`disjointVarEnv` CvSubstEnv
cenv2 )
    InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope1 InScopeSet -> InScopeSet -> InScopeSet
`unionInScope` InScopeSet
in_scope2)
           (IdSubstEnv
ids1      IdSubstEnv -> IdSubstEnv -> IdSubstEnv
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv`   IdSubstEnv
ids2)
           (TvSubstEnv
tenv1     TvSubstEnv -> TvSubstEnv -> TvSubstEnv
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv`   TvSubstEnv
tenv2)
           (CvSubstEnv
cenv1     CvSubstEnv -> CvSubstEnv -> CvSubstEnv
forall a. VarEnv a -> VarEnv a -> VarEnv a
`plusVarEnv`   CvSubstEnv
cenv2)

-- | Generates the in-scope set for the 'Subst' from the types in the incoming
-- environment. No CoVars or Ids, please!
zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> Subst
zipTvSubst :: HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys
  = InScopeSet -> TvSubstEnv -> Subst
mkTvSubst (VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
shallowTyCoVarsOfTypes [Type]
tys)) TvSubstEnv
tenv
  where
    tenv :: TvSubstEnv
tenv = [Var] -> [Type] -> TvSubstEnv
HasDebugCallStack => [Var] -> [Type] -> TvSubstEnv
zipTyEnv [Var]
tvs [Type]
tys

-- | Generates the in-scope set for the 'Subst' from the types in the incoming
-- environment.  No TyVars, please!
zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> Subst
zipCvSubst :: HasDebugCallStack => [Var] -> [Coercion] -> Subst
zipCvSubst [Var]
cvs [Coercion]
cos
  = InScopeSet -> CvSubstEnv -> Subst
mkCvSubst (VarSet -> InScopeSet
mkInScopeSet ([Coercion] -> VarSet
shallowTyCoVarsOfCos [Coercion]
cos)) CvSubstEnv
cenv
  where
    cenv :: CvSubstEnv
cenv = [Var] -> [Coercion] -> CvSubstEnv
HasDebugCallStack => [Var] -> [Coercion] -> CvSubstEnv
zipCoEnv [Var]
cvs [Coercion]
cos


zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> Subst
zipTCvSubst :: HasDebugCallStack => [Var] -> [Type] -> Subst
zipTCvSubst [Var]
tcvs [Type]
tys
  = [Var] -> [Type] -> Subst -> Subst
zip_tcvsubst [Var]
tcvs [Type]
tys (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$
    InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
shallowTyCoVarsOfTypes [Type]
tys
  where zip_tcvsubst :: [TyCoVar] -> [Type] -> Subst -> Subst
        zip_tcvsubst :: [Var] -> [Type] -> Subst -> Subst
zip_tcvsubst (Var
tv:[Var]
tvs) (Type
ty:[Type]
tys) Subst
subst
          = [Var] -> [Type] -> Subst -> Subst
zip_tcvsubst [Var]
tvs [Type]
tys (Subst -> Var -> Type -> Subst
extendTCvSubst Subst
subst Var
tv Type
ty)
        zip_tcvsubst [] [] Subst
subst = Subst
subst -- empty case
        zip_tcvsubst [Var]
_  [Type]
_  Subst
_     = String -> SDoc -> Subst
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"zipTCvSubst: length mismatch"
                                   ([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
tcvs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)

-- | Generates the in-scope set for the 'TCvSubst' from the types in the
-- incoming environment. No CoVars, please! The InScopeSet is just a thunk
--  so with a bit of luck it'll never be evaluated
mkTvSubstPrs :: [(TyVar, Type)] -> Subst
mkTvSubstPrs :: [(Var, Type)] -> Subst
mkTvSubstPrs []  = Subst
emptySubst
mkTvSubstPrs [(Var, Type)]
prs =
    Bool -> SDoc -> Subst -> Subst
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr Bool
onlyTyVarsAndNoCoercionTy (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"prs" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(Var, Type)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Var, Type)]
prs) (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$
    InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
in_scope TvSubstEnv
tenv
  where tenv :: TvSubstEnv
tenv = [(Var, Type)] -> TvSubstEnv
forall a. [(Var, a)] -> VarEnv a
mkVarEnv [(Var, Type)]
prs
        in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
shallowTyCoVarsOfTypes ([Type] -> VarSet) -> [Type] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Var, Type) -> Type) -> [(Var, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Type) -> Type
forall a b. (a, b) -> b
snd [(Var, Type)]
prs
        onlyTyVarsAndNoCoercionTy :: Bool
onlyTyVarsAndNoCoercionTy =
          [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ Var -> Bool
isTyVar Var
tv Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isCoercionTy Type
ty)
              | (Var
tv, Type
ty) <- [(Var, Type)]
prs ]

-- | The InScopeSet is just a thunk so with a bit of luck it'll never be evaluated
zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
zipTyEnv :: HasDebugCallStack => [Var] -> [Type] -> TvSubstEnv
zipTyEnv [Var]
tyvars [Type]
tys
  | Bool
debugIsOn
  , Bool -> Bool
not ((Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Var -> Bool
isTyVar [Var]
tyvars Bool -> Bool -> Bool
&& ([Var]
tyvars [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys))
  = String -> SDoc -> TvSubstEnv
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"zipTyEnv" ([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
tyvars SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
  | Bool
otherwise
  = Bool
-> ([Var] -> [Type] -> TvSubstEnv) -> [Var] -> [Type] -> TvSubstEnv
forall a. HasCallStack => Bool -> a -> a
assert ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
isCoercionTy) [Type]
tys )
    [Var] -> [Type] -> TvSubstEnv
forall key elt. Uniquable key => [key] -> [elt] -> UniqFM key elt
zipToUFM [Var]
tyvars [Type]
tys
        -- There used to be a special case for when
        --      ty == TyVarTy tv
        -- (a not-uncommon case) in which case the substitution was dropped.
        -- But the type-tidier changes the print-name of a type variable without
        -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
        -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
        -- And it happened that t was the type variable of the class.  Post-tiding,
        -- it got turned into {Foo t2}.  The ext-core printer expanded this using
        -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
        -- and so generated a rep type mentioning t not t2.
        --
        -- Simplest fix is to nuke the "optimisation"

zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv
zipCoEnv :: HasDebugCallStack => [Var] -> [Coercion] -> CvSubstEnv
zipCoEnv [Var]
cvs [Coercion]
cos
  | Bool
debugIsOn
  , Bool -> Bool
not ((Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Var -> Bool
isCoVar [Var]
cvs)
  = String -> SDoc -> CvSubstEnv
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"zipCoEnv" ([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
cvs SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
cos)
  | Bool
otherwise
  = [(Var, Coercion)] -> CvSubstEnv
forall a. [(Var, a)] -> VarEnv a
mkVarEnv (String -> [Var] -> [Coercion] -> [(Var, Coercion)]
forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
zipEqual String
"zipCoEnv" [Var]
cvs [Coercion]
cos)

-- Pretty printing, for debugging only

instance Outputable Subst where
  ppr :: Subst -> SDoc
ppr (Subst InScopeSet
in_scope IdSubstEnv
ids TvSubstEnv
tvs CvSubstEnv
cvs)
        =  String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"<InScope =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
in_scope_doc
        SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" IdSubst   =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> IdSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr IdSubstEnv
ids
        SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" TvSubst   =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr TvSubstEnv
tvs
        SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
" CvSubst   =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr CvSubstEnv
cvs
         SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'>'
    where
    in_scope_doc :: SDoc
in_scope_doc = VarSet -> ([Var] -> SDoc) -> SDoc
pprVarSet (InScopeSet -> VarSet
getInScopeVars InScopeSet
in_scope) (SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (SDoc -> SDoc) -> ([Var] -> SDoc) -> [Var] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep ([SDoc] -> SDoc) -> ([Var] -> [SDoc]) -> [Var] -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> SDoc) -> [Var] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr)

{-
%************************************************************************
%*                                                                      *
                Performing type or kind substitutions
%*                                                                      *
%************************************************************************

Note [Sym and ForAllCo]
~~~~~~~~~~~~~~~~~~~~~~~
In OptCoercion, we try to push "sym" out to the leaves of a coercion. But,
how do we push sym into a ForAllCo? It's a little ugly.

Here is the typing rule:

h : k1 ~# k2
(tv : k1) |- g : ty1 ~# ty2
----------------------------
ForAllCo tv h g : (ForAllTy (tv : k1) ty1) ~#
                  (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h]))

Here is what we want:

ForAllCo tv h' g' : (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h])) ~#
                    (ForAllTy (tv : k1) ty1)


Because the kinds of the type variables to the right of the colon are the kinds
coerced by h', we know (h' : k2 ~# k1). Thus, (h' = sym h).

Now, we can rewrite ty1 to be (ty1[tv |-> tv |> sym h' |> h']). We thus want

ForAllCo tv h' g' :
  (ForAllTy (tv : k2) (ty2[tv |-> tv |> h'])) ~#
  (ForAllTy (tv : k1) (ty1[tv |-> tv |> h'][tv |-> tv |> sym h']))

We thus see that we want

g' : ty2[tv |-> tv |> h'] ~# ty1[tv |-> tv |> h']

and thus g' = sym (g[tv |-> tv |> h']).

Putting it all together, we get this:

sym (ForAllCo tv h g)
==>
ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h])

Note [Substituting in a coercion hole]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It seems highly suspicious to be substituting in a coercion that still
has coercion holes. Yet, this can happen in a situation like this:

  f :: forall k. k :~: Type -> ()
  f Refl = let x :: forall (a :: k). [a] -> ...
               x = ...

When we check x's type signature, we require that k ~ Type. We indeed
know this due to the Refl pattern match, but the eager unifier can't
make use of givens. So, when we're done looking at x's type, a coercion
hole will remain. Then, when we're checking x's definition, we skolemise
x's type (in order to, e.g., bring the scoped type variable `a` into scope).
This requires performing a substitution for the fresh skolem variables.

This substitution needs to affect the kind of the coercion hole, too --
otherwise, the kind will have an out-of-scope variable in it. More problematically
in practice (we won't actually notice the out-of-scope variable ever), skolems
in the kind might have too high a level, triggering a failure to uphold the
invariant that no free variables in a type have a higher level than the
ambient level in the type checker. In the event of having free variables in the
hole's kind, I'm pretty sure we'll always have an erroneous program, so we
don't need to worry what will happen when the hole gets filled in. After all,
a hole relating a locally-bound type variable will be unable to be solved. This
is why it's OK not to look through the IORef of a coercion hole during
substitution.

-}

-- | Type substitution, see 'zipTvSubst'
substTyWith :: HasDebugCallStack => [TyVar] -> [Type] -> Type -> Type
-- Works only if the domain of the substitution is a
-- superset of the type being substituted into
substTyWith :: HasDebugCallStack => [Var] -> [Type] -> Type -> Type
substTyWith [Var]
tvs [Type]
tys = {-#SCC "substTyWith" #-}
                      Bool -> (Subst -> Type -> Type) -> Subst -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
                      HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)

-- | Type substitution, see 'zipTvSubst'. Disables sanity checks.
-- The problems that the sanity checks in substTy catch are described in
-- Note [The substitution invariant].
-- 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.
substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
substTyWithUnchecked :: [Var] -> [Type] -> Type -> Type
substTyWithUnchecked [Var]
tvs [Type]
tys
  = Bool -> (Subst -> Type -> Type) -> Subst -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
    Subst -> Type -> Type
substTyUnchecked ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)

-- | Substitute tyvars within a type using a known 'InScopeSet'.
-- Pre-condition: the 'in_scope' set should satisfy Note [The substitution
-- invariant]; specifically it should include the free vars of 'tys',
-- and of 'ty' minus the domain of the subst.
substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
substTyWithInScope :: InScopeSet -> [Var] -> [Type] -> Type -> Type
substTyWithInScope InScopeSet
in_scope [Var]
tvs [Type]
tys Type
ty =
  Bool -> (Subst -> Type -> Type) -> Subst -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
  HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
in_scope TvSubstEnv
tenv) Type
ty
  where tenv :: TvSubstEnv
tenv = [Var] -> [Type] -> TvSubstEnv
HasDebugCallStack => [Var] -> [Type] -> TvSubstEnv
zipTyEnv [Var]
tvs [Type]
tys

-- | Coercion substitution, see 'zipTvSubst'
substCoWith :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
substCoWith :: HasDebugCallStack => [Var] -> [Type] -> Coercion -> Coercion
substCoWith [Var]
tvs [Type]
tys = Bool
-> (Subst -> Coercion -> Coercion) -> Subst -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
                      HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)

-- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks.
-- The problems that the sanity checks in substCo catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substCoUnchecked to
-- substCo and remove this function. Please don't use in new code.
substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked :: [Var] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked [Var]
tvs [Type]
tys
  = Bool
-> (Subst -> Coercion -> Coercion) -> Subst -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
    Subst -> Coercion -> Coercion
substCoUnchecked ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)



-- | Substitute covars within a type
substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars :: [Var] -> [Coercion] -> Type -> Type
substTyWithCoVars [Var]
cvs [Coercion]
cos = HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy ([Var] -> [Coercion] -> Subst
HasDebugCallStack => [Var] -> [Coercion] -> Subst
zipCvSubst [Var]
cvs [Coercion]
cos)

-- | Type substitution, see 'zipTvSubst'
substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
substTysWith :: [Var] -> [Type] -> [Type] -> [Type]
substTysWith [Var]
tvs [Type]
tys = Bool -> (Subst -> [Type] -> [Type]) -> Subst -> [Type] -> [Type]
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
tvs [Var] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys )
                       HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var]
tvs [Type]
tys)

-- | Type substitution, see 'zipTvSubst'
substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars :: [Var] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars [Var]
cvs [Coercion]
cos = Bool -> (Subst -> [Type] -> [Type]) -> Subst -> [Type] -> [Type]
forall a. HasCallStack => Bool -> a -> a
assert ([Var]
cvs [Var] -> [Coercion] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Coercion]
cos )
                             HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys ([Var] -> [Coercion] -> Subst
HasDebugCallStack => [Var] -> [Coercion] -> Subst
zipCvSubst [Var]
cvs [Coercion]
cos)

-- | 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 [The substitution invariant].
substTyAddInScope :: Subst -> Type -> Type
substTyAddInScope :: Subst -> Type -> Type
substTyAddInScope Subst
subst Type
ty =
  HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy (Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (VarSet -> Subst) -> VarSet -> Subst
forall a b. (a -> b) -> a -> b
$ Type -> VarSet
tyCoVarsOfType Type
ty) Type
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 [The substitution invariant].
-- TODO: take into account ids and rename as isValidSubst
isValidTCvSubst :: Subst -> Bool
isValidTCvSubst :: Subst -> Bool
isValidTCvSubst (Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
cenv) =
  (VarSet
tenvFVs VarSet -> InScopeSet -> Bool
`varSetInScope` InScopeSet
in_scope) Bool -> Bool -> Bool
&&
  (VarSet
cenvFVs VarSet -> InScopeSet -> Bool
`varSetInScope` InScopeSet
in_scope)
  where
  tenvFVs :: VarSet
tenvFVs = TvSubstEnv -> VarSet
shallowTyCoVarsOfTyVarEnv TvSubstEnv
tenv
  cenvFVs :: VarSet
cenvFVs = CvSubstEnv -> VarSet
shallowTyCoVarsOfCoVarEnv CvSubstEnv
cenv

-- | This checks if the substitution satisfies the invariant from
-- Note [The substitution invariant].
checkValidSubst :: HasDebugCallStack => Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst :: forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst subst :: Subst
subst@(Subst InScopeSet
in_scope IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
cenv) [Type]
tys [Coercion]
cos a
a
  = Bool -> SDoc -> a -> a
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Subst -> Bool
isValidTCvSubst Subst
subst)
              (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in_scope" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InScopeSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr InScopeSet
in_scope SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tenv" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr TvSubstEnv
tenv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tenvFVs" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TvSubstEnv -> VarSet
shallowTyCoVarsOfTyVarEnv TvSubstEnv
tenv) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cenv" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr CvSubstEnv
cenv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cenvFVs" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CvSubstEnv -> VarSet
shallowTyCoVarsOfCoVarEnv CvSubstEnv
cenv) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tys" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cos" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
cos) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$
    Bool -> SDoc -> a -> a
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr Bool
tysCosFVsInScope
              (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"in_scope" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InScopeSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr InScopeSet
in_scope SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tenv" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr TvSubstEnv
tenv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cenv" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CvSubstEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr CvSubstEnv
cenv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tys" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cos" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Coercion] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Coercion]
cos SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$
               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"needInScope" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> VarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr VarSet
needInScope)
    a
a
  where
  substDomain :: [Unique]
substDomain = TvSubstEnv -> [Unique]
forall key elt. UniqFM key elt -> [Unique]
nonDetKeysUFM TvSubstEnv
tenv [Unique] -> [Unique] -> [Unique]
forall a. [a] -> [a] -> [a]
++ CvSubstEnv -> [Unique]
forall key elt. UniqFM key elt -> [Unique]
nonDetKeysUFM CvSubstEnv
cenv
    -- It's OK to use nonDetKeysUFM here, because we only use this list to
    -- remove some elements from a set
  needInScope :: VarSet
needInScope = ([Type] -> VarSet
shallowTyCoVarsOfTypes [Type]
tys VarSet -> VarSet -> VarSet
`unionVarSet`
                 [Coercion] -> VarSet
shallowTyCoVarsOfCos [Coercion]
cos)
                VarSet -> [Unique] -> VarSet
forall a. UniqSet a -> [Unique] -> UniqSet a
`delListFromUniqSet_Directly` [Unique]
substDomain
  tysCosFVsInScope :: Bool
tysCosFVsInScope = VarSet
needInScope VarSet -> InScopeSet -> Bool
`varSetInScope` InScopeSet
in_scope


-- | Substitute within a 'Type'
-- The substitution has to satisfy the invariants described in
-- Note [The substitution invariant].
substTy :: HasDebugCallStack => Subst -> Type  -> Type
substTy :: HasDebugCallStack => Subst -> Type -> Type
substTy Subst
subst Type
ty
  | Subst -> Bool
isEmptyTCvSubst    Subst
subst = Type
ty
  | Bool
otherwise             = Subst -> [Type] -> [Coercion] -> Type -> Type
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
subst [Type
ty] [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                            Subst -> Type -> Type
subst_ty Subst
subst Type
ty

-- | Substitute within a 'Type' disabling the sanity checks.
-- The problems that the sanity checks in substTy catch are described in
-- Note [The substitution invariant].
-- 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 :: Subst -> Type -> Type
substTyUnchecked :: Subst -> Type -> Type
substTyUnchecked Subst
subst Type
ty
                 | Subst -> Bool
isEmptyTCvSubst Subst
subst    = Type
ty
                 | Bool
otherwise             = Subst -> Type -> Type
subst_ty Subst
subst Type
ty

substScaledTy :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substScaledTy :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substScaledTy Subst
subst Scaled Type
scaled_ty = (Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) Scaled Type
scaled_ty

substScaledTyUnchecked :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substScaledTyUnchecked :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substScaledTyUnchecked Subst
subst Scaled Type
scaled_ty = (Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType (Subst -> Type -> Type
substTyUnchecked Subst
subst) Scaled Type
scaled_ty

-- | Substitute within several 'Type's
-- The substitution has to satisfy the invariants described in
-- Note [The substitution invariant].
substTys :: HasDebugCallStack => Subst -> [Type] -> [Type]
substTys :: HasDebugCallStack => Subst -> [Type] -> [Type]
substTys Subst
subst [Type]
tys
  | Subst -> Bool
isEmptyTCvSubst Subst
subst = [Type]
tys
  | Bool
otherwise = Subst -> [Type] -> [Coercion] -> [Type] -> [Type]
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
subst [Type]
tys [] ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
subst_ty Subst
subst) [Type]
tys

substScaledTys :: HasDebugCallStack => Subst -> [Scaled Type] -> [Scaled Type]
substScaledTys :: HasDebugCallStack => Subst -> [Scaled Type] -> [Scaled Type]
substScaledTys Subst
subst [Scaled Type]
scaled_tys
  | Subst -> Bool
isEmptyTCvSubst Subst
subst = [Scaled Type]
scaled_tys
  | Bool
otherwise = Subst -> [Type] -> [Coercion] -> [Scaled Type] -> [Scaled Type]
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
subst ((Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> Type
scaledMult [Scaled Type]
scaled_tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
scaled_tys) [] ([Scaled Type] -> [Scaled Type]) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> a -> b
$
                (Scaled Type -> Scaled Type) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType (Subst -> Type -> Type
subst_ty Subst
subst)) [Scaled Type]
scaled_tys

-- | Substitute within several 'Type's disabling the sanity checks.
-- The problems that the sanity checks in substTys catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substTysUnchecked to
-- substTys and remove this function. Please don't use in new code.
substTysUnchecked :: Subst -> [Type] -> [Type]
substTysUnchecked :: Subst -> [Type] -> [Type]
substTysUnchecked Subst
subst [Type]
tys
                 | Subst -> Bool
isEmptyTCvSubst Subst
subst = [Type]
tys
                 | Bool
otherwise             = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
subst_ty Subst
subst) [Type]
tys

substScaledTysUnchecked :: Subst -> [Scaled Type] -> [Scaled Type]
substScaledTysUnchecked :: Subst -> [Scaled Type] -> [Scaled Type]
substScaledTysUnchecked Subst
subst [Scaled Type]
tys
                 | Subst -> Bool
isEmptyTCvSubst Subst
subst = [Scaled Type]
tys
                 | Bool
otherwise             = (Scaled Type -> Scaled Type) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType (Subst -> Type -> Type
subst_ty Subst
subst)) [Scaled Type]
tys

-- | Substitute within a 'ThetaType'
-- The substitution has to satisfy the invariants described in
-- Note [The substitution invariant].
substTheta :: HasDebugCallStack => Subst -> ThetaType -> ThetaType
substTheta :: HasDebugCallStack => Subst -> [Type] -> [Type]
substTheta = HasDebugCallStack => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys

-- | Substitute within a 'ThetaType' disabling the sanity checks.
-- The problems that the sanity checks in substTys catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substThetaUnchecked to
-- substTheta and remove this function. Please don't use in new code.
substThetaUnchecked :: Subst -> ThetaType -> ThetaType
substThetaUnchecked :: Subst -> [Type] -> [Type]
substThetaUnchecked = Subst -> [Type] -> [Type]
substTysUnchecked


subst_ty :: Subst -> Type -> Type
-- subst_ty is the main workhorse for type substitution
--
-- Note that the in_scope set is poked only if we hit a forall
-- so it may often never be fully computed
subst_ty :: Subst -> Type -> Type
subst_ty Subst
subst Type
ty
   = Type -> Type
go Type
ty
  where
    go :: Type -> Type
go (TyVarTy Var
tv)      = Subst -> Var -> Type
substTyVar Subst
subst Var
tv
    go (AppTy Type
fun Type
arg)   = (Type -> Type -> Type
mkAppTy (Type -> Type -> Type) -> Type -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go Type
fun)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go Type
arg)
                -- The mkAppTy smart constructor is important
                -- we might be replacing (a Int), represented with App
                -- by [Int], represented with TyConApp
    go ty :: Type
ty@(TyConApp TyCon
tc []) = TyCon
tc TyCon -> Type -> Type
forall a b. a -> b -> b
`seq` Type
ty  -- avoid allocation in this common case
    go (TyConApp TyCon
tc [Type]
tys) = (TyCon -> [Type] -> Type
mkTyConApp (TyCon -> [Type] -> Type) -> TyCon -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$! TyCon
tc) ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$! (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
strictMap Type -> Type
go [Type]
tys
                               -- NB: mkTyConApp, not TyConApp.
                               -- mkTyConApp has optimizations.
                               -- See Note [Using synonyms to compress types]
                               -- in GHC.Core.Type
    go ty :: Type
ty@(FunTy { ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res })
      = let !mult' :: Type
mult' = Type -> Type
go Type
mult
            !arg' :: Type
arg' = Type -> Type
go Type
arg
            !res' :: Type
res' = Type -> Type
go Type
res
        in Type
ty { ft_mult = mult', ft_arg = arg', ft_res = res' }
    go (ForAllTy (Bndr Var
tv ForAllTyFlag
vis) Type
ty)
                         = case Subst -> Var -> (Subst, Var)
substVarBndrUnchecked Subst
subst Var
tv of
                             (Subst
subst', Var
tv') ->
                               (VarBndr Var ForAllTyFlag -> Type -> Type
ForAllTy (VarBndr Var ForAllTyFlag -> Type -> Type)
-> VarBndr Var ForAllTyFlag -> Type -> Type
forall a b. (a -> b) -> a -> b
$! ((Var -> ForAllTyFlag -> VarBndr Var ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr (Var -> ForAllTyFlag -> VarBndr Var ForAllTyFlag)
-> Var -> ForAllTyFlag -> VarBndr Var ForAllTyFlag
forall a b. (a -> b) -> a -> b
$! Var
tv') ForAllTyFlag
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$!
                                            (Subst -> Type -> Type
subst_ty Subst
subst' Type
ty)
    go (LitTy TyLit
n)         = TyLit -> Type
LitTy (TyLit -> Type) -> TyLit -> Type
forall a b. (a -> b) -> a -> b
$! TyLit
n
    go (CastTy Type
ty Coercion
co)    = (Type -> Coercion -> Type
mkCastTy (Type -> Coercion -> Type) -> Type -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go Type
ty)) (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! (Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co)
    go (CoercionTy Coercion
co)   = Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$! (Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co)

substTyVar :: Subst -> TyVar -> Type
substTyVar :: Subst -> Var -> Type
substTyVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
_) Var
tv
  = Bool -> Type -> Type
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
tv) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    case TvSubstEnv -> Var -> Maybe Type
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv TvSubstEnv
tenv Var
tv of
      Just Type
ty -> Type
ty
      Maybe Type
Nothing -> Var -> Type
TyVarTy Var
tv

substTyVarToTyVar :: HasDebugCallStack => Subst -> TyVar -> TyVar
-- Apply the substitution, expecing the result to be a TyVarTy
substTyVarToTyVar :: HasDebugCallStack => Subst -> Var -> Var
substTyVarToTyVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
_) Var
tv
  = Bool -> Var -> Var
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
tv) (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
    case TvSubstEnv -> Var -> Maybe Type
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv TvSubstEnv
tenv Var
tv of
      Just Type
ty -> case Type -> Maybe Var
getTyVar_maybe Type
ty of
                    Just Var
tv -> Var
tv
                    Maybe Var
Nothing -> String -> SDoc -> Var
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"substTyVarToTyVar" (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
      Maybe Type
Nothing -> Var
tv

substTyVars :: Subst -> [TyVar] -> [Type]
substTyVars :: Subst -> [Var] -> [Type]
substTyVars Subst
subst = (Var -> Type) -> [Var] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Var -> Type) -> [Var] -> [Type])
-> (Var -> Type) -> [Var] -> [Type]
forall a b. (a -> b) -> a -> b
$ Subst -> Var -> Type
substTyVar Subst
subst

substTyCoVars :: Subst -> [TyCoVar] -> [Type]
substTyCoVars :: Subst -> [Var] -> [Type]
substTyCoVars Subst
subst = (Var -> Type) -> [Var] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Var -> Type) -> [Var] -> [Type])
-> (Var -> Type) -> [Var] -> [Type]
forall a b. (a -> b) -> a -> b
$ Subst -> Var -> Type
substTyCoVar Subst
subst

substTyCoVar :: Subst -> TyCoVar -> Type
substTyCoVar :: Subst -> Var -> Type
substTyCoVar Subst
subst Var
tv
  | Var -> Bool
isTyVar Var
tv = Subst -> Var -> Type
substTyVar Subst
subst Var
tv
  | Bool
otherwise = Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$ Subst -> Var -> Coercion
substCoVar Subst
subst Var
tv

lookupTyVar :: Subst -> TyVar  -> Maybe Type
        -- See Note [Extending the TvSubstEnv and CvSubstEnv]
lookupTyVar :: Subst -> Var -> Maybe Type
lookupTyVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
tenv CvSubstEnv
_) Var
tv
  = Bool
-> (TvSubstEnv -> Var -> Maybe Type)
-> TvSubstEnv
-> Var
-> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
tv )
    TvSubstEnv -> Var -> Maybe Type
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv TvSubstEnv
tenv Var
tv

-- | Substitute within a 'Coercion'
-- The substitution has to satisfy the invariants described in
-- Note [The substitution invariant].
substCo :: HasDebugCallStack => Subst -> Coercion -> Coercion
substCo :: HasDebugCallStack => Subst -> Coercion -> Coercion
substCo Subst
subst Coercion
co
  | Subst -> Bool
isEmptyTCvSubst Subst
subst = Coercion
co
  | Bool
otherwise = Subst -> [Type] -> [Coercion] -> Coercion -> Coercion
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
subst [] [Coercion
co] (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co

-- | Substitute within a 'Coercion' disabling sanity checks.
-- The problems that the sanity checks in substCo catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substCoUnchecked to
-- substCo and remove this function. Please don't use in new code.
substCoUnchecked :: Subst -> Coercion -> Coercion
substCoUnchecked :: Subst -> Coercion -> Coercion
substCoUnchecked Subst
subst Coercion
co
  | Subst -> Bool
isEmptyTCvSubst Subst
subst = Coercion
co
  | Bool
otherwise = Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co

-- | Substitute within several 'Coercion's
-- The substitution has to satisfy the invariants described in
-- Note [The substitution invariant].
substCos :: HasDebugCallStack => Subst -> [Coercion] -> [Coercion]
substCos :: HasDebugCallStack => Subst -> [Coercion] -> [Coercion]
substCos Subst
subst [Coercion]
cos
  | Subst -> Bool
isEmptyTCvSubst Subst
subst = [Coercion]
cos
  | Bool
otherwise = Subst -> [Type] -> [Coercion] -> [Coercion] -> [Coercion]
forall a.
HasDebugCallStack =>
Subst -> [Type] -> [Coercion] -> a -> a
checkValidSubst Subst
subst [] [Coercion]
cos ([Coercion] -> [Coercion]) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> a -> b
$ (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Coercion -> Coercion
subst_co Subst
subst) [Coercion]
cos

subst_co :: Subst -> Coercion -> Coercion
subst_co :: Subst -> Coercion -> Coercion
subst_co Subst
subst Coercion
co
  = Coercion -> Coercion
go Coercion
co
  where
    go_ty :: Type -> Type
    go_ty :: Type -> Type
go_ty = Subst -> Type -> Type
subst_ty Subst
subst

    go_mco :: MCoercion -> MCoercion
    go_mco :: MCoercion -> MCoercion
go_mco MCoercion
MRefl    = MCoercion
MRefl
    go_mco (MCo Coercion
co) = Coercion -> MCoercion
MCo (Coercion -> Coercion
go Coercion
co)

    go :: Coercion -> Coercion
    go :: Coercion -> Coercion
go (Refl Type
ty)             = Type -> Coercion
mkNomReflCo (Type -> Coercion) -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go_ty Type
ty)
    go (GRefl Role
r Type
ty MCoercion
mco)      = (Role -> Type -> MCoercion -> Coercion
mkGReflCo Role
r (Type -> MCoercion -> Coercion) -> Type -> MCoercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go_ty Type
ty)) (MCoercion -> Coercion) -> MCoercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (MCoercion -> MCoercion
go_mco MCoercion
mco)
    go (TyConAppCo Role
r TyCon
tc [Coercion]
args)= let args' :: [Coercion]
args' = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
go [Coercion]
args
                               in  [Coercion]
args' [Coercion] -> Coercion -> Coercion
forall a b. [a] -> b -> b
`seqList` HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc [Coercion]
args'
    go (AppCo Coercion
co Coercion
arg)        = (Coercion -> Coercion -> Coercion
mkAppCo (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
arg
    go (ForAllCo Var
tv Coercion
kind_co Coercion
co)
      = case Subst -> Var -> Coercion -> (Subst, Var, Coercion)
substForAllCoBndrUnchecked Subst
subst Var
tv Coercion
kind_co of
         (Subst
subst', Var
tv', Coercion
kind_co') ->
          ((Var -> Coercion -> Coercion -> Coercion
mkForAllCo (Var -> Coercion -> Coercion -> Coercion)
-> Var -> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Var
tv') (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion
kind_co') (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Subst -> Coercion -> Coercion
subst_co Subst
subst' Coercion
co
    go (FunCo Role
r FunTyFlag
afl FunTyFlag
afr Coercion
w Coercion
co1 Coercion
co2)   = ((Role
-> FunTyFlag
-> FunTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkFunCo2 Role
r FunTyFlag
afl FunTyFlag
afr (Coercion -> Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
w) (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co1) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
co2
    go (CoVarCo Var
cv)          = Subst -> Var -> Coercion
substCoVar Subst
subst Var
cv
    go (AxiomInstCo CoAxiom Branched
con BranchIndex
ind [Coercion]
cos) = CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkAxiomInstCo CoAxiom Branched
con BranchIndex
ind ([Coercion] -> Coercion) -> [Coercion] -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
go [Coercion]
cos
    go (UnivCo UnivCoProvenance
p Role
r Type
t1 Type
t2)    = (((UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (UnivCoProvenance -> Role -> Type -> Type -> Coercion)
-> UnivCoProvenance -> Role -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! UnivCoProvenance -> UnivCoProvenance
go_prov UnivCoProvenance
p) (Role -> Type -> Type -> Coercion)
-> Role -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! Role
r) (Type -> Type -> Coercion) -> Type -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$!
                                (Type -> Type
go_ty Type
t1)) (Type -> Coercion) -> Type -> Coercion
forall a b. (a -> b) -> a -> b
$! (Type -> Type
go_ty Type
t2)
    go (SymCo Coercion
co)            = Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
    go (TransCo Coercion
co1 Coercion
co2)     = (Coercion -> Coercion -> Coercion
mkTransCo (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co1)) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co2)
    go (SelCo CoSel
d Coercion
co)          = HasDebugCallStack => CoSel -> Coercion -> Coercion
CoSel -> Coercion -> Coercion
mkSelCo CoSel
d (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
    go (LRCo LeftOrRight
lr Coercion
co)          = LeftOrRight -> Coercion -> Coercion
mkLRCo LeftOrRight
lr (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
    go (InstCo Coercion
co Coercion
arg)       = (Coercion -> Coercion -> Coercion
mkInstCo (Coercion -> Coercion -> Coercion)
-> Coercion -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)) (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! Coercion -> Coercion
go Coercion
arg
    go (KindCo Coercion
co)           = Coercion -> Coercion
mkKindCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
    go (SubCo Coercion
co)            = HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
mkSubCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$! (Coercion -> Coercion
go Coercion
co)
    go (AxiomRuleCo CoAxiomRule
c [Coercion]
cs)    = let cs1 :: [Coercion]
cs1 = (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Coercion
go [Coercion]
cs
                                in [Coercion]
cs1 [Coercion] -> Coercion -> Coercion
forall a b. [a] -> b -> b
`seqList` CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo CoAxiomRule
c [Coercion]
cs1
    go (HoleCo CoercionHole
h)            = CoercionHole -> Coercion
HoleCo (CoercionHole -> Coercion) -> CoercionHole -> Coercion
forall a b. (a -> b) -> a -> b
$! CoercionHole -> CoercionHole
go_hole CoercionHole
h

    go_prov :: UnivCoProvenance -> UnivCoProvenance
go_prov (PhantomProv Coercion
kco)    = Coercion -> UnivCoProvenance
PhantomProv (Coercion -> Coercion
go Coercion
kco)
    go_prov (ProofIrrelProv Coercion
kco) = Coercion -> UnivCoProvenance
ProofIrrelProv (Coercion -> Coercion
go Coercion
kco)
    go_prov p :: UnivCoProvenance
p@(PluginProv String
_)     = UnivCoProvenance
p
    go_prov p :: UnivCoProvenance
p@(CorePrepProv Bool
_)   = UnivCoProvenance
p

    -- See Note [Substituting in a coercion hole]
    go_hole :: CoercionHole -> CoercionHole
go_hole h :: CoercionHole
h@(CoercionHole { ch_co_var :: CoercionHole -> Var
ch_co_var = Var
cv })
      = CoercionHole
h { ch_co_var = updateVarType go_ty cv }

substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion
                  -> (Subst, TyCoVar, Coercion)
substForAllCoBndr :: Subst -> Var -> Coercion -> (Subst, Var, Coercion)
substForAllCoBndr Subst
subst
  = Bool
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoBndrUsing Bool
False (HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo Subst
subst) Subst
subst

-- | Like 'substForAllCoBndr', but disables sanity checks.
-- The problems that the sanity checks in substCo catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substCoUnchecked to
-- substCo and remove this function. Please don't use in new code.
substForAllCoBndrUnchecked :: Subst -> TyCoVar -> KindCoercion
                           -> (Subst, TyCoVar, Coercion)
substForAllCoBndrUnchecked :: Subst -> Var -> Coercion -> (Subst, Var, Coercion)
substForAllCoBndrUnchecked Subst
subst
  = Bool
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoBndrUsing Bool
False (Subst -> Coercion -> Coercion
substCoUnchecked Subst
subst) Subst
subst

-- See Note [Sym and ForAllCo]
substForAllCoBndrUsing :: Bool  -- apply sym to binder?
                       -> (Coercion -> Coercion)  -- transformation to kind co
                       -> Subst -> TyCoVar -> KindCoercion
                       -> (Subst, TyCoVar, KindCoercion)
substForAllCoBndrUsing :: Bool
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoBndrUsing Bool
sym Coercion -> Coercion
sco Subst
subst Var
old_var
  | Var -> Bool
isTyVar Var
old_var = Bool
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoTyVarBndrUsing Bool
sym Coercion -> Coercion
sco Subst
subst Var
old_var
  | Bool
otherwise       = Bool
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoCoVarBndrUsing Bool
sym Coercion -> Coercion
sco Subst
subst Var
old_var

substForAllCoTyVarBndrUsing :: Bool  -- apply sym to binder?
                            -> (Coercion -> Coercion)  -- transformation to kind co
                            -> Subst -> TyVar -> KindCoercion
                            -> (Subst, TyVar, KindCoercion)
substForAllCoTyVarBndrUsing :: Bool
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoTyVarBndrUsing Bool
sym Coercion -> Coercion
sco (Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv) Var
old_var Coercion
old_kind_co
  = Bool -> (Subst, Var, Coercion) -> (Subst, Var, Coercion)
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
old_var )
    ( InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
new_var) IdSubstEnv
idenv TvSubstEnv
new_env CvSubstEnv
cenv
    , Var
new_var, Coercion
new_kind_co )
  where
    new_env :: TvSubstEnv
new_env | Bool
no_change Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
sym = TvSubstEnv -> Var -> TvSubstEnv
forall a. VarEnv a -> Var -> VarEnv a
delVarEnv TvSubstEnv
tenv Var
old_var
            | Bool
sym       = TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tenv Var
old_var (Type -> TvSubstEnv) -> Type -> TvSubstEnv
forall a b. (a -> b) -> a -> b
$
                          Var -> Type
TyVarTy Var
new_var Type -> Coercion -> Type
`CastTy` Coercion
new_kind_co
            | Bool
otherwise = TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tenv Var
old_var (Var -> Type
TyVarTy Var
new_var)

    no_kind_change :: Bool
no_kind_change = Coercion -> Bool
noFreeVarsOfCo Coercion
old_kind_co
    no_change :: Bool
no_change = Bool
no_kind_change Bool -> Bool -> Bool
&& (Var
new_var Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
old_var)

    new_kind_co :: Coercion
new_kind_co | Bool
no_kind_change = Coercion
old_kind_co
                | Bool
otherwise      = Coercion -> Coercion
sco Coercion
old_kind_co

    new_ki1 :: Type
new_ki1 = Coercion -> Type
coercionLKind Coercion
new_kind_co
    -- We could do substitution to (tyVarKind old_var). We don't do so because
    -- we already substituted new_kind_co, which contains the kind information
    -- we want. We don't want to do substitution once more. Also, in most cases,
    -- new_kind_co is a Refl, in which case coercionKind is really fast.

    new_var :: Var
new_var  = InScopeSet -> Var -> Var
uniqAway InScopeSet
in_scope (Var -> Type -> Var
setTyVarKind Var
old_var Type
new_ki1)

substForAllCoCoVarBndrUsing :: Bool  -- apply sym to binder?
                            -> (Coercion -> Coercion)  -- transformation to kind co
                            -> Subst -> CoVar -> KindCoercion
                            -> (Subst, CoVar, KindCoercion)
substForAllCoCoVarBndrUsing :: Bool
-> (Coercion -> Coercion)
-> Subst
-> Var
-> Coercion
-> (Subst, Var, Coercion)
substForAllCoCoVarBndrUsing Bool
sym Coercion -> Coercion
sco (Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv)
                            Var
old_var Coercion
old_kind_co
  = Bool -> (Subst, Var, Coercion) -> (Subst, Var, Coercion)
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isCoVar Var
old_var )
    ( InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
new_var) IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
new_cenv
    , Var
new_var, Coercion
new_kind_co )
  where
    new_cenv :: CvSubstEnv
new_cenv | Bool
no_change Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
sym = CvSubstEnv -> Var -> CvSubstEnv
forall a. VarEnv a -> Var -> VarEnv a
delVarEnv CvSubstEnv
cenv Var
old_var
             | Bool
otherwise = CvSubstEnv -> Var -> Coercion -> CvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv CvSubstEnv
cenv Var
old_var (Var -> Coercion
mkCoVarCo Var
new_var)

    no_kind_change :: Bool
no_kind_change = Coercion -> Bool
noFreeVarsOfCo Coercion
old_kind_co
    no_change :: Bool
no_change = Bool
no_kind_change Bool -> Bool -> Bool
&& (Var
new_var Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
old_var)

    new_kind_co :: Coercion
new_kind_co | Bool
no_kind_change = Coercion
old_kind_co
                | Bool
otherwise      = Coercion -> Coercion
sco Coercion
old_kind_co

    Pair Type
h1 Type
h2 = Coercion -> Pair Type
coercionKind Coercion
new_kind_co

    new_var :: Var
new_var       = InScopeSet -> Var -> Var
uniqAway InScopeSet
in_scope (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$ Name -> Type -> Var
mkCoVar (Var -> Name
varName Var
old_var) Type
new_var_type
    new_var_type :: Type
new_var_type  | Bool
sym       = Type
h2
                  | Bool
otherwise = Type
h1

substCoVar :: Subst -> CoVar -> Coercion
substCoVar :: Subst -> Var -> Coercion
substCoVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
cenv) Var
cv
  = case CvSubstEnv -> Var -> Maybe Coercion
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv CvSubstEnv
cenv Var
cv of
      Just Coercion
co -> Coercion
co
      Maybe Coercion
Nothing -> Var -> Coercion
CoVarCo Var
cv

substCoVars :: Subst -> [CoVar] -> [Coercion]
substCoVars :: Subst -> [Var] -> [Coercion]
substCoVars Subst
subst [Var]
cvs = (Var -> Coercion) -> [Var] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Var -> Coercion
substCoVar Subst
subst) [Var]
cvs

lookupCoVar :: Subst -> Var -> Maybe Coercion
lookupCoVar :: Subst -> Var -> Maybe Coercion
lookupCoVar (Subst InScopeSet
_ IdSubstEnv
_ TvSubstEnv
_ CvSubstEnv
cenv) Var
v = CvSubstEnv -> Var -> Maybe Coercion
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv CvSubstEnv
cenv Var
v

substTyVarBndr :: HasDebugCallStack => Subst -> TyVar -> (Subst, TyVar)
substTyVarBndr :: HasDebugCallStack => Subst -> Var -> (Subst, Var)
substTyVarBndr = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substTyVarBndrUsing HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy

substTyVarBndrs :: HasDebugCallStack => Subst -> [TyVar] -> (Subst, [TyVar])
substTyVarBndrs :: HasDebugCallStack => Subst -> [Var] -> (Subst, [Var])
substTyVarBndrs = (Subst -> Var -> (Subst, Var)) -> Subst -> [Var] -> (Subst, [Var])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL HasDebugCallStack => Subst -> Var -> (Subst, Var)
Subst -> Var -> (Subst, Var)
substTyVarBndr

substVarBndr :: HasDebugCallStack => Subst -> TyCoVar -> (Subst, TyCoVar)
substVarBndr :: HasDebugCallStack => Subst -> Var -> (Subst, Var)
substVarBndr = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substVarBndrUsing HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy

substVarBndrs :: HasDebugCallStack => Subst -> [TyCoVar] -> (Subst, [TyCoVar])
substVarBndrs :: HasDebugCallStack => Subst -> [Var] -> (Subst, [Var])
substVarBndrs = (Subst -> Var -> (Subst, Var)) -> Subst -> [Var] -> (Subst, [Var])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL HasDebugCallStack => Subst -> Var -> (Subst, Var)
Subst -> Var -> (Subst, Var)
substVarBndr

substCoVarBndr :: HasDebugCallStack => Subst -> CoVar -> (Subst, CoVar)
substCoVarBndr :: HasDebugCallStack => Subst -> Var -> (Subst, Var)
substCoVarBndr = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substCoVarBndrUsing HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy

-- | Like 'substVarBndr', but disables sanity checks.
-- The problems that the sanity checks in substTy catch are described in
-- Note [The substitution invariant].
-- 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.
substVarBndrUnchecked :: Subst -> TyCoVar -> (Subst, TyCoVar)
substVarBndrUnchecked :: Subst -> Var -> (Subst, Var)
substVarBndrUnchecked = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substVarBndrUsing Subst -> Type -> Type
substTyUnchecked

substVarBndrUsing :: (Subst -> Type -> Type)
                  -> Subst -> TyCoVar -> (Subst, TyCoVar)
substVarBndrUsing :: (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substVarBndrUsing Subst -> Type -> Type
subst_fn Subst
subst Var
v
  | Var -> Bool
isTyVar Var
v = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substTyVarBndrUsing Subst -> Type -> Type
subst_fn Subst
subst Var
v
  | Bool
otherwise = (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substCoVarBndrUsing Subst -> Type -> Type
subst_fn Subst
subst Var
v

-- | Substitute a tyvar in a binding position, returning an
-- extended subst and a new tyvar.
-- Use the supplied function to substitute in the kind
substTyVarBndrUsing
  :: (Subst -> Type -> Type)  -- ^ Use this to substitute in the kind
  -> Subst -> TyVar -> (Subst, TyVar)
substTyVarBndrUsing :: (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substTyVarBndrUsing Subst -> Type -> Type
subst_fn subst :: Subst
subst@(Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv) Var
old_var
  = Bool -> SDoc -> (Subst, Var) -> (Subst, Var)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr Bool
_no_capture (Var -> SDoc
pprTyVar Var
old_var SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Var -> SDoc
pprTyVar Var
new_var SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Subst -> SDoc
forall a. Outputable a => a -> SDoc
ppr Subst
subst) ((Subst, Var) -> (Subst, Var)) -> (Subst, Var) -> (Subst, Var)
forall a b. (a -> b) -> a -> b
$
    Bool -> (Subst, Var) -> (Subst, Var)
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isTyVar Var
old_var )
    (InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
new_var) IdSubstEnv
idenv TvSubstEnv
new_env CvSubstEnv
cenv, Var
new_var)
  where
    new_env :: TvSubstEnv
new_env | Bool
no_change = TvSubstEnv -> Var -> TvSubstEnv
forall a. VarEnv a -> Var -> VarEnv a
delVarEnv TvSubstEnv
tenv Var
old_var
            | Bool
otherwise = TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tenv Var
old_var (Var -> Type
TyVarTy Var
new_var)

    _no_capture :: Bool
_no_capture = Bool -> Bool
not (Var
new_var Var -> VarSet -> Bool
`elemVarSet` TvSubstEnv -> VarSet
shallowTyCoVarsOfTyVarEnv TvSubstEnv
tenv)
    -- Assertion check that we are not capturing something in the substitution

    old_ki :: Type
old_ki = Var -> Type
tyVarKind Var
old_var
    no_kind_change :: Bool
no_kind_change = Type -> Bool
noFreeVarsOfType Type
old_ki -- verify that kind is closed
    no_change :: Bool
no_change = Bool
no_kind_change Bool -> Bool -> Bool
&& (Var
new_var Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
old_var)
        -- no_change means that the new_var is identical in
        -- all respects to the old_var (same unique, same kind)
        -- See Note [Extending the TvSubstEnv and CvSubstEnv]
        --
        -- In that case we don't need to extend the substitution
        -- to map old to new.  But instead we must zap any
        -- current substitution for the variable. For example:
        --      (\x.e) with id_subst = [x |-> e']
        -- Here we must simply zap the substitution for x

    new_var :: Var
new_var | Bool
no_kind_change = InScopeSet -> Var -> Var
uniqAway InScopeSet
in_scope Var
old_var
            | Bool
otherwise = InScopeSet -> Var -> Var
uniqAway InScopeSet
in_scope (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
                          Var -> Type -> Var
setTyVarKind Var
old_var (Subst -> Type -> Type
subst_fn Subst
subst Type
old_ki)
        -- The uniqAway part makes sure the new variable is not already in scope

-- | Substitute a covar in a binding position, returning an
-- extended subst and a new covar.
-- Use the supplied function to substitute in the kind
substCoVarBndrUsing
  :: (Subst -> Type -> Type)
  -> Subst -> CoVar -> (Subst, CoVar)
substCoVarBndrUsing :: (Subst -> Type -> Type) -> Subst -> Var -> (Subst, Var)
substCoVarBndrUsing Subst -> Type -> Type
subst_fn subst :: Subst
subst@(Subst InScopeSet
in_scope IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
cenv) Var
old_var
  = Bool -> (Subst, Var) -> (Subst, Var)
forall a. HasCallStack => Bool -> a -> a
assert (Var -> Bool
isCoVar Var
old_var)
    (InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet
in_scope InScopeSet -> Var -> InScopeSet
`extendInScopeSet` Var
new_var) IdSubstEnv
idenv TvSubstEnv
tenv CvSubstEnv
new_cenv, Var
new_var)
  where
    new_co :: Coercion
new_co         = Var -> Coercion
mkCoVarCo Var
new_var
    no_kind_change :: Bool
no_kind_change = [Type] -> Bool
noFreeVarsOfTypes [Type
t1, Type
t2]
    no_change :: Bool
no_change      = Var
new_var Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
old_var Bool -> Bool -> Bool
&& Bool
no_kind_change

    new_cenv :: CvSubstEnv
new_cenv | Bool
no_change = CvSubstEnv -> Var -> CvSubstEnv
forall a. VarEnv a -> Var -> VarEnv a
delVarEnv CvSubstEnv
cenv Var
old_var
             | Bool
otherwise = CvSubstEnv -> Var -> Coercion -> CvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv CvSubstEnv
cenv Var
old_var Coercion
new_co

    new_var :: Var
new_var = InScopeSet -> Var -> Var
uniqAway InScopeSet
in_scope Var
subst_old_var
    subst_old_var :: Var
subst_old_var = Name -> Type -> Var
mkCoVar (Var -> Name
varName Var
old_var) Type
new_var_type

    (Type
_, Type
_, Type
t1, Type
t2, Role
role) = HasDebugCallStack => Var -> (Type, Type, Type, Type, Role)
Var -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole Var
old_var
    t1' :: Type
t1' = Subst -> Type -> Type
subst_fn Subst
subst Type
t1
    t2' :: Type
t2' = Subst -> Type -> Type
subst_fn Subst
subst Type
t2
    new_var_type :: Type
new_var_type = Role -> Type -> Type -> Type
mkCoercionType Role
role Type
t1' Type
t2'
                  -- It's important to do the substitution for coercions,
                  -- because they can have free type variables

cloneTyVarBndr :: Subst -> TyVar -> Unique -> (Subst, TyVar)
cloneTyVarBndr :: Subst -> Var -> Unique -> (Subst, Var)
cloneTyVarBndr subst :: Subst
subst@(Subst InScopeSet
in_scope IdSubstEnv
id_env TvSubstEnv
tv_env CvSubstEnv
cv_env) Var
tv Unique
uniq
  = Bool -> SDoc -> (Subst, Var) -> (Subst, Var)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Var -> Bool
isTyVar Var
tv) (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv)   -- I think it's only called on TyVars
    ( InScopeSet -> IdSubstEnv -> TvSubstEnv -> CvSubstEnv -> Subst
Subst (InScopeSet -> Var -> InScopeSet
extendInScopeSet InScopeSet
in_scope Var
tv')
            IdSubstEnv
id_env
            (TvSubstEnv -> Var -> Type -> TvSubstEnv
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv TvSubstEnv
tv_env Var
tv (Var -> Type
mkTyVarTy Var
tv'))
            CvSubstEnv
cv_env
    , Var
tv')
  where
    old_ki :: Type
old_ki = Var -> Type
tyVarKind Var
tv
    no_kind_change :: Bool
no_kind_change = Type -> Bool
noFreeVarsOfType Type
old_ki -- verify that kind is closed

    tv1 :: Var
tv1 | Bool
no_kind_change = Var
tv
        | Bool
otherwise      = Var -> Type -> Var
setTyVarKind Var
tv (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
old_ki)

    tv' :: Var
tv' = Var -> Unique -> Var
setVarUnique Var
tv1 Unique
uniq

cloneTyVarBndrs :: Subst -> [TyVar] -> UniqSupply -> (Subst, [TyVar])
cloneTyVarBndrs :: Subst -> [Var] -> UniqSupply -> (Subst, [Var])
cloneTyVarBndrs Subst
subst []     UniqSupply
_usupply = (Subst
subst, [])
cloneTyVarBndrs Subst
subst (Var
t:[Var]
ts)  UniqSupply
usupply = (Subst
subst'', Var
tvVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
tvs)
  where
    (Unique
uniq, UniqSupply
usupply') = UniqSupply -> (Unique, UniqSupply)
takeUniqFromSupply UniqSupply
usupply
    (Subst
subst' , Var
tv )   = Subst -> Var -> Unique -> (Subst, Var)
cloneTyVarBndr Subst
subst Var
t Unique
uniq
    (Subst
subst'', [Var]
tvs)   = Subst -> [Var] -> UniqSupply -> (Subst, [Var])
cloneTyVarBndrs Subst
subst' [Var]
ts UniqSupply
usupply'

substTyCoBndr :: Subst -> PiTyBinder -> (Subst, PiTyBinder)
substTyCoBndr :: Subst -> PiTyBinder -> (Subst, PiTyBinder)
substTyCoBndr Subst
subst (Anon Scaled Type
ty FunTyFlag
af)          = (Subst
subst, Scaled Type -> FunTyFlag -> PiTyBinder
Anon (HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
Subst -> Scaled Type -> Scaled Type
substScaledTy Subst
subst Scaled Type
ty) FunTyFlag
af)
substTyCoBndr Subst
subst (Named (Bndr Var
tv ForAllTyFlag
vis)) = (Subst
subst', VarBndr Var ForAllTyFlag -> PiTyBinder
Named (Var -> ForAllTyFlag -> VarBndr Var ForAllTyFlag
forall var argf. var -> argf -> VarBndr var argf
Bndr Var
tv' ForAllTyFlag
vis))
                                          where
                                            (Subst
subst', Var
tv') = HasDebugCallStack => Subst -> Var -> (Subst, Var)
Subst -> Var -> (Subst, Var)
substVarBndr Subst
subst Var
tv