-- editorconfig-checker-disable-file
-- | Combinators.

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections     #-}

module PlutusCore.StdLib.Data.Function
    ( const
    , idFun
    , applyFun
    , selfData
    , unroll
    , fix
    , fixAndType
    , fixBy
    , fixByAndType
    , fixN
    , fixNAndType
    , FunctionDef (..)
    , getMutualFixOf
    , getSingleFixOf
    ) where

import PlutusPrelude
import Prelude hiding (const)

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

import PlutusCore.StdLib.Meta.Data.Tuple
import PlutusCore.StdLib.Type

import Control.Lens.Indexed (ifor)
import Control.Monad

-- | 'id' as a PLC term.
--
-- > /\(A :: *) -> \(x : A) -> x
idFun :: TermLike term TyName Name uni fun => term ()
idFun :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
idFun = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
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
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x

-- | 'const' as a PLC term.
--
-- > /\(A B :: *) -> \(x : A) (y : B) -> x
const :: TermLike term TyName Name uni fun => term ()
const :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
const = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
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
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
    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 () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
y (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x

-- | '($)' as a PLC term.
--
-- > /\(A B :: *) -> \(f : A -> B) (x : A) -> f x
applyFun :: TermLike term TyName Name uni fun => term ()
applyFun :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
applyFun = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
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
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
    Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
f (()
-> 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 ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f) (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x)

{- Note [Recursion combinators]
We create singly recursive and mutually recursive functions using different combinators.

For singly recursive functions we use the Z combinator (a strict cousin of the Y combinator) that in
UPLC looks like this:

    \f -> (\s -> s s) (\s -> f (\x -> s s x))

We have benchmarked its Haskell version at
  https://github.com/IntersectMBO/plutus/tree/9538fc9829426b2ecb0628d352e2d7af96ec8204/doc/notes/fomega/z-combinator-benchmarks
and observed that in Haskell there's no detectable difference in performance of functions defined
using explicit recursion versus the Z combinator. However Haskell is a compiled language and Plutus
is interpreted, so it's very likely that natively supporting recursion in Plutus instead of
compiling recursive functions to combinators would significantly boost performance.

We've tried using

   \f -> (\s -> s s) (\s x -> f (s s) x)

instead of

   \f -> (\s -> s s) (\s -> f (\x -> s s x))

and while it worked OK at the PLC level, it wasn't a suitable primitive for compilation of recursive
functions, because it would add laziness in unexpected places, see
  https://github.com/IntersectMBO/plutus/issues/5961
so we had to change it.

We use

   \f -> (\s -> s s) (\s x -> f (s s) x)

instead of the more standard

   \f -> (\s x -> f (s s) x) (\s x -> f (s s) x)

because in practice @f@ gets inlined and we wouldn't be able to do so if it occurred twice in the
term. Plus the former also allows us to save on the size of the term.

For mutually recursive functions we use the 'fixBy' combinator, which is, to the best of our
knowledge, our own invention. It was first described at
  https://github.com/IntersectMBO/plutus/blob/067e74f0606fddc5e183dd45209b461e293a6224/doc/notes/fomega/mutual-term-level-recursion/FixN.agda
and fully specified in our "Unraveling recursion: compiling an IR with recursion to System F" paper.
-}

-- | @Self@ as a PLC type.
--
-- > fix \(self :: * -> *) (a :: *) -> self a -> a
selfData :: RecursiveType uni fun ()
selfData :: forall (uni :: * -> *) fun. RecursiveType uni fun ()
selfData = Quote (RecursiveType uni fun ()) -> RecursiveType uni fun ()
forall a. Quote a -> a
runQuote (Quote (RecursiveType uni fun ()) -> RecursiveType uni fun ())
-> Quote (RecursiveType uni fun ()) -> RecursiveType uni fun ()
forall a b. (a -> b) -> a -> b
$ do
    TyName
self <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"self"
    TyName
a    <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    FromDataPieces uni () (RecursiveType uni fun ())
forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (RecursiveType uni fun ann)
makeRecursiveType () TyName
self [() -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a (Kind () -> TyVarDecl TyName ()) -> Kind () -> TyVarDecl TyName ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()]
        (Type TyName uni () -> Quote (RecursiveType uni fun ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (RecursiveType uni fun ())
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
self) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a))
        (Type TyName uni () -> Quote (RecursiveType uni fun ()))
-> Type TyName uni () -> Quote (RecursiveType 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

-- | @unroll@ as a PLC term.
--
-- > /\(a :: *) -> \(s : self a) -> unwrap s s
unroll :: TermLike term TyName Name uni fun => term ()
unroll :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
unroll = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    let self :: Type TyName uni ()
self = RecursiveType uni Any () -> Type TyName uni ()
forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann -> Type TyName uni ann
_recursiveType RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
selfData
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    Name
s <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"s"
    term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
s (()
-> 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 () Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
self (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 () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> term ()
forall ann. ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann
unwrap () (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
s)
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
s

-- | 'fix' as a PLC term.
--
-- > /\(a b :: *) -> \(f : (a -> b) -> a -> b) ->
-- >     unroll {a -> b} (iwrap selfF (a -> b) \(s : self (a -> b)) ->
-- >         f (\(x : a) -> unroll {a -> b} s x))
--
-- See @plutus/runQuote $ docs/fomega/z-combinator-benchmarks@ for details.
fix :: TermLike term TyName Name uni fun => term ()
fix :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix = (term (), Type TyName uni ()) -> term ()
forall a b. (a, b) -> a
fst (term (), Type TyName uni ())
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(term (), Type TyName uni ())
fixAndType

fixAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ())
fixAndType :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(term (), Type TyName uni ())
fixAndType = Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a. Quote a -> a
runQuote (Quote (term (), Type TyName uni ())
 -> (term (), Type TyName uni ()))
-> Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ do
    let RecursiveType Type TyName uni ()
self forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapSelf = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
selfData
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    TyName
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
    Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Name
s <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"s"
    Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    let funAB :: Type TyName uni ()
funAB = ()
-> 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 ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b
        unrollFunAB :: term ()
unrollFunAB = () -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
unroll Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
funAB
    let selfFunAB :: Type TyName uni ()
selfFunAB = ()
-> 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 () Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
self Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
funAB
    let fixTerm :: term ()
fixTerm =
            () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
f (()
-> 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 ()
forall {uni :: * -> *}. Type TyName uni ()
funAB Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
funAB)
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () term ()
unrollFunAB
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type TyName uni ()] -> term () -> term ()
forall {uni :: * -> *} {fun} (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapSelf [Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
funAB]
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
s Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
selfFunAB
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f)
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
            (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn term ()
unrollFunAB
                [ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
s
                , () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x
                ]
    let fixType :: Type TyName uni ()
fixType =
            () -> 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 ()
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
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
            (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ ()
-> 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
TyFun () Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
funAB Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
funAB) Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
funAB
    (term (), Type TyName uni ())
-> Quote (term (), Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ()
fixTerm, Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
fixType)

-- | A type that looks like a transformation.
--
-- > trans F G Q : F Q -> G Q
trans :: Type tyname uni () -> Type tyname uni () -> Type tyname uni () -> Quote (Type tyname uni ())
trans :: forall tyname (uni :: * -> *).
Type tyname uni ()
-> Type tyname uni ()
-> Type tyname uni ()
-> Quote (Type tyname uni ())
trans Type tyname uni ()
f Type tyname uni ()
g Type tyname uni ()
q = Type tyname uni () -> QuoteT Identity (Type tyname uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type tyname uni () -> QuoteT Identity (Type tyname uni ()))
-> Type tyname uni () -> QuoteT Identity (Type tyname uni ())
forall a b. (a -> b) -> a -> b
$ ()
-> 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 () Type tyname uni ()
f Type tyname uni ()
q) (()
-> 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 () Type tyname uni ()
g Type tyname uni ()
q)

-- | A type that looks like a natural transformation, sometimes written 'F ~> G'.
--
-- > natTrans F G : forall Q :: * . F Q -> G Q
natTrans :: Type TyName uni () -> Type TyName uni () -> Quote (Type TyName uni ())
natTrans :: forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans Type TyName uni ()
f Type TyName uni ()
g = Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q" QuoteT Identity TyName
-> (TyName -> QuoteT Identity (Type TyName uni ()))
-> QuoteT Identity (Type TyName uni ())
forall a b.
QuoteT Identity a -> (a -> QuoteT Identity b) -> QuoteT Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TyName
q -> () -> 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
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type TyName uni () -> Type TyName uni ())
-> QuoteT Identity (Type TyName uni ())
-> QuoteT Identity (Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ()
-> Type TyName uni ()
-> Type TyName uni ()
-> QuoteT Identity (Type TyName uni ())
forall tyname (uni :: * -> *).
Type tyname uni ()
-> Type tyname uni ()
-> Type tyname uni ()
-> Quote (Type tyname uni ())
trans Type TyName uni ()
f Type TyName uni ()
g (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)

-- | A type that looks like a natural transformation to Id.
--
-- > natTransId F : forall Q :: * . F Q -> Q
natTransId :: Type TyName uni () -> Quote (Type TyName uni ())
natTransId :: forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId Type TyName uni ()
f = do
    TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
    Type TyName uni () -> Quote (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ () -> 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
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (()
-> 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 () Type TyName uni ()
f (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q))

-- | The 'fixBy' combinator.
--
-- > fixBy :
-- >     forall (F :: * -> *) .
-- >     ((F ~> Id) -> (F ~> Id)) ->
-- >     ((F ~> F) -> (F ~> Id))
fixBy :: TermLike term TyName Name uni fun => term ()
fixBy :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fixBy = (term (), Type TyName uni ()) -> term ()
forall a b. (a, b) -> a
fst (term (), Type TyName uni ())
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(term (), Type TyName uni ())
fixByAndType

fixByAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ())
fixByAndType :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(term (), Type TyName uni ())
fixByAndType = Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a. Quote a -> a
runQuote (Quote (term (), Type TyName uni ())
 -> (term (), Type TyName uni ()))
-> Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ do
    TyName
f <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"F"

    -- by : (F ~> Id) -> (F ~> Id)
    Name
by <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"by"
    Type TyName uni ()
byTy <- do
        Type TyName uni ()
nt1 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni ()
nt2 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
nt1 Type TyName uni ()
nt2

    Type TyName uni ()
resTy <- do
        Type TyName uni ()
nt1 <- Type TyName uni ()
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni ()
nt2 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
nt1 Type TyName uni ()
nt2

    -- instantiatedFix = fix {F ~> F} {F ~> Id}
    term ()
instantiatedFix <- do
        Type TyName uni ()
nt1 <- Type TyName uni ()
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni ()
nt2 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        term () -> QuoteT Identity (term ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> QuoteT Identity (term ()))
-> term () -> QuoteT Identity (term ())
forall a b. (a -> b) -> a -> b
$ () -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix Type TyName uni ()
nt1) Type TyName uni ()
nt2

    -- rec : (F ~> F) -> (F ~> Id)
    Name
recc <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"rec"
    Type TyName uni ()
reccTy <- do
      Type TyName uni ()
nt <- Type TyName uni ()
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
      Type TyName uni ()
nt2 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
      Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
nt Type TyName uni ()
nt2

    -- h : F ~> F
    Name
h <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"h"
    Type TyName uni ()
hty <- Type TyName uni ()
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)

    -- R :: *
    -- fr : F R
    TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"R"
    Name
fr <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fr"
    let frTy :: Type TyName uni ()
frTy = ()
-> 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) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)

    -- Q :: *
    -- fq : F Q
    TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
    Name
fq <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fq"
    let fqTy :: Type TyName uni ()
fqTy = ()
-> 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) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)

    -- inner = (/\ (Q :: *) -> \ q : F Q -> rec h {Q} (h {Q} q))
    let inner :: term ()
inner =
            () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
by) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
fq Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
fqTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
recc) (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
h)) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
h) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fq)
    let fixByTerm :: term ()
fixByTerm =
            () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term 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 ()
forall ann. ann -> Kind ann
Type ())) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
by Type TyName uni ()
byTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () term ()
instantiatedFix (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
recc Type TyName uni ()
reccTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
h Type TyName uni ()
hty (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
fr Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
frTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
inner (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)) (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fr)
    let fixByType :: Type TyName uni ()
fixByType =
            () -> 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
f (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (() -> Kind ()
forall ann. ann -> Kind ann
Type ())) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$
            ()
-> 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 ()
byTy Type TyName uni ()
resTy
    (term (), Type TyName uni ())
-> Quote (term (), Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ()
fixByTerm, Type TyName uni ()
fixByType)


-- | Make a @n@-ary fixpoint combinator.
--
-- > FixN n :
-- >     forall A1 B1 ... An Bn :: * .
-- >     (forall Q :: * .
-- >         ((A1 -> B1) -> ... -> (An -> Bn) -> Q) ->
-- >         (A1 -> B1) ->
-- >         ... ->
-- >         (An -> Bn) ->
-- >         Q) ->
-- >     (forall R :: * . ((A1 -> B1) -> ... (An -> Bn) -> R) -> R)
fixN :: TermLike term TyName Name uni fun => Integer -> term () -> term ()
fixN :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term () -> term ()
fixN Integer
n term ()
fixByTerm = (term (), Type TyName uni ()) -> term ()
forall a b. (a, b) -> a
fst (Integer -> term () -> (term (), Type TyName uni ())
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term () -> (term (), Type TyName uni ())
fixNAndType Integer
n term ()
fixByTerm)

fixNAndType :: TermLike term TyName Name uni fun => Integer -> term () -> (term (), Type TyName uni ())
fixNAndType :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term () -> (term (), Type TyName uni ())
fixNAndType Integer
n term ()
fixByTerm = Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a. Quote a -> a
runQuote (Quote (term (), Type TyName uni ())
 -> (term (), Type TyName uni ()))
-> Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ do
    -- the list of pairs of A and B types
    [(TyName, TyName)]
asbs <- Int
-> QuoteT Identity (TyName, TyName)
-> QuoteT Identity [(TyName, TyName)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n) (QuoteT Identity (TyName, TyName)
 -> QuoteT Identity [(TyName, TyName)])
-> QuoteT Identity (TyName, TyName)
-> QuoteT Identity [(TyName, TyName)]
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
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
        (TyName, TyName) -> QuoteT Identity (TyName, TyName)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyName
a, TyName
b)

    let abFuns :: [Type TyName uni ()]
abFuns = ((TyName, TyName) -> Type TyName uni ())
-> [(TyName, TyName)] -> [Type TyName uni ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TyName
a, TyName
b) -> ()
-> 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) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)) [(TyName, TyName)]
asbs
    let abTyVars :: [TyVarDecl TyName ()]
abTyVars = ((TyName, TyName) -> [TyVarDecl TyName ()])
-> [(TyName, TyName)] -> [TyVarDecl TyName ()]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(TyName
a, TyName
b) -> [ () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ()), () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())]) [(TyName, TyName)]
asbs

    -- funTysTo X = (A1 -> B1) -> ... -> (An -> Bn) -> X
    let funTysTo :: Type TyName uni () -> Type TyName uni ()
funTysTo = ()
-> [Type TyName uni ()] -> Type TyName uni () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () [Type TyName uni ()]
forall {uni :: * -> *}. [Type TyName uni ()]
abFuns

    -- the type of fixN, as in the header comment
    Type TyName uni ()
fixNType <- do
        TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
        let qvar :: Type TyName uni ()
qvar = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q
        let argTy :: Type TyName uni ()
argTy = () -> 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
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (()
-> 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 ()
forall {uni :: * -> *}. Type TyName uni () -> Type TyName uni ()
funTysTo Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
qvar) (Type TyName uni () -> Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni () -> Type TyName uni ()
funTysTo Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
qvar))
        TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"R"
        let rvar :: Type TyName uni ()
rvar = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r
        let resTy :: Type TyName uni ()
resTy = () -> 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 ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Type TyName uni () -> Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni () -> Type TyName uni ()
funTysTo Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
rvar) Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
rvar)
        let fullTy :: Type TyName uni ()
fullTy = [TyVarDecl TyName ()] -> Type TyName uni () -> Type TyName uni ()
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyForall [TyVarDecl TyName ()]
abTyVars (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
forall {uni :: * -> *}. Type TyName uni ()
argTy Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
resTy
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
fullTy

    -- instantiatedFix = fixBy { \X :: * -> (A1 -> B1) -> ... -> (An -> Bn) -> X }
    term ()
instantiatedFix <- do
        TyName
x <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"X"
        term () -> QuoteT Identity (term ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> QuoteT Identity (term ()))
-> term () -> QuoteT Identity (term ())
forall a b. (a -> b) -> a -> b
$ () -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
fixByTerm (() -> 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
x (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type TyName uni () -> Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
x)))

    -- f : forall Q :: * . ((A1 -> B1) -> ... -> (An -> Bn) -> Q) -> (A1 -> B1) -> ... -> (An -> Bn) -> Q)
    Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Type TyName uni ()
fTy <- do
        TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ () -> 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
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
forall {uni :: * -> *}. Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (Type TyName uni () -> Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q))

    -- k : forall Q :: * . ((A1 -> B1) -> ... -> (An -> Bn) -> Q) -> Q)
    Name
k <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"k"
    Type TyName uni ()
kTy <- do
        TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ () -> 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
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
forall {uni :: * -> *}. Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)

    TyName
s <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"S"

    -- h : (A1 -> B1) -> ... -> (An -> Bn) -> S
    Name
h <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"h"
    let hTy :: Type TyName uni ()
hTy = Type TyName uni () -> Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
s)

    -- branch (ai, bi) i = \x : ai -> k { bi } \(f1 : A1 -> B1) ... (fn : An -> Bn) . fi x
    let branch :: (TyName, TyName) -> Int -> m (term ())
branch (TyName
a, TyName
b) Int
i = do
            -- names and types for the f arguments
            [VarDecl TyName Name uni ()]
fs <- [(TyName, TyName)]
-> (Int -> (TyName, TyName) -> m (VarDecl TyName Name uni ()))
-> m [VarDecl TyName Name uni ()]
forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
t a -> (i -> a -> f b) -> f (t b)
ifor [(TyName, TyName)]
asbs ((Int -> (TyName, TyName) -> m (VarDecl TyName Name uni ()))
 -> m [VarDecl TyName Name uni ()])
-> (Int -> (TyName, TyName) -> m (VarDecl TyName Name uni ()))
-> m [VarDecl TyName Name uni ()]
forall a b. (a -> b) -> a -> b
$ \Int
j (TyName
a',TyName
b') -> do
                Name
f_j <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName (Text -> m Name) -> Text -> m Name
forall a b. (a -> b) -> a -> b
$ Text
"f_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
j
                VarDecl TyName Name uni () -> m (VarDecl TyName Name uni ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni () -> m (VarDecl TyName Name uni ()))
-> VarDecl TyName Name uni () -> m (VarDecl TyName Name uni ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> Type TyName uni () -> VarDecl TyName Name uni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () Name
f_j (()
-> 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') (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b'))

            Name
x <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"

            term () -> m (term ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> m (term ())) -> term () -> m (term ())
forall a b. (a -> b) -> a -> b
$
                () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
k) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                [VarDecl TyName Name uni ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs [VarDecl TyName Name uni ()]
fs (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                -- this is an ugly but straightforward way of getting the right fi
                () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> VarDecl TyName Name uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni ann -> term ann
mkVar () ([VarDecl TyName Name uni ()]
fs [VarDecl TyName Name uni ()] -> Int -> VarDecl TyName Name uni ()
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)) (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x)

    -- a list of all the branches
    [term ()]
branches <- [((TyName, TyName), Int)]
-> (((TyName, TyName), Int) -> QuoteT Identity (term ()))
-> QuoteT Identity [term ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([(TyName, TyName)] -> [Int] -> [((TyName, TyName), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(TyName, TyName)]
asbs [Int
0..]) ((((TyName, TyName), Int) -> QuoteT Identity (term ()))
 -> QuoteT Identity [term ()])
-> (((TyName, TyName), Int) -> QuoteT Identity (term ()))
-> QuoteT Identity [term ()]
forall a b. (a -> b) -> a -> b
$ ((TyName, TyName) -> Int -> QuoteT Identity (term ()))
-> ((TyName, TyName), Int) -> QuoteT Identity (term ())
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (TyName, TyName) -> Int -> QuoteT Identity (term ())
forall {m :: * -> *} {term :: * -> *} {uni :: * -> *} {fun}.
(MonadQuote m, TermLike term TyName Name uni fun) =>
(TyName, TyName) -> Int -> m (term ())
branch

    -- [A1, B1, ..., An, Bn]
    let allAsBs :: [TyName]
allAsBs = ((TyName, TyName) -> [TyName]) -> [(TyName, TyName)] -> [TyName]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(TyName
a, TyName
b) -> [TyName
a, TyName
b]) [(TyName, TyName)]
asbs
    let fixNTerm :: term ()
fixNTerm =
          -- abstract out all the As and Bs
          [TyVarDecl TyName ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
mkIterTyAbs ((TyName -> TyVarDecl TyName ())
-> [TyName] -> [TyVarDecl TyName ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\TyName
tn -> () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
tn (() -> Kind ()
forall ann. ann -> Kind ann
Type ())) [TyName]
allAsBs) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
          () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
f Type TyName uni ()
fTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
          term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn term ()
instantiatedFix
              [ () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
k Type TyName uni ()
kTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
s (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
h Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
hTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
h) [term ()]
branches
              , () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f
              ]
    (term (), Type TyName uni ())
-> Quote (term (), Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ()
fixNTerm, Type TyName uni ()
fixNType)

-- See Note [Recursion combinators].
-- | Get the fixed-point of a single recursive function.
getSingleFixOf
    :: (TermLike term TyName Name uni fun)
    => ann -> term ann -> FunctionDef term TyName Name uni fun ann -> term ann
getSingleFixOf :: forall (term :: * -> *) (uni :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
ann
-> term ann -> FunctionDef term TyName Name uni fun ann -> term ann
getSingleFixOf ann
ann term ann
fix1 fun :: FunctionDef term TyName Name uni fun ann
fun@FunctionDef{_functionDefType :: forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann
-> FunctionType tyname uni ann
_functionDefType=(FunctionType ann
_ Type TyName uni ann
dom Type TyName uni ann
cod)} =
    let instantiatedFix :: term ann
instantiatedFix = term ann -> [(ann, Type TyName uni ann)] -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, Type tyname uni ann)] -> term ann
mkIterInst term ann
fix1 [(ann
ann, Type TyName uni ann
dom), (ann
ann, Type TyName uni ann
cod)]
        abstractedBody :: term ann
abstractedBody = [VarDecl TyName Name uni ann] -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs [FunctionDef term TyName Name uni fun ann
-> VarDecl TyName Name uni ann
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann
-> VarDecl tyname name uni ann
functionDefVarDecl FunctionDef term TyName Name uni fun ann
fun] (term ann -> term ann) -> term ann -> term ann
forall a b. (a -> b) -> a -> b
$ FunctionDef term TyName Name uni fun ann -> term ann
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann -> term ann
_functionDefTerm FunctionDef term TyName Name uni fun ann
fun
    in ann -> term ann -> term ann -> term ann
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ann
ann term ann
instantiatedFix term ann
abstractedBody

-- See Note [Recursion combinators].
-- | Get the fixed-point of a list of mutually recursive functions.
--
-- > MutualFixOf _ fixN [ FunctionDef _ fN1 (FunctionType _ a1 b1) f1
-- >                    , ...
-- >                    , FunctionDef _ fNn (FunctionType _ an bn) fn
-- >                    ] =
-- >     Tuple [(a1 -> b1) ... (an -> bn)] $
-- >         fixN {a1} {b1} ... {an} {bn}
-- >             /\(q :: *) -> \(choose : (a1 -> b1) -> ... -> (an -> bn) -> q) ->
-- >                 \(fN1 : a1 -> b1) ... (fNn : an -> bn) -> choose f1 ... fn
getMutualFixOf
    :: (TermLike term TyName Name uni fun)
    => ann -> term ann -> [FunctionDef term TyName Name uni fun ann] -> Quote (Tuple term uni ann)
getMutualFixOf :: forall (term :: * -> *) (uni :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
ann
-> term ann
-> [FunctionDef term TyName Name uni fun ann]
-> Quote (Tuple term uni ann)
getMutualFixOf ann
ann term ann
fixn [FunctionDef term TyName Name uni fun ann]
funs = do
    let funTys :: [Type TyName uni ann]
funTys = (FunctionDef term TyName Name uni fun ann -> Type TyName uni ann)
-> [FunctionDef term TyName Name uni fun ann]
-> [Type TyName uni ann]
forall a b. (a -> b) -> [a] -> [b]
map FunctionDef term TyName Name uni fun ann -> Type TyName uni ann
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann -> Type tyname uni ann
functionDefToType [FunctionDef term TyName Name uni fun ann]
funs

    TyName
q <- QuoteT Identity TyName -> QuoteT Identity TyName
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity TyName -> QuoteT Identity TyName)
-> QuoteT Identity TyName -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
    -- TODO: It was 'safeFreshName' previously. Should we perhaps have @freshName = safeFreshName@?
    Name
choose <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"choose"
    let chooseTy :: Type TyName uni ann
chooseTy = ann
-> [Type TyName uni ann]
-> Type TyName uni ann
-> Type TyName uni ann
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun ann
ann [Type TyName uni ann]
funTys (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
q)

    -- \v1 ... vn -> choose f1 ... fn
    let rhss :: [term ann]
rhss    = (FunctionDef term TyName Name uni fun ann -> term ann)
-> [FunctionDef term TyName Name uni fun ann] -> [term ann]
forall a b. (a -> b) -> [a] -> [b]
map FunctionDef term TyName Name uni fun ann -> term ann
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann -> term ann
_functionDefTerm [FunctionDef term TyName Name uni fun ann]
funs
        chosen :: term ann
chosen  = term ann -> [(ann, term ann)] -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (ann -> Name -> term ann
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var ann
ann Name
choose) ((ann
ann,) (term ann -> (ann, term ann)) -> [term ann] -> [(ann, term ann)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [term ann]
rhss)
        vsLam :: term ann
vsLam   = [VarDecl TyName Name uni ann] -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs ((FunctionDef term TyName Name uni fun ann
 -> VarDecl TyName Name uni ann)
-> [FunctionDef term TyName Name uni fun ann]
-> [VarDecl TyName Name uni ann]
forall a b. (a -> b) -> [a] -> [b]
map FunctionDef term TyName Name uni fun ann
-> VarDecl TyName Name uni ann
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann
-> VarDecl tyname name uni ann
functionDefVarDecl [FunctionDef term TyName Name uni fun ann]
funs) term ann
chosen

    -- abstract out Q and choose
    let cLam :: term ann
cLam = ann -> TyName -> Kind ann -> term ann -> term ann
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs ann
ann TyName
q (ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann) (term ann -> term ann) -> term ann -> term ann
forall a b. (a -> b) -> a -> b
$ ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs ann
ann Name
choose Type TyName uni ann
chooseTy term ann
vsLam

    -- fixN {A1} {B1} ... {An} {Bn}
    term ann
instantiatedFix <- do
        let domCods :: [Type TyName uni ann]
domCods = (FunctionDef term TyName Name uni fun ann -> [Type TyName uni ann])
-> [FunctionDef term TyName Name uni fun ann]
-> [Type TyName uni ann]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(FunctionDef ann
_ Name
_ (FunctionType ann
_ Type TyName uni ann
dom Type TyName uni ann
cod) term ann
_) -> [Type TyName uni ann
dom, Type TyName uni ann
cod]) [FunctionDef term TyName Name uni fun ann]
funs
        term ann -> QuoteT Identity (term ann)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ann -> QuoteT Identity (term ann))
-> term ann -> QuoteT Identity (term ann)
forall a b. (a -> b) -> a -> b
$ term ann -> [(ann, Type TyName uni ann)] -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, Type tyname uni ann)] -> term ann
mkIterInst term ann
fixn ((ann
ann,) (Type TyName uni ann -> (ann, Type TyName uni ann))
-> [Type TyName uni ann] -> [(ann, Type TyName uni ann)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type TyName uni ann]
domCods)

    let term :: term ann
term = ann -> term ann -> term ann -> term ann
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ann
ann term ann
instantiatedFix term ann
cLam

    Tuple term uni ann -> Quote (Tuple term uni ann)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tuple term uni ann -> Quote (Tuple term uni ann))
-> Tuple term uni ann -> Quote (Tuple term uni ann)
forall a b. (a -> b) -> a -> b
$ [Type TyName uni ann] -> term ann -> Tuple term uni ann
forall (term :: * -> *) (uni :: * -> *) ann.
[Type TyName uni ann] -> term ann -> Tuple term uni ann
Tuple [Type TyName uni ann]
funTys term ann
term