{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module PlutusCore.Examples.Data.Shad
  ( shad
  , mkShad
  , recUnit
  , runRecUnit
  ) where

import PlutusCore.Core
import PlutusCore.MkPlc
import PlutusCore.Name.Unique
import PlutusCore.Quote

{-|

> getShadF a = \(rec :: * -> *) (i :: *) -> a -> all (a :: * -> *). a i -> integer -}
getShadF :: uni `HasTypeLevel` Integer => TyName -> Quote (Type TyName uni ())
getShadF :: forall (uni :: * -> *).
HasTypeLevel uni Integer =>
TyName -> Quote (Type TyName uni ())
getShadF TyName
a = do
  TyName
rec <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"rec"
  TyName
i <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"i"
  Type TyName uni () -> Quote (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
    (Type TyName uni () -> Quote (Type TyName uni ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (Type TyName uni ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
rec (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Kind () -> Kind ()) -> Kind () -> Kind ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
i (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
a (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Kind () -> Kind ()) -> Kind () -> Kind ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
i)
    (Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()

{-|

> \(a :: *) -> ifix (getShadF a) a -}
shad :: uni `HasTypeLevel` Integer => Type TyName uni ()
shad :: forall (uni :: * -> *).
HasTypeLevel uni Integer =>
Type TyName uni ()
shad = Quote (Type TyName uni ()) -> Type TyName uni ()
forall a. Quote a -> a
runQuote (Quote (Type TyName uni ()) -> Type TyName uni ())
-> Quote (Type TyName uni ()) -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ do
  TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
  Type TyName uni ()
shadF <- TyName -> Quote (Type TyName uni ())
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
TyName -> Quote (Type TyName uni ())
getShadF TyName
a
  Type TyName uni () -> Quote (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
    (Type TyName uni () -> Quote (Type TyName uni ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (Type TyName uni ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () Type TyName uni ()
shadF
    (Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a

{-| Test that shadowing does not result in variable capture. The definition is as follows:

> /\(a :: *) -> wrap (getShadF a) a (\(x : a) -> /\(f :: * -> *) -> \(y : f i) -> 0)

Type checking this term we eventually reach

> NORM (vPat (\(a :: k) -> ifix vPat a) arg)

(where in our case @vPat@ is @shadF@ and @arg@ is @a@), which, if we were naive,
would unfold into

> a -> all (a :: * -> *). a a -> integer

i.e. we substituted the outer @a@ for @i@, but due to variable capture via @all@ that outer @a@
now became an inner one, which would be a bug.

But that problem is already solved before type checking starts as we rename the program and that
makes all binders uniques, so no variable capture is possible due to the outer and inner bindings
being distinct. -}
mkShad :: uni `HasTypeAndTermLevel` Integer => Term TyName Name uni fun ()
mkShad :: forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni Integer =>
Term TyName Name uni fun ()
mkShad = Quote (Term TyName Name uni fun ()) -> Term TyName Name uni fun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name uni fun ())
 -> Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ do
  TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
  TyName
f <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"f"
  Type TyName uni ()
shadF <- TyName -> Quote (Type TyName uni ())
forall (uni :: * -> *).
HasTypeLevel uni Integer =>
TyName -> Quote (Type TyName uni ())
getShadF TyName
a
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
  Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
    (Term TyName Name uni fun ()
 -> Quote (Term TyName Name uni fun ()))
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap () Type TyName uni ()
shadF (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
f (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Kind () -> Kind ()) -> Kind () -> Kind ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
y (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    (Term TyName Name uni fun ()
 -> Quote (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0

{-|

> recUnitF = \(rec :: * -> *) (i :: *) -> all (r :: *). rec i -> r -> r -}
recUnitF :: Type TyName uni ()
recUnitF :: forall (uni :: * -> *). Type TyName uni ()
recUnitF = Quote (Type TyName uni ()) -> Type TyName uni ()
forall a. Quote a -> a
runQuote (Quote (Type TyName uni ()) -> Type TyName uni ())
-> Quote (Type TyName uni ()) -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ do
  TyName
rec <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"rec"
  TyName
i <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"i"
  TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
  Type TyName uni () -> Quote (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
    (Type TyName uni () -> Quote (Type TyName uni ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (Type TyName uni ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
rec (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Kind () -> Kind ()) -> Kind () -> Kind ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
i (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
rec) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
i)
    (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
    (Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r

{-|

> ifix recUnitF () -}
recUnit :: uni `HasTypeLevel` () => Type TyName uni ()
recUnit :: forall (uni :: * -> *). HasTypeLevel uni () => Type TyName uni ()
recUnit = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
recUnitF (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @() ()

{-|  Test that a binder in a pattern functor does not get duplicated. The definition is as follows:

> /\(a :: *) -> \(ru : recUnit) -> unwrap ru {a} ru

Type checking this term we eventually reach

> NORM (vPat (\(a :: k) -> ifix vPat a) arg)

(where in our case @vPat@ is @recUnitF@ and @arg@ is @()@), which, if we were naive,
would unfold into

> all (r :: *). ifix (\(rec :: * -> *) (i :: *) -> all (r :: *). rec i -> r -> r) () -> r -> r

and break global uniqueness as the @all (r :: *)@ binder appears twice.

But this doesn't happen in the actual code, since when a variable gets looked up during type
normalization, its value gets renamed, which means that a fresh variable will be generated for
the inner binder and there will be no shadowing. -}
runRecUnit :: uni `HasTypeAndTermLevel` () => Term TyName Name uni fun ()
runRecUnit :: forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni () =>
Term TyName Name uni fun ()
runRecUnit = Quote (Term TyName Name uni fun ()) -> Term TyName Name uni fun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name uni fun ())
 -> Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ do
  TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
  Name
ru <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"ru"
  Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
    (Term TyName Name uni fun ()
 -> Quote (Term TyName Name uni fun ()))
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
    (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
ru Type TyName uni ()
forall (uni :: * -> *). HasTypeLevel uni () => Type TyName uni ()
recUnit
    (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (() -> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap () (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
ru) (Type TyName uni () -> Term TyName Name uni fun ())
-> Type TyName uni () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    (Term TyName Name uni fun ()
 -> Quote (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
ru