1 {-# LANGUAGE ModalTypes, MultiParamTypeClasses, KindSignatures, FlexibleContexts #-}
2 -----------------------------------------------------------------------------
4 -- Module : GHC.HetMet.CodeTypes
6 -- License : public domain
8 -- Maintainer : Adam Megacz <megacz@acm.org>
9 -- Stability : experimental
10 -- Portability : portable
11 module GHC.HetMet.CodeTypes (
17 GuestIntegerLiteral, guestIntegerLiteral,
18 GuestStringLiteral, guestStringLiteral,
19 GuestCharLiteral, guestCharLiteral
22 hetmet_brak :: forall (c :: * -> * -> *). forall a. a -> <{a}>@c
23 hetmet_brak = Prelude.error "hetmet_brak should never be evaluated; did you forget to compile with -fcoqpass?"
25 hetmet_esc :: forall (c :: * -> * -> *). forall a. <{a}>@c -> a
26 hetmet_esc = Prelude.error "hetmet_esc should never be evaluated; did you forget to compile with -fcoqpass?"
28 hetmet_csp :: forall (c :: * -> * -> *). forall a. a -> a
29 hetmet_csp = Prelude.error "hetmet_csp should never be evaluated; did you forget to compile with -fcoqpass?"
31 hetmet_kappa :: forall a b c . (( () -> a ) -> ( b -> c )) -> ( (a,b) -> c )
32 hetmet_kappa = Prelude.error "hetmet_kappa should never be evaluated; did you forget to compile with -fcoqpass?"
34 hetmet_kappa_app :: forall a b c . ( (a,b) -> c ) -> ( () -> a ) -> ( b -> c )
35 hetmet_kappa_app = Prelude.error "hetmet_kappa_app should never be evaluated; did you forget to compile with -fcoqpass?"
37 -- Technically these functions ought to be invoked *during
38 -- compilation*; in the future I would like to use Template Haskell to
40 class GuestIntegerLiteral c where
41 guestIntegerLiteral :: Integer -> <{ Integer }>@c
42 class GuestStringLiteral c where
43 guestStringLiteral :: String -> <{ String }>@c
44 class GuestCharLiteral c where
45 guestCharLiteral :: Char -> <{ Char }>@c