{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE StandaloneDeriving        #-}

{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1.
{-# OPTIONS_GHC -Wno-orphans #-}

module Language.Haskell.Liquid.GHC.TypeRep (
  mkTyArg, 

  showTy
  ) where

import           Language.Haskell.Liquid.GHC.Misc (showPpr)
import           Liquid.GHC.API as Ghc hiding (mkTyArg, showPpr, panic)
import           Language.Fixpoint.Types (symbol)

-- e368f3265b80aeb337fbac3f6a70ee54ab14edfd

mkTyArg :: TyVar -> TyVarBinder
mkTyArg :: TyVar -> TyVarBinder
mkTyArg TyVar
v = TyVar -> ForAllTyFlag -> TyVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
v ForAllTyFlag
Required

instance Eq Type where
  Type
t1 == :: Type -> Type -> Bool
== Type
t2 = Type -> Type -> Bool
eqType' Type
t1 Type
t2

eqType' :: Type -> Type -> Bool 
eqType' :: Type -> Type -> Bool
eqType' (LitTy TyLit
l1) (LitTy TyLit
l2) 
  = TyLit
l1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
l2  
eqType' (CoercionTy Coercion
c1) (CoercionTy Coercion
c2) 
  = Coercion
c1 Coercion -> Coercion -> Bool
forall a. Eq a => a -> a -> Bool
== Coercion
c2  
eqType'(CastTy Type
t1 Coercion
c1) (CastTy Type
t2 Coercion
c2) 
  = Type -> Type -> Bool
eqType' Type
t1 Type
t2 Bool -> Bool -> Bool
&& Coercion
c1 Coercion -> Coercion -> Bool
forall a. Eq a => a -> a -> Bool
== Coercion
c2 
eqType' (FunTy FunTyFlag
a1 Type
m1 Type
t11 Type
t12) (FunTy FunTyFlag
a2 Type
m2 Type
t21 Type
t22)
  = FunTyFlag
a1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
a2 Bool -> Bool -> Bool
&& Type
m1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
m2 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqType' Type
t11 Type
t21 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqType' Type
t12 Type
t22  
eqType' (ForAllTy (Bndr TyVar
v1 ForAllTyFlag
_) Type
t1) (ForAllTy (Bndr TyVar
v2 ForAllTyFlag
_) Type
t2) 
  = Type -> Type -> Bool
eqType' Type
t1 (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
v2 (TyVar -> Type
TyVarTy TyVar
v1) Type
t2) 
eqType' (TyVarTy TyVar
v1) (TyVarTy TyVar
v2) 
  = TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v2 
eqType' (AppTy Type
t11 Type
t12) (AppTy Type
t21 Type
t22) 
  = Type -> Type -> Bool
eqType' Type
t11 Type
t21 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqType' Type
t12 Type
t22  
eqType' (TyConApp TyCon
c1 [Type]
ts1) (TyConApp TyCon
c2 [Type]
ts2) 
  = TyCon
c1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
c2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Type -> Type -> Bool) -> [Type] -> [Type] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Type -> Bool
eqType' [Type]
ts1 [Type]
ts2) 
eqType' Type
_ Type
_ 
  = Bool
False 


deriving instance (Eq tyvar, Eq argf) => Eq (VarBndr tyvar argf)

instance Eq Coercion where
  Coercion
_ == :: Coercion -> Coercion -> Bool
== Coercion
_ = Bool
True 


showTy :: Type -> String 
showTy :: Type -> [Char]
showTy (TyConApp TyCon
c [Type]
ts) = [Char]
"(RApp   " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyCon -> [Char]
forall a. Outputable a => a -> [Char]
showPpr TyCon
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
sep' [Char]
", " (Type -> [Char]
showTy (Type -> [Char]) -> [Type] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (AppTy Type
t1 Type
t2)   = [Char]
"(TAppTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Type -> [Char]
showTy Type
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showTy Type
t2) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")" 
showTy (TyVarTy TyVar
v)   = [Char]
"(RVar " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v)  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")" 
showTy (ForAllTy (Bndr TyVar
v ForAllTyFlag
_) Type
t)  = [Char]
"ForAllTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
". (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++  Type -> [Char]
showTy Type
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (FunTy FunTyFlag
af Type
_m1 Type
t1 Type
t2) = [Char]
"FunTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FunTyFlag -> [Char]
forall a. Outputable a => a -> [Char]
showPpr FunTyFlag
af [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showTy Type
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
". (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++  Type -> [Char]
showTy Type
t2 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (CastTy Type
_ Coercion
_)    = [Char]
"CastTy"
showTy (CoercionTy Coercion
_)  = [Char]
"CoercionTy"
showTy (LitTy TyLit
_)       = [Char]
"LitTy"

sep' :: String -> [String] -> String
sep' :: [Char] -> [[Char]] -> [Char]
sep' [Char]
_ [[Char]
x] = [Char]
x
sep' [Char]
_ []  = []
sep' [Char]
s ([Char]
x:[[Char]]
xs) = [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
sep' [Char]
s [[Char]]
xs 



-------------------------------------------------------------------------------
-- | GHC Type Substitutions ---------------------------------------------------
-------------------------------------------------------------------------------

class SubstTy a where
  subst :: TyVar -> Type -> a -> a
  subst TyVar
_ Type
_ = a -> a
forall a. a -> a
id  

instance SubstTy Type where
  subst :: TyVar -> Type -> Type -> Type
subst = TyVar -> Type -> Type -> Type
substType

substType :: TyVar -> Type -> Type -> Type
substType :: TyVar -> Type -> Type -> Type
substType TyVar
x Type
tx (TyConApp TyCon
c [Type]
ts) 
  = TyCon -> [Type] -> Type
TyConApp TyCon
c (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts)
substType TyVar
x Type
tx (AppTy Type
t1 Type
t2)   
  = Type -> Type -> Type
AppTy (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2) 
substType TyVar
x Type
tx (TyVarTy TyVar
y)   
  | TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y
  = Type
tx 
  | Bool
otherwise
  = TyVar -> Type
TyVarTy TyVar
y 
substType TyVar
x Type
tx (FunTy FunTyFlag
aaf Type
m Type
t1 Type
t2)
  = FunTyFlag -> Type -> Type -> Type -> Type
FunTy FunTyFlag
aaf Type
m (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2)
substType TyVar
x Type
tx f :: Type
f@(ForAllTy b :: TyVarBinder
b@(Bndr TyVar
y ForAllTyFlag
_) Type
t)  
  | TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y 
  = Type
f
  | Bool
otherwise 
  = TyVarBinder -> Type -> Type
ForAllTy TyVarBinder
b (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t)
substType TyVar
x Type
tx (CastTy Type
t Coercion
c)    
  = Type -> Coercion -> Type
CastTy (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substType TyVar
x Type
tx (CoercionTy Coercion
c)  
  = Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c 
substType TyVar
_ Type
_  (LitTy TyLit
l)
  = TyLit -> Type
LitTy TyLit
l  


instance SubstTy Coercion where
  subst :: TyVar -> Type -> Coercion -> Coercion
subst = TyVar -> Type -> Coercion -> Coercion
substCoercion

substCoercion :: TyVar -> Type -> Coercion -> Coercion
substCoercion :: TyVar -> Type -> Coercion -> Coercion
substCoercion TyVar
x Type
tx (TyConAppCo Role
r TyCon
c [Coercion]
cs)
  = Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) TyCon
c (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)
substCoercion TyVar
x Type
tx (AppCo Coercion
c1 Coercion
c2)
  = Coercion -> Coercion -> Coercion
AppCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (FunCo Role
r FunTyFlag
afl FunTyFlag
afr Coercion
cN Coercion
c1 Coercion
c2)
  = Role
-> FunTyFlag
-> FunTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
FunCo Role
r FunTyFlag
afl FunTyFlag
afr Coercion
cN (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2) -- TODO(adinapoli) Is this the correct substitution?
substCoercion TyVar
x Type
tx (ForAllCo TyVar
y Coercion
c1 Coercion
c2)
  | TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y 
  = TyVar -> Coercion -> Coercion -> Coercion
ForAllCo TyVar
y Coercion
c1 Coercion
c2
  | Bool
otherwise 
  = TyVar -> Coercion -> Coercion -> Coercion
ForAllCo TyVar
y (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
_ Type
_ (CoVarCo TyVar
y)
  = TyVar -> Coercion
CoVarCo TyVar
y 
substCoercion TyVar
x Type
tx (AxiomInstCo CoAxiom Branched
co BranchIndex
bi [Coercion]
cs)
  = CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
AxiomInstCo (TyVar -> Type -> CoAxiom Branched -> CoAxiom Branched
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx CoAxiom Branched
co) BranchIndex
bi (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)  
substCoercion TyVar
x Type
tx (UnivCo UnivCoProvenance
y Role
r Type
t1 Type
t2)
  = UnivCoProvenance -> Role -> Type -> Type -> Coercion
UnivCo (TyVar -> Type -> UnivCoProvenance -> UnivCoProvenance
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx UnivCoProvenance
y) (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2)
substCoercion TyVar
x Type
tx (SymCo Coercion
c)
  = Coercion -> Coercion
SymCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (TransCo Coercion
c1 Coercion
c2)
  = Coercion -> Coercion -> Coercion
TransCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (AxiomRuleCo CoAxiomRule
ca [Coercion]
cs)
  = CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo (TyVar -> Type -> CoAxiomRule -> CoAxiomRule
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx CoAxiomRule
ca)  (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)  
substCoercion TyVar
x Type
tx (SelCo CoSel
i Coercion
c)
  = CoSel -> Coercion -> Coercion
SelCo CoSel
i (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (LRCo LeftOrRight
i Coercion
c)
  = LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
i (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (InstCo Coercion
c1 Coercion
c2)
  = Coercion -> Coercion -> Coercion
InstCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (KindCo Coercion
c)
  = Coercion -> Coercion
KindCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (SubCo Coercion
c)
  = Coercion -> Coercion
SubCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
_x Type
_tx (Refl Type
t)
  = Type -> Coercion
Refl Type
t
substCoercion TyVar
_x Type
_tx (GRefl Role
r Type
t MCoercionN
c)
  = Role -> Type -> MCoercionN -> Coercion
GRefl Role
r Type
t MCoercionN
c
substCoercion TyVar
_x Type
_tx (HoleCo CoercionHole
c)
  = CoercionHole -> Coercion
HoleCo CoercionHole
c

instance SubstTy Role where
instance SubstTy (CoAxiom Branched) where

instance SubstTy UnivCoProvenance where
  subst :: TyVar -> Type -> UnivCoProvenance -> UnivCoProvenance
subst TyVar
x Type
tx (PhantomProv Coercion
c)
    = Coercion -> UnivCoProvenance
PhantomProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c 
  subst TyVar
x Type
tx (ProofIrrelProv Coercion
c)
    = Coercion -> UnivCoProvenance
ProofIrrelProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c 
  subst TyVar
_ Type
_ UnivCoProvenance
ch 
    = UnivCoProvenance
ch 

instance SubstTy CoAxiomRule where
  subst :: TyVar -> Type -> CoAxiomRule -> CoAxiomRule
subst TyVar
x Type
tx (CoAxiomRule FastString
n [Role]
rs Role
r [TypeEqn] -> Maybe TypeEqn
ps) 
    = FastString
-> [Role] -> Role -> ([TypeEqn] -> Maybe TypeEqn) -> CoAxiomRule
CoAxiomRule FastString
n (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Role -> Role) -> [Role] -> [Role]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Role]
rs) (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) (\[TypeEqn]
eq -> TyVar -> Type -> Maybe TypeEqn -> Maybe TypeEqn
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx ([TypeEqn] -> Maybe TypeEqn
ps (TyVar -> Type -> [TypeEqn] -> [TypeEqn]
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx [TypeEqn]
eq)))

instance (SubstTy a, Functor m) => SubstTy (m a) where
  subst :: TyVar -> Type -> m a -> m a
subst TyVar
x Type
tx m a
xs = TyVar -> Type -> a -> a
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (a -> a) -> m a -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
xs