{-# LANGUAGE ConstraintKinds  #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs            #-}
{-# LANGUAGE LambdaCase       #-}
{-# LANGUAGE TypeFamilies     #-}

{- |
Call site inlining machinery. We inline if the size of the inlined result is not larger.
See Note [Inlining and beta reduction of functions].
-}
module PlutusIR.Transform.Inline.CallSiteInline where

import PlutusCore qualified as PLC
import PlutusCore.Rename (rename)
import PlutusCore.Rename.Internal (Dupable (Dupable))
import PlutusIR.Analysis.Size (Size, termSize)
import PlutusIR.Contexts
import PlutusIR.Core
import PlutusIR.Transform.Inline.Utils
import PlutusIR.Transform.Substitute

{- Note [Inlining and beta reduction of functions]

We inline if its cost and size are acceptable.

For size, we compare the sizes (in terms of AST nodes before and after the inlining and beta
reduction), and inline only if it does not increase the size. In the above example, we count
the number of AST nodes in `f a b` and in `a`. The latter is smaller, which means inlining
reduces the size.

We care about program size increases primarily because it
affects the size of the serialized script, which appears on chain and must be paid for.
This is different to many compilers which care about this also because e.g. larger ASTs
slow down compilation. We care about this too, but the serialized size is the main driver for us.

The number of AST nodes is an approximate rather than a precise measure. It correlates,
but doesn't directly map to the size of the serialised script. Different kinds of AST nodes
may take different number of bits to encode; in particular, a `Constant` node always
counts as one AST node, but the constant in it can be of arbitrary size. Then, would it be
better to use the size of the serialised term, instead of the number of AST nodes? Not
necessarily, because other transformations, such as CSE, may change the size further;
specifically, if a large constant occurs multiple times in a program, it may get CSE'd.

In general there's no reliable way to precisely predict the size impact of an inlining
decision, and we believe the number of AST nodes is in fact a good approximation.

For cost, we check whether the RHS (in this example, `\x. \y -> x`) has a small cost.
If the RHS has a non-zero arity, then the cost is always small (since a lambda or a type
abstraction is already a value). This may not be the case if the arity is zero.

For effect-safety, we require: (1) the RHS be pure, i.e., evaluating it is guaranteed to
not have side effects; (2) all arguments be pure, since otherwise it is unsafe to
perform beta reduction.

-}

{- | Apply the RHS of the given variable to the given arguments, and beta-reduce
the application, if possible.
-}
applyAndBetaReduce ::
  forall tyname name uni fun ann.
  (InliningConstraints tyname name uni fun) =>
  -- | The rhs of the variable, should have been renamed already
  Term tyname name uni fun ann ->
  -- | The arguments, already processed
  AppContext tyname name uni fun ann ->
  InlineM tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
applyAndBetaReduce :: forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
applyAndBetaReduce Term tyname name uni fun ann
rhs AppContext tyname name uni fun ann
args0 = do
  let go ::
        Term tyname name uni fun ann ->
        AppContext tyname name uni fun ann ->
        InlineM tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
      go :: Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
go Term tyname name uni fun ann
acc AppContext tyname name uni fun ann
args = case (Term tyname name uni fun ann
acc, AppContext tyname name uni fun ann
args) of
        (LamAbs ann
_ann name
n Type tyname uni ann
_ty Term tyname name uni fun ann
tm, TermAppContext Term tyname name uni fun ann
arg ann
_ AppContext tyname name uni fun ann
args') -> do
          Bool
safe <- name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
safeToBetaReduce name
n Term tyname name uni fun ann
arg Term tyname name uni fun ann
acc
          if Bool
safe -- we only do substitution if it is safe to beta reduce
            then do
              Term tyname name uni fun ann
acc' <- do
                (name
 -> InlineM
      tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Term tyname name uni fun ann)
forall (m :: * -> *) name tyname (uni :: * -> *) fun ann.
Monad m =>
(name -> m (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstNamesM -- substitute the term param with the arg in the function body
                  -- rename before substitution to ensure global uniqueness (may not be needed but
                  -- no harm in renaming just to be sure)
                  (\name
tmName -> if name
tmName name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
n then Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
forall a. a -> Maybe a
Just (Term tyname name uni fun ann
 -> Maybe (Term tyname name uni fun ann))
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Term tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Term tyname name uni fun ann)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
PLC.rename Term tyname name uni fun ann
arg else Maybe (Term tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing)
                  Term tyname name uni fun ann
tm -- drop the beta reduced term lambda
              Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
go Term tyname name uni fun ann
acc' AppContext tyname name uni fun ann
args'
            -- if it is not safe to beta reduce, just return the processed application
            else Maybe (Term tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term tyname name uni fun ann)
 -> InlineM
      tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> (Term tyname name uni fun ann
    -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
forall a. a -> Maybe a
Just (Term tyname name uni fun ann
 -> InlineM
      tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
fillAppContext Term tyname name uni fun ann
acc AppContext tyname name uni fun ann
args
        (TyAbs ann
_ann tyname
n Kind ann
_kd Term tyname name uni fun ann
tm, TypeAppContext Type tyname uni ann
arg ann
_ AppContext tyname name uni fun ann
args') -> do
          Term tyname name uni fun ann
acc' <-
            (tyname
 -> ReaderT
      (InlineInfo tyname name uni fun ann)
      (StateT (InlinerState tyname name uni fun ann) Quote)
      (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Term tyname name uni fun ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann name fun.
Monad m =>
(tyname -> m (Maybe (Type tyname uni ann)))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
termSubstTyNamesM -- substitute the type param with the arg
              (\tyname
tyName -> if tyname
tyName tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== tyname
n then Type tyname uni ann -> Maybe (Type tyname uni ann)
forall a. a -> Maybe a
Just (Type tyname uni ann -> Maybe (Type tyname uni ann))
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Type tyname uni ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Type tyname uni ann))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Type tyname uni ann)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.rename Type tyname uni ann
arg else Maybe (Type tyname uni ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Type tyname uni ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Type tyname uni ann)
forall a. Maybe a
Nothing)
              Term tyname name uni fun ann
tm -- drop the beta reduced type lambda
          Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
go Term tyname name uni fun ann
acc' AppContext tyname name uni fun ann
args'
        -- term/type argument mismatch, don't inline
        (LamAbs{}, TypeAppContext{}) -> Maybe (Term tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing
        (TyAbs{}, TermAppContext{}) -> Maybe (Term tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing
        -- no more lambda abstraction, just return the processed application
        (Term tyname name uni fun ann
_, AppContext tyname name uni fun ann
_) -> Maybe (Term tyname name uni fun ann)
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term tyname name uni fun ann)
 -> InlineM
      tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> (Term tyname name uni fun ann
    -> Maybe (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
forall a. a -> Maybe a
Just (Term tyname name uni fun ann
 -> InlineM
      tyname name uni fun ann (Maybe (Term tyname name uni fun ann)))
-> Term tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> Term tyname name uni fun ann
fillAppContext Term tyname name uni fun ann
acc AppContext tyname name uni fun ann
args

      -- Is it safe to turn `(\a -> body) arg` into `body [a := arg]`?
      -- The criteria is the same as the criteria for inlining `a` in
      -- `let !a = arg in body`.
      safeToBetaReduce ::
        -- `a`
        name ->
        -- `arg`
        Term tyname name uni fun ann ->
        -- the body `a` will be beta reduced in
        Term tyname name uni fun ann ->
        InlineM tyname name uni fun ann Bool
      safeToBetaReduce :: name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
safeToBetaReduce = Strictness
-> name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Strictness
-> name
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
shouldUnconditionallyInline Strictness
Strict
  Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
go Term tyname name uni fun ann
rhs AppContext tyname name uni fun ann
args0

-- | Consider inlining a variable. For applications, consider whether to apply and beta reduce.
callSiteInline ::
  forall tyname name uni fun ann.
  (InliningConstraints tyname name uni fun) =>
  -- | The term size if it were not inlined.
  Size ->
  -- | The `Utils.VarInfo` of the variable (the head of the term).
  InlineVarInfo tyname name uni fun ann ->
  -- | The application context of the term, already processed.
  AppContext tyname name uni fun ann ->
  InlineM tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
callSiteInline :: forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Size
-> InlineVarInfo tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
callSiteInline Size
processedTSize = InlineVarInfo tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Term tyname name uni fun ann))
go
  where
    go :: InlineVarInfo tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Term tyname name uni fun ann))
go InlineVarInfo tyname name uni fun ann
varInfo AppContext tyname name uni fun ann
args = do
        let
          defAsInlineTerm :: InlineTerm tyname name uni fun ann
defAsInlineTerm = InlineVarInfo tyname name uni fun ann
-> InlineTerm tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
InlineVarInfo tyname name uni fun ann
-> InlineTerm tyname name uni fun ann
varRhs InlineVarInfo tyname name uni fun ann
varInfo
          inlineTermToTerm :: InlineTerm tyname name uni fun ann
              -> Term tyname name uni fun ann
          inlineTermToTerm :: InlineTerm tyname name uni fun ann -> Term tyname name uni fun ann
inlineTermToTerm (Done (Dupable Term tyname name uni fun ann
var)) = Term tyname name uni fun ann
var
          -- extract out the rhs without renaming, we only rename
          -- when we know there's substitution
          headRhs :: Term tyname name uni fun ann
headRhs = InlineTerm tyname name uni fun ann -> Term tyname name uni fun ann
inlineTermToTerm InlineTerm tyname name uni fun ann
defAsInlineTerm
          -- The definition itself will be inlined, so we need to check that the cost
          -- of that is acceptable. Note that we do _not_ check the cost of the _body_.
          -- We would have paid that regardless.
          -- Consider e.g. `let y = \x. f x`. We pay the cost of the `f x` at
          -- every call site regardless. The work that is being duplicated is
          -- the work for the lambda.
          costIsOk :: Bool
costIsOk = Term tyname name uni fun ann -> Bool
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Bool
costIsAcceptable Term tyname name uni fun ann
headRhs
        -- check if binding is pure to avoid duplicated effects.
        -- For strict bindings we can't accidentally make any effects happen less often
        -- than it would have before, but we can make it happen more often.
        -- We could potentially do this safely in non-conservative mode.
        Bool
rhsPure <- Strictness
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Strictness
-> Term tyname name uni fun ann
-> InlineM tyname name uni fun ann Bool
isTermBindingPure (InlineVarInfo tyname name uni fun ann -> Strictness
forall tyname name (uni :: * -> *) fun ann.
InlineVarInfo tyname name uni fun ann -> Strictness
varStrictness InlineVarInfo tyname name uni fun ann
varInfo) Term tyname name uni fun ann
headRhs
        if Bool
costIsOk Bool -> Bool -> Bool
&& Bool
rhsPure then do
          -- rename the rhs of the variable before any substitution
          Term tyname name uni fun ann
renamedRhs <- Term tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Term tyname name uni fun ann)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
rename Term tyname name uni fun ann
headRhs
          Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Term tyname name uni fun ann))
forall tyname name (uni :: * -> *) fun ann.
InliningConstraints tyname name uni fun =>
Term tyname name uni fun ann
-> AppContext tyname name uni fun ann
-> InlineM
     tyname name uni fun ann (Maybe (Term tyname name uni fun ann))
applyAndBetaReduce Term tyname name uni fun ann
renamedRhs AppContext tyname name uni fun ann
args ReaderT
  (InlineInfo tyname name uni fun ann)
  (StateT (InlinerState tyname name uni fun ann) Quote)
  (Maybe (Term tyname name uni fun ann))
-> (Maybe (Term tyname name uni fun ann)
    -> ReaderT
         (InlineInfo tyname name uni fun ann)
         (StateT (InlinerState tyname name uni fun ann) Quote)
         (Maybe (Term tyname name uni fun ann)))
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Term tyname name uni fun ann))
forall a b.
ReaderT
  (InlineInfo tyname name uni fun ann)
  (StateT (InlinerState tyname name uni fun ann) Quote)
  a
-> (a
    -> ReaderT
         (InlineInfo tyname name uni fun ann)
         (StateT (InlinerState tyname name uni fun ann) Quote)
         b)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just Term tyname name uni fun ann
inlined -> do
              let -- Inline only if the size is no bigger than not inlining.
                  sizeIsOk :: Bool
sizeIsOk = Term tyname name uni fun ann -> Size
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Size
termSize Term tyname name uni fun ann
inlined Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
<= Size
processedTSize
              Maybe (Term tyname name uni fun ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term tyname name uni fun ann)
 -> ReaderT
      (InlineInfo tyname name uni fun ann)
      (StateT (InlinerState tyname name uni fun ann) Quote)
      (Maybe (Term tyname name uni fun ann)))
-> Maybe (Term tyname name uni fun ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Term tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ if Bool
sizeIsOk then Term tyname name uni fun ann
-> Maybe (Term tyname name uni fun ann)
forall a. a -> Maybe a
Just Term tyname name uni fun ann
inlined else Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing
            Maybe (Term tyname name uni fun ann)
Nothing -> Maybe (Term tyname name uni fun ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing
        else Maybe (Term tyname name uni fun ann)
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     (Maybe (Term tyname name uni fun ann))
forall a.
a
-> ReaderT
     (InlineInfo tyname name uni fun ann)
     (StateT (InlinerState tyname name uni fun ann) Quote)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Term tyname name uni fun ann)
forall a. Maybe a
Nothing