All kinds of tweaks

plutus-conformance/uplc/evaluation/builtin/mkNilData/mkNilData.uplc.expected

@@ -1 +1 @@
-(program 0.0.0 (con list data []))
+(program 0.0.0 (con (list data) []))

plutus-conformance/uplc/evaluation/builtin/mkNilPairData/mkNilPairData.uplc.expected

@@ -1 +1 @@
-(program 0.0.0 (con list (pair data data) []))
+(program 0.0.0 (con (list (pair data data)) []))

plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs

@@ -141,8 +141,14 @@ instance HasRenderContext config => PrettyBy config (DefaultUni a) where
         DefaultUniProtoPair       -> "pair"
         DefaultUniApply uniF uniA -> uniF `juxtPrettyM` uniA
         DefaultUniData            -> "data"
+
+-- | This always pretty-prints parens around type applications (e.g. @(list bool)@) and
+-- doesn't pretty-print them otherwise (e.g. @integer@).
+-- This is so we can have a single instance that is safe to use with both the classic and the
+-- readable pretty-printers, even though for the latter it may result in redundant parens being
+-- shown. We are planning to change the classic syntax to remove this silliness.
 instance Pretty (DefaultUni a) where
-    pretty = prettyBy botRenderContext
+    pretty = prettyBy $ RenderContext ToTheRight juxtFixity
 instance Pretty (SomeTypeIn DefaultUni) where
     pretty (SomeTypeIn uni) = pretty uni
 

plutus-core/plutus-core/src/PlutusCore/Parser/Builtin.hs

@@ -8,15 +8,15 @@ import PlutusPrelude (Word8, reoption)
 import PlutusCore.Default
 import PlutusCore.Error (ParserError (UnknownBuiltinFunction))
 import PlutusCore.Parser.ParserCommon
-import PlutusCore.Parser.Type (defaultUniType)
+import PlutusCore.Parser.Type (defaultUni)
 import PlutusCore.Pretty (display)
 
-import Control.Applicative
+import Control.Monad.Combinators
 import Data.ByteString (ByteString, pack)
 import Data.Map.Strict qualified as Map
 import Data.Text qualified as T
 import Data.Text.Internal.Read (hexDigitToInt)
-import Text.Megaparsec (MonadParsec (takeWhileP), choice, customFailure, getSourcePos, manyTill)
+import Text.Megaparsec (customFailure, getSourcePos, takeWhileP)
 import Text.Megaparsec.Char (char, hexDigitChar)
 import Text.Megaparsec.Char.Lexer qualified as Lex
 
@@ -64,22 +64,19 @@ conBool = choice
     , False <$ symbol "False"
     ]
 
--- Taken verbatim from https://hackage.haskell.org/package/parsec-3.1.15.1/docs/Text-Parsec-Combinator.html#v:sepBy
-sepBy :: Alternative m => m a -> m sep -> m [a]
-sepBy p sep = sepBy1 p sep <|> pure []
-sepBy1 :: Alternative m => m a -> m sep -> m [a]
-sepBy1 p sep = (:) <$> p <*> many (sep *> p)
-
+-- | Parser for lists.
 conList :: DefaultUni (Esc a) -> Parser [a]
 conList uniA = inBrackets $ constantOf uniA `sepBy` symbol ","
 
+-- | Parser for pairs.
 conPair :: DefaultUni (Esc a) -> DefaultUni (Esc b) -> Parser (a, b)
 conPair uniA uniB = inParens $ do
     a <- constantOf uniA
     _ <- symbol ","
     b <- constantOf uniB
     pure (a, b)
 
+-- | Parser for constants of the given type.
 constantOf :: DefaultUni (Esc a) -> Parser a
 constantOf uni = case uni of
     DefaultUniInteger                                                 -> conInteger
@@ -91,10 +88,14 @@ constantOf uni = case uni of
     DefaultUniProtoPair `DefaultUniApply` uniA `DefaultUniApply` uniB -> conPair uniA uniB
     f `DefaultUniApply` _ `DefaultUniApply` _ `DefaultUniApply` _     -> noMoreTypeFunctions f
     DefaultUniData                                                    ->
-        error "Data not supported"
+        fail "Data not supported"
 
+-- | Parser of constants whose type is in 'DefaultUni'.
 constant :: Parser (Some (ValueOf DefaultUni))
 constant = do
-    SomeTypeIn (Kinded uni) <- defaultUniType
+    -- Parse the type tag.
+    SomeTypeIn (Kinded uni) <- defaultUni
+    -- Check it's of kind @*@.
     Refl <- reoption $ checkStar uni
+    -- Parse the constant of the type represented by the type tag.
     someValueOf uni <$> constantOf uni

plutus-core/plutus-core/src/PlutusCore/Parser/ParserCommon.hs

@@ -21,9 +21,16 @@ import PlutusCore.Error
 import PlutusCore.Name
 import PlutusCore.Quote
 
+{- Note [Whitespace invariant]
+Every top-level 'Parser' must consume all whitespace after the thing that it parses, hence make
+sure to enclose every 'Parser' that doesn't consume trailing whitespce (e.g. 'takeWhileP',
+'manyTill', 'Lex.decimal' etc) in a call to 'lexeme'.
+-}
+
 topSourcePos :: SourcePos
 topSourcePos = initialPos "top"
 
+-- | The opposite of @optional :: Alternative f => f a -> f (Maybe a)@.
 required :: MonadPlus m => m (Maybe a) -> m a
 required a = a >>= maybe mzero pure
 
@@ -110,4 +117,3 @@ name = lexeme $ try $ do
     void $ lookAhead letterChar
     str <- takeWhileP (Just "identifier") isIdentifierChar
     Name str <$> intern str
-

plutus-core/plutus-core/src/PlutusCore/Parser/Type.hs

@@ -2,18 +2,22 @@
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PolyKinds         #-}
+{-# LANGUAGE TypeApplications  #-}
 
 module PlutusCore.Parser.Type where
 
 import PlutusPrelude
 
 import PlutusCore.Core.Type
+import PlutusCore.Data
 import PlutusCore.Default
 import PlutusCore.MkPlc (mkIterTyApp)
 import PlutusCore.Name
 import PlutusCore.Parser.ParserCommon
 
 import Control.Monad
+import Data.ByteString (ByteString)
+import Data.Text (Text)
 import Text.Megaparsec hiding (ParseError, State, many, parse, some)
 
 -- | A PLC @Type@ to be parsed. ATM the parser only works
@@ -36,7 +40,10 @@ ifixType :: Parser PType
 ifixType = inParens $ TyIFix <$> wordPos "ifix" <*> pType <*> pType
 
 builtinType :: Parser PType
-builtinType = inParens $ TyBuiltin <$> wordPos "con" <*> ((\(SomeTypeIn (Kinded uni)) -> SomeTypeIn uni) <$> defaultUniType)
+builtinType = inParens $ do
+    ann <- wordPos "con"
+    SomeTypeIn (Kinded uni) <- defaultUni
+    pure . TyBuiltin ann $ SomeTypeIn uni
 
 appType :: Parser PType
 appType = inBrackets $ do
@@ -63,23 +70,57 @@ pType = choice $ map try
     , varType
     ]
 
-defaultUniPart :: Parser (SomeTypeIn (Kinded DefaultUni))
-defaultUniPart = choice $ map try
-    [ inParens defaultUniType
-    , SomeTypeIn (Kinded DefaultUniInteger) <$ symbol "integer"
-    , SomeTypeIn (Kinded DefaultUniByteString) <$ symbol "bytestring"
-    , SomeTypeIn (Kinded DefaultUniString) <$ symbol "string"
-    , SomeTypeIn (Kinded DefaultUniUnit) <$ symbol "unit"
-    , SomeTypeIn (Kinded DefaultUniBool) <$ symbol "bool"
-    , SomeTypeIn (Kinded DefaultUniProtoList) <$ symbol "list"
-    , SomeTypeIn (Kinded DefaultUniProtoPair) <$ symbol "pair"
-    , SomeTypeIn (Kinded DefaultUniData) <$ symbol "data"
+-- | Parser for built-in type applications.
+defaultUniApplication :: Parser (SomeTypeIn (Kinded DefaultUni))
+defaultUniApplication = do
+    -- Parse the head of the application.
+    f <- defaultUni
+    -- Parse the arguments.
+    as <- many defaultUni
+    -- Iteratively apply the head to the arguments checking that the kinds match and
+    -- failing otherwise.
+    foldM tryUniApply f as
+
+-- | Parser for built-in types (the ones from 'DefaultUni' specifically).
+--
+-- 'Kinded' is needed for checking that a type function can be applied to its argument.
+-- I.e. we do Plutus kind checking of builtin type applications during parsing, which is
+-- unfortunate, but there's no way we could construct a 'DefaultUni' otherwise.
+--
+-- In case of kind error no sensible message is shown, only an overly general one:
+--
+-- >>> :set -XTypeApplications
+-- >>> :set -XOverloadedStrings
+-- >>> import PlutusCore.Error
+-- >>> import PlutusCore.Quote
+-- >>> let runP = either show display . runQuoteT . parseGen @ParserErrorBundle defaultUni
+-- >>> runP "(list integer)"
+-- "(list integer)"
+-- >>> runP "(bool integer)"
+-- "ParseErrorB (ParseErrorBundle {bundleErrors = TrivialError 13 Nothing (fromList [Tokens ('(' :| \"\"),Tokens ('b' :| \"ool\"),Tokens ('b' :| \"ytestring\"),Tokens ('d' :| \"ata\"),Tokens ('i' :| \"nteger\"),Tokens ('l' :| \"ist\"),Tokens ('p' :| \"air\"),Tokens ('s' :| \"tring\"),Tokens ('u' :| \"nit\")]) :| [], bundlePosState = PosState {pstateInput = \"(bool integer)\", pstateOffset = 0, pstateSourcePos = SourcePos {sourceName = \"test\", sourceLine = Pos 1, sourceColumn = Pos 1}, pstateTabWidth = Pos 8, pstateLinePrefix = \"\"}})"
+--
+-- This is to be fixed.
+--
+-- One thing we could do to avoid doing kind checking during parsing is to parse into
+--
+--     data TextualUni a where
+--         TextualUni :: TextualUni (Esc (Tree Text))
+--
+-- i.e. parse into @Tree Text@ and do the kind checking afterwards, but given that we'll still need
+-- to do the kind checking of builtins regardless (even for UPLC), we don't win much by deferring
+-- doing it.
+defaultUni :: Parser (SomeTypeIn (Kinded DefaultUni))
+defaultUni = choice $ map try
+    [ inParens defaultUniApplication
+    , someType @_ @Integer <$ symbol "integer"
+    , someType @_ @ByteString <$ symbol "bytestring"
+    , someType @_ @Text <$ symbol "string"
+    , someType @_ @() <$ symbol "unit"
+    , someType @_ @Bool <$ symbol "bool"
+    , someType @_ @[] <$ symbol "list"
+    , someType @_ @(,) <$ symbol "pair"
+    , someType @_ @Data <$ symbol "data"
     ]
-defaultUniType :: Parser (SomeTypeIn (Kinded DefaultUni))
-defaultUniType = do
-    f <- defaultUniPart
-    as <- many defaultUniPart
-    foldM uniApplyM f as
 
 tyName :: Parser TyName
 tyName = TyName <$> name

plutus-core/plutus-core/src/PlutusCore/Pretty/PrettyConst.hs

@@ -118,6 +118,9 @@ asBytes x = Text 2 $ T.pack $ addLeadingZero $ showHex x mempty
 instance PrettyBy ConstConfig Data where
     prettyBy c d = prettyBy c $ BSL.toStrict $ serialise d
 
+instance Pretty (SomeTypeIn uni) => Pretty (SomeTypeIn (Kinded uni)) where
+    pretty (SomeTypeIn (Kinded uni)) = pretty (SomeTypeIn uni)
+
 -- | Special treatment for built-in constants: see the Note in PlutusCore.Pretty.PrettyConst.
 instance (Closed uni, uni `Everywhere` PrettyConst) => Pretty (ValueOf uni a) where
     pretty (ValueOf uni x) = bring (Proxy @PrettyConst) uni $ prettyConst x

plutus-core/plutus-core/src/Universe/Core.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes      #-}
 {-# LANGUAGE ConstraintKinds          #-}
 {-# LANGUAGE DataKinds                #-}
 {-# LANGUAGE FlexibleInstances        #-}
@@ -21,11 +22,13 @@ module Universe.Core
     , SomeTypeIn (..)
     , Kinded (..)
     , ValueOf (..)
+    , Contains (..)
+    , Includes
+    , knownUniOf
+    , someType
     , someValueOf
     , someValue
     , someValueType
-    , Contains (..)
-    , Includes
     , DecodeUniM (..)
     , Closed (..)
     , decodeKindedUni
@@ -36,8 +39,7 @@ module Universe.Core
     , HasUniApply (..)
     , checkStar
     , withApplicable
-    , uniApplyM
-    , knownUniOf
+    , tryUniApply
     , GShow (..)
     , gshow
     , GEq (..)
@@ -400,6 +402,10 @@ at the use site, so instead we define 'Includes' as a type alias of one argument
 has to be immediately applied only to a @uni@ at the use site).
 -}
 
+-- | A @Kinded uni@ contains an @a :: k@ whenever @uni@ contains it and @k@ is 'Typeable'.
+instance (Typeable k, uni `Contains` a) => Kinded uni `Contains` (a :: k) where
+    knownUni = Kinded knownUni
+
 -- See Note [The definition of Includes].
 -- | @uni `Includes` a@ reads as \"@a@ is in the @uni@\". @a@ can be of a higher-kind,
 -- see the docs of 'Contains' on why you might want that.
@@ -410,6 +416,10 @@ type Includes uni = Permits (Contains uni)
 knownUniOf :: uni `Contains` a => proxy a -> uni (Esc a)
 knownUniOf _ = knownUni
 
+-- | Wrap a type into @SomeTypeIn@, provided it's in the universe.
+someType :: forall k (a :: k) uni. uni `Contains` a => SomeTypeIn uni
+someType = SomeTypeIn $ knownUni @k @uni @a
+
 -- | Wrap a value into @Some (ValueOf uni)@, given its explicit type tag.
 someValueOf :: forall a uni. uni (Esc a) -> a -> Some (ValueOf uni)
 someValueOf uni = Some . ValueOf uni
@@ -552,6 +562,7 @@ type uni1 <: uni2 = uni1 `Everywhere` Includes uni2
 
 -- | A class for \"@uni@ has general type application\".
 class HasUniApply (uni :: Type -> Type) where
+    -- | Apply a type constructor to an argument.
     uniApply :: forall k l (f :: k -> l) a. uni (Esc f) -> uni (Esc a) -> uni (Esc (f a))
 
     -- | Deconstruct a type application into the function and the argument and feed them to the
@@ -598,10 +609,11 @@ withApplicable _ _ k =
             withTypeable repB k
         _ -> mzero
 
-uniApplyM
+-- | Apply a type constructor to an argument, provided kinds match.
+tryUniApply
     :: (MonadPlus m, HasUniApply uni)
     => SomeTypeIn (Kinded uni) -> SomeTypeIn (Kinded uni) -> m (SomeTypeIn (Kinded uni))
-uniApplyM (SomeTypeIn (Kinded uniF)) (SomeTypeIn (Kinded uniA)) =
+tryUniApply (SomeTypeIn (Kinded uniF)) (SomeTypeIn (Kinded uniA)) =
     withApplicable uniF uniA $
         pure . SomeTypeIn . Kinded $ uniF `uniApply` uniA
 

plutus-core/plutus-core/test/Pretty/Golden/Readable/Examples/Data/ofoldrData.plc.golden

@@ -1 +1 @@
-\(fConstr : integer -> list data -> data) -> \(fMap : list (pair data data) -> data) -> \(fList : list data -> data) -> \(fI : integer -> data) -> \(fB : bytestring -> data) -> (/\a -> /\b -> \(f : (a -> b) -> a -> b) -> (/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \a -> self a -> a) (a -> b) (\(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {data} {data} (\(rec : data -> data) -> \(d : data) -> (\(d : data) -> /\r -> \(fConstr : integer -> list data -> r) -> \(fMap : list (pair data data) -> r) -> \(fList : list data -> r) -> \(fI : integer -> r) -> \(fB : bytestring -> r) -> (Left chooseData) {unit -> r} d (\(u : unit) -> (/\a -> /\b -> /\c -> \(f : a -> b -> c) -> \(p : pair a b) -> f ((Left fstPair) {a} {b} p) ((Left sndPair) {a} {b} p)) {integer} {list data} {r} fConstr ((Left unConstrData) d)) (\(u : unit) -> fMap ((Left unMapData) d)) (\(u : unit) -> fList ((Left unListData) d)) (\(u : unit) -> fI ((Left unIData) d)) (\(u : unit) -> fB ((Left unBData) d)) ()) d {data} (\(i : integer) -> \(ds : list data) -> fConstr i ((/\a -> \(f : a -> a) -> (/\a -> /\b -> \(f : (a -> b) -> a -> b) -> (/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \a -> self a -> a) (a -> b) (\(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\a -> \(x : list a) -> /\r -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Left mkCons) {a} (f x) (rec xs')))) {data} rec ds)) (\(es : list (pair data data)) -> fMap ((/\a -> \(f : a -> a) -> (/\a -> /\b -> \(f : (a -> b) -> a -> b) -> (/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \a -> self a -> a) (a -> b) (\(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\a -> \(x : list a) -> /\r -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Left mkCons) {a} (f x) (rec xs')))) {pair data data} ((/\a -> \(f : a -> a) -> \(p : pair a a) -> (Right Comma) {a} {a} (f ((Left fstPair) {a} {a} p)) (f ((Left sndPair) {a} {a} p))) {data} rec) es)) (\(ds : list data) -> fList ((/\a -> \(f : a -> a) -> (/\a -> /\b -> \(f : (a -> b) -> a -> b) -> (/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \a -> self a -> a) (a -> b) (\(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\a -> \(x : list a) -> /\r -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Left mkCons) {a} (f x) (rec xs')))) {data} rec ds)) fI fB)
+\(fConstr : integer -> list data -> data) -> \(fMap : list (pair data data) -> data) -> \(fList : list data -> data) -> \(fI : integer -> data) -> \(fB : bytestring -> data) -> (/\a -> /\b -> \(f : (a -> b) -> a -> b) -> (/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \a -> self a -> a) (a -> b) (\(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {data} {data} (\(rec : data -> data) -> \(d : data) -> (\(d : data) -> /\r -> \(fConstr : integer -> (list data) -> r) -> \(fMap : (list (pair data data)) -> r) -> \(fList : (list data) -> r) -> \(fI : integer -> r) -> \(fB : bytestring -> r) -> (Left chooseData) {unit -> r} d (\(u : unit) -> (/\a -> /\b -> /\c -> \(f : a -> b -> c) -> \(p : pair a b) -> f ((Left fstPair) {a} {b} p) ((Left sndPair) {a} {b} p)) {integer} {(list data)} {r} fConstr ((Left unConstrData) d)) (\(u : unit) -> fMap ((Left unMapData) d)) (\(u : unit) -> fList ((Left unListData) d)) (\(u : unit) -> fI ((Left unIData) d)) (\(u : unit) -> fB ((Left unBData) d)) ()) d {data} (\(i : integer) -> \(ds : (list data)) -> fConstr i ((/\a -> \(f : a -> a) -> (/\a -> /\b -> \(f : (a -> b) -> a -> b) -> (/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \a -> self a -> a) (a -> b) (\(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\a -> \(x : list a) -> /\r -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Left mkCons) {a} (f x) (rec xs')))) {data} rec ds)) (\(es : list (pair data data)) -> fMap ((/\a -> \(f : a -> a) -> (/\a -> /\b -> \(f : (a -> b) -> a -> b) -> (/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \a -> self a -> a) (a -> b) (\(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\a -> \(x : list a) -> /\r -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Left mkCons) {a} (f x) (rec xs')))) {pair data data} ((/\a -> \(f : a -> a) -> \(p : pair a a) -> (Right Comma) {a} {a} (f ((Left fstPair) {a} {a} p)) (f ((Left sndPair) {a} {a} p))) {data} rec) es)) (\(ds : (list data)) -> fList ((/\a -> \(f : a -> a) -> (/\a -> /\b -> \(f : (a -> b) -> a -> b) -> (/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} (iwrap (\(self :: * -> *) -> \a -> self a -> a) (a -> b) (\(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) (a -> b)) -> \(x : a) -> f ((/\a -> \(s : (\a -> ifix (\(self :: * -> *) -> \a -> self a -> a) a) a) -> unwrap s s) {a -> b} s) x))) {list a} {list a} (\(rec : list a -> list a) -> \(xs : list a) -> (/\a -> \(x : list a) -> /\r -> \(z : r) -> \(f : a -> list a -> r) -> (Left chooseList) {a} {unit -> r} x (\(u : unit) -> z) (\(u : unit) -> f ((Left headList) {a} x) ((Left tailList) {a} x)) ()) {a} xs {list a} xs (\(x : a) -> \(xs' : list a) -> (Left mkCons) {a} (f x) (rec xs')))) {data} rec ds)) fI fB)