{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}

-- | Optimization passes for removing dead code, mainly dead let bindings.
module PlutusIR.Transform.DeadCode
  ( removeDeadBindings
  , removeDeadBindingsPass
  , removeDeadBindingsPassSC
  ) where

import PlutusIR
import PlutusIR.Analysis.Dependencies qualified as Deps
import PlutusIR.MkPir
import PlutusIR.Transform.Rename ()

import PlutusCore qualified as PLC
import PlutusCore.Builtin qualified as PLC
import PlutusCore.Name.Unique qualified as PLC

import Control.Lens
import Control.Monad.Reader

import Data.Coerce
import Data.Set qualified as Set

import Algebra.Graph qualified as G
import Algebra.Graph.ToGraph qualified as T
import Data.List.NonEmpty qualified as NE
import PlutusCore.Quote (MonadQuote, freshTyName)
import PlutusCore.StdLib.Data.ScottUnit qualified as Unit
import PlutusIR.Analysis.Builtins
import PlutusIR.Analysis.VarInfo
import PlutusIR.Pass
import PlutusIR.TypeCheck qualified as TC
import Witherable (Witherable (wither))

removeDeadBindingsPassSC ::
  (PLC.Typecheckable uni fun, PLC.GEq uni, Ord a, MonadQuote m)
  => TC.PirTCConfig uni fun
  -> BuiltinsInfo uni fun
  -> Pass m TyName Name uni fun a
removeDeadBindingsPassSC :: forall (uni :: * -> *) fun a (m :: * -> *).
(Typecheckable uni fun, GEq uni, Ord a, MonadQuote m) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Pass m TyName Name uni fun a
removeDeadBindingsPassSC PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo =
  Pass m TyName Name uni fun a
forall name tyname (m :: * -> *) a (uni :: * -> *) fun.
(HasUnique name TermUnique, HasUnique tyname TypeUnique,
 MonadQuote m, Ord a) =>
Pass m tyname name uni fun a
renamePass Pass m TyName Name uni fun a
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall a. Semigroup a => a -> a -> a
<> PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Pass m TyName Name uni fun a
forall (uni :: * -> *) fun a (m :: * -> *).
(Typecheckable uni fun, GEq uni, Ord a, MonadQuote m) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Pass m TyName Name uni fun a
removeDeadBindingsPass PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo

removeDeadBindingsPass ::
  (PLC.Typecheckable uni fun, PLC.GEq uni, Ord a, MonadQuote m)
  => TC.PirTCConfig uni fun
  -> BuiltinsInfo uni fun
  -> Pass m TyName Name uni fun a
removeDeadBindingsPass :: forall (uni :: * -> *) fun a (m :: * -> *).
(Typecheckable uni fun, GEq uni, Ord a, MonadQuote m) =>
PirTCConfig uni fun
-> BuiltinsInfo uni fun -> Pass m TyName Name uni fun a
removeDeadBindingsPass PirTCConfig uni fun
tcconfig BuiltinsInfo uni fun
binfo =
  String
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
String
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
NamedPass String
"dead code elimination" (Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a)
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall a b. (a -> b) -> a -> b
$
    (Term TyName Name uni fun a -> m (Term TyName Name uni fun a))
-> [Condition TyName Name uni fun a]
-> [BiCondition TyName Name uni fun a]
-> Pass m TyName Name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> [Condition tyname name uni fun a]
-> [BiCondition tyname name uni fun a]
-> Pass m tyname name uni fun a
Pass
      (BuiltinsInfo uni fun
-> Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
forall name (uni :: * -> *) fun (m :: * -> *) a.
(HasUnique name TermUnique, ToBuiltinMeaning uni fun,
 MonadQuote m) =>
BuiltinsInfo uni fun
-> Term TyName name uni fun a -> m (Term TyName name uni fun a)
removeDeadBindings BuiltinsInfo uni fun
binfo)
      [PirTCConfig uni fun -> Condition TyName Name uni fun a
forall (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni) =>
PirTCConfig uni fun -> Condition TyName Name uni fun a
Typechecks PirTCConfig uni fun
tcconfig, Condition TyName Name uni fun a
forall tyname name a (uni :: * -> *) fun.
(HasUnique tyname TypeUnique, HasUnique name TermUnique, Ord a) =>
Condition tyname name uni fun a
GloballyUniqueNames]
      [Condition TyName Name uni fun a
-> BiCondition TyName Name uni fun a
forall tyname name (uni :: * -> *) fun a.
Condition tyname name uni fun a
-> BiCondition tyname name uni fun a
ConstCondition (PirTCConfig uni fun -> Condition TyName Name uni fun a
forall (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni) =>
PirTCConfig uni fun -> Condition TyName Name uni fun a
Typechecks PirTCConfig uni fun
tcconfig)]

-- We only need MonadQuote to make new types for bindings
-- | Remove all the dead let bindings in a term.
removeDeadBindings
    :: (PLC.HasUnique name PLC.TermUnique,
       PLC.ToBuiltinMeaning uni fun, PLC.MonadQuote m)
    => BuiltinsInfo uni fun
    -> Term TyName name uni fun a
    -> m (Term TyName name uni fun a)
removeDeadBindings :: forall name (uni :: * -> *) fun (m :: * -> *) a.
(HasUnique name TermUnique, ToBuiltinMeaning uni fun,
 MonadQuote m) =>
BuiltinsInfo uni fun
-> Term TyName name uni fun a -> m (Term TyName name uni fun a)
removeDeadBindings BuiltinsInfo uni fun
binfo Term TyName name uni fun a
t = do
    let vinfo :: VarsInfo TyName name uni a
vinfo = Term TyName name uni fun a -> VarsInfo TyName name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term TyName name uni fun a
t
    ReaderT Liveness m (Term TyName name uni fun a)
-> Liveness -> m (Term TyName name uni fun a)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (LensLike
  (WrappedMonad (ReaderT Liveness m))
  (Term TyName name uni fun a)
  (Term TyName name uni fun a)
  (Term TyName name uni fun a)
  (Term TyName name uni fun a)
-> (Term TyName name uni fun a
    -> ReaderT Liveness m (Term TyName name uni fun a))
-> Term TyName name uni fun a
-> ReaderT Liveness m (Term TyName name uni fun a)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
  (WrappedMonad (ReaderT Liveness m))
  (Term TyName name uni fun a)
  (Term TyName name uni fun a)
  (Term TyName name uni fun a)
  (Term TyName name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term TyName name uni fun a
-> ReaderT Liveness m (Term TyName name uni fun a)
forall (m :: * -> *) name (uni :: * -> *) fun a.
(MonadReader Liveness m, HasUnique name TermUnique,
 MonadQuote m) =>
Term TyName name uni fun a -> m (Term TyName name uni fun a)
processTerm Term TyName name uni fun a
t) (BuiltinsInfo uni fun
-> VarsInfo TyName name uni a
-> Term TyName name uni fun a
-> Liveness
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique,
 ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> Liveness
calculateLiveness BuiltinsInfo uni fun
binfo VarsInfo TyName name uni a
vinfo Term TyName name uni fun a
t)

type Liveness = Set.Set Deps.Node

calculateLiveness
    :: (PLC.HasUnique name PLC.TermUnique, PLC.HasUnique tyname PLC.TypeUnique,
       PLC.ToBuiltinMeaning uni fun)
    => BuiltinsInfo uni fun
    -> VarsInfo tyname name uni a
    -> Term tyname name uni fun a
    -> Liveness
calculateLiveness :: forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique,
 ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> Liveness
calculateLiveness BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
t =
    let
        depGraph :: G.Graph Deps.Node
        depGraph :: Graph Node
depGraph = BuiltinsInfo uni fun
-> VarsInfo tyname name uni a
-> Term tyname name uni fun a
-> Graph Node
forall g tyname name (uni :: * -> *) fun a.
(DepGraph g, HasUnique tyname TypeUnique,
 HasUnique name TermUnique, ToBuiltinMeaning uni fun) =>
BuiltinsInfo uni fun
-> VarsInfo tyname name uni a -> Term tyname name uni fun a -> g
Deps.runTermDeps BuiltinsInfo uni fun
binfo VarsInfo tyname name uni a
vinfo Term tyname name uni fun a
t
    in [Node] -> Liveness
forall a. Ord a => [a] -> Set a
Set.fromList ([Node] -> Liveness) -> [Node] -> Liveness
forall a b. (a -> b) -> a -> b
$ Graph Node -> ToVertex (Graph Node) -> [ToVertex (Graph Node)]
forall t.
(ToGraph t, Ord (ToVertex t)) =>
t -> ToVertex t -> [ToVertex t]
T.reachable Graph Node
depGraph ToVertex (Graph Node)
Node
Deps.Root

live :: (MonadReader Liveness m, PLC.HasUnique n unique) => n -> m Bool
live :: forall (m :: * -> *) n unique.
(MonadReader Liveness m, HasUnique n unique) =>
n -> m Bool
live n
n =
    let
        u :: Unique
u = unique -> Unique
forall a b. Coercible a b => a -> b
coerce (unique -> Unique) -> unique -> Unique
forall a b. (a -> b) -> a -> b
$ n
n n -> Getting unique n unique -> unique
forall s a. s -> Getting a s a -> a
^. Getting unique n unique
forall a unique. HasUnique a unique => Lens' a unique
Lens' n unique
PLC.unique
    in (Liveness -> Bool) -> m Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Liveness -> Bool) -> m Bool) -> (Liveness -> Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ Node -> Liveness -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Unique -> Node
Deps.Variable Unique
u)

liveBinding
    :: (MonadReader Liveness m, PLC.HasUnique name PLC.TermUnique, MonadQuote m)
    => Binding TyName name uni fun a
    -> m (Maybe (Binding TyName name uni fun a))
liveBinding :: forall (m :: * -> *) name (uni :: * -> *) fun a.
(MonadReader Liveness m, HasUnique name TermUnique,
 MonadQuote m) =>
Binding TyName name uni fun a
-> m (Maybe (Binding TyName name uni fun a))
liveBinding =
    let
        -- TODO: HasUnique instances for VarDecl and TyVarDecl?
        liveVarDecl :: VarDecl tyname n uni ann -> m Bool
liveVarDecl (VarDecl ann
_ n
n Type tyname uni ann
_) = n -> m Bool
forall (m :: * -> *) n unique.
(MonadReader Liveness m, HasUnique n unique) =>
n -> m Bool
live n
n
        liveTyVarDecl :: TyVarDecl n ann -> m Bool
liveTyVarDecl (TyVarDecl ann
_ n
n Kind ann
_) = n -> m Bool
forall (m :: * -> *) n unique.
(MonadReader Liveness m, HasUnique n unique) =>
n -> m Bool
live n
n
    in \case
        b :: Binding TyName name uni fun a
b@(TermBind a
_ Strictness
_ VarDecl TyName name uni a
d Term TyName name uni fun a
_) -> do
            Bool
l <- VarDecl TyName name uni a -> m Bool
forall {unique} {m :: * -> *} {n} {tyname} {uni :: * -> *} {ann}.
(Coercible unique Int, MonadReader Liveness m,
 HasUnique n unique) =>
VarDecl tyname n uni ann -> m Bool
liveVarDecl VarDecl TyName name uni a
d
            Maybe (Binding TyName name uni fun a)
-> m (Maybe (Binding TyName name uni fun a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Binding TyName name uni fun a)
 -> m (Maybe (Binding TyName name uni fun a)))
-> Maybe (Binding TyName name uni fun a)
-> m (Maybe (Binding TyName name uni fun a))
forall a b. (a -> b) -> a -> b
$ if Bool
l then Binding TyName name uni fun a
-> Maybe (Binding TyName name uni fun a)
forall a. a -> Maybe a
Just Binding TyName name uni fun a
b else Maybe (Binding TyName name uni fun a)
forall a. Maybe a
Nothing
        b :: Binding TyName name uni fun a
b@(TypeBind a
_ TyVarDecl TyName a
d Type TyName uni a
_) -> do
            Bool
l <- TyVarDecl TyName a -> m Bool
forall {unique} {m :: * -> *} {n} {ann}.
(Coercible unique Int, MonadReader Liveness m,
 HasUnique n unique) =>
TyVarDecl n ann -> m Bool
liveTyVarDecl TyVarDecl TyName a
d
            Maybe (Binding TyName name uni fun a)
-> m (Maybe (Binding TyName name uni fun a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Binding TyName name uni fun a)
 -> m (Maybe (Binding TyName name uni fun a)))
-> Maybe (Binding TyName name uni fun a)
-> m (Maybe (Binding TyName name uni fun a))
forall a b. (a -> b) -> a -> b
$ if Bool
l then Binding TyName name uni fun a
-> Maybe (Binding TyName name uni fun a)
forall a. a -> Maybe a
Just Binding TyName name uni fun a
b else Maybe (Binding TyName name uni fun a)
forall a. Maybe a
Nothing
        b :: Binding TyName name uni fun a
b@(DatatypeBind a
x (Datatype a
_ TyVarDecl TyName a
d [TyVarDecl TyName a]
_ name
destr [VarDecl TyName name uni a]
constrs)) -> do
            Bool
dtypeLive <- TyVarDecl TyName a -> m Bool
forall {unique} {m :: * -> *} {n} {ann}.
(Coercible unique Int, MonadReader Liveness m,
 HasUnique n unique) =>
TyVarDecl n ann -> m Bool
liveTyVarDecl TyVarDecl TyName a
d
            Bool
destrLive <- name -> m Bool
forall (m :: * -> *) n unique.
(MonadReader Liveness m, HasUnique n unique) =>
n -> m Bool
live name
destr
            [Bool]
constrsLive <- (VarDecl TyName name uni a -> m Bool)
-> [VarDecl TyName name uni a] -> m [Bool]
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 VarDecl TyName name uni a -> m Bool
forall {unique} {m :: * -> *} {n} {tyname} {uni :: * -> *} {ann}.
(Coercible unique Int, MonadReader Liveness m,
 HasUnique n unique) =>
VarDecl tyname n uni ann -> m Bool
liveVarDecl [VarDecl TyName name uni a]
constrs
            let termLive :: Bool
termLive = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (Bool
destrLive Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: [Bool]
constrsLive)
            case (Bool
dtypeLive, Bool
termLive) of
                 -- At least one term-level part is live, keep the whole thing
                (Bool
_, Bool
True)      -> Maybe (Binding TyName name uni fun a)
-> m (Maybe (Binding TyName name uni fun a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Binding TyName name uni fun a)
 -> m (Maybe (Binding TyName name uni fun a)))
-> Maybe (Binding TyName name uni fun a)
-> m (Maybe (Binding TyName name uni fun a))
forall a b. (a -> b) -> a -> b
$ Binding TyName name uni fun a
-> Maybe (Binding TyName name uni fun a)
forall a. a -> Maybe a
Just Binding TyName name uni fun a
b
                -- Nothing is live, remove the whole thing
                (Bool
False, Bool
False) -> Maybe (Binding TyName name uni fun a)
-> m (Maybe (Binding TyName name uni fun a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Binding TyName name uni fun a)
forall a. Maybe a
Nothing
                -- See Note [Dependencies for datatype bindings, and pruning them]
                -- Datatype is live but no term-level parts are, replace with a trivial type binding
                (Bool
True, Bool
False)  -> Binding TyName name uni fun a
-> Maybe (Binding TyName name uni fun a)
forall a. a -> Maybe a
Just (Binding TyName name uni fun a
 -> Maybe (Binding TyName name uni fun a))
-> (Type TyName uni a -> Binding TyName name uni fun a)
-> Type TyName uni a
-> Maybe (Binding TyName name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a
-> TyVarDecl TyName a
-> Type TyName uni a
-> Binding TyName name uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind a
x TyVarDecl TyName a
d (Type TyName uni a -> Maybe (Binding TyName name uni fun a))
-> m (Type TyName uni a)
-> m (Maybe (Binding TyName name uni fun a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind a -> m (Type TyName uni a)
forall (m :: * -> *) a (uni :: * -> *).
MonadQuote m =>
Kind a -> m (Type TyName uni a)
mkTypeOfKind (TyVarDecl TyName a -> Kind a
forall tyname ann. TyVarDecl tyname ann -> Kind ann
_tyVarDeclKind TyVarDecl TyName a
d)

-- | Given a kind, make a type (any type!) of that kind.
-- Generates things of the form 'unit -> unit -> ... -> unit'
mkTypeOfKind :: MonadQuote m => Kind a -> m (Type TyName uni a)
mkTypeOfKind :: forall (m :: * -> *) a (uni :: * -> *).
MonadQuote m =>
Kind a -> m (Type TyName uni a)
mkTypeOfKind = \case
    -- The scott-encoded unit here is a little bulky but it continues to be the easiest
    -- way to get a type of kind Type without relying on builtins.
    Type a
a -> Type TyName uni a -> m (Type TyName uni a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni a -> m (Type TyName uni a))
-> Type TyName uni a -> m (Type TyName uni a)
forall a b. (a -> b) -> a -> b
$ a
a a -> Type TyName uni () -> Type TyName uni a
forall a b. a -> Type TyName uni b -> Type TyName uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
Unit.unit
    KindArrow a
a Kind a
ki Kind a
ki' -> do
        TyName
n <- Text -> m TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
        a -> TyName -> Kind a -> Type TyName uni a -> Type TyName uni a
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam a
a TyName
n Kind a
ki (Type TyName uni a -> Type TyName uni a)
-> m (Type TyName uni a) -> m (Type TyName uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind a -> m (Type TyName uni a)
forall (m :: * -> *) a (uni :: * -> *).
MonadQuote m =>
Kind a -> m (Type TyName uni a)
mkTypeOfKind Kind a
ki'

processTerm
    :: (MonadReader Liveness m, PLC.HasUnique name PLC.TermUnique, MonadQuote m)
    => Term TyName name uni fun a
    -> m (Term TyName name uni fun a)
processTerm :: forall (m :: * -> *) name (uni :: * -> *) fun a.
(MonadReader Liveness m, HasUnique name TermUnique,
 MonadQuote m) =>
Term TyName name uni fun a -> m (Term TyName name uni fun a)
processTerm = \case
    -- throw away dead bindings
    Let a
x Recursivity
r NonEmpty (Binding TyName name uni fun a)
bs Term TyName name uni fun a
t -> a
-> Recursivity
-> [Binding TyName name uni fun a]
-> Term TyName name uni fun a
-> Term TyName name uni fun a
forall a tyname name (uni :: * -> *) fun.
a
-> Recursivity
-> [Binding tyname name uni fun a]
-> Term tyname name uni fun a
-> Term tyname name uni fun a
mkLet a
x Recursivity
r ([Binding TyName name uni fun a]
 -> Term TyName name uni fun a -> Term TyName name uni fun a)
-> m [Binding TyName name uni fun a]
-> m (Term TyName name uni fun a -> Term TyName name uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Binding TyName name uni fun a
 -> m (Maybe (Binding TyName name uni fun a)))
-> [Binding TyName name uni fun a]
-> m [Binding TyName name uni fun a]
forall (t :: * -> *) (f :: * -> *) a b.
(Witherable t, Applicative f) =>
(a -> f (Maybe b)) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f (Maybe b)) -> [a] -> f [b]
wither Binding TyName name uni fun a
-> m (Maybe (Binding TyName name uni fun a))
forall (m :: * -> *) name (uni :: * -> *) fun a.
(MonadReader Liveness m, HasUnique name TermUnique,
 MonadQuote m) =>
Binding TyName name uni fun a
-> m (Maybe (Binding TyName name uni fun a))
liveBinding (NonEmpty (Binding TyName name uni fun a)
-> [Binding TyName name uni fun a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Binding TyName name uni fun a)
bs) m (Term TyName name uni fun a -> Term TyName name uni fun a)
-> m (Term TyName name uni fun a) -> m (Term TyName name uni fun a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term TyName name uni fun a -> m (Term TyName name uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term TyName name uni fun a
t
    Term TyName name uni fun a
x            -> Term TyName name uni fun a -> m (Term TyName name uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term TyName name uni fun a
x