module Internal.Type (substType) where

import Data.Maybe (fromMaybe)
import GHC.Tc.Utils.TcType (TcType)
import GHC.Core.TyCo.Rep (Type (..))
import GHC.Types.Var (TcTyVar)

-- | Apply substitutions in Types

--

-- __NB:__ Doesn't substitute under binders

substType
  :: [(TcTyVar, TcType)]
  -> TcType
  -> TcType
substType :: [(Var, TcType)] -> TcType -> TcType
substType [(Var, TcType)]
subst tv :: TcType
tv@(TyVarTy Var
v) =
  forall a. a -> Maybe a -> a
fromMaybe TcType
tv (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v [(Var, TcType)]
subst)
substType [(Var, TcType)]
subst (AppTy TcType
t1 TcType
t2) =
  TcType -> TcType -> TcType
AppTy ([(Var, TcType)] -> TcType -> TcType
substType [(Var, TcType)]
subst TcType
t1) ([(Var, TcType)] -> TcType -> TcType
substType [(Var, TcType)]
subst TcType
t2)
substType [(Var, TcType)]
subst (TyConApp TyCon
tc [TcType]
xs) =
  TyCon -> [TcType] -> TcType
TyConApp TyCon
tc (forall a b. (a -> b) -> [a] -> [b]
map ([(Var, TcType)] -> TcType -> TcType
substType [(Var, TcType)]
subst) [TcType]
xs)
substType [(Var, TcType)]
_subst t :: TcType
t@(ForAllTy TyCoVarBinder
_tv TcType
_ty) =
  -- TODO: Is it safe to do "dumb" substitution under binders?

  -- ForAllTy tv (substType subst ty)

  TcType
t
substType [(Var, TcType)]
subst (FunTy AnonArgFlag
k1 TcType
k2 TcType
t1 TcType
t2) =
  AnonArgFlag -> TcType -> TcType -> TcType -> TcType
FunTy AnonArgFlag
k1 TcType
k2 ([(Var, TcType)] -> TcType -> TcType
substType [(Var, TcType)]
subst TcType
t1) ([(Var, TcType)] -> TcType -> TcType
substType [(Var, TcType)]
subst TcType
t2)
substType [(Var, TcType)]
_ l :: TcType
l@(LitTy TyLit
_) = TcType
l
substType [(Var, TcType)]
subst (CastTy TcType
ty KindCoercion
co) =
  TcType -> KindCoercion -> TcType
CastTy ([(Var, TcType)] -> TcType -> TcType
substType [(Var, TcType)]
subst TcType
ty) KindCoercion
co
substType [(Var, TcType)]
_ co :: TcType
co@(CoercionTy KindCoercion
_) = TcType
co