-- editorconfig-checker-disable-file
{-# LANGUAGE CPP                   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE ViewPatterns          #-}
module PlutusTx.Lift.Class
    ( Typeable (..)
    , Lift (..)
    , RTCompile
    , makeTypeable
    , makeLift
    , withTyVars
    , LiftError (..)
    ) where

import PlutusTx.Lift.THUtils

import PlutusIR
import PlutusIR.Compiler.Definitions
import PlutusIR.Compiler.Names
import PlutusIR.MkPir

import PlutusCore.Default qualified as PLC
import PlutusCore.MkPlc qualified as PLC
import PlutusCore.Quote

import Control.Monad.Except hiding (lift)
import Control.Monad.Reader hiding (lift)
import Control.Monad.State hiding (lift)
import Control.Monad.Trans qualified as Trans

import Language.Haskell.TH qualified as TH hiding (newName)
import Language.Haskell.TH.Datatype qualified as TH
import Language.Haskell.TH.Syntax qualified as TH hiding (newName)
import Language.Haskell.TH.Syntax.Compat qualified as TH

import Data.Map qualified as Map
import Data.Set qualified as Set

import Control.Exception qualified as Prelude (Exception, throw)
import Data.Foldable
import Data.List (sortBy)
import Data.Maybe
import Data.Proxy
import Data.Text qualified as T
import Data.Traversable
import ErrorCode
import Prettyprinter qualified as PP

-- We do not use qualified import because the whole module contains off-chain code
import Prelude as Haskell

{- Note [Compiling at TH time and runtime]
We want to reuse PIR's machinery for defining datatypes. However, one cannot
get a PLC Type consisting of the compiled PIR type, because the compilation of the
definitions is done by making a *term*.

So we use the abstract support for handling definitions in PIR, MonadDefs. Typeable
then has `typeRep :: Proxy a -> RTCompile uni fun (Type TyName uni ())`,
which says that you can get the type in some compilation monad (which
you will later have to discharge yourself).

This means that the TH expressions we are generating are not for `Type`s directly, but rather
for monadic expressions that will, at runtime, compute types. We are effectively generating
a specialized compiler.

We thus have two pieces of compilation going on here:
- At TH time, we reify information about datatypes, and construct specialized compilation expressions
  for the various parts.
- At runtime, we actually run these and create definitions etc.

The interplay between the parts happening at TH time and the parts happening at runtime is somewhat
awkward, but I couldn't think of a better way of doing it.

A particularly awkward feature is that the typeclass constraints required by the code in each
instance are going to be different, and so we can't use reusable functions, instead we need to
inline all the definitions so that the overall expression can have the right constraints inferred.
-}

type RTCompile uni fun = DefT TH.Name uni fun () Quote
type RTCompileScope uni fun = ReaderT (LocalVars uni) (RTCompile uni fun)
type THCompile = StateT Deps (ReaderT THLocalVars (ExceptT LiftError TH.Q))

data LiftError = UnsupportedLiftKind TH.Kind
               | UnsupportedLiftType TH.Type
               | UserLiftError T.Text
               | LiftMissingDataCons TH.Name
               | LiftMissingVar TH.Name
               deriving anyclass (Show LiftError
Typeable LiftError
SomeException -> Maybe LiftError
LiftError -> String
LiftError -> SomeException
forall e.
Typeable e
-> Show e
-> (e -> SomeException)
-> (SomeException -> Maybe e)
-> (e -> String)
-> Exception e
displayException :: LiftError -> String
$cdisplayException :: LiftError -> String
fromException :: SomeException -> Maybe LiftError
$cfromException :: SomeException -> Maybe LiftError
toException :: LiftError -> SomeException
$ctoException :: LiftError -> SomeException
Prelude.Exception)

instance PP.Pretty LiftError where
    pretty :: forall ann. LiftError -> Doc ann
pretty (UnsupportedLiftType Pred
t) = Doc ann
"Unsupported lift type: " forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> forall a ann. Show a => a -> Doc ann
PP.viaShow Pred
t
    pretty (UnsupportedLiftKind Pred
t) = Doc ann
"Unsupported lift kind: " forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> forall a ann. Show a => a -> Doc ann
PP.viaShow Pred
t
    pretty (UserLiftError Text
t)       = forall a ann. Pretty a => a -> Doc ann
PP.pretty Text
t
    pretty (LiftMissingDataCons Name
n) = Doc ann
"Constructors not created for type: " forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> forall a ann. Show a => a -> Doc ann
PP.viaShow Name
n
    pretty (LiftMissingVar Name
n)      = Doc ann
"Unknown local variable: " forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> forall a ann. Show a => a -> Doc ann
PP.viaShow Name
n

instance Show LiftError where
    show :: LiftError -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
PP.pretty -- for Control.Exception

instance HasErrorCode LiftError where
    errorCode :: LiftError -> ErrorCode
errorCode UnsupportedLiftType {} = Natural -> ErrorCode
ErrorCode Natural
44
    errorCode UnsupportedLiftKind {} = Natural -> ErrorCode
ErrorCode Natural
45
    errorCode UserLiftError {}       = Natural -> ErrorCode
ErrorCode Natural
46
    errorCode LiftMissingDataCons {} = Natural -> ErrorCode
ErrorCode Natural
47
    errorCode LiftMissingVar {}      = Natural -> ErrorCode
ErrorCode Natural
48

{- Note [Impredicative function universe wrappers]
We are completely independent of the function universe. We generate constants (so we care about the type universe),
but we never generate builtin functions.

This is indicated in the fact that e.g. 'typeRep' has type 'forall fun . ...'. Note what this says: the
*caller* of 'typeRep` can decide on 'fun'.

So how do we deal with this? A wrong way is to parameterize our (TH) functions by 'fun'. This is wrong, because
this 'fun' is a type variable at TH-generation time, and we want a type variable in the generated code.
Sometimes this will even appear to work, and I don't know what kind of awful magic is going on in trying to persist
type variables into the quote, but I'm pretty sure it's wrong.

We could use 'InstanceSigs', bind 'fun', and then pass it down and use it in our signatures. But you can't splice
types into signatures in typed TH, you need to go to untyped TH and 'unsafeCoerceTExp' back again, which is pretty ugly.

Alternatively, we can *generate* functions which are parameterized over 'fun', and instantiate them at the top-level.
This is totally fine... except that the representation of expressions in typed TH has a type parameter for the type of
the expression, so we would need to write 'TExp (forall fun . ...)'... which is an impredicative type.

The usual solution is to make a datatype that wraps up the quantification, so you write 'newtype X = X (forall a . ...)',
and then you can write 'TExp X' just fine.

We do this, but annoyingly due to the fact that 'fun' appears inside the *value* of our monadic types (e.g. when we compile
to a term we need to have 'fun' in there) we can't do this generically, and instead we end up with a set of repetitive wrappers
for different variants of this impredicative type. Which is annoying, but does work.
-}

-- See Note [Impredicative function universe wrappers]
newtype CompileType = CompileType { CompileType
-> forall fun. RTCompile DefaultUni fun (Type TyName DefaultUni ())
unCompileType :: forall fun . RTCompile PLC.DefaultUni fun (Type TyName PLC.DefaultUni ()) }
newtype CompileTypeScope = CompileTypeScope { CompileTypeScope
-> forall fun.
   RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
unCompileTypeScope :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ()) }
newtype CompileDeclFun = CompileDeclFun { CompileDeclFun
-> forall fun.
   Type TyName DefaultUni ()
   -> RTCompileScope
        DefaultUni fun (VarDecl TyName Name DefaultUni ())
unCompileDeclFun :: forall fun . Type TyName PLC.DefaultUni () -> RTCompileScope PLC.DefaultUni fun (VarDecl TyName Name PLC.DefaultUni ()) }

{- Note [Type variables]
We handle types in almost exactly the same way when we are constructing Typeable
instances and when we are constructing Lift instances. However, there is one key difference
in how we handle type variables.

In the Typeable case, the type variables we see will be the type variables of the
datatype, which we want to map into the variable declarations that we construct. This requires
us to do some mapping between them at *runtime*, and keep a scope around to map between the TH names
and the PLC types.

In the Lift case, type variables will be free type variables in the instance, and should be handled
by appropriate Typeable constraints for those variables. We get the PLC types by just calling
typeRep.

However, for simplicity we always act as though we have a local scope, and fall back to Typeable,
but in the Lift case we will never populate the local scope.
-}

-- | A scope for type variables. See note [Type variables].
type LocalVars uni = Map.Map TH.Name (Type TyName uni ())
type THLocalVars = Set.Set TH.Name

withTyVars :: (MonadReader (LocalVars uni) m) => [(TH.Name, TyVarDecl TyName ())] -> m a -> m a
withTyVars :: forall (uni :: * -> *) (m :: * -> *) a.
MonadReader (LocalVars uni) m =>
[(Name, TyVarDecl TyName ())] -> m a -> m a
withTyVars [(Name, TyVarDecl TyName ())]
mappings = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\LocalVars uni
scope -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\LocalVars uni
acc (Name
n, TyVarDecl TyName ()
tvd) -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () TyVarDecl TyName ()
tvd) LocalVars uni
acc) LocalVars uni
scope [(Name, TyVarDecl TyName ())]
mappings)

thWithTyVars :: (MonadReader THLocalVars m) => [TH.Name] -> m a -> m a
thWithTyVars :: forall (m :: * -> *) a.
MonadReader THLocalVars m =>
[Name] -> m a -> m a
thWithTyVars [Name]
names = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\THLocalVars
scope -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Ord a => a -> Set a -> Set a
Set.insert THLocalVars
scope [Name]
names)

{- Note [Lifting newtypes]
Newtypes are handled differently in the compiler, in that we identify them with their underlying type.
See Note [Coercions and newtypes] for details.

So we need to do the same here. This means two things:
- For Typeable, we look for the unique field of the unique constructor, and then make a type lambda
  binding the type variables whose body is that type.
- For Lift, we assert that all constructors must have precisely one argument (as newtypes do), and we
  simply call lift on that.

Since we don't "compile" all the way, rather relying on the typeclass system, lifting recursive
newtypes will hang a runtime. Don't do that. (This is worse than what we do in the compiler, see
Note [Occurrences of recursive names])
-}

-- Dependencies at TH time

{- Note [Tracking dependencies]
While running at TH time, we track the requirements that we need in order to be able to compile
the given type/term, which are things like "must be able to type the constructor argument types".

These are then cashed out into constraints on the instance.
-}

data Dep = TypeableDep TH.Type | LiftDep TH.Type deriving stock (Int -> Dep -> ShowS
[Dep] -> ShowS
Dep -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Dep] -> ShowS
$cshowList :: [Dep] -> ShowS
show :: Dep -> String
$cshow :: Dep -> String
showsPrec :: Int -> Dep -> ShowS
$cshowsPrec :: Int -> Dep -> ShowS
Show, Dep -> Dep -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Dep -> Dep -> Bool
$c/= :: Dep -> Dep -> Bool
== :: Dep -> Dep -> Bool
$c== :: Dep -> Dep -> Bool
Eq, Eq Dep
Dep -> Dep -> Bool
Dep -> Dep -> Ordering
Dep -> Dep -> Dep
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Dep -> Dep -> Dep
$cmin :: Dep -> Dep -> Dep
max :: Dep -> Dep -> Dep
$cmax :: Dep -> Dep -> Dep
>= :: Dep -> Dep -> Bool
$c>= :: Dep -> Dep -> Bool
> :: Dep -> Dep -> Bool
$c> :: Dep -> Dep -> Bool
<= :: Dep -> Dep -> Bool
$c<= :: Dep -> Dep -> Bool
< :: Dep -> Dep -> Bool
$c< :: Dep -> Dep -> Bool
compare :: Dep -> Dep -> Ordering
$ccompare :: Dep -> Dep -> Ordering
Ord)
type Deps = Set.Set Dep

-- | Get all the named types which we depend on to define the current type.
-- Note that this relies on dependencies having been added with type synonyms
-- resolved!
getTyConDeps :: Deps -> Set.Set TH.Name
getTyConDeps :: Deps -> THLocalVars
getTyConDeps Deps
deps = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Dep -> Maybe Name
typeableDep forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Deps
deps
    where
        typeableDep :: Dep -> Maybe Name
typeableDep (TypeableDep (TH.ConT Name
n)) = forall a. a -> Maybe a
Just Name
n
        typeableDep Dep
_                         = forall a. Maybe a
Nothing

addTypeableDep :: TH.Type -> THCompile ()
addTypeableDep :: Pred -> THCompile ()
addTypeableDep Pred
ty = do
    Pred
ty' <- Pred -> THCompile Pred
normalizeAndResolve Pred
ty
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.insert forall a b. (a -> b) -> a -> b
$ Pred -> Dep
TypeableDep Pred
ty'

addLiftDep :: TH.Type -> THCompile ()
addLiftDep :: Pred -> THCompile ()
addLiftDep Pred
ty = do
    Pred
ty' <- Pred -> THCompile Pred
normalizeAndResolve Pred
ty
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.insert forall a b. (a -> b) -> a -> b
$ Pred -> Dep
LiftDep Pred
ty'

-- Constraints

-- | Make a 'Typeable' constraint.
typeablePir :: TH.Type -> TH.Type -> TH.Type
typeablePir :: Pred -> Pred -> Pred
typeablePir Pred
uni Pred
ty = Name -> [Pred] -> Pred
TH.classPred ''Typeable [Pred
uni, Pred
ty]

-- | Make a 'Lift' constraint.
liftPir :: TH.Type -> TH.Type -> TH.Type
liftPir :: Pred -> Pred -> Pred
liftPir Pred
uni Pred
ty = Name -> [Pred] -> Pred
TH.classPred ''Lift [Pred
uni, Pred
ty]

toConstraint :: TH.Type -> Dep -> TH.Pred
toConstraint :: Pred -> Dep -> Pred
toConstraint Pred
uni = \case
    TypeableDep Pred
n -> Pred -> Pred -> Pred
typeablePir Pred
uni Pred
n
    LiftDep Pred
ty    -> Pred -> Pred -> Pred
liftPir Pred
uni Pred
ty

{- Note [Closed constraints]
There is no point adding constraints that are "closed", i.e. don't mention any of the
instance type variables. These will either be satisfied by other instances in scope
(in which case GHC will complain at you), or be unsatisfied in which case the user will
get a useful error anyway.
-}

isClosedConstraint :: TH.Pred -> Bool
isClosedConstraint :: Pred -> Bool
isClosedConstraint = forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TypeSubstitution a => a -> [Name]
TH.freeVariables

-- | Convenience wrapper around 'normalizeType' and 'TH.resolveTypeSynonyms'.
normalizeAndResolve :: TH.Type -> THCompile TH.Type
normalizeAndResolve :: Pred -> THCompile Pred
normalizeAndResolve Pred
ty = Pred -> Pred
normalizeType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift forall a b. (a -> b) -> a -> b
$ Pred -> Q Pred
TH.resolveTypeSynonyms Pred
ty)

-- See Note [Ordering of constructors]
sortedCons :: TH.DatatypeInfo -> [TH.ConstructorInfo]
sortedCons :: DatatypeInfo -> [ConstructorInfo]
sortedCons TH.DatatypeInfo{datatypeName :: DatatypeInfo -> Name
TH.datatypeName=Name
tyName, datatypeCons :: DatatypeInfo -> [ConstructorInfo]
TH.datatypeCons=[ConstructorInfo]
cons} =
    -- We need to compare 'TH.Name's on their string name *not* on the unique
    let sorted :: [ConstructorInfo]
sorted = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(ConstructorInfo -> Name
TH.constructorName -> (TH.Name OccName
o1 NameFlavour
_)) (ConstructorInfo -> Name
TH.constructorName -> (TH.Name OccName
o2 NameFlavour
_)) -> forall a. Ord a => a -> a -> Ordering
compare OccName
o1 OccName
o2) [ConstructorInfo]
cons
    in if Name
tyName forall a. Eq a => a -> a -> Bool
== ''Bool Bool -> Bool -> Bool
|| Name
tyName forall a. Eq a => a -> a -> Bool
== ''[] then forall a. [a] -> [a]
reverse [ConstructorInfo]
sorted else [ConstructorInfo]
sorted

#if MIN_VERSION_template_haskell(2,17,0)
tvNameAndKind :: TH.TyVarBndrUnit -> THCompile (TH.Name, Kind ())
tvNameAndKind :: TyVarBndrUnit -> THCompile (Name, Kind ())
tvNameAndKind = \case
    TH.KindedTV Name
name ()
_ Pred
kind -> do
        Kind ()
kind' <- (Pred -> THCompile (Kind ())
compileKind forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Pred -> THCompile Pred
normalizeAndResolve) Pred
kind
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
name, Kind ()
kind')
    -- TODO: is this what PlainTV actually means? That it's of kind Type?
    TH.PlainTV Name
name ()
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
name, forall ann. ann -> Kind ann
Type ())
#else
tvNameAndKind :: TH.TyVarBndr -> THCompile (TH.Name, Kind ())
tvNameAndKind = \case
    TH.KindedTV name kind -> do
        kind' <- (compileKind <=< normalizeAndResolve) kind
        pure (name, kind')
    -- TODO: is this what PlainTV actually means? That it's of kind Type?
    TH.PlainTV name -> pure (name, Type ())
#endif

------------------
-- Types and kinds
------------------

-- Note: we can actually do this entirely at TH-time, which is nice
compileKind :: TH.Kind -> THCompile (Kind ())
compileKind :: Pred -> THCompile (Kind ())
compileKind = \case
    Pred
TH.StarT                          -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall ann. ann -> Kind ann
Type ()
    TH.AppT (TH.AppT Pred
TH.ArrowT Pred
k1) Pred
k2 -> forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pred -> THCompile (Kind ())
compileKind Pred
k1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pred -> THCompile (Kind ())
compileKind Pred
k2
    Pred
k                                 -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Pred -> LiftError
UnsupportedLiftKind Pred
k

compileType :: TH.Type -> THCompile (TH.TExpQ CompileTypeScope)
compileType :: Pred -> THCompile (TExpQ CompileTypeScope)
compileType = \case
    TH.AppT Pred
t1 Pred
t2 -> do
        TExpQ CompileTypeScope
t1' <- Pred -> THCompile (TExpQ CompileTypeScope)
compileType Pred
t1
        TExpQ CompileTypeScope
t2' <- Pred -> THCompile (TExpQ CompileTypeScope)
compileType Pred
t2
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice forall a b. (a -> b) -> a -> b
$ [|| CompileTypeScope (TyApp () <$> unCompileTypeScope ($$(TH.liftSplice t1')) <*> unCompileTypeScope ($$(TH.liftSplice t2'))) ||]
    t :: Pred
t@(TH.ConT Name
name) -> Pred -> Name -> THCompile (TExpQ CompileTypeScope)
compileTypeableType Pred
t Name
name
    -- See note [Type variables]
    t :: Pred
t@(TH.VarT Name
name) -> do
        Bool
isLocal <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (forall a. Ord a => a -> Set a -> Bool
Set.member Name
name)
        if Bool
isLocal
        then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice forall a b. (a -> b) -> a -> b
$ [||
              CompileTypeScope $ do
                  vars <- ask
                  case Map.lookup name vars of
                      Just ty -> pure ty
                      Nothing -> Prelude.throw $ LiftMissingVar name
             ||]
        else Pred -> Name -> THCompile (TExpQ CompileTypeScope)
compileTypeableType Pred
t Name
name
    Pred
t -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Pred -> LiftError
UnsupportedLiftType Pred
t

-- | Compile a type with the given name using 'typeRep' and incurring a corresponding 'Typeable' dependency.
compileTypeableType :: TH.Type -> TH.Name -> THCompile (TH.TExpQ CompileTypeScope)
compileTypeableType :: Pred -> Name -> THCompile (TExpQ CompileTypeScope)
compileTypeableType Pred
ty Name
name = do
    Pred -> THCompile ()
addTypeableDep Pred
ty
    -- We need the `unsafeTExpCoerce` since this will necessarily involve
    -- types we don't know now: the type which this instance is for (which
    -- appears in the proxy argument). However, since we know the type of
    -- `typeRep` we can get back into typed land quickly.
    let trep :: TH.TExpQ CompileType
        trep :: TExpQ CompileType
trep = forall a (m :: * -> *). Quote m => m Exp -> m (TExp a)
TH.unsafeTExpCoerce [| CompileType (typeRep (Proxy :: Proxy $(pure ty))) |]
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice forall a b. (a -> b) -> a -> b
$ [||
          let trep' :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
              trep' = Trans.lift $ unCompileType ($$(TH.liftSplice trep))
          in CompileTypeScope $ do
              maybeType <- lookupType () name
              case maybeType of
                  Just t  -> pure t
                  -- this will need some additional constraints in scope
                  Nothing -> trep'
          ||]

-----------
-- Typeable
-----------

-- TODO: try and make this work with type applications
-- | Class for types which have a corresponding Plutus IR type. Instances should always be derived, do not write
-- your own instance!
class Typeable uni (a :: k) where
    -- | Get the Plutus IR type corresponding to this type.
    typeRep :: Proxy a -> RTCompile uni fun (Type TyName uni ())

-- Just here so we can pin down the type variables without using TypeApplications in the generated code
recordAlias' :: TH.Name -> RTCompileScope PLC.DefaultUni fun ()
recordAlias' :: forall fun. Name -> RTCompileScope DefaultUni fun ()
recordAlias' = forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> m ()
recordAlias

-- Just here so we can pin down the type variables without using TypeApplications in the generated code
defineDatatype' :: TH.Name -> DatatypeDef TyName Name PLC.DefaultUni () -> Set.Set TH.Name -> RTCompileScope PLC.DefaultUni fun ()
defineDatatype' :: forall fun.
Name
-> DatatypeDef TyName Name DefaultUni ()
-> THLocalVars
-> RTCompileScope DefaultUni fun ()
defineDatatype' = forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> DatatypeDef TyName Name uni ann -> Set key -> m ()
defineDatatype

-- TODO: there is an unpleasant amount of duplication between this and the main compiler, but
-- I'm not sure how to unify them better
compileTypeRep :: TH.DatatypeInfo -> THCompile (TH.TExpQ CompileType)
compileTypeRep :: DatatypeInfo -> THCompile (TExpQ CompileType)
compileTypeRep dt :: DatatypeInfo
dt@TH.DatatypeInfo{datatypeName :: DatatypeInfo -> Name
TH.datatypeName=Name
tyName, datatypeVars :: DatatypeInfo -> [TyVarBndrUnit]
TH.datatypeVars=[TyVarBndrUnit]
tvs} = do
    [(Name, Kind ())]
tvNamesAndKinds <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TyVarBndrUnit -> THCompile (Name, Kind ())
tvNameAndKind [TyVarBndrUnit]
tvs
    -- annoyingly th-abstraction doesn't give us a kind we can compile here
    let typeKind :: Kind ()
typeKind = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
_, Kind ()
k) Kind ()
acc -> forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k Kind ()
acc) (forall ann. ann -> Kind ann
Type ()) [(Name, Kind ())]
tvNamesAndKinds
    let cons :: [ConstructorInfo]
cons = DatatypeInfo -> [ConstructorInfo]
sortedCons DatatypeInfo
dt

    forall (m :: * -> *) a.
MonadReader THLocalVars m =>
[Name] -> m a -> m a
thWithTyVars (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst [(Name, Kind ())]
tvNamesAndKinds) forall a b. (a -> b) -> a -> b
$ if DatatypeInfo -> Bool
isNewtype DatatypeInfo
dt
    then do
        -- Extract the unique field of the unique constructor
        TExpQ CompileTypeScope
argTy <- case [ConstructorInfo]
cons of
            [ TH.ConstructorInfo {constructorFields :: ConstructorInfo -> [Pred]
TH.constructorFields=[Pred
argTy]} ] -> (Pred -> THCompile (TExpQ CompileTypeScope)
compileType forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Pred -> THCompile Pred
normalizeAndResolve) Pred
argTy
            [ConstructorInfo]
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Text -> LiftError
UserLiftError Text
"Newtypes must have a single constructor with a single argument"
        THLocalVars
deps <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Deps -> THLocalVars
getTyConDeps
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice forall a b. (a -> b) -> a -> b
$ [||
            let
                argTy' :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
                argTy' = unCompileTypeScope $$(TH.liftSplice argTy)
                act :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
                act = do
                    maybeDefined <- lookupType () tyName
                    case maybeDefined of
                        Just ty -> pure ty
                        Nothing -> do
                            (_, dtvd) <- mkTyVarDecl tyName typeKind
                            tvds <- traverse (uncurry mkTyVarDecl) tvNamesAndKinds

                            alias <- withTyVars tvds $ mkIterTyLam (fmap snd tvds) <$> argTy'
                            defineType tyName (PLC.Def dtvd alias) deps
                            recordAlias' tyName
                            pure alias
            in CompileType $ runReaderT act mempty
         ||]
    else do
        [TExpQ CompileDeclFun]
constrExprs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ConstructorInfo -> THCompile (TExpQ CompileDeclFun)
compileConstructorDecl [ConstructorInfo]
cons
        THLocalVars
deps <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Deps -> THLocalVars
getTyConDeps
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice forall a b. (a -> b) -> a -> b
$ [||
          let
              constrExprs' :: [CompileDeclFun]
              constrExprs' = $$(TH.liftSplice $ tyListE constrExprs)
              act :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
              act = do
                maybeDefined <- lookupType () tyName
                case maybeDefined of
                    Just ty -> pure ty
                    Nothing -> do
                        (_, dtvd) <- mkTyVarDecl tyName typeKind
                        tvds <- traverse (uncurry mkTyVarDecl) tvNamesAndKinds

                        let resultType = mkIterTyApp () (mkTyVar () dtvd) (fmap (mkTyVar () . snd) tvds)
                        matchName <- safeFreshName (T.pack "match_" <> showName tyName)

                        -- See Note [Occurrences of recursive names]
                        let fakeDatatype = Datatype () dtvd [] matchName []

                        defineDatatype' tyName (PLC.Def dtvd fakeDatatype) Set.empty

                        withTyVars tvds $ do
                            -- The TH expressions are in fact all functions that take the result type, so
                            -- we need to apply them
                            let constrActs :: RTCompileScope PLC.DefaultUni fun [VarDecl TyName Name PLC.DefaultUni ()]
                                constrActs = sequence $ fmap (\x -> unCompileDeclFun x) constrExprs' <*> [resultType]
                            constrs <- constrActs

                            let datatype = Datatype () dtvd (fmap snd tvds) matchName constrs

                            defineDatatype tyName (PLC.Def dtvd datatype) deps
                        pure $ mkTyVar () dtvd
          in CompileType $ runReaderT act mempty
          ||]

compileConstructorDecl
    :: TH.ConstructorInfo
    -> THCompile (TH.TExpQ CompileDeclFun)
compileConstructorDecl :: ConstructorInfo -> THCompile (TExpQ CompileDeclFun)
compileConstructorDecl TH.ConstructorInfo{constructorName :: ConstructorInfo -> Name
TH.constructorName=Name
name, constructorFields :: ConstructorInfo -> [Pred]
TH.constructorFields=[Pred]
argTys} = do
    [TExpQ CompileTypeScope]
tyExprs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Pred -> THCompile (TExpQ CompileTypeScope)
compileType forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Pred -> THCompile Pred
normalizeAndResolve) [Pred]
argTys
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice forall a b. (a -> b) -> a -> b
$ [||
         let
             tyExprs' :: forall fun . [RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())]
             tyExprs' = fmap (\x -> unCompileTypeScope x) $$(TH.liftSplice $ tyListE tyExprs)
          -- we won't know the result type until runtime, so take it as an argument
          in CompileDeclFun $ \resultType -> do
              tys' <- sequence tyExprs'
              let constrTy = mkIterTyFun () tys' resultType
              constrName <- safeFreshName $ showName name
              pure $ VarDecl () constrName constrTy
          ||]

makeTypeable :: TH.Type -> TH.Name -> TH.Q [TH.Dec]
makeTypeable :: Pred -> Name -> Q [Dec]
makeTypeable Pred
uni Name
name = do
    Extension -> Q ()
requireExtension Extension
TH.ScopedTypeVariables

    DatatypeInfo
info <- Name -> Q DatatypeInfo
TH.reifyDatatype Name
name
    (TExpQ CompileType
rhs, Deps
deps) <- forall a. THCompile a -> Q (a, Deps)
runTHCompile forall a b. (a -> b) -> a -> b
$ DatatypeInfo -> THCompile (TExpQ CompileType)
compileTypeRep DatatypeInfo
info

    -- See Note [Closed constraints]
    let constraints :: [Pred]
constraints = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Bool
isClosedConstraint) forall a b. (a -> b) -> a -> b
$ Pred -> Dep -> Pred
toConstraint Pred
uni forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Set a -> [a]
Set.toList Deps
deps
    -- We need to unwrap the wrapper at the last minute, see Note [Impredicative function universe wrappers]
    let unwrappedRhs :: Q Exp
unwrappedRhs = [| unCompileType |] forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`TH.appE` forall a (m :: * -> *). Quote m => m (TExp a) -> m Exp
TH.unTypeQ TExpQ CompileType
rhs

    Dec
decl <- forall (m :: * -> *). Quote m => Name -> [m Clause] -> m Dec
TH.funD 'typeRep [forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
TH.clause [forall (m :: * -> *). Quote m => m Pat
TH.wildP] (forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB Q Exp
unwrappedRhs) []]
    forall (f :: * -> *) a. Applicative f => a -> f a
pure [Maybe Overlap -> [Pred] -> Pred -> [Dec] -> Dec
TH.InstanceD forall a. Maybe a
Nothing [Pred]
constraints (Pred -> Pred -> Pred
typeablePir Pred
uni (Name -> Pred
TH.ConT Name
name)) [Dec
decl]]

-------
-- Lift
-------

-- | Class for types which can be lifted into Plutus IR. Instances should be derived, do not write your
-- own instance!
class Lift uni a where
    -- | Get a Plutus IR term corresponding to the given value.
    lift :: a -> RTCompile uni fun (Term TyName Name uni fun ())

compileLift :: TH.DatatypeInfo -> THCompile [TH.Q TH.Clause]
compileLift :: DatatypeInfo -> THCompile [Q Clause]
compileLift DatatypeInfo
dt = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (DatatypeInfo -> Int -> ConstructorInfo -> THCompile (Q Clause)
compileConstructorClause DatatypeInfo
dt)) (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (DatatypeInfo -> [ConstructorInfo]
sortedCons DatatypeInfo
dt))

compileConstructorClause
    :: TH.DatatypeInfo -> Int -> TH.ConstructorInfo -> THCompile (TH.Q TH.Clause)
compileConstructorClause :: DatatypeInfo -> Int -> ConstructorInfo -> THCompile (Q Clause)
compileConstructorClause dt :: DatatypeInfo
dt@TH.DatatypeInfo{datatypeName :: DatatypeInfo -> Name
TH.datatypeName=Name
tyName, datatypeVars :: DatatypeInfo -> [TyVarBndrUnit]
TH.datatypeVars=[TyVarBndrUnit]
tvs} Int
index TH.ConstructorInfo{constructorName :: ConstructorInfo -> Name
TH.constructorName=Name
name, constructorFields :: ConstructorInfo -> [Pred]
TH.constructorFields=[Pred]
argTys} = do
    -- need to be able to lift the argument types
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Pred -> THCompile ()
addLiftDep [Pred]
argTys

    -- We need the actual type parameters for the non-newtype case, and we have to do
    -- it out here, but it will give us redundant constraints in the newtype case,
    -- so we fudge it.
    [TExpQ CompileTypeScope]
tyExprs <- if DatatypeInfo -> Bool
isNewtype DatatypeInfo
dt then forall (f :: * -> *) a. Applicative f => a -> f a
pure [] else forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [TyVarBndrUnit]
tvs forall a b. (a -> b) -> a -> b
$ \TyVarBndrUnit
tv -> do
      (Name
n, Kind ()
_) <- TyVarBndrUnit -> THCompile (Name, Kind ())
tvNameAndKind TyVarBndrUnit
tv
      Pred -> THCompile (TExpQ CompileTypeScope)
compileType (Name -> Pred
TH.VarT Name
n)

    -- Build the patter for the clause definition. All the argument will be called "arg".
    [Name]
patNames <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Pred]
argTys forall a b. (a -> b) -> a -> b
$ \Pred
_ -> forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"arg"
    let pat :: Q Pat
pat = forall (m :: * -> *). Quote m => Name -> [m Pat] -> m Pat
TH.conP Name
name (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *). Quote m => Name -> m Pat
TH.varP [Name]
patNames)

    -- `lift arg` for each arg we bind in the pattern. We need the `unsafeTExpCoerce` since this will
    -- necessarily involve types we don't know now: the types of each argument. However, since we
    -- know the type of `lift arg` we can get back into typed land quickly.
    let liftExprs :: [TH.TExpQ (RTCompile PLC.DefaultUni fun (Term TyName Name PLC.DefaultUni fun ()))]
        liftExprs :: forall fun.
[TExpQ
   (RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ()))]
liftExprs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Name
pn -> forall a (m :: * -> *). Quote m => m Exp -> m (TExp a)
TH.unsafeTExpCoerce forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE 'lift forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`TH.appE` forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
pn) [Name]
patNames

    TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
rhsExpr <- if DatatypeInfo -> Bool
isNewtype DatatypeInfo
dt
            then case forall fun.
[TExpQ
   (RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ()))]
liftExprs of
                    [TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
argExpr] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
argExpr
                    [TExpQ
   (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))]
_         -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ Text -> LiftError
UserLiftError Text
"Newtypes must have a single constructor with a single argument"
            else
                forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice forall a b. (a -> b) -> a -> b
$ [||
                    -- We bind all the splices with explicit signatures to ensure we
                    -- get type errors as soon as possible, and to aid debugging.
                    let
                        liftExprs' :: forall fun . [RTCompile PLC.DefaultUni fun (Term TyName Name PLC.DefaultUni fun ())]
                        liftExprs' = $$(TH.liftSplice $ tyListE liftExprs)
                        -- We need the `unsafeTExpCoerce` since this will necessarily involve
                        -- types we don't know now: the type which this instance is for (which
                        -- appears in the proxy argument). However, since we know the type of
                        -- `typeRep` we can get back into typed land quickly.
                        trep :: forall fun . RTCompile PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
                        trep = $$(TH.unsafeSpliceCoerce [| typeRep (Proxy :: Proxy $(TH.conT tyName)) |])
                    in do
                        -- force creation of datatype
                        _ <- trep

                        -- get the right constructor
                        maybeConstructors <- lookupConstructors () tyName
                        constrs <- case maybeConstructors of
                            Nothing -> Prelude.throw $ LiftMissingDataCons tyName
                            Just cs -> pure cs
                        let constr = constrs !! index

                        lifts :: [Term TyName Name PLC.DefaultUni fun ()] <- sequence liftExprs'
                        -- The 'fun' that is referenced here is the 'fun' that we bind the line above.
                        -- If it was forall-bound instead, 'typeExprs\'' wouldn't type check,
                        -- because 'Type' does not determine 'fun' (unlike 'Term' in 'liftExprs\''
                        -- above).
                        let tyExprs' :: [RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())]
                            tyExprs' = fmap (\x -> unCompileTypeScope x) $$(TH.liftSplice $ tyListE tyExprs)
                        -- The types are compiled in an (empty) local scope.
                        types <- flip runReaderT mempty $ sequence tyExprs'

                        pure $ mkIterApp () (mkIterInst () constr types) lifts
                  ||]
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
TH.clause [Q Pat
pat] (forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). Quote m => m (TExp a) -> m Exp
TH.unTypeQ TExpQ
  (RTCompile DefaultUni Any (Term TyName Name DefaultUni Any ()))
rhsExpr) []

makeLift :: TH.Name -> TH.Q [TH.Dec]
makeLift :: Name -> Q [Dec]
makeLift Name
name = do
    Extension -> Q ()
requireExtension Extension
TH.ScopedTypeVariables

    let uni :: Pred
uni = Name -> Pred
TH.ConT ''PLC.DefaultUni
    -- we need this too if we're lifting
    [Dec]
typeableDecs <- Pred -> Name -> Q [Dec]
makeTypeable Pred
uni Name
name
    DatatypeInfo
info <- Name -> Q DatatypeInfo
TH.reifyDatatype Name
name

    let datatypeType :: Pred
datatypeType = DatatypeInfo -> Pred
TH.datatypeType DatatypeInfo
info

    ([Q Clause]
clauses, Deps
deps) <- forall a. THCompile a -> Q (a, Deps)
runTHCompile forall a b. (a -> b) -> a -> b
$ DatatypeInfo -> THCompile [Q Clause]
compileLift DatatypeInfo
info

    {-
    Here we *do* need to add some constraints, because we're going to generate things like
    `instance Lift a => Lift (Maybe a)`. We can't just leave these open because they refer to type variables.

    We *could* put in a Typeable constraint for the type itself. This is somewhat more correct,
    but GHC warns us if we do this because we always also define the instance alongside. So we just
    leave it out.

    We also need to remove any Lift constraints we get for the type we're defining. This can happen if
    we're recursive, since we'll probably end up with constructor arguments of the current type.
    We don't want `instance Lift [a] => Lift [a]`!
    -}
    let prunedDeps :: Deps
prunedDeps = forall a. Ord a => a -> Set a -> Set a
Set.delete (Pred -> Dep
LiftDep Pred
datatypeType) Deps
deps
    -- See Note [Closed constraints]
    let constraints :: [Pred]
constraints = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Bool
isClosedConstraint) forall a b. (a -> b) -> a -> b
$ Pred -> Dep -> Pred
toConstraint Pred
uni forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Set a -> [a]
Set.toList Deps
prunedDeps

    Dec
decl <- forall (m :: * -> *). Quote m => Name -> [m Clause] -> m Dec
TH.funD 'lift [Q Clause]
clauses
    let liftDecs :: [Dec]
liftDecs = [Maybe Overlap -> [Pred] -> Pred -> [Dec] -> Dec
TH.InstanceD forall a. Maybe a
Nothing [Pred]
constraints (Pred -> Pred -> Pred
liftPir Pred
uni Pred
datatypeType) [Dec
decl]]
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Dec]
typeableDecs forall a. [a] -> [a] -> [a]
++ [Dec]
liftDecs

-- | In case of exception, it will call `fail` in TemplateHaskell
runTHCompile :: THCompile a -> TH.Q (a, Deps)
runTHCompile :: forall a. THCompile a -> Q (a, Deps)
runTHCompile THCompile a
m = do
    Either LiftError (a, Deps)
res <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
          forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT forall a. Monoid a => a
mempty THCompile a
m
    case Either LiftError (a, Deps)
res of
        Left LiftError
a  -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Generating Lift instances: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a ann. Pretty a => a -> Doc ann
PP.pretty LiftError
a)
        Right (a, Deps)
b -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a, Deps)
b