module Internal.Evidence (evByFiat, evByFiatWithDependencies) where

import GHC.Tc.Types.Evidence (EvTerm(..))
import GHC.Core.TyCo.Rep (UnivCoProvenance (..))

import GhcApi.GhcPlugins

-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce'
evByFiat :: String -- ^ Name the coercion should have
         -> Type   -- ^ The LHS of the equivalence relation (~)
         -> Type   -- ^ The RHS of the equivalence relation (~)
         -> EvTerm
evByFiat :: String -> Type -> Type -> EvTerm
evByFiat String
name Type
t1 Type
t2 =
  EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion (Coercion -> EvExpr) -> Coercion -> EvExpr
forall a b. (a -> b) -> a -> b
$ UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (String -> UnivCoProvenance
PluginProv String
name) Role
Nominal Type
t1 Type
t2

-- | The 'EvTerm' equivalent for 'Unsafe.unsafeCoerce'
evByFiatWithDependencies ::
  String -- ^ Name the coercion should have
  -> [Coercion] -- ^ The set of all the in-scope coercion that the proof makes use of.
  -> Type -- ^ The LHS of the equivalence relation (~)
  -> Type -- ^ The RHS of the equivalence relation (~)
  -> EvTerm
evByFiatWithDependencies :: String -> [Coercion] -> Type -> Type -> EvTerm
evByFiatWithDependencies String
name [Coercion]
_deps Type
t1 Type
t2 =
  EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion (Coercion -> EvExpr) -> Coercion -> EvExpr
forall a b. (a -> b) -> a -> b
$ UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (String -> UnivCoProvenance
PluginProv String
name) Role
Nominal Type
t1 Type
t2