{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}
{-# LANGUAGE TypeOperators     #-}
-- | Functions for compiling let-bound PIR datatypes into PLC.
module PlutusIR.Compiler.Datatype
    ( compileDatatype
    , compileDatatypeDefs
    , compileRecDatatypes
    , funTyArgs
    , funResultType
    , mkDatatypeValueType
    , mkDestructorTy
    , replaceFunTyTarget
    , resultTypeName
    ) where

import PlutusPrelude (showText)

import PlutusIR
import PlutusIR.Compiler.Names
import PlutusIR.Compiler.Provenance
import PlutusIR.Compiler.Types
import PlutusIR.Error
import PlutusIR.MkPir qualified as PIR
import PlutusIR.Transform.Substitute

import PlutusCore.MkPlc qualified as PLC
import PlutusCore.Quote
import PlutusCore.StdLib.Type qualified as Types

import Control.Monad.Error.Lens

import Data.Text qualified as T
import Data.Traversable

import Data.List.NonEmpty qualified as NE

{- NOTE [Normalization of data-constructors' types]

Currently the typechecking and compilation of dataconstructors/destructor
assume that the data-constructors' types (of the parsed PIR input) are in normalized form.
If these types are not normalized, the compilation will generate failing plc code.

There are no checks in place to enforce this normalization, and while
plutus-tx plugin is unlikely to generate PIR code with unnormalized types inside
these dataconstructor locations, it may still need to be taken into account in
the unlikely case that a user has manually modified the PIR input.

Future solutions:

1) disallow unnormalized types in dataconstructors, by adding a "isNormalized" check  prior to compilation.
2) allow unnormalized types in dataconstructors and normalize them prior to compilation.
-}

-- Utilities

-- | @replaceFunTyTarget X (A->..->Z) = (A->..->X)@
replaceFunTyTarget :: Type tyname uni a -> Type tyname uni a -> Type tyname uni a
replaceFunTyTarget :: Type tyname uni a -> Type tyname uni a -> Type tyname uni a
replaceFunTyTarget Type tyname uni a
newTarget Type tyname uni a
t = case Type tyname uni a
t of
    TyFun a
a Type tyname uni a
t1 Type tyname uni a
t2 -> a -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun a
a Type tyname uni a
t1 (Type tyname uni a -> Type tyname uni a)
-> Type tyname uni a -> Type tyname uni a
forall a b. (a -> b) -> a -> b
$ Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) a.
Type tyname uni a -> Type tyname uni a -> Type tyname uni a
replaceFunTyTarget Type tyname uni a
newTarget Type tyname uni a
t2
    Type tyname uni a
_             -> Type tyname uni a
newTarget

-- | Given the type of a constructor, get the type of the "case" type with the given result type.
-- @constructorCaseType R (A->Maybe A) = (A -> R)@
constructorCaseType :: Type tyname uni a -> VarDecl tyname name uni fun a -> Type tyname uni a
constructorCaseType :: Type tyname uni a
-> VarDecl tyname name uni fun a -> Type tyname uni a
constructorCaseType Type tyname uni a
resultType = Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) a.
Type tyname uni a -> Type tyname uni a -> Type tyname uni a
replaceFunTyTarget Type tyname uni a
resultType (Type tyname uni a -> Type tyname uni a)
-> (VarDecl tyname name uni fun a -> Type tyname uni a)
-> VarDecl tyname name uni fun a
-> Type tyname uni a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname name uni fun a -> Type tyname uni a
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> Type tyname uni ann
_varDeclType

-- | Get recursively all the domains and codomains of a type.
-- @funTySections (A->B->C) = [A, B, C]@
-- @funTySections (X) = [X]@
funTySections :: Type tyname uni a -> NE.NonEmpty (Type tyname uni a)
funTySections :: Type tyname uni a -> NonEmpty (Type tyname uni a)
funTySections = \case
    TyFun a
_ Type tyname uni a
t1 Type tyname uni a
t2 -> Type tyname uni a
t1 Type tyname uni a
-> NonEmpty (Type tyname uni a) -> NonEmpty (Type tyname uni a)
forall a. a -> NonEmpty a -> NonEmpty a
NE.<| Type tyname uni a -> NonEmpty (Type tyname uni a)
forall tyname (uni :: * -> *) a.
Type tyname uni a -> NonEmpty (Type tyname uni a)
funTySections Type tyname uni a
t2
    Type tyname uni a
t             -> Type tyname uni a -> NonEmpty (Type tyname uni a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni a
t

-- | Get the argument types of a function type.
-- @funTyArgs (A->B->C) = [A, B]@
funTyArgs :: Type tyname uni a ->  [Type tyname uni a]
funTyArgs :: Type tyname uni a -> [Type tyname uni a]
funTyArgs = NonEmpty (Type tyname uni a) -> [Type tyname uni a]
forall a. NonEmpty a -> [a]
NE.init (NonEmpty (Type tyname uni a) -> [Type tyname uni a])
-> (Type tyname uni a -> NonEmpty (Type tyname uni a))
-> Type tyname uni a
-> [Type tyname uni a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni a -> NonEmpty (Type tyname uni a)
forall tyname (uni :: * -> *) a.
Type tyname uni a -> NonEmpty (Type tyname uni a)
funTySections

-- | Get the result type of a function.
-- If not a function, then is the same as `id`
-- @funResultType (A->B->C) = C@
-- @funResultType (X) = X@
funResultType :: Type tyname uni a ->  Type tyname uni a
funResultType :: Type tyname uni a -> Type tyname uni a
funResultType = NonEmpty (Type tyname uni a) -> Type tyname uni a
forall a. NonEmpty a -> a
NE.last (NonEmpty (Type tyname uni a) -> Type tyname uni a)
-> (Type tyname uni a -> NonEmpty (Type tyname uni a))
-> Type tyname uni a
-> Type tyname uni a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni a -> NonEmpty (Type tyname uni a)
forall tyname (uni :: * -> *) a.
Type tyname uni a -> NonEmpty (Type tyname uni a)
funTySections

-- | Given the type of a constructor, get its argument types.
-- @constructorArgTypes (A->Maybe A) = [A]
constructorArgTypes :: VarDecl tyname name uni fun a -> [Type tyname uni a]
constructorArgTypes :: VarDecl tyname name uni fun a -> [Type tyname uni a]
constructorArgTypes = Type tyname uni a -> [Type tyname uni a]
forall tyname (uni :: * -> *) a.
Type tyname uni a -> [Type tyname uni a]
funTyArgs (Type tyname uni a -> [Type tyname uni a])
-> (VarDecl tyname name uni fun a -> Type tyname uni a)
-> VarDecl tyname name uni fun a
-> [Type tyname uni a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname name uni fun a -> Type tyname uni a
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> Type tyname uni ann
_varDeclType

-- | "Unveil" a datatype definition in a type, by replacing uses of the name as a type variable with the concrete definition.
unveilDatatype :: Eq tyname => Type tyname uni a -> Datatype tyname name uni fun a -> Type tyname uni a -> Type tyname uni a
unveilDatatype :: Type tyname uni a
-> Datatype tyname name uni fun a
-> Type tyname uni a
-> Type tyname uni a
unveilDatatype Type tyname uni a
dty (Datatype a
_ TyVarDecl tyname a
tn [TyVarDecl tyname a]
_ name
_ [VarDecl tyname name uni fun a]
_) = (tyname -> Maybe (Type tyname uni a))
-> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
(tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann -> Type tyname uni ann
typeSubstTyNames (\tyname
n -> if tyname
n tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== TyVarDecl tyname a -> tyname
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName TyVarDecl tyname a
tn then Type tyname uni a -> Maybe (Type tyname uni a)
forall a. a -> Maybe a
Just Type tyname uni a
dty else Maybe (Type tyname uni a)
forall a. Maybe a
Nothing)

resultTypeName :: MonadQuote m => Datatype TyName Name uni fun a -> m TyName
resultTypeName :: Datatype TyName Name uni fun a -> m TyName
resultTypeName (Datatype a
_ TyVarDecl TyName a
tn [TyVarDecl TyName a]
_ Name
_ [VarDecl TyName Name uni fun a]
_) = Quote TyName -> m TyName
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote TyName -> m TyName) -> Quote TyName -> m TyName
forall a b. (a -> b) -> a -> b
$ Text -> Quote TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName (Text -> Quote TyName) -> Text -> Quote TyName
forall a b. (a -> b) -> a -> b
$ Text
"out_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (Name -> Text
nameString (Name -> Text) -> Name -> Text
forall a b. (a -> b) -> a -> b
$ TyName -> Name
unTyName (TyName -> Name) -> TyName -> Name
forall a b. (a -> b) -> a -> b
$ TyVarDecl TyName a -> TyName
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName TyVarDecl TyName a
tn)

-- Datatypes

{- Note [Scott encoding of datatypes]
(This describes the conceptual scheme for converting data types - in fact we translate
them as abstract, so see also Note [Abstract data types].)

We translate our datatypes using the Scott encoding. The fundamental idea is that there is one thing
you can do with a datatype value: pattern match on it. A datatype value is therefore represented by
precisely the thing you need to do a pattern match. Namely, a function that takes functions implementing
each arm of the match, and then gives you a result.

We also need to think about the types. In general, we need:
- The encoded type corresponding to the datatype itself
- The encoded type of each constructor
- The encoded term for each constructor
- The encoded type of the destructor
- The encoded term for the destructor

-- Basic example

For example, consider 'Maybe a'. Then:
- The type corresponding to the datatype is:
  Maybe = \(a :: *) -> forall out_Maybe . out_maybe -> (a -> out_Maybe) -> out_Maybe
- The type of the constructors are:
  Just : forall (a :: *) . a -> Maybe a
  Nothing : forall (a :: *) . Maybe a
- The terms for the constructors are:
  Just = \(arg1 : a). /\ (out_Maybe :: *) . \(case_Nothing : out_Maybe) (case_Just : a -> out_Maybe) . case_Just arg1
  Nothing = /\ (out_Maybe :: *) . \(case_Nothing : out_Maybe) (caseJust : a -> out_Maybe) . caseNothing
- The type of the destructor is:
  match_Maybe : forall (a :: *) . Maybe a -> forall (out_Maybe :: *) . out_maybe -> (a -> out_maybe) -> out_maybe
- The term for the destructor is:
  match_Maybe = /\(a :: *) -> \(x : Maybe a) -> x

(Constructors and destructors are much more necessary when we define the datatype as abstract,
rather than inlining it, see Note [Abstract data types]. However, it is easier to present them here
as a slightly unnecessary generality.)

-- General case

Consider a datatype as defined in Plutus IR:
(datatype
  (tyvardecl T (type))
  (tyvardecl a_1 t_1)
  ..
  (tyvardecl a_n t_n)
  match_T
  (vardecl c_1 (fun t_c_1_1 .. (fun t_c_1_(c_1_k)) [T t1 .. tn]))
  ..
  (vardecl c_j (fun t_c_j_1 .. (fun t_c_j_(c_j_k)) [T t1 .. tn]))
)

That is, it has:
- Name T
- Kind *
- n type parameters of type t_1 to t_n
- Destructor match_t
_ j constructors with c_i_k arguments each of types t_c_i_1 to t_c_i_(c_i_k)

The type corresponding to the datatype is:
\(t_1 :: *) .. (t_n :: *) .
  forall out_T :: * .
    (t_c_1_1 -> .. -> t_c_1_(c_1_k) -> out_T) -> .. -> (t_c_j_1 -> .. -> t_c_j_(c_j_k) -> out_T) ->
      out_T

The type of the constructor c_i is:
forall (t_1 :: *) .. (t_n :: *) .
  t_c_i_1 -> .. -> t_c_i_(c_i_k) ->
    (T t_1 .. t_n)
This is actually declared for us in the datatype declaration, but without the type
variables being abstracted out. We use this to get the argument types of the constructor.

The term for the constructor c_i is:
/\(t_1 :: *) .. (t_n :: *) .
  \(a_1 : t_c_j_1) .. (a_c_i_(c_i_k) : t_c_i_(c_i_k)) .
    abs out_T :: * .
      \(case_c_1 : (t_c_1_1 -> .. -> t_c_1_(c_1_k) -> out_T)) .. (case_c_j : (t_c_j_1 -> .. -> t_c_j_(c_j_k) -> out_T)) .
        case_c_i a_1 .. a_c_i_(c_i_k)

The type of the destructor is:
forall (t_1 :: *) .. (t_n :: *) .
  (T t_1 .. t_n) ->
    forall out_T :: * .
      (t_c_1_1 -> .. -> t_c_1_(c_1_k) -> out_T) -> .. -> (t_c_j_1 -> .. -> t_c_j_(c_j_k) -> out_T) ->
        out_T

The term for the destructor is:
/\(t_1 :: *) .. (t_n :: *) .
  \(x :: (T t_1 .. t_n)) ->
    x

-- Compiling uses of datatypes

We turn constructor invocations into calls to the constructor functions.

Pattern matching is slightly more complex as we need to turn it into an invocation of the destructor:
- We take each alternative, turn it into a function of its bound variables.
- We apply the destructor to the scrutinee, and then instantiate that (which will be polymorphic
  in the result type) at the type of the overall match expression.
    - This does indicate one wrinkle: we need to know the overall type, we can't infer it.
- We apply the instantiated value to the functions for each alternative.
-}

{- Note [Abstract data types]
While the Scott encoding makes it easy to simply convert all types inline, it
is convenient for a number of reasons to instead abstract out data types. Namely:
- The resulting code is much more readable, since we have named types instead
of (potentially big) inlined types.
- We generate less code because we're not repeating the definition at every use site.

The basic idea is to "let-bind" types using type abstractions, and values using
lambda abstractions. There are a few considerations that make this tricky, however:

1. When types are inlined, the Scott encoding allows us to construct values by
  constructing the matching function inline. When they are abstract, we need to provide
  (suitably polymorphic) constructors abstractly.
2. When types are inlined, the Scott encoding allows us to match against a type by
  simply using it as a function. When they are abstract, we need to provide a
  (suitably polymorphic) matching function abstractly.
3. The definition of a type must be abstract in the binding types of the constructors and destructors
  (so they can be used alongside the abstract type), but it must *not* be abstract in the
  *definition* of the constructors or destructors, because they depend on knowing the real structure
  of the type.
    1. In fact we can do slightly better than this: in the constructors of a recursive datatype we can use the type
       as a name inside the 'wrap'.

Consequently, for a single type we end up with something like the following:

(/\ ty :: * .
  -- ty abstract in these types
  \(c_1 : <constructor type i>) .. (c_j : <constructor type j>) .
    -- ty abstract in this type
    \match : <destructor type> .
      <user term>
)
<defn of ty>
-- ty concrete in these terms, except maybe inside a 'wrap'
<defn of c_1>
..
<defn of c_j>
-- ty concrete in this term
<defn of match>

(see Note [Scott encoding of datatypes] for how the actual definitions are constructed)
-}

{- Note [Recursive data types]
Recursive data types make the scheme described in [Scott encoding of datatypes] a bit more
complex. At the moment we only support self-recursive datatypes.

For a (self-)recursive datatype we have to change three things:
- The type of the datatype itself must have an enclosing fix over the type variable for
  the type itself.
- Constructors must include a wrap.
- Destructors must include an unwrap.
-}

-- See note [Scott encoding of datatypes]
-- | Make the "Scott-encoded" type for a 'Datatype', with type variables free.
-- @mkScottTy Maybe = forall out_Maybe. out_Maybe -> (a -> out_Maybe) -> out_Maybe@
mkScottTy :: MonadQuote m => ann -> Datatype TyName Name uni fun ann -> m (Type TyName uni ann)
mkScottTy :: ann -> Datatype TyName Name uni fun ann -> m (Type TyName uni ann)
mkScottTy ann
ann d :: Datatype TyName Name uni fun ann
d@(Datatype ann
_ TyVarDecl TyName ann
_ [TyVarDecl TyName ann]
_ Name
_ [VarDecl TyName Name uni fun ann]
constrs) = do
    TyName
resultType <- Datatype TyName Name uni fun ann -> m TyName
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
Datatype TyName Name uni fun a -> m TyName
resultTypeName Datatype TyName Name uni fun ann
d
     -- FIXME: normalize datacons' types also here
    let caseTys :: [Type TyName uni ann]
caseTys = (VarDecl TyName Name uni fun ann -> Type TyName uni ann)
-> [VarDecl TyName Name uni fun ann] -> [Type TyName uni ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type TyName uni ann
-> VarDecl TyName Name uni fun ann -> Type TyName uni ann
forall tyname (uni :: * -> *) a name fun.
Type tyname uni a
-> VarDecl tyname name uni fun a -> Type tyname uni a
constructorCaseType (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
resultType)) [VarDecl TyName Name uni fun ann]
constrs
    Type TyName uni ann -> m (Type TyName uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni ann -> m (Type TyName uni ann))
-> Type TyName uni ann -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$
        -- forall resultType
        ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann TyName
resultType (ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann) (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$
        -- c_1 -> .. -> c_n -> resultType
        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
PIR.mkIterTyFun ann
ann [Type TyName uni ann]
caseTys (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
resultType)

-- | Make the "pattern functor" of a 'Datatype'. This is just the normal type, but with the
-- type variable for the type itself free and its type variables free.
-- @mkDatatypePatternFunctor List = forall (r :: *) . r -> (a -> List a -> r) -> r@
-- FIXME: inline this
mkDatatypePatternFunctor :: MonadQuote m => ann -> Datatype TyName Name uni fun ann -> m (Type TyName uni ann)
mkDatatypePatternFunctor :: ann -> Datatype TyName Name uni fun ann -> m (Type TyName uni ann)
mkDatatypePatternFunctor ann
ann Datatype TyName Name uni fun ann
d = ann -> Datatype TyName Name uni fun ann -> m (Type TyName uni ann)
forall (m :: * -> *) ann (uni :: * -> *) fun.
MonadQuote m =>
ann -> Datatype TyName Name uni fun ann -> m (Type TyName uni ann)
mkScottTy ann
ann Datatype TyName Name uni fun ann
d

-- | Make the real PLC type corresponding to a 'Datatype' with the given pattern functor.
-- @
--     mkDatatypeType List <pattern functor of List>
--         = fix list . <pattern functor of List>
--         = fix list . \(a :: *) -> forall (r :: *) . r -> (a -> List a -> r) -> r
-- @
mkDatatypeType :: forall m uni fun a. MonadQuote m => Recursivity -> PIRType uni a -> Datatype TyName Name uni fun (Provenance a) -> m (PLCRecType uni fun a)
mkDatatypeType :: Recursivity
-> PIRType uni a
-> Datatype TyName Name uni fun (Provenance a)
-> m (PLCRecType uni fun a)
mkDatatypeType Recursivity
r PIRType uni a
pf (Datatype Provenance a
ann TyVarDecl TyName (Provenance a)
tn [TyVarDecl TyName (Provenance a)]
tvs Name
_ [VarDecl TyName Name uni fun (Provenance a)]
_) = case Recursivity
r of
    Recursivity
NonRec -> PIRType uni a -> PLCRecType uni fun a
forall (uni :: * -> *) fun a. PLCType uni a -> PLCRecType uni fun a
PlainType (PIRType uni a -> PLCRecType uni fun a)
-> m (PIRType uni a) -> m (PLCRecType uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([TyVarDecl TyName (Provenance a)] -> PIRType uni a -> PIRType uni a
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
PLC.mkIterTyLam ([TyVarDecl TyName (Provenance a)]
 -> PIRType uni a -> PIRType uni a)
-> m [TyVarDecl TyName (Provenance a)]
-> m (PIRType uni a -> PIRType uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyVarDecl TyName (Provenance a)]
-> m [TyVarDecl TyName (Provenance a)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [TyVarDecl TyName (Provenance a)]
tvs m (PIRType uni a -> PIRType uni a)
-> m (PIRType uni a) -> m (PIRType uni a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PIRType uni a -> m (PIRType uni a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRType uni a
pf)
    -- See note [Recursive datatypes]
    -- We are reusing the same type name for the fixpoint variable. This is fine
    -- so long as we do renaming later, since we only reuse the name inside an inner binder
    Recursivity
Rec    -> do
        RecursiveType uni fun (Provenance a) -> PLCRecType uni fun a
forall (uni :: * -> *) fun a.
RecursiveType uni fun (Provenance a) -> PLCRecType uni fun a
RecursiveType (RecursiveType uni fun (Provenance a) -> PLCRecType uni fun a)
-> m (RecursiveType uni fun (Provenance a))
-> m (PLCRecType uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Quote (RecursiveType uni fun (Provenance a))
-> m (RecursiveType uni fun (Provenance a))
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (RecursiveType uni fun (Provenance a))
 -> m (RecursiveType uni fun (Provenance a)))
-> Quote (RecursiveType uni fun (Provenance a))
-> m (RecursiveType uni fun (Provenance a))
forall a b. (a -> b) -> a -> b
$ FromDataPieces
  uni (Provenance a) (RecursiveType uni fun (Provenance a))
forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (RecursiveType uni fun ann)
Types.makeRecursiveType @uni @(Provenance a) Provenance a
ann (TyVarDecl TyName (Provenance a) -> TyName
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName TyVarDecl TyName (Provenance a)
tn) [TyVarDecl TyName (Provenance a)]
tvs PIRType uni a
pf)

-- | The type of a datatype-value is of the form `[TyCon tyarg1 tyarg2 ... tyargn]`
mkDatatypeValueType :: a -> Datatype TyName Name uni fun a -> Type TyName uni a
mkDatatypeValueType :: a -> Datatype TyName Name uni fun a -> Type TyName uni a
mkDatatypeValueType a
ann (Datatype a
_ TyVarDecl TyName a
tn [TyVarDecl TyName a]
tvs Name
_ [VarDecl TyName Name uni fun a]
_)  = a -> Type TyName uni a -> [Type TyName uni a] -> Type TyName uni a
forall ann tyname (uni :: * -> *).
ann
-> Type tyname uni ann
-> [Type tyname uni ann]
-> Type tyname uni ann
PIR.mkIterTyApp a
ann (a -> TyVarDecl TyName a -> Type TyName uni a
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar a
ann TyVarDecl TyName a
tn) ([Type TyName uni a] -> Type TyName uni a)
-> [Type TyName uni a] -> Type TyName uni a
forall a b. (a -> b) -> a -> b
$ a -> TyVarDecl TyName a -> Type TyName uni a
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar a
ann (TyVarDecl TyName a -> Type TyName uni a)
-> [TyVarDecl TyName a] -> [Type TyName uni a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyVarDecl TyName a]
tvs

-- Constructors

-- | Make the type of a constructor of a 'Datatype'. This is not quite the same as the declared type because the declared type has the
-- type variables free.
-- @
--     mkConstructorType List Cons = forall (a :: *) . a -> List a -> List a
-- @
mkConstructorType :: Datatype TyName Name uni fun (Provenance a) -> VarDecl TyName Name uni fun (Provenance a) -> PIRType uni a
-- this type appears *inside* the scope of the abstraction for the datatype so we can just reference the name and
-- we don't need to do anything to the declared type
-- see note [Abstract data types]
-- FIXME: normalize constructors also here
mkConstructorType :: Datatype TyName Name uni fun (Provenance a)
-> VarDecl TyName Name uni fun (Provenance a) -> PIRType uni a
mkConstructorType (Datatype Provenance a
_ TyVarDecl TyName (Provenance a)
_ [TyVarDecl TyName (Provenance a)]
tvs Name
_ [VarDecl TyName Name uni fun (Provenance a)]
_) VarDecl TyName Name uni fun (Provenance a)
constr =
    let constrTy :: PIRType uni a
constrTy = [TyVarDecl TyName (Provenance a)] -> PIRType uni a -> PIRType uni a
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
PIR.mkIterTyForall [TyVarDecl TyName (Provenance a)]
tvs (PIRType uni a -> PIRType uni a) -> PIRType uni a -> PIRType uni a
forall a b. (a -> b) -> a -> b
$ VarDecl TyName Name uni fun (Provenance a) -> PIRType uni a
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> Type tyname uni ann
_varDeclType VarDecl TyName Name uni fun (Provenance a)
constr
    in (Provenance a -> Provenance a) -> PIRType uni a -> PIRType uni a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Provenance a
a -> DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
ConstructorType Provenance a
a) PIRType uni a
constrTy

-- See note [Scott encoding of datatypes]
-- | Make a constructor of a 'Datatype' with the given pattern functor. The constructor argument mostly serves to identify the constructor
-- that we are interested in in the list of constructors.
-- @
--     mkConstructor <definition of List> <pattern functor of List> List Cons
--         = /\(a :: *) . \(arg1 : a) (arg2 : <definition of List> a) .
--             wrap <pattern functor of List> /\(out_List :: *) .
--                 \(case_Nil : out_List) (case_Cons : a -> List a -> out_List) . case_Cons arg1 arg2
-- @
mkConstructor :: MonadQuote m => PLCRecType uni fun a -> Datatype TyName Name uni fun (Provenance a) -> Int -> m (PIRTerm uni fun a)
mkConstructor :: PLCRecType uni fun a
-> Datatype TyName Name uni fun (Provenance a)
-> Int
-> m (PIRTerm uni fun a)
mkConstructor PLCRecType uni fun a
dty d :: Datatype TyName Name uni fun (Provenance a)
d@(Datatype Provenance a
ann TyVarDecl TyName (Provenance a)
_ [TyVarDecl TyName (Provenance a)]
tvs Name
_ [VarDecl TyName Name uni fun (Provenance a)]
constrs) Int
index = do
    TyName
resultType <- Datatype TyName Name uni fun (Provenance a) -> m TyName
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
Datatype TyName Name uni fun a -> m TyName
resultTypeName Datatype TyName Name uni fun (Provenance a)
d

    -- case arguments and their types
    [VarDecl TyName Name uni fun (Provenance a)]
casesAndTypes <- do
          -- these types appear *outside* the scope of the abstraction for the datatype, so we need to use the concrete datatype here
          -- see note [Abstract data types]
          -- FIXME: normalize datacons' types also here
          let caseTypes :: [Type TyName uni (Provenance a)]
caseTypes = Type TyName uni (Provenance a)
-> Datatype TyName Name uni fun (Provenance a)
-> Type TyName uni (Provenance a)
-> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) a name fun.
Eq tyname =>
Type tyname uni a
-> Datatype tyname name uni fun a
-> Type tyname uni a
-> Type tyname uni a
unveilDatatype (PLCRecType uni fun a -> Type TyName uni (Provenance a)
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType PLCRecType uni fun a
dty) Datatype TyName Name uni fun (Provenance a)
d (Type TyName uni (Provenance a) -> Type TyName uni (Provenance a))
-> [Type TyName uni (Provenance a)]
-> [Type TyName uni (Provenance a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarDecl TyName Name uni fun (Provenance a)
 -> Type TyName uni (Provenance a))
-> [VarDecl TyName Name uni fun (Provenance a)]
-> [Type TyName uni (Provenance a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type TyName uni (Provenance a)
-> VarDecl TyName Name uni fun (Provenance a)
-> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) a name fun.
Type tyname uni a
-> VarDecl tyname name uni fun a -> Type tyname uni a
constructorCaseType (Provenance a -> TyName -> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar Provenance a
ann TyName
resultType)) [VarDecl TyName Name uni fun (Provenance a)]
constrs
          [Name]
caseArgNames <- [VarDecl TyName Name uni fun (Provenance a)]
-> (VarDecl TyName Name uni fun (Provenance a) -> m Name)
-> m [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [VarDecl TyName Name uni fun (Provenance a)]
constrs (\VarDecl TyName Name uni fun (Provenance a)
c -> Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
safeFreshName (Text -> m Name) -> Text -> m Name
forall a b. (a -> b) -> a -> b
$ Text
"case_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (VarDecl TyName Name uni fun (Provenance a) -> String
forall tyname (uni :: * -> *) fun a.
VarDecl tyname Name uni fun a -> String
varDeclNameString VarDecl TyName Name uni fun (Provenance a)
c))
          [VarDecl TyName Name uni fun (Provenance a)]
-> m [VarDecl TyName Name uni fun (Provenance a)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VarDecl TyName Name uni fun (Provenance a)]
 -> m [VarDecl TyName Name uni fun (Provenance a)])
-> [VarDecl TyName Name uni fun (Provenance a)]
-> m [VarDecl TyName Name uni fun (Provenance a)]
forall a b. (a -> b) -> a -> b
$ (Name
 -> Type TyName uni (Provenance a)
 -> VarDecl TyName Name uni fun (Provenance a))
-> [Name]
-> [Type TyName uni (Provenance a)]
-> [VarDecl TyName Name uni fun (Provenance a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni fun (Provenance a)
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl Provenance a
ann) [Name]
caseArgNames [Type TyName uni (Provenance a)]
caseTypes

    -- This is inelegant, but it should never fail
    let thisConstr :: VarDecl TyName Name uni fun (Provenance a)
thisConstr = [VarDecl TyName Name uni fun (Provenance a)]
constrs [VarDecl TyName Name uni fun (Provenance a)]
-> Int -> VarDecl TyName Name uni fun (Provenance a)
forall a. [a] -> Int -> a
!! Int
index
    let thisCase :: PIRTerm uni fun a
thisCase = Provenance a
-> VarDecl TyName Name uni fun (Provenance a) -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni fun ann -> term ann
PIR.mkVar Provenance a
ann (VarDecl TyName Name uni fun (Provenance a) -> PIRTerm uni fun a)
-> VarDecl TyName Name uni fun (Provenance a) -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$ [VarDecl TyName Name uni fun (Provenance a)]
casesAndTypes [VarDecl TyName Name uni fun (Provenance a)]
-> Int -> VarDecl TyName Name uni fun (Provenance a)
forall a. [a] -> Int -> a
!! Int
index

    -- constructor args and their types
    [VarDecl TyName Name uni fun (Provenance a)]
argsAndTypes <- do
        -- these types appear *outside* the scope of the abstraction for the datatype, so we need to use the concrete datatype here
        -- see note [Abstract data types]
        -- FIXME: normalize datacons' types also here
        let argTypes :: [Type TyName uni (Provenance a)]
argTypes = Type TyName uni (Provenance a)
-> Datatype TyName Name uni fun (Provenance a)
-> Type TyName uni (Provenance a)
-> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) a name fun.
Eq tyname =>
Type tyname uni a
-> Datatype tyname name uni fun a
-> Type tyname uni a
-> Type tyname uni a
unveilDatatype (PLCRecType uni fun a -> Type TyName uni (Provenance a)
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType PLCRecType uni fun a
dty) Datatype TyName Name uni fun (Provenance a)
d (Type TyName uni (Provenance a) -> Type TyName uni (Provenance a))
-> [Type TyName uni (Provenance a)]
-> [Type TyName uni (Provenance a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarDecl TyName Name uni fun (Provenance a)
-> [Type TyName uni (Provenance a)]
forall tyname name (uni :: * -> *) fun a.
VarDecl tyname name uni fun a -> [Type tyname uni a]
constructorArgTypes VarDecl TyName Name uni fun (Provenance a)
thisConstr
        -- we don't have any names for these things, we just had the type, so we call them "arg_i
        [Name]
argNames <- [Int] -> (Int -> m Name) -> m [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Int
0..([Type TyName uni (Provenance a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type TyName uni (Provenance a)]
argTypes Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] (\Int
i -> Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
safeFreshName (Text -> m Name) -> Text -> m Name
forall a b. (a -> b) -> a -> b
$ Text
"arg_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
i)
        [VarDecl TyName Name uni fun (Provenance a)]
-> m [VarDecl TyName Name uni fun (Provenance a)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VarDecl TyName Name uni fun (Provenance a)]
 -> m [VarDecl TyName Name uni fun (Provenance a)])
-> [VarDecl TyName Name uni fun (Provenance a)]
-> m [VarDecl TyName Name uni fun (Provenance a)]
forall a b. (a -> b) -> a -> b
$ (Name
 -> Type TyName uni (Provenance a)
 -> VarDecl TyName Name uni fun (Provenance a))
-> [Name]
-> [Type TyName uni (Provenance a)]
-> [VarDecl TyName Name uni fun (Provenance a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni fun (Provenance a)
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl Provenance a
ann) [Name]
argNames [Type TyName uni (Provenance a)]
argTypes


    let constr :: PIRTerm uni fun a
constr =
            -- /\t_1 .. t_n
            [TyVarDecl TyName (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
PIR.mkIterTyAbs [TyVarDecl TyName (Provenance a)]
tvs (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
            -- \arg_1 .. arg_m
            [VarDecl TyName Name uni fun (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni fun ann] -> term ann -> term ann
PIR.mkIterLamAbs [VarDecl TyName Name uni fun (Provenance a)]
argsAndTypes (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
            -- See Note [Recursive datatypes]
            -- wrap
            Provenance a
-> PLCRecType uni fun a
-> [Type TyName uni (Provenance a)]
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall a (uni :: * -> *) fun.
Provenance a
-> PLCRecType uni fun a
-> [PLCType uni a]
-> PIRTerm uni fun a
-> PIRTerm uni fun a
wrap Provenance a
ann PLCRecType uni fun a
dty ((TyVarDecl TyName (Provenance a) -> Type TyName uni (Provenance a))
-> [TyVarDecl TyName (Provenance a)]
-> [Type TyName uni (Provenance a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Provenance a
-> TyVarDecl TyName (Provenance a)
-> Type TyName uni (Provenance a)
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar Provenance a
ann) [TyVarDecl TyName (Provenance a)]
tvs)(PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
            -- forall out
            Provenance a
-> TyName
-> Kind (Provenance a)
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs Provenance a
ann TyName
resultType (Provenance a -> Kind (Provenance a)
forall ann. ann -> Kind ann
Type Provenance a
ann) (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
            -- \case_1 .. case_j
            [VarDecl TyName Name uni fun (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni fun ann] -> term ann -> term ann
PIR.mkIterLamAbs [VarDecl TyName Name uni fun (Provenance a)]
casesAndTypes (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
            -- c_i arg_1 .. arg_m
            Provenance a
-> PIRTerm uni fun a -> [PIRTerm uni fun a] -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
PIR.mkIterApp Provenance a
ann PIRTerm uni fun a
thisCase ((VarDecl TyName Name uni fun (Provenance a) -> PIRTerm uni fun a)
-> [VarDecl TyName Name uni fun (Provenance a)]
-> [PIRTerm uni fun a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Provenance a
-> VarDecl TyName Name uni fun (Provenance a) -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni fun ann -> term ann
PIR.mkVar Provenance a
ann) [VarDecl TyName Name uni fun (Provenance a)]
argsAndTypes)
    PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ (Provenance a -> Provenance a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Provenance a
a -> DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
Constructor Provenance a
a) PIRTerm uni fun a
constr

-- Destructors

-- See note [Scott encoding of datatypes]
-- | Make the destructor for a 'Datatype'.
-- @
--     mkDestructor <definition of List> List
--        = /\(a :: *) -> \(x : (<definition of List> a)) -> unwrap x
--        = /\(a :: *) -> \(x : (fix List . \(a :: *) -> forall (r :: *) . r -> (a -> List a -> r) -> r) a) -> unwrap x
-- @
mkDestructor :: MonadQuote m => PLCRecType uni fun a -> Datatype TyName Name uni fun (Provenance a) -> m (PIRTerm uni fun a)
mkDestructor :: PLCRecType uni fun a
-> Datatype TyName Name uni fun (Provenance a)
-> m (PIRTerm uni fun a)
mkDestructor PLCRecType uni fun a
dty (Datatype Provenance a
ann TyVarDecl TyName (Provenance a)
_ [TyVarDecl TyName (Provenance a)]
tvs Name
_ [VarDecl TyName Name uni fun (Provenance a)]
_) = do
    -- This term appears *outside* the scope of the abstraction for the datatype, so we need to put in the Scott-encoded type here
    -- see note [Abstract data types]
    -- dty t_1 .. t_n
    let appliedReal :: Type TyName uni (Provenance a)
appliedReal = Provenance a
-> Type TyName uni (Provenance a)
-> [Type TyName uni (Provenance a)]
-> Type TyName uni (Provenance a)
forall ann tyname (uni :: * -> *).
ann
-> Type tyname uni ann
-> [Type tyname uni ann]
-> Type tyname uni ann
PIR.mkIterTyApp Provenance a
ann (PLCRecType uni fun a -> Type TyName uni (Provenance a)
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType PLCRecType uni fun a
dty) ((TyVarDecl TyName (Provenance a) -> Type TyName uni (Provenance a))
-> [TyVarDecl TyName (Provenance a)]
-> [Type TyName uni (Provenance a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Provenance a
-> TyVarDecl TyName (Provenance a)
-> Type TyName uni (Provenance a)
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar Provenance a
ann) [TyVarDecl TyName (Provenance a)]
tvs)

    Name
xn <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
safeFreshName Text
"x"
    let destr :: PIRTerm uni fun a
destr =
            -- /\t_1 .. t_n
            [TyVarDecl TyName (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
PIR.mkIterTyAbs [TyVarDecl TyName (Provenance a)]
tvs (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
            -- \x
            Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs Provenance a
ann Name
xn Type TyName uni (Provenance a)
appliedReal (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
            -- See note [Recursive datatypes]
            -- unwrap
            Provenance a
-> PLCRecType uni fun a -> PIRTerm uni fun a -> PIRTerm uni fun a
forall a (uni :: * -> *) fun.
Provenance a
-> PLCRecType uni fun a -> PIRTerm uni fun a -> PIRTerm uni fun a
unwrap Provenance a
ann PLCRecType uni fun a
dty (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
            Provenance a -> Name -> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var Provenance a
ann Name
xn
    PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ (Provenance a -> Provenance a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Provenance a
a -> DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
Destructor Provenance a
a) PIRTerm uni fun a
destr

-- See note [Scott encoding of datatypes]
-- | Make the type of a destructor for a 'Datatype'.
-- @
--     mkDestructorTy <pattern functor of List> List
--         = forall (a :: *) . (List a) -> (<pattern functor of List>)
--         = forall (a :: *) . (List a) -> (forall (out_List :: *) . (out_List -> (a -> List a -> out_List) -> out_List))
-- @
mkDestructorTy :: PIRType uni a -> Datatype TyName Name uni fun (Provenance a) -> PIRType uni a
mkDestructorTy :: PIRType uni a
-> Datatype TyName Name uni fun (Provenance a) -> PIRType uni a
mkDestructorTy PIRType uni a
pf dt :: Datatype TyName Name uni fun (Provenance a)
dt@(Datatype Provenance a
ann TyVarDecl TyName (Provenance a)
_ [TyVarDecl TyName (Provenance a)]
tvs Name
_ [VarDecl TyName Name uni fun (Provenance a)]
_) =
    -- we essentially "unveil" the abstract type, so this
    -- is a function from the (instantiated) abstract type
    -- to the (unwrapped, i.e. the pattern functor of the) "real" Scott-encoded type that we can use as
    -- a destructor

    -- these types appears *inside* the scope of the abstraction for the datatype, so we can use a references to the name
    -- and we don't need to do anything to the pattern functor
    -- see note [Abstract data types]
    -- t t_1 .. t_n
    let appliedAbstract :: PIRType uni a
appliedAbstract = Provenance a
-> Datatype TyName Name uni fun (Provenance a) -> PIRType uni a
forall a (uni :: * -> *) fun.
a -> Datatype TyName Name uni fun a -> Type TyName uni a
mkDatatypeValueType Provenance a
ann Datatype TyName Name uni fun (Provenance a)
dt
    -- forall t_1 .. t_n
        destrTy :: PIRType uni a
destrTy = [TyVarDecl TyName (Provenance a)] -> PIRType uni a -> PIRType uni a
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
PIR.mkIterTyForall [TyVarDecl TyName (Provenance a)]
tvs (PIRType uni a -> PIRType uni a) -> PIRType uni a -> PIRType uni a
forall a b. (a -> b) -> a -> b
$ Provenance a -> PIRType uni a -> PIRType uni a -> PIRType uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun Provenance a
ann PIRType uni a
appliedAbstract PIRType uni a
pf
    in (Provenance a -> Provenance a) -> PIRType uni a -> PIRType uni a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Provenance a
a -> DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
DestructorType Provenance a
a) PIRType uni a
destrTy

-- The main function

-- | Compile a 'Datatype' bound with the given body.
compileDatatype :: Compiling m e uni fun a => Recursivity -> PIRTerm uni fun a -> Datatype TyName Name uni fun (Provenance a) -> m (PIRTerm uni fun a)
compileDatatype :: Recursivity
-> PIRTerm uni fun a
-> Datatype TyName Name uni fun (Provenance a)
-> m (PIRTerm uni fun a)
compileDatatype Recursivity
r PIRTerm uni fun a
body Datatype TyName Name uni fun (Provenance a)
d = do
    Provenance a
p <- m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing

    (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef, [Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
constrDefs, Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
destrDef) <- Recursivity
-> Datatype TyName Name uni fun (Provenance a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
      [Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)],
      Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
Recursivity
-> Datatype TyName Name uni fun (Provenance a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
      [Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)],
      Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
compileDatatypeDefs Recursivity
r Datatype TyName Name uni fun (Provenance a)
d

    let
        tyVars :: [TyVarDecl TyName (Provenance a)]
tyVars = [Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
-> TyVarDecl TyName (Provenance a)
forall var val. Def var val -> var
PIR.defVar Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef]
        tys :: [PLCType uni a]
tys = [PLCRecType uni fun a -> PLCType uni a
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType (PLCRecType uni fun a -> PLCType uni a)
-> PLCRecType uni fun a -> PLCType uni a
forall a b. (a -> b) -> a -> b
$ Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
-> PLCRecType uni fun a
forall var val. Def var val -> val
PIR.defVal Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef]
        vars :: [VarDecl TyName Name uni fun (Provenance a)]
vars = (Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
 -> VarDecl TyName Name uni fun (Provenance a))
-> [Def
      (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
-> [VarDecl TyName Name uni fun (Provenance a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
-> VarDecl TyName Name uni fun (Provenance a)
forall var val. Def var val -> var
PIR.defVar [Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
constrDefs [VarDecl TyName Name uni fun (Provenance a)]
-> [VarDecl TyName Name uni fun (Provenance a)]
-> [VarDecl TyName Name uni fun (Provenance a)]
forall a. [a] -> [a] -> [a]
++ [ Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
-> VarDecl TyName Name uni fun (Provenance a)
forall var val. Def var val -> var
PIR.defVar Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
destrDef ]
        vals :: [PIRTerm uni fun a]
vals = (Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
 -> PIRTerm uni fun a)
-> [Def
      (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
-> [PIRTerm uni fun a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
-> PIRTerm uni fun a
forall var val. Def var val -> val
PIR.defVal [Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
constrDefs [PIRTerm uni fun a] -> [PIRTerm uni fun a] -> [PIRTerm uni fun a]
forall a. [a] -> [a] -> [a]
++ [ Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
-> PIRTerm uni fun a
forall var val. Def var val -> val
PIR.defVal Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
destrDef ]
    -- See note [Abstract data types]
    PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ Provenance a
-> PIRTerm uni fun a -> [PIRTerm uni fun a] -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
PIR.mkIterApp Provenance a
p (Provenance a
-> PIRTerm uni fun a -> [PLCType uni a] -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
PIR.mkIterInst Provenance a
p ([TyVarDecl TyName (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
PIR.mkIterTyAbs [TyVarDecl TyName (Provenance a)]
tyVars ([VarDecl TyName Name uni fun (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni fun ann] -> term ann -> term ann
PIR.mkIterLamAbs [VarDecl TyName Name uni fun (Provenance a)]
vars PIRTerm uni fun a
body)) [PLCType uni a]
tys) [PIRTerm uni fun a]
vals

-- | Compile a 'Datatype' to a triple of type-constructor, data-constructors, destructor definitions.
compileDatatypeDefs  :: MonadQuote m => Recursivity
                     -> Datatype TyName Name uni fun (Provenance a)
                     -> m (PLC.Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
                          [PLC.Def (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)],
                          PLC.Def (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
compileDatatypeDefs :: Recursivity
-> Datatype TyName Name uni fun (Provenance a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
      [Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)],
      Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
compileDatatypeDefs Recursivity
r d :: Datatype TyName Name uni fun (Provenance a)
d@(Datatype Provenance a
ann TyVarDecl TyName (Provenance a)
tn [TyVarDecl TyName (Provenance a)]
_ Name
destr [VarDecl TyName Name uni fun (Provenance a)]
constrs) = do
    -- we compute the pattern functor and pass it around to avoid recomputing it
    Type TyName uni (Provenance a)
pf <- Provenance a
-> Datatype TyName Name uni fun (Provenance a)
-> m (Type TyName uni (Provenance a))
forall (m :: * -> *) ann (uni :: * -> *) fun.
MonadQuote m =>
ann -> Datatype TyName Name uni fun ann -> m (Type TyName uni ann)
mkDatatypePatternFunctor Provenance a
ann Datatype TyName Name uni fun (Provenance a)
d
    Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef <- TyVarDecl TyName (Provenance a)
-> PLCRecType uni fun a
-> Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
forall var val. var -> val -> Def var val
PIR.Def TyVarDecl TyName (Provenance a)
tn (PLCRecType uni fun a
 -> Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a))
-> m (PLCRecType uni fun a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Recursivity
-> Type TyName uni (Provenance a)
-> Datatype TyName Name uni fun (Provenance a)
-> m (PLCRecType uni fun a)
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
Recursivity
-> PIRType uni a
-> Datatype TyName Name uni fun (Provenance a)
-> m (PLCRecType uni fun a)
mkDatatypeType Recursivity
r Type TyName uni (Provenance a)
pf Datatype TyName Name uni fun (Provenance a)
d

    [Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
constrDefs <- [(VarDecl TyName Name uni fun (Provenance a), Int)]
-> ((VarDecl TyName Name uni fun (Provenance a), Int)
    -> m (Def
            (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
-> m [Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for ([VarDecl TyName Name uni fun (Provenance a)]
-> [Int] -> [(VarDecl TyName Name uni fun (Provenance a), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VarDecl TyName Name uni fun (Provenance a)]
constrs [Int
0..]) (((VarDecl TyName Name uni fun (Provenance a), Int)
  -> m (Def
          (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
 -> m [Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)])
-> ((VarDecl TyName Name uni fun (Provenance a), Int)
    -> m (Def
            (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
-> m [Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
forall a b. (a -> b) -> a -> b
$ \(VarDecl TyName Name uni fun (Provenance a)
c, Int
i) -> do
        let constrTy :: Type TyName uni (Provenance a)
constrTy = Datatype TyName Name uni fun (Provenance a)
-> VarDecl TyName Name uni fun (Provenance a)
-> Type TyName uni (Provenance a)
forall (uni :: * -> *) fun a.
Datatype TyName Name uni fun (Provenance a)
-> VarDecl TyName Name uni fun (Provenance a) -> PIRType uni a
mkConstructorType Datatype TyName Name uni fun (Provenance a)
d VarDecl TyName Name uni fun (Provenance a)
c
        VarDecl TyName Name uni fun (Provenance a)
-> PIRTerm uni fun a
-> Def
     (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
forall var val. var -> val -> Def var val
PIR.Def (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni fun (Provenance a)
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl (DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
Constructor Provenance a
ann) (VarDecl TyName Name uni fun (Provenance a) -> Name
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> name
_varDeclName VarDecl TyName Name uni fun (Provenance a)
c) Type TyName uni (Provenance a)
constrTy) (PIRTerm uni fun a
 -> Def
      (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
-> m (PIRTerm uni fun a)
-> m (Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PLCRecType uni fun a
-> Datatype TyName Name uni fun (Provenance a)
-> Int
-> m (PIRTerm uni fun a)
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
PLCRecType uni fun a
-> Datatype TyName Name uni fun (Provenance a)
-> Int
-> m (PIRTerm uni fun a)
mkConstructor (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
-> PLCRecType uni fun a
forall var val. Def var val -> val
PIR.defVal Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef) Datatype TyName Name uni fun (Provenance a)
d Int
i

    Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
destrDef <- do
        let destTy :: Type TyName uni (Provenance a)
destTy = Type TyName uni (Provenance a)
-> Datatype TyName Name uni fun (Provenance a)
-> Type TyName uni (Provenance a)
forall (uni :: * -> *) a fun.
PIRType uni a
-> Datatype TyName Name uni fun (Provenance a) -> PIRType uni a
mkDestructorTy Type TyName uni (Provenance a)
pf Datatype TyName Name uni fun (Provenance a)
d
        VarDecl TyName Name uni fun (Provenance a)
-> PIRTerm uni fun a
-> Def
     (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
forall var val. var -> val -> Def var val
PIR.Def (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni fun (Provenance a)
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl (DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
Destructor Provenance a
ann) Name
destr Type TyName uni (Provenance a)
destTy) (PIRTerm uni fun a
 -> Def
      (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
-> m (PIRTerm uni fun a)
-> m (Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PLCRecType uni fun a
-> Datatype TyName Name uni fun (Provenance a)
-> m (PIRTerm uni fun a)
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
PLCRecType uni fun a
-> Datatype TyName Name uni fun (Provenance a)
-> m (PIRTerm uni fun a)
mkDestructor (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
-> PLCRecType uni fun a
forall var val. Def var val -> val
PIR.defVal Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef) Datatype TyName Name uni fun (Provenance a)
d

    (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
 [Def
    (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)],
 Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
      [Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)],
      Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef, [Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)]
constrDefs, Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
destrDef)

compileRecDatatypes :: Compiling m e uni fun a => PIRTerm uni fun a -> NE.NonEmpty (Datatype TyName Name uni fun (Provenance a)) -> m (PIRTerm uni fun a)
compileRecDatatypes :: PIRTerm uni fun a
-> NonEmpty (Datatype TyName Name uni fun (Provenance a))
-> m (PIRTerm uni fun a)
compileRecDatatypes PIRTerm uni fun a
body NonEmpty (Datatype TyName Name uni fun (Provenance a))
ds = case NonEmpty (Datatype TyName Name uni fun (Provenance a))
ds of
    Datatype TyName Name uni fun (Provenance a)
d NE.:| [] -> Recursivity
-> PIRTerm uni fun a
-> Datatype TyName Name uni fun (Provenance a)
-> m (PIRTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Recursivity
-> PIRTerm uni fun a
-> Datatype TyName Name uni fun (Provenance a)
-> m (PIRTerm uni fun a)
compileDatatype Recursivity
Rec PIRTerm uni fun a
body Datatype TyName Name uni fun (Provenance a)
d
    NonEmpty (Datatype TyName Name uni fun (Provenance a))
_          -> m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (Provenance a)
-> (Provenance a -> m (PIRTerm uni fun a)) -> m (PIRTerm uni fun a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Provenance a
p -> AReview e (Error uni fun (Provenance a))
-> Error uni fun (Provenance a) -> m (PIRTerm uni fun a)
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e (Error uni fun (Provenance a))
forall r (uni :: * -> *) fun a.
AsError r uni fun a =>
Prism' r (Error uni fun a)
_Error (Error uni fun (Provenance a) -> m (PIRTerm uni fun a))
-> Error uni fun (Provenance a) -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ Provenance a -> Text -> Error uni fun (Provenance a)
forall (uni :: * -> *) fun a. a -> Text -> Error uni fun a
UnsupportedError Provenance a
p Text
"Mutually recursive datatypes"