module GHC.Corroborate.Shim
( tyVarsOfType
, tyVarsOfTypes
, promoteTyCon
, mkEqPred
, mkHEqPred
, mkFunnyEqEvidence
) where
import GHC.Corroborate
import GHC.Corroborate.Evidence (evDFunApp', evCast', terms)
tyVarsOfType :: Type -> TyCoVarSet
tyVarsOfType :: Type -> TyCoVarSet
tyVarsOfType = Type -> TyCoVarSet
tyCoVarsOfType
tyVarsOfTypes :: [Type] -> TyCoVarSet
tyVarsOfTypes :: [Type] -> TyCoVarSet
tyVarsOfTypes = [Type] -> TyCoVarSet
tyCoVarsOfTypes
promoteTyCon :: TyCon -> TyCon
promoteTyCon :: TyCon -> TyCon
promoteTyCon = TyCon -> TyCon
forall a. a -> a
id
mkEqPred :: Type -> Type -> Type
mkEqPred :: Type -> Type -> Type
mkEqPred = Type -> Type -> Type
mkPrimEqPred
mkHEqPred :: Type -> Type -> Type
mkHEqPred :: Type -> Type -> Type
mkHEqPred Type
t1 Type
t2 = TyCon -> [Type] -> Type
TyConApp TyCon
heqTyCon [HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
t1, HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
t2, Type
t1, Type
t2]
mkFunnyEqEvidence :: String -> Type -> Type -> Type -> EvTerm
mkFunnyEqEvidence :: String -> Type -> Type -> Type -> EvTerm
mkFunnyEqEvidence String
s Type
t Type
t1 Type
t2 =
EvTerm
castFrom EvTerm -> TcCoercion -> EvTerm
`evCast'` TcCoercion
castTo
where
castFrom :: EvTerm
castFrom :: EvTerm
castFrom = DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp' DFunId
funId [Type]
tys ([EvExpr] -> EvTerm) -> [EvExpr] -> EvTerm
forall a b. (a -> b) -> a -> b
$ String -> Type -> Type -> [EvExpr]
terms String
s Type
t1 Type
t2
where
funId :: Id
funId :: DFunId
funId = DataCon -> DFunId
dataConWrapId DataCon
heqDataCon
tys :: [Kind]
tys :: [Type]
tys = [HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
t1, HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
t2, Type
t1, Type
t2]
castTo :: TcCoercion
castTo :: TcCoercion
castTo =
UnivCoProvenance -> Role -> Type -> Type -> TcCoercion
mkUnivCo UnivCoProvenance
from Role
Representational Type
tySource Type
t
where
from :: UnivCoProvenance
from :: UnivCoProvenance
from = String -> UnivCoProvenance
PluginProv String
s
tySource :: Type
tySource :: Type
tySource = Type -> Type -> Type
mkHEqPred Type
t1 Type
t2