module GHC.Corroborate.Evidence (evDFunApp', evCast', terms) where

import GHC.Corroborate

evDFunApp' :: DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp' :: DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp' = DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp

evCast' :: EvTerm -> TcCoercion -> EvTerm
evCast' :: EvTerm -> TcCoercion -> EvTerm
evCast' (EvExpr EvExpr
e)  = EvExpr -> TcCoercion -> EvTerm
evCast EvExpr
e
evCast' EvTypeable{} = [Char] -> TcCoercion -> EvTerm
forall a. HasCallStack => [Char] -> a
error [Char]
"Can't evCast EvTypeable{}"
evCast' EvFun{} = [Char] -> TcCoercion -> EvTerm
forall a. HasCallStack => [Char] -> a
error [Char]
"Can't evCast EvFun{}"

terms :: String -> Type -> Type -> [EvExpr]
terms :: [Char] -> Type -> Type -> [EvExpr]
terms [Char]
s Type
t1 Type
t2 =
    case [Char] -> Type -> Type -> EvTerm
evByFiat [Char]
s Type
t1 Type
t2 of
        EvExpr EvExpr
e -> [EvExpr
e]
        EvTypeable{} -> []
        EvFun{} -> []