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]

-- | Make up evidence for a fake equality constraint @t1 ~~ t2@ by
-- coercing bogus evidence of type @t1 ~ t2@ (or its heterogeneous
-- variant, in GHC 8.0).
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