-- 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          #-}
-- It is complex to mix TH with polymorphisms. Core lint can sometimes catch problems
-- caused by using polymorphisms the wrong way, e.g., accidentally using impredicative types.
{-# OPTIONS_GHC -dcore-lint #-}
module PlutusTx.Lift.TH (
    makeTypeable
    , makeLift
    , LiftError (..)
    ) where

import PlutusTx.Lift.Class
import PlutusTx.Lift.THUtils

import PlutusIR
import PlutusIR.Compiler.Definitions
import PlutusIR.Compiler.Names
import PlutusIR.MkPir hiding (constr)

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

import Control.Monad ((<=<))
import Control.Monad.Except (ExceptT, runExceptT, throwError)
import Control.Monad.Reader (MonadReader, ReaderT, ask, asks, local, runReaderT)
import Control.Monad.State (StateT, gets, modify, runStateT)
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 Prettyprinter qualified as PP

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

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
(Typeable LiftError, Show LiftError) =>
(LiftError -> SomeException)
-> (SomeException -> Maybe LiftError)
-> (LiftError -> String)
-> Exception LiftError
SomeException -> Maybe LiftError
LiftError -> String
LiftError -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> String) -> Exception e
$ctoException :: LiftError -> SomeException
toException :: LiftError -> SomeException
$cfromException :: SomeException -> Maybe LiftError
fromException :: SomeException -> Maybe LiftError
$cdisplayException :: LiftError -> String
displayException :: LiftError -> String
Prelude.Exception)

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

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

{- 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 CompileTerm = CompileTerm
  { CompileTerm
-> forall fun.
   RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ())
unCompileTerm ::
      forall fun.
      RTCompile PLC.DefaultUni fun (Term TyName Name PLC.DefaultUni fun ())
  }
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

{- 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
(Int -> Dep -> ShowS)
-> (Dep -> String) -> ([Dep] -> ShowS) -> Show Dep
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Dep -> ShowS
showsPrec :: Int -> Dep -> ShowS
$cshow :: Dep -> String
show :: Dep -> String
$cshowList :: [Dep] -> ShowS
showList :: [Dep] -> ShowS
Show, Dep -> Dep -> Bool
(Dep -> Dep -> Bool) -> (Dep -> Dep -> Bool) -> Eq Dep
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Dep -> Dep -> Bool
== :: Dep -> Dep -> Bool
$c/= :: Dep -> Dep -> Bool
/= :: Dep -> Dep -> Bool
Eq, Eq Dep
Eq Dep =>
(Dep -> Dep -> Ordering)
-> (Dep -> Dep -> Bool)
-> (Dep -> Dep -> Bool)
-> (Dep -> Dep -> Bool)
-> (Dep -> Dep -> Bool)
-> (Dep -> Dep -> Dep)
-> (Dep -> Dep -> Dep)
-> Ord 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
$ccompare :: Dep -> Dep -> Ordering
compare :: Dep -> Dep -> Ordering
$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
>= :: Dep -> Dep -> Bool
$cmax :: Dep -> Dep -> Dep
max :: Dep -> Dep -> Dep
$cmin :: Dep -> Dep -> Dep
min :: Dep -> Dep -> Dep
Ord)
type Deps = Set.Set Dep

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 = (LocalVars uni -> LocalVars uni) -> m a -> m a
forall a. (LocalVars uni -> LocalVars uni) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\LocalVars uni
scope -> (LocalVars uni -> (Name, TyVarDecl TyName ()) -> LocalVars uni)
-> LocalVars uni -> [(Name, TyVarDecl TyName ())] -> LocalVars uni
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\LocalVars uni
acc (Name
n, TyVarDecl TyName ()
tvd) -> Name -> Type TyName uni () -> LocalVars uni -> LocalVars uni
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (() -> TyVarDecl TyName () -> Type TyName uni ()
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 = (THLocalVars -> THLocalVars) -> m a -> m a
forall a. (THLocalVars -> THLocalVars) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\THLocalVars
scope -> (Name -> THLocalVars -> THLocalVars)
-> THLocalVars -> [Name] -> THLocalVars
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> THLocalVars -> THLocalVars
forall a. Ord a => a -> Set a -> Set a
Set.insert THLocalVars
scope [Name]
names)

-- | 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 = [Name] -> THLocalVars
forall a. Ord a => [a] -> Set a
Set.fromList ([Name] -> THLocalVars) -> [Name] -> THLocalVars
forall a b. (a -> b) -> a -> b
$ (Dep -> Maybe Name) -> [Dep] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Dep -> Maybe Name
typeableDep ([Dep] -> [Name]) -> [Dep] -> [Name]
forall a b. (a -> b) -> a -> b
$ Deps -> [Dep]
forall a. Set a -> [a]
Set.toList Deps
deps
    where
        typeableDep :: Dep -> Maybe Name
typeableDep (TypeableDep (TH.ConT Name
n)) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
        typeableDep Dep
_                         = Maybe Name
forall a. Maybe a
Nothing

addTypeableDep :: TH.Type -> THCompile ()
addTypeableDep :: Pred -> THCompile ()
addTypeableDep Pred
ty = do
    Pred
ty' <- Pred -> THCompile Pred
normalizeAndResolve Pred
ty
    (Deps -> Deps) -> THCompile ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Deps -> Deps) -> THCompile ()) -> (Deps -> Deps) -> THCompile ()
forall a b. (a -> b) -> a -> b
$ Dep -> Deps -> Deps
forall a. Ord a => a -> Set a -> Set a
Set.insert (Dep -> Deps -> Deps) -> Dep -> Deps -> Deps
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
    (Deps -> Deps) -> THCompile ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Deps -> Deps) -> THCompile ()) -> (Deps -> Deps) -> THCompile ()
forall a b. (a -> b) -> a -> b
$ Dep -> Deps -> Deps
forall a. Ord a => a -> Set a -> Set a
Set.insert (Dep -> Deps -> Deps) -> Dep -> Deps -> Deps
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 = [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Name] -> Bool) -> (Pred -> [Name]) -> Pred -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> [Name]
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 (Pred -> Pred) -> THCompile Pred -> THCompile Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ReaderT THLocalVars (ExceptT LiftError Q) Pred -> THCompile Pred
forall (m :: * -> *) a. Monad m => m a -> StateT Deps m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (ReaderT THLocalVars (ExceptT LiftError Q) Pred -> THCompile Pred)
-> ReaderT THLocalVars (ExceptT LiftError Q) Pred -> THCompile Pred
forall a b. (a -> b) -> a -> b
$ ExceptT LiftError Q Pred
-> ReaderT THLocalVars (ExceptT LiftError Q) Pred
forall (m :: * -> *) a. Monad m => m a -> ReaderT THLocalVars m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (ExceptT LiftError Q Pred
 -> ReaderT THLocalVars (ExceptT LiftError Q) Pred)
-> ExceptT LiftError Q Pred
-> ReaderT THLocalVars (ExceptT LiftError Q) Pred
forall a b. (a -> b) -> a -> b
$ Q Pred -> ExceptT LiftError Q Pred
forall (m :: * -> *) a. Monad m => m a -> ExceptT LiftError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (Q Pred -> ExceptT LiftError Q Pred)
-> Q Pred -> ExceptT LiftError Q Pred
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 = (ConstructorInfo -> ConstructorInfo -> Ordering)
-> [ConstructorInfo] -> [ConstructorInfo]
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
_)) -> OccName -> OccName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare OccName
o1 OccName
o2) [ConstructorInfo]
cons
    in if Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Bool Bool -> Bool -> Bool
|| Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''[] then [ConstructorInfo] -> [ConstructorInfo]
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 (Pred -> THCompile (Kind ()))
-> (Pred -> THCompile Pred) -> Pred -> THCompile (Kind ())
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Pred -> THCompile Pred
normalizeAndResolve) Pred
kind
        (Name, Kind ()) -> THCompile (Name, Kind ())
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
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 ()
_ -> (Name, Kind ()) -> THCompile (Name, Kind ())
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
name, () -> Kind ()
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                          -> Kind () -> THCompile (Kind ())
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> THCompile (Kind ())) -> Kind () -> THCompile (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
    TH.AppT (TH.AppT Pred
TH.ArrowT Pred
k1) Pred
k2 -> () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (Kind () -> Kind () -> Kind ())
-> THCompile (Kind ())
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (Kind () -> Kind ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pred -> THCompile (Kind ())
compileKind Pred
k1 StateT
  Deps
  (ReaderT THLocalVars (ExceptT LiftError Q))
  (Kind () -> Kind ())
-> THCompile (Kind ()) -> THCompile (Kind ())
forall a b.
StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) (a -> b)
-> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
-> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pred -> THCompile (Kind ())
compileKind Pred
k2
    Pred
k                                 -> LiftError -> THCompile (Kind ())
forall a.
LiftError
-> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LiftError -> THCompile (Kind ()))
-> LiftError -> THCompile (Kind ())
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
        TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> (Splice Q CompileTypeScope -> TExpQ CompileTypeScope)
-> Splice Q CompileTypeScope
-> THCompile (TExpQ CompileTypeScope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Splice Q CompileTypeScope -> TExpQ CompileTypeScope
forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice (Splice Q CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> Splice Q CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall a b. (a -> b) -> a -> b
$ [|| (forall fun.
 RTCompileScope DefaultUni fun (Type TyName DefaultUni ()))
-> CompileTypeScope
CompileTypeScope (ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CompileTypeScope
-> forall fun.
   RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
unCompileTypeScope ($$(TExpQ CompileTypeScope -> Splice Q CompileTypeScope
forall a (m :: * -> *). m (TExp a) -> Splice m a
TH.liftSplice TExpQ CompileTypeScope
t1')) f (a -> b) -> f a -> f b
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CompileTypeScope
-> forall fun.
   RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
unCompileTypeScope ($$(TExpQ CompileTypeScope -> Splice Q CompileTypeScope
forall a (m :: * -> *). m (TExp a) -> Splice m a
TH.liftSplice TExpQ CompileTypeScope
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 <- (THLocalVars -> Bool)
-> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Name -> THLocalVars -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name
name)
        if Bool
isLocal
        then TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> (Splice Q CompileTypeScope -> TExpQ CompileTypeScope)
-> Splice Q CompileTypeScope
-> THCompile (TExpQ CompileTypeScope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Splice Q CompileTypeScope -> TExpQ CompileTypeScope
forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice (Splice Q CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> Splice Q CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall a b. (a -> b) -> a -> b
$ [||
              (forall fun.
 RTCompileScope DefaultUni fun (Type TyName DefaultUni ()))
-> CompileTypeScope
CompileTypeScope (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ do
                  a
vars <- m r
forall r (m :: * -> *). MonadReader r m => m r
ask
                  case k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name a
vars of
                      Just a
ty -> a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
ty
                      Maybe a
Nothing -> e -> a
forall a e. Exception e => e -> a
Prelude.throw (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Name -> LiftError
LiftMissingVar Name
name
             ||]
        else Pred -> Name -> THCompile (TExpQ CompileTypeScope)
compileTypeableType Pred
t Name
name
    Pred
t -> LiftError -> THCompile (TExpQ CompileTypeScope)
forall a.
LiftError
-> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LiftError -> THCompile (TExpQ CompileTypeScope))
-> LiftError -> THCompile (TExpQ CompileTypeScope)
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 = Q Exp -> TExpQ CompileType
forall a (m :: * -> *). Quote m => m Exp -> m (TExp a)
TH.unsafeTExpCoerce [| CompileType (typeRep (Proxy :: Proxy $(Pred -> Q Pred
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pred
ty))) |]
    TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> (Splice Q CompileTypeScope -> TExpQ CompileTypeScope)
-> Splice Q CompileTypeScope
-> THCompile (TExpQ CompileTypeScope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Splice Q CompileTypeScope -> TExpQ CompileTypeScope
forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice (Splice Q CompileTypeScope -> THCompile (TExpQ CompileTypeScope))
-> Splice Q CompileTypeScope -> THCompile (TExpQ CompileTypeScope)
forall a b. (a -> b) -> a -> b
$ [||
          let trep' :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
              trep' :: forall fun.
RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
trep' = m a -> t m a
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ CompileType
-> forall fun. RTCompile DefaultUni fun (Type TyName DefaultUni ())
unCompileType ($$(TExpQ CompileType -> Splice Q CompileType
forall a (m :: * -> *). m (TExp a) -> Splice m a
TH.liftSplice TExpQ CompileType
trep))
          in (forall fun.
 RTCompileScope DefaultUni fun (Type TyName DefaultUni ()))
-> CompileTypeScope
CompileTypeScope (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ do
              a
maybeType <- ann -> key -> m (Maybe (Type TyName uni ann))
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe (Type TyName uni ann))
lookupType () Name
name
              case a
maybeType of
                  Just Type TyName uni ann
t  -> a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type TyName uni ann
t
                  -- this will need some additional constraints in scope
                  Maybe (Type TyName uni ann)
Nothing -> RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
forall fun.
RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
trep'
          ||]

-- 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' = Name
-> ReaderT (LocalVars DefaultUni) (RTCompile DefaultUni fun) ()
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' = Name
-> DatatypeDef TyName Name DefaultUni ()
-> THLocalVars
-> ReaderT (LocalVars DefaultUni) (RTCompile DefaultUni fun) ()
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 <- (TyVarBndrUnit -> THCompile (Name, Kind ()))
-> [TyVarBndrUnit]
-> StateT
     Deps (ReaderT THLocalVars (ExceptT LiftError Q)) [(Name, Kind ())]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [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 = ((Name, Kind ()) -> Kind () -> Kind ())
-> Kind () -> [(Name, Kind ())] -> Kind ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
_, Kind ()
k) Kind ()
acc -> () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k Kind ()
acc) (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) [(Name, Kind ())]
tvNamesAndKinds
    let cons :: [ConstructorInfo]
cons = DatatypeInfo -> [ConstructorInfo]
sortedCons DatatypeInfo
dt

    [Name]
-> THCompile (TExpQ CompileType) -> THCompile (TExpQ CompileType)
forall (m :: * -> *) a.
MonadReader THLocalVars m =>
[Name] -> m a -> m a
thWithTyVars (((Name, Kind ()) -> Name) -> [(Name, Kind ())] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Kind ()) -> Name
forall a b. (a, b) -> a
fst [(Name, Kind ())]
tvNamesAndKinds) (THCompile (TExpQ CompileType) -> THCompile (TExpQ CompileType))
-> THCompile (TExpQ CompileType) -> THCompile (TExpQ CompileType)
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 (Pred -> THCompile (TExpQ CompileTypeScope))
-> (Pred -> THCompile Pred)
-> Pred
-> THCompile (TExpQ CompileTypeScope)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Pred -> THCompile Pred
normalizeAndResolve) Pred
argTy
            [ConstructorInfo]
_ -> LiftError -> THCompile (TExpQ CompileTypeScope)
forall a.
LiftError
-> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LiftError -> THCompile (TExpQ CompileTypeScope))
-> LiftError -> THCompile (TExpQ CompileTypeScope)
forall a b. (a -> b) -> a -> b
$ Text -> LiftError
UserLiftError Text
"Newtypes must have a single constructor with a single argument"
        THLocalVars
deps <- (Deps -> THLocalVars)
-> StateT
     Deps (ReaderT THLocalVars (ExceptT LiftError Q)) THLocalVars
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Deps -> THLocalVars
getTyConDeps
        TExpQ CompileType -> THCompile (TExpQ CompileType)
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileType -> THCompile (TExpQ CompileType))
-> (Splice Q CompileType -> TExpQ CompileType)
-> Splice Q CompileType
-> THCompile (TExpQ CompileType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Splice Q CompileType -> TExpQ CompileType
forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice (Splice Q CompileType -> THCompile (TExpQ CompileType))
-> Splice Q CompileType -> THCompile (TExpQ CompileType)
forall a b. (a -> b) -> a -> b
$ [||
            let
                argTy' :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
                argTy' :: forall fun.
RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
argTy' = CompileTypeScope
-> forall fun.
   RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
unCompileTypeScope $$(TExpQ CompileTypeScope -> Splice Q CompileTypeScope
forall a (m :: * -> *). m (TExp a) -> Splice m a
TH.liftSplice TExpQ CompileTypeScope
argTy)
                act :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
                act :: forall fun.
RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
act = do
                    a
maybeDefined <- ann -> key -> m (Maybe (Type TyName uni ann))
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe (Type TyName uni ann))
lookupType () Name
tyName
                    case a
maybeDefined of
                        Just Type TyName uni ann
ty -> a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type TyName uni ann
ty
                        Maybe (Type TyName uni ann)
Nothing -> do
                            (Name
_, TyVarDecl TyName ()
dtvd) <- Name -> Kind () -> m (Name, TyVarDecl TyName ())
forall (m :: * -> *).
MonadQuote m =>
Name -> Kind () -> m (Name, TyVarDecl TyName ())
mkTyVarDecl Name
tyName Kind ()
typeKind
                            a
tvds <- (a -> f b) -> t a -> f (t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Kind () -> m (Name, TyVarDecl TyName ())
forall (m :: * -> *).
MonadQuote m =>
Name -> Kind () -> m (Name, TyVarDecl TyName ())
mkTyVarDecl) a
tvNamesAndKinds

                            a
alias <- [(Name, TyVarDecl TyName ())] -> m a -> m a
forall (uni :: * -> *) (m :: * -> *) a.
MonadReader (LocalVars uni) m =>
[(Name, TyVarDecl TyName ())] -> m a -> m a
withTyVars a
tvds (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ [TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, b) -> b
forall a b. (a, b) -> b
snd a
tvds) (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
forall fun.
RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
argTy'
                            key -> TypeDef TyName uni ann -> Set key -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> TypeDef TyName uni ann -> Set key -> m ()
defineType Name
tyName (var -> val -> Def var val
forall var val. var -> val -> Def var val
PLC.Def TyVarDecl TyName ()
dtvd a
alias) a
deps
                            Name -> RTCompileScope DefaultUni fun ()
forall fun. Name -> RTCompileScope DefaultUni fun ()
recordAlias' Name
tyName
                            a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
alias
            in (forall fun. RTCompile DefaultUni fun (Type TyName DefaultUni ()))
-> CompileType
CompileType (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ ReaderT r m a -> r -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
forall fun.
RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
act a
forall a. Monoid a => a
mempty
         ||]
    else do
        [TExpQ CompileDeclFun]
constrExprs <- (ConstructorInfo
 -> StateT
      Deps
      (ReaderT THLocalVars (ExceptT LiftError Q))
      (TExpQ CompileDeclFun))
-> [ConstructorInfo]
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     [TExpQ CompileDeclFun]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ConstructorInfo
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
compileConstructorDecl [ConstructorInfo]
cons
        THLocalVars
deps <- (Deps -> THLocalVars)
-> StateT
     Deps (ReaderT THLocalVars (ExceptT LiftError Q)) THLocalVars
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Deps -> THLocalVars
getTyConDeps
        TExpQ CompileType -> THCompile (TExpQ CompileType)
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileType -> THCompile (TExpQ CompileType))
-> (Splice Q CompileType -> TExpQ CompileType)
-> Splice Q CompileType
-> THCompile (TExpQ CompileType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Splice Q CompileType -> TExpQ CompileType
forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice (Splice Q CompileType -> THCompile (TExpQ CompileType))
-> Splice Q CompileType -> THCompile (TExpQ CompileType)
forall a b. (a -> b) -> a -> b
$ [||
          let
              constrExprs' :: [CompileDeclFun]
              constrExprs' :: [CompileDeclFun]
constrExprs' = $$(Q (TExp [CompileDeclFun]) -> Splice Q [CompileDeclFun]
forall a (m :: * -> *). m (TExp a) -> Splice m a
TH.liftSplice (Q (TExp [CompileDeclFun]) -> Splice Q [CompileDeclFun])
-> Q (TExp [CompileDeclFun]) -> Splice Q [CompileDeclFun]
forall a b. (a -> b) -> a -> b
$ [TExpQ CompileDeclFun] -> Q (TExp [CompileDeclFun])
forall a. [TExpQ a] -> TExpQ [a]
tyListE [TExpQ CompileDeclFun]
constrExprs)
              act :: forall fun . RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())
              act :: forall fun.
RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
act = do
                a
maybeDefined <- ann -> key -> m (Maybe (Type TyName uni ann))
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe (Type TyName uni ann))
lookupType () Name
tyName
                case a
maybeDefined of
                    Just Type TyName uni ann
ty -> a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type TyName uni ann
ty
                    Maybe (Type TyName uni ann)
Nothing -> do
                        (Name
_, TyVarDecl TyName ()
dtvd) <- Name -> Kind () -> m (Name, TyVarDecl TyName ())
forall (m :: * -> *).
MonadQuote m =>
Name -> Kind () -> m (Name, TyVarDecl TyName ())
mkTyVarDecl Name
tyName Kind ()
typeKind
                        a
tvds <- (a -> f b) -> t a -> f (t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Kind () -> m (Name, TyVarDecl TyName ())
forall (m :: * -> *).
MonadQuote m =>
Name -> Kind () -> m (Name, TyVarDecl TyName ())
mkTyVarDecl) a
tvNamesAndKinds

                        let resultType :: Type tyname uni ()
resultType = Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn (ann -> TyVarDecl tyname ann -> Type tyname uni ann
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () TyVarDecl TyName ()
dtvd) ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ann -> TyVarDecl tyname ann -> Type tyname uni ann
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> b
forall a b. (a, b) -> b
snd) a
tvds)
                        a
matchName <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
safeFreshName (String -> Text
T.pack String
"match_" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Name -> Text
showName Name
tyName)

                        -- See Note [Occurrences of recursive names]
                        let fakeDatatype :: Datatype tyname name uni a
fakeDatatype = a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype () TyVarDecl TyName ()
dtvd [] a
matchName []

                        Name
-> DatatypeDef TyName Name DefaultUni ()
-> THLocalVars
-> RTCompileScope DefaultUni fun ()
forall fun.
Name
-> DatatypeDef TyName Name DefaultUni ()
-> THLocalVars
-> RTCompileScope DefaultUni fun ()
defineDatatype' Name
tyName (var -> val -> Def var val
forall var val. var -> val -> Def var val
PLC.Def TyVarDecl TyName ()
dtvd Datatype TyName Name uni ()
forall {uni :: * -> *}. Datatype TyName Name uni ()
fakeDatatype) Set a
forall a. Set a
Set.empty

                        [(Name, TyVarDecl TyName ())] -> m a -> m a
forall (uni :: * -> *) (m :: * -> *) a.
MonadReader (LocalVars uni) m =>
[(Name, TyVarDecl TyName ())] -> m a -> m a
withTyVars a
tvds (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ 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 :: RTCompileScope DefaultUni fun [VarDecl TyName Name DefaultUni ()]
constrActs = t (m a) -> m (t a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => t (m a) -> m (t a)
sequence (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
x -> CompileDeclFun
-> forall fun.
   Type TyName DefaultUni ()
   -> RTCompileScope
        DefaultUni fun (VarDecl TyName Name DefaultUni ())
unCompileDeclFun a
x) [CompileDeclFun]
constrExprs' f (a -> b) -> f a -> f b
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
resultType]
                            a
constrs <- RTCompileScope DefaultUni fun [VarDecl TyName Name DefaultUni ()]
constrActs

                            let datatype :: Datatype tyname name uni a
datatype = a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype () TyVarDecl TyName ()
dtvd ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, b) -> b
forall a b. (a, b) -> b
snd a
tvds) a
matchName a
constrs

                            key -> DatatypeDef TyName Name uni ann -> Set key -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> DatatypeDef TyName Name uni ann -> Set key -> m ()
defineDatatype Name
tyName (var -> val -> Def var val
forall var val. var -> val -> Def var val
PLC.Def TyVarDecl TyName ()
dtvd Datatype TyName Name DefaultUni ()
datatype) a
deps
                        a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ ann -> TyVarDecl tyname ann -> Type tyname uni ann
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () TyVarDecl TyName ()
dtvd
          in (forall fun. RTCompile DefaultUni fun (Type TyName DefaultUni ()))
-> CompileType
CompileType (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ ReaderT r m a -> r -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
forall fun.
RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
act a
forall a. Monoid a => a
mempty
          ||]

compileConstructorDecl
    :: TH.ConstructorInfo
    -> THCompile (TH.TExpQ CompileDeclFun)
compileConstructorDecl :: ConstructorInfo
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
compileConstructorDecl TH.ConstructorInfo{constructorName :: ConstructorInfo -> Name
TH.constructorName=Name
name, constructorFields :: ConstructorInfo -> [Pred]
TH.constructorFields=[Pred]
argTys} = do
    [TExpQ CompileTypeScope]
tyExprs <- (Pred -> THCompile (TExpQ CompileTypeScope))
-> [Pred]
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     [TExpQ CompileTypeScope]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Pred -> THCompile (TExpQ CompileTypeScope)
compileType (Pred -> THCompile (TExpQ CompileTypeScope))
-> (Pred -> THCompile Pred)
-> Pred
-> THCompile (TExpQ CompileTypeScope)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Pred -> THCompile Pred
normalizeAndResolve) [Pred]
argTys
    TExpQ CompileDeclFun
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileDeclFun
 -> StateT
      Deps
      (ReaderT THLocalVars (ExceptT LiftError Q))
      (TExpQ CompileDeclFun))
-> (Splice Q CompileDeclFun -> TExpQ CompileDeclFun)
-> Splice Q CompileDeclFun
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Splice Q CompileDeclFun -> TExpQ CompileDeclFun
forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice (Splice Q CompileDeclFun
 -> StateT
      Deps
      (ReaderT THLocalVars (ExceptT LiftError Q))
      (TExpQ CompileDeclFun))
-> Splice Q CompileDeclFun
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileDeclFun)
forall a b. (a -> b) -> a -> b
$ [||
         let
             tyExprs' :: forall fun . [RTCompileScope PLC.DefaultUni fun (Type TyName PLC.DefaultUni ())]
             tyExprs' :: forall fun.
[RTCompileScope DefaultUni fun (Type TyName DefaultUni ())]
tyExprs' = (a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
x -> CompileTypeScope
-> forall fun.
   RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
unCompileTypeScope a
x) $$(Q (TExp [CompileTypeScope]) -> Splice Q [CompileTypeScope]
forall a (m :: * -> *). m (TExp a) -> Splice m a
TH.liftSplice (Q (TExp [CompileTypeScope]) -> Splice Q [CompileTypeScope])
-> Q (TExp [CompileTypeScope]) -> Splice Q [CompileTypeScope]
forall a b. (a -> b) -> a -> b
$ [TExpQ CompileTypeScope] -> Q (TExp [CompileTypeScope])
forall a. [TExpQ a] -> TExpQ [a]
tyListE [TExpQ CompileTypeScope]
tyExprs)
          -- we won't know the result type until runtime, so take it as an argument
          in (forall fun.
 Type TyName DefaultUni ()
 -> RTCompileScope
      DefaultUni fun (VarDecl TyName Name DefaultUni ()))
-> CompileDeclFun
CompileDeclFun (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ \Type TyName DefaultUni ()
resultType -> do
              a
tys' <- t (m a) -> m (t a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => t (m a) -> m (t a)
sequence [RTCompileScope DefaultUni fun (Type TyName DefaultUni ())]
forall fun.
[RTCompileScope DefaultUni fun (Type TyName DefaultUni ())]
tyExprs'
              let constrTy :: Type tyname uni ann
constrTy = ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () a
tys' Type TyName DefaultUni ()
resultType
              a
constrName <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
safeFreshName (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Name -> Text
showName Name
name
              a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () a
constrName Type TyName DefaultUni ()
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) <- THCompile (TExpQ CompileType) -> Q (TExpQ CompileType, Deps)
forall a. THCompile a -> Q (a, Deps)
runTHCompile (THCompile (TExpQ CompileType) -> Q (TExpQ CompileType, Deps))
-> THCompile (TExpQ CompileType) -> Q (TExpQ CompileType, Deps)
forall a b. (a -> b) -> a -> b
$ DatatypeInfo -> THCompile (TExpQ CompileType)
compileTypeRep DatatypeInfo
info

    -- See Note [Closed constraints]
    let constraints :: [Pred]
constraints = (Pred -> Bool) -> [Pred] -> [Pred]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Pred -> Bool) -> Pred -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Bool
isClosedConstraint) ([Pred] -> [Pred]) -> [Pred] -> [Pred]
forall a b. (a -> b) -> a -> b
$ Pred -> Dep -> Pred
toConstraint Pred
uni (Dep -> Pred) -> [Dep] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Deps -> [Dep]
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 |] Q Exp -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`TH.appE` TExpQ CompileType -> Q Exp
forall a (m :: * -> *). Quote m => m (TExp a) -> m Exp
TH.unTypeQ TExpQ CompileType
rhs

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

compileLift :: TH.DatatypeInfo -> THCompile [TH.Q TH.Clause]
compileLift :: DatatypeInfo -> THCompile [Q Clause]
compileLift DatatypeInfo
dt = ((Int, ConstructorInfo)
 -> StateT
      Deps (ReaderT THLocalVars (ExceptT LiftError Q)) (Q Clause))
-> [(Int, ConstructorInfo)] -> THCompile [Q Clause]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Int
 -> ConstructorInfo
 -> StateT
      Deps (ReaderT THLocalVars (ExceptT LiftError Q)) (Q Clause))
-> (Int, ConstructorInfo)
-> StateT
     Deps (ReaderT THLocalVars (ExceptT LiftError Q)) (Q Clause)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (DatatypeInfo
-> Int
-> ConstructorInfo
-> StateT
     Deps (ReaderT THLocalVars (ExceptT LiftError Q)) (Q Clause)
compileConstructorClause DatatypeInfo
dt)) ([Int] -> [ConstructorInfo] -> [(Int, ConstructorInfo)]
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
-> StateT
     Deps (ReaderT THLocalVars (ExceptT LiftError Q)) (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
    (Pred -> THCompile ()) -> [Pred] -> THCompile ()
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 [TExpQ CompileTypeScope]
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     [TExpQ CompileTypeScope]
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [] else [TyVarBndrUnit]
-> (TyVarBndrUnit -> THCompile (TExpQ CompileTypeScope))
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     [TExpQ CompileTypeScope]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [TyVarBndrUnit]
tvs ((TyVarBndrUnit -> THCompile (TExpQ CompileTypeScope))
 -> StateT
      Deps
      (ReaderT THLocalVars (ExceptT LiftError Q))
      [TExpQ CompileTypeScope])
-> (TyVarBndrUnit -> THCompile (TExpQ CompileTypeScope))
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     [TExpQ CompileTypeScope]
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 <- ReaderT THLocalVars (ExceptT LiftError Q) [Name]
-> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) [Name]
forall (m :: * -> *) a. Monad m => m a -> StateT Deps m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (ReaderT THLocalVars (ExceptT LiftError Q) [Name]
 -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) [Name])
-> ReaderT THLocalVars (ExceptT LiftError Q) [Name]
-> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) [Name]
forall a b. (a -> b) -> a -> b
$ ExceptT LiftError Q [Name]
-> ReaderT THLocalVars (ExceptT LiftError Q) [Name]
forall (m :: * -> *) a. Monad m => m a -> ReaderT THLocalVars m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (ExceptT LiftError Q [Name]
 -> ReaderT THLocalVars (ExceptT LiftError Q) [Name])
-> ExceptT LiftError Q [Name]
-> ReaderT THLocalVars (ExceptT LiftError Q) [Name]
forall a b. (a -> b) -> a -> b
$ Q [Name] -> ExceptT LiftError Q [Name]
forall (m :: * -> *) a. Monad m => m a -> ExceptT LiftError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Trans.lift (Q [Name] -> ExceptT LiftError Q [Name])
-> Q [Name] -> ExceptT LiftError Q [Name]
forall a b. (a -> b) -> a -> b
$ [Pred] -> (Pred -> Q Name) -> Q [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Pred]
argTys ((Pred -> Q Name) -> Q [Name]) -> (Pred -> Q Name) -> Q [Name]
forall a b. (a -> b) -> a -> b
$ \Pred
_ -> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"arg"
    let pat :: Q Pat
pat = Name -> [Q Pat] -> Q Pat
forall (m :: * -> *). Quote m => Name -> [m Pat] -> m Pat
TH.conP Name
name ((Name -> Q Pat) -> [Name] -> [Q Pat]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Q Pat
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 CompileTerm]
        liftExprs :: [TExpQ CompileTerm]
liftExprs = (Name -> TExpQ CompileTerm) -> [Name] -> [TExpQ CompileTerm]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Name
pn -> Q Exp -> TExpQ CompileTerm
forall a (m :: * -> *). Quote m => m Exp -> m (TExp a)
TH.unsafeTExpCoerce (Q Exp -> TExpQ CompileTerm) -> Q Exp -> TExpQ CompileTerm
forall a b. (a -> b) -> a -> b
$ [| CompileTerm $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE 'lift Q Exp -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`TH.appE` Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
pn) |]) [Name]
patNames

    TExpQ CompileTerm
rhsExpr <- if DatatypeInfo -> Bool
isNewtype DatatypeInfo
dt
            then case [TExpQ CompileTerm]
liftExprs of
                    [TExpQ CompileTerm
argExpr] -> TExpQ CompileTerm
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileTerm)
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TExpQ CompileTerm
argExpr
                    [TExpQ CompileTerm]
_         -> LiftError
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileTerm)
forall a.
LiftError
-> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LiftError
 -> StateT
      Deps
      (ReaderT THLocalVars (ExceptT LiftError Q))
      (TExpQ CompileTerm))
-> LiftError
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileTerm)
forall a b. (a -> b) -> a -> b
$ Text -> LiftError
UserLiftError Text
"Newtypes must have a single constructor with a single argument"
            else
                TExpQ CompileTerm
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileTerm)
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TExpQ CompileTerm
 -> StateT
      Deps
      (ReaderT THLocalVars (ExceptT LiftError Q))
      (TExpQ CompileTerm))
-> (Splice Q CompileTerm -> TExpQ CompileTerm)
-> Splice Q CompileTerm
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileTerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Splice Q CompileTerm -> TExpQ CompileTerm
forall (m :: * -> *) a. Splice m a -> m (TExp a)
TH.examineSplice (Splice Q CompileTerm
 -> StateT
      Deps
      (ReaderT THLocalVars (ExceptT LiftError Q))
      (TExpQ CompileTerm))
-> Splice Q CompileTerm
-> StateT
     Deps
     (ReaderT THLocalVars (ExceptT LiftError Q))
     (TExpQ CompileTerm)
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' :: [CompileTerm]
                        liftExprs' :: [CompileTerm]
liftExprs' = $$(Q (TExp [CompileTerm]) -> Splice Q [CompileTerm]
forall a (m :: * -> *). m (TExp a) -> Splice m a
TH.liftSplice (Q (TExp [CompileTerm]) -> Splice Q [CompileTerm])
-> Q (TExp [CompileTerm]) -> Splice Q [CompileTerm]
forall a b. (a -> b) -> a -> b
$ [TExpQ CompileTerm] -> Q (TExp [CompileTerm])
forall a. [TExpQ a] -> TExpQ [a]
tyListE [TExpQ CompileTerm]
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 :: CompileType
                        trep :: CompileType
trep = $$(Q Exp -> Splice Q CompileType
forall a (m :: * -> *). Quote m => m Exp -> Splice m a
TH.unsafeSpliceCoerce [| CompileType (typeRep (Proxy :: Proxy $(Name -> Q Pred
forall (m :: * -> *). Quote m => Name -> m Pred
TH.conT Name
tyName))) |])
                    in (forall fun.
 RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ()))
-> CompileTerm
CompileTerm (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ do
                        -- force creation of datatype
                        a
_ <- CompileType
-> forall fun. RTCompile DefaultUni fun (Type TyName DefaultUni ())
unCompileType CompileType
trep

                        -- get the right constructor
                        a
maybeConstructors <- ann -> key -> m (Maybe [Term TyName Name uni fun ann])
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe [Term TyName Name uni fun ann])
lookupConstructors () Name
tyName
                        a
constrs <- case a
maybeConstructors of
                            Maybe [Term TyName Name uni fun ann]
Nothing -> e -> a
forall a e. Exception e => e -> a
Prelude.throw (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Name -> LiftError
LiftMissingDataCons Name
tyName
                            Just [Term TyName Name uni fun ann]
cs -> a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term TyName Name uni fun ann]
cs
                        let constr :: a
constr = a
constrs [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
index

                        [Term TyName Name DefaultUni fun ()]
lifts :: [Term TyName Name PLC.DefaultUni fun ()] <- t (m a) -> m (t a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => t (m a) -> m (t a)
sequence (a -> RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ())
CompileTerm
-> forall fun.
   RTCompile DefaultUni fun (Term TyName Name DefaultUni fun ())
unCompileTerm (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CompileTerm]
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' :: [RTCompileScope DefaultUni fun (Type TyName DefaultUni ())]
tyExprs' = (a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
x -> CompileTypeScope
-> forall fun.
   RTCompileScope DefaultUni fun (Type TyName DefaultUni ())
unCompileTypeScope a
x) $$(Q (TExp [CompileTypeScope]) -> Splice Q [CompileTypeScope]
forall a (m :: * -> *). m (TExp a) -> Splice m a
TH.liftSplice (Q (TExp [CompileTypeScope]) -> Splice Q [CompileTypeScope])
-> Q (TExp [CompileTypeScope]) -> Splice Q [CompileTypeScope]
forall a b. (a -> b) -> a -> b
$ [TExpQ CompileTypeScope] -> Q (TExp [CompileTypeScope])
forall a. [TExpQ a] -> TExpQ [a]
tyListE [TExpQ CompileTypeScope]
tyExprs)
                        -- The types are compiled in an (empty) local scope.
                        a
types <- (a -> b -> c) -> b -> a -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT r m a -> r -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT a
forall a. Monoid a => a
mempty (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ t (m a) -> m (t a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => t (m a) -> m (t a)
sequence [RTCompileScope DefaultUni fun (Type TyName DefaultUni ())]
tyExprs'

                        a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (term () -> [Type tyname uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name uni fun ()
constr a
types) [Term TyName Name DefaultUni fun ()]
lifts
                  ||]
    Q Clause
-> StateT
     Deps (ReaderT THLocalVars (ExceptT LiftError Q)) (Q Clause)
forall a.
a -> StateT Deps (ReaderT THLocalVars (ExceptT LiftError Q)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Q Clause
 -> StateT
      Deps (ReaderT THLocalVars (ExceptT LiftError Q)) (Q Clause))
-> Q Clause
-> StateT
     Deps (ReaderT THLocalVars (ExceptT LiftError Q)) (Q Clause)
forall a b. (a -> b) -> a -> b
$ [Q Pat] -> Q Body -> [Q Dec] -> Q Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
TH.clause [Q Pat
pat] (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB (Q Exp -> Q Body) -> Q Exp -> Q Body
forall a b. (a -> b) -> a -> b
$ [| unCompileTerm $(TExpQ CompileTerm -> Q Exp
forall a (m :: * -> *). Quote m => m (TExp a) -> m Exp
TH.unTypeQ TExpQ CompileTerm
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) <- THCompile [Q Clause] -> Q ([Q Clause], Deps)
forall a. THCompile a -> Q (a, Deps)
runTHCompile (THCompile [Q Clause] -> Q ([Q Clause], Deps))
-> THCompile [Q Clause] -> Q ([Q Clause], Deps)
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 = Dep -> Deps -> Deps
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 = (Pred -> Bool) -> [Pred] -> [Pred]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Pred -> Bool) -> Pred -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Bool
isClosedConstraint) ([Pred] -> [Pred]) -> [Pred] -> [Pred]
forall a b. (a -> b) -> a -> b
$ Pred -> Dep -> Pred
toConstraint Pred
uni (Dep -> Pred) -> [Dep] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Deps -> [Dep]
forall a. Set a -> [a]
Set.toList Deps
prunedDeps

    Dec
decl <- Name -> [Q Clause] -> Q Dec
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 Maybe Overlap
forall a. Maybe a
Nothing [Pred]
constraints (Pred -> Pred -> Pred
liftPir Pred
uni Pred
datatypeType) [Dec
decl]]
    [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ [Dec]
typeableDecs [Dec] -> [Dec] -> [Dec]
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 <- ExceptT LiftError Q (a, Deps) -> Q (Either LiftError (a, Deps))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT LiftError Q (a, Deps) -> Q (Either LiftError (a, Deps)))
-> (ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps)
    -> ExceptT LiftError Q (a, Deps))
-> ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps)
-> Q (Either LiftError (a, Deps))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          (ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps)
 -> THLocalVars -> ExceptT LiftError Q (a, Deps))
-> THLocalVars
-> ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps)
-> ExceptT LiftError Q (a, Deps)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps)
-> THLocalVars -> ExceptT LiftError Q (a, Deps)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT THLocalVars
forall a. Monoid a => a
mempty (ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps)
 -> Q (Either LiftError (a, Deps)))
-> ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps)
-> Q (Either LiftError (a, Deps))
forall a b. (a -> b) -> a -> b
$
          (THCompile a
 -> Deps -> ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps))
-> Deps
-> THCompile a
-> ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps)
forall a b c. (a -> b -> c) -> b -> a -> c
flip THCompile a
-> Deps -> ReaderT THLocalVars (ExceptT LiftError Q) (a, Deps)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Deps
forall a. Monoid a => a
mempty THCompile a
m
    case Either LiftError (a, Deps)
res of
        Left LiftError
a  -> String -> Q (a, Deps)
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q (a, Deps)) -> String -> Q (a, Deps)
forall a b. (a -> b) -> a -> b
$ String
"Generating Lift instances: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (LiftError -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. LiftError -> Doc ann
PP.pretty LiftError
a)
        Right (a, Deps)
b -> (a, Deps) -> Q (a, Deps)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a, Deps)
b