From fc0884a75108380c942f052e814575b58792bc68 Mon Sep 17 00:00:00 2001
From: Las Safin <me@las.rs>
Date: Thu, 27 Jan 2022 10:50:53 +0000
Subject: [PATCH 1/6] phoistAcyclic: move lambda further inside

This should help GHC cache more.
---
 Plutarch/Internal.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Plutarch/Internal.hs b/Plutarch/Internal.hs
index 402329e56..d946e2805 100644
--- a/Plutarch/Internal.hs
+++ b/Plutarch/Internal.hs
@@ -310,13 +310,13 @@ asClosedRawTerm t = asRawTerm t 0
 
 -- FIXME: Give proper error message when mutually recursive.
 phoistAcyclic :: HasCallStack => ClosedTerm a -> Term s a
-phoistAcyclic t = Term $ \_ -> case asRawTerm t 0 of
+phoistAcyclic t = case asRawTerm t 0 of
   -- FIXME: is this worth it?
-  t'@(getTerm -> RBuiltin _) -> t'
+  t'@(getTerm -> RBuiltin _) -> Term $ \_ -> t'
   t' -> case evaluateScript . Script $ UPLC.Program () (PLC.defaultVersion ()) (compile' t') of
     Right _ ->
       let hoisted = HoistedTerm (hashRawTerm . getTerm $ t') (getTerm t')
-       in TermResult (RHoisted hoisted) (hoisted : getDeps t')
+       in Term $ \_ -> TermResult (RHoisted hoisted) (hoisted : getDeps t')
     Left e -> error $ "Hoisted term errs! " <> show e
 
 rawTermToUPLC ::

From 889f8169cbeb668032c0402e47044850a0988997 Mon Sep 17 00:00:00 2001
From: Las Safin <me@las.rs>
Date: Thu, 27 Jan 2022 12:24:27 +0000
Subject: [PATCH 2/6] pconstant: Hoist when constants are big

---
 Plutarch/Internal.hs                         | 14 +++++++++---
 plutarch-benchmark/bench/Main.hs             | 23 ++++++++++++++++----
 plutarch-benchmark/plutarch-benchmark.cabal  |  1 +
 plutarch-benchmark/src/Plutarch/Benchmark.hs |  7 +++++-
 4 files changed, 37 insertions(+), 8 deletions(-)

diff --git a/Plutarch/Internal.hs b/Plutarch/Internal.hs
index d946e2805..659e01d11 100644
--- a/Plutarch/Internal.hs
+++ b/Plutarch/Internal.hs
@@ -43,7 +43,7 @@ import GHC.Stack (HasCallStack)
 import Numeric.Natural (Natural)
 import Plutarch.Evaluate (evaluateScript)
 import Plutus.V1.Ledger.Scripts (Script (Script))
-import PlutusCore (Some, ValueOf)
+import PlutusCore (Some (Some), ValueOf (ValueOf))
 import qualified PlutusCore as PLC
 import PlutusCore.DeBruijn (DeBruijn (DeBruijn), Index (Index))
 import qualified UntypedPlutusCore as UPLC
@@ -303,7 +303,15 @@ punsafeConstant :: Some (ValueOf PLC.DefaultUni) -> Term s a
 punsafeConstant = punsafeConstantInternal
 
 punsafeConstantInternal :: Some (ValueOf PLC.DefaultUni) -> Term s a
-punsafeConstantInternal c = Term $ \_ -> mkTermRes $ RConstant c
+punsafeConstantInternal c = Term $ \_ ->
+  case c of
+    -- These constants are smaller than variable references.
+    Some (ValueOf PLC.DefaultUniBool _) -> mkTermRes $ RConstant c
+    Some (ValueOf PLC.DefaultUniUnit _) -> mkTermRes $ RConstant c
+    Some (ValueOf PLC.DefaultUniInteger n) | n < 256 -> mkTermRes $ RConstant c
+    _ ->
+      let hoisted = HoistedTerm (hashRawTerm $ RConstant c) (RConstant c)
+       in TermResult (RHoisted hoisted) [hoisted]
 
 asClosedRawTerm :: ClosedTerm a -> TermResult
 asClosedRawTerm t = asRawTerm t 0
@@ -311,7 +319,7 @@ asClosedRawTerm t = asRawTerm t 0
 -- FIXME: Give proper error message when mutually recursive.
 phoistAcyclic :: HasCallStack => ClosedTerm a -> Term s a
 phoistAcyclic t = case asRawTerm t 0 of
-  -- FIXME: is this worth it?
+  -- Built-ins are smaller than variable references
   t'@(getTerm -> RBuiltin _) -> Term $ \_ -> t'
   t' -> case evaluateScript . Script $ UPLC.Program () (PLC.defaultVersion ()) (compile' t') of
     Right _ ->
diff --git a/plutarch-benchmark/bench/Main.hs b/plutarch-benchmark/bench/Main.hs
index 3b33ef2fc..faf58bc49 100644
--- a/plutarch-benchmark/bench/Main.hs
+++ b/plutarch-benchmark/bench/Main.hs
@@ -1,12 +1,11 @@
 module Main (main) where
 
-import Plutarch
-import Plutarch.Benchmark (NamedBenchmark, bench, benchGroup, benchMain)
+import Data.ByteString (ByteString)
+import Plutarch.Benchmark (NamedBenchmark, bench, bench', benchGroup, benchMain)
 import Plutarch.Bool
 import Plutarch.Builtin
-import Plutarch.Integer
-import Plutarch.Lift
 import qualified Plutarch.List as List
+import Plutarch.Prelude
 
 main :: IO ()
 main = do
@@ -114,4 +113,20 @@ intListBench =
           , bench "/=(n=4)" $ List.plistEquals @PBuiltinList @PInteger # pconstant [1, 2, 3, 4] # pconstant [1, 2, 3]
           , bench "/=(empty;n=3)" $ List.plistEquals @PBuiltinList @PInteger # pconstant [] # pconstant [1, 2, 3]
           ]
+      , benchGroup
+          "pconstant"
+          [ bench' $ plam $ \_ -> pconstant True
+          , bench' $ plam $ \_ -> (0 :: Term _ PInteger)
+          , bench' $ plam $ \_ -> (1 :: Term _ PInteger)
+          , bench' $ plam $ \_ -> (512 :: Term _ PInteger)
+          , bench' $ plam $ \_ -> (1048576 :: Term _ PInteger)
+          , bench' $ plam $ \_ -> pconstant ("1" :: ByteString)
+          , bench' $ plam $ \_ -> pconstant ("1111111" :: ByteString)
+          , bench' $ plam $ \_ -> pconstant ([()] :: [()])
+          , bench' $ plam $ \_ -> pconstant ()
+          , bench' $ pconstant ()
+          , bench' $ plam $ \x -> x
+          , bench' $ plam $ \_ -> (plam (+) :: Term _ (PInteger :--> PInteger :--> PInteger))
+          , bench' $ (plam (+) :: Term _ (PInteger :--> PInteger :--> PInteger))
+          ]
       ]
diff --git a/plutarch-benchmark/plutarch-benchmark.cabal b/plutarch-benchmark/plutarch-benchmark.cabal
index e9c5eb357..40a230049 100644
--- a/plutarch-benchmark/plutarch-benchmark.cabal
+++ b/plutarch-benchmark/plutarch-benchmark.cabal
@@ -101,6 +101,7 @@ benchmark benchmark
     , base
     , plutarch
     , plutarch-benchmark
+    , bytestring
 
 executable benchmark-diff
   import:         c
diff --git a/plutarch-benchmark/src/Plutarch/Benchmark.hs b/plutarch-benchmark/src/Plutarch/Benchmark.hs
index 863010c55..addc0a31d 100644
--- a/plutarch-benchmark/src/Plutarch/Benchmark.hs
+++ b/plutarch-benchmark/src/Plutarch/Benchmark.hs
@@ -10,6 +10,7 @@ module Plutarch.Benchmark (
   benchmarkScript,
   -- | * Benchmark entrypoints
   bench,
+  bench',
   benchGroup,
   benchMain,
   -- | * Working with benchmark results
@@ -47,7 +48,7 @@ import qualified Data.List as List
 import Data.Maybe (fromJust)
 import GHC.Generics (Generic)
 import GHC.Stack (HasCallStack)
-import Plutarch (ClosedTerm, compile)
+import Plutarch (ClosedTerm, compile, printTerm)
 import Plutus.V1.Ledger.Api (
   ExBudget (ExBudget),
   ExCPU (ExCPU),
@@ -117,6 +118,10 @@ bench :: String -> ClosedTerm a -> [NamedBenchmark]
 bench name prog =
   [coerce . benchmarkScript name $ compile prog]
 
+-- | Create a benchmark with itself as name
+bench' :: ClosedTerm a -> [NamedBenchmark]
+bench' prog = bench (init . drop (length ("(program 1.0.0 " :: String)) $ printTerm prog) prog
+
 -- | Decode benchmark results from a CSV file
 decodeBenchmarks :: LB.ByteString -> Either String [NamedBenchmark]
 decodeBenchmarks =

From 40122663ce98fcb1dbbe7d7d9838fff3333ec7e9 Mon Sep 17 00:00:00 2001
From: Las Safin <me@las.rs>
Date: Thu, 27 Jan 2022 16:47:18 +0000
Subject: [PATCH 3/6] Export constructor for PRational

---
 Plutarch/Rational.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Plutarch/Rational.hs b/Plutarch/Rational.hs
index d123bd8a7..5affa89bf 100644
--- a/Plutarch/Rational.hs
+++ b/Plutarch/Rational.hs
@@ -1,5 +1,5 @@
 module Plutarch.Rational (
-  PRational,
+  PRational(..),
   preduce,
   pnumerator,
   pdenominator,

From e937da28fa61a057904dd6da2f017a3b50f521e6 Mon Sep 17 00:00:00 2001
From: Las Safin <me@las.rs>
Date: Thu, 27 Jan 2022 16:52:19 +0000
Subject: [PATCH 4/6] Inline trivial arguments

---
 Plutarch/Internal.hs             | 21 ++++++++++++++++++++-
 Plutarch/Rational.hs             |  2 +-
 examples/Main.hs                 |  4 +++-
 plutarch-benchmark/bench/Main.hs |  2 +-
 4 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/Plutarch/Internal.hs b/Plutarch/Internal.hs
index 659e01d11..8b484fa01 100644
--- a/Plutarch/Internal.hs
+++ b/Plutarch/Internal.hs
@@ -327,6 +327,17 @@ phoistAcyclic t = case asRawTerm t 0 of
        in Term $ \_ -> TermResult (RHoisted hoisted) (hoisted : getDeps t')
     Left e -> error $ "Hoisted term errs! " <> show e
 
+-- Couldn't find a definition for this in plutus-core
+subst :: Natural -> (Natural -> UPLC.Term DeBruijn UPLC.DefaultUni UPLC.DefaultFun ()) -> UPLC.Term DeBruijn UPLC.DefaultUni UPLC.DefaultFun () -> UPLC.Term DeBruijn UPLC.DefaultUni UPLC.DefaultFun ()
+subst idx x (UPLC.Apply () yx yy) = UPLC.Apply () (subst idx x yx) (subst idx x yy)
+subst idx x (UPLC.LamAbs () name y) = UPLC.LamAbs () name (subst (idx + 1) x y)
+subst idx x (UPLC.Delay () y) = UPLC.Delay () (subst idx x y)
+subst idx x (UPLC.Force () y) = UPLC.Force () (subst idx x y)
+subst idx x (UPLC.Var () (DeBruijn (Index idx'))) | idx == idx' = x idx
+subst idx _ y@(UPLC.Var () (DeBruijn (Index idx'))) | idx > idx' = y
+subst idx _ (UPLC.Var () (DeBruijn (Index idx'))) | idx < idx' = UPLC.Var () (DeBruijn . Index $ idx' - 1)
+subst _ _ y = y
+
 rawTermToUPLC ::
   (HoistedTerm -> Natural -> UPLC.Term DeBruijn UPLC.DefaultUni UPLC.DefaultFun ()) ->
   Natural ->
@@ -340,7 +351,15 @@ rawTermToUPLC m l (RLamAbs n t) =
     (replicate (fromIntegral $ n + 1) $ UPLC.LamAbs () (DeBruijn . Index $ 0))
     $ (rawTermToUPLC m (l + n + 1) t)
 rawTermToUPLC m l (RApply x y) =
-  foldr (.) id ((\y' t -> UPLC.Apply () t (rawTermToUPLC m l y')) <$> y) $ (rawTermToUPLC m l x)
+  let f y t@(UPLC.LamAbs () _ body) =
+        case rawTermToUPLC m l y of
+          -- Inline unconditionally if it's a variable or built-in.
+          -- These terms are very small and are always WHNF.
+          UPLC.Var () (DeBruijn (Index idx)) -> subst 1 (\lvl -> UPLC.Var () (DeBruijn . Index $ idx + lvl - 1)) body
+          arg@UPLC.Builtin {} -> subst 1 (\_ -> arg) body
+          arg -> UPLC.Apply () t arg
+      f y t = UPLC.Apply () t (rawTermToUPLC m l y)
+   in foldr (.) id (f <$> y) $ (rawTermToUPLC m l x)
 rawTermToUPLC m l (RDelay t) = UPLC.Delay () (rawTermToUPLC m l t)
 rawTermToUPLC m l (RForce t) = UPLC.Force () (rawTermToUPLC m l t)
 rawTermToUPLC _ _ (RBuiltin f) = UPLC.Builtin () f
diff --git a/Plutarch/Rational.hs b/Plutarch/Rational.hs
index 5affa89bf..2d6049d93 100644
--- a/Plutarch/Rational.hs
+++ b/Plutarch/Rational.hs
@@ -1,5 +1,5 @@
 module Plutarch.Rational (
-  PRational(..),
+  PRational (..),
   preduce,
   pnumerator,
   pdenominator,
diff --git a/examples/Main.hs b/examples/Main.hs
index 1f6857572..c2a1eb725 100644
--- a/examples/Main.hs
+++ b/examples/Main.hs
@@ -244,7 +244,9 @@ plutarchTests =
         , testCase "let f = hoist (λx. x) in λx y. f x y => λx y. x y" $
             printTerm ((plam $ \x y -> (phoistAcyclic $ plam $ \x -> x) # x # y)) @?= "(program 1.0.0 (\\i0 -> \\i0 -> i2 i1))"
         , testCase "let f = hoist (λx. x True) in λx y. f x y => λx y. (λz. z True) x y" $
-            printTerm ((plam $ \x y -> ((phoistAcyclic $ plam $ \x -> x # pcon PTrue)) # x # y)) @?= "(program 1.0.0 (\\i0 -> \\i0 -> (\\i0 -> i1 True) i2 i1))"
+            printTerm ((plam $ \x y -> ((phoistAcyclic $ plam $ \x -> x # pcon PTrue)) # x # y)) @?= "(program 1.0.0 (\\i0 -> \\i0 -> i2 True i1))"
+        , testCase "λy. (λx. x + x) y" $
+            printTerm (plam $ \y -> (plam $ \(x :: Term _ PInteger) -> x + x) # y) @?= "(program 1.0.0 (\\i0 -> addInteger i1 i1))"
         ]
     , testGroup
         "Lifting of constants"
diff --git a/plutarch-benchmark/bench/Main.hs b/plutarch-benchmark/bench/Main.hs
index faf58bc49..71816a761 100644
--- a/plutarch-benchmark/bench/Main.hs
+++ b/plutarch-benchmark/bench/Main.hs
@@ -114,7 +114,7 @@ intListBench =
           , bench "/=(empty;n=3)" $ List.plistEquals @PBuiltinList @PInteger # pconstant [] # pconstant [1, 2, 3]
           ]
       , benchGroup
-          "pconstant"
+          "primitives"
           [ bench' $ plam $ \_ -> pconstant True
           , bench' $ plam $ \_ -> (0 :: Term _ PInteger)
           , bench' $ plam $ \_ -> (1 :: Term _ PInteger)

From 7ebef083839a0a34ff64608bd86c7b02f2b889a5 Mon Sep 17 00:00:00 2001
From: Las Safin <me@las.rs>
Date: Thu, 27 Jan 2022 17:15:19 +0000
Subject: [PATCH 5/6] Optimise pdrop

---
 Plutarch/DataRepr/Internal/Field.hs | 26 +++++++++++++++++++++++++-
 Plutarch/List.hs                    |  9 ++++++---
 2 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/Plutarch/DataRepr/Internal/Field.hs b/Plutarch/DataRepr/Internal/Field.hs
index d17287197..294b5f3fd 100644
--- a/Plutarch/DataRepr/Internal/Field.hs
+++ b/Plutarch/DataRepr/Internal/Field.hs
@@ -166,10 +166,34 @@ instance {-# OVERLAPPABLE #-} (BindFields ps bs) => BindFields ((l ':= p) ': ps)
     xs <- bindFields @ps @bs (pdropDataRecord (Proxy @1) t')
     pure $ HCons (Labeled $ pindexDataRecord (Proxy @0) t') xs
 
-instance (BindFields ps bs) => BindFields (p ': ps) ( 'Skip ': bs) where
+instance {-# OVERLAPPING #-} (BindFields ps bs) => BindFields (p1 ': ps) ( 'Skip ': bs) where
   bindFields t = do
     bindFields @ps @bs $ pdropDataRecord (Proxy @1) t
 
+instance {-# OVERLAPPING #-} (BindFields ps bs) => BindFields (p1 ': p2 ': ps) ( 'Skip ': 'Skip ': bs) where
+  bindFields t = do
+    bindFields @ps @bs $ pdropDataRecord (Proxy @2) t
+
+instance {-# OVERLAPPING #-} (BindFields ps bs) => BindFields (p1 ': p2 ': p3 ': ps) ( 'Skip ': 'Skip ': 'Skip ': bs) where
+  bindFields t = do
+    bindFields @ps @bs $ pdropDataRecord (Proxy @3) t
+
+instance {-# OVERLAPPING #-} (BindFields ps bs) => BindFields (p1 ': p2 ': p3 ': p4 ': ps) ( 'Skip ': 'Skip ': 'Skip ': 'Skip ': bs) where
+  bindFields t = do
+    bindFields @ps @bs $ pdropDataRecord (Proxy @4) t
+
+instance {-# OVERLAPPING #-} (BindFields ps bs) => BindFields (p1 ': p2 ': p3 ': p4 ': p5 ': ps) ( 'Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': bs) where
+  bindFields t = do
+    bindFields @ps @bs $ pdropDataRecord (Proxy @5) t
+
+instance {-# OVERLAPPING #-} (BindFields ps bs) => BindFields (p1 ': p2 ': p3 ': p4 ': p5 ': p6 ': ps) ( 'Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': bs) where
+  bindFields t = do
+    bindFields @ps @bs $ pdropDataRecord (Proxy @6) t
+
+instance {-# OVERLAPPING #-} (BindFields ps bs) => BindFields (p1 ': p2 ': p3 ': p4 ': p5 ': p6 ': p7 ': ps) ( 'Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': bs) where
+  bindFields t = do
+    bindFields @ps @bs $ pdropDataRecord (Proxy @7) t
+
 --------------------------------------------------------------------------------
 
 {- |
diff --git a/Plutarch/List.hs b/Plutarch/List.hs
index 63c431b8a..ba09ad1d9 100644
--- a/Plutarch/List.hs
+++ b/Plutarch/List.hs
@@ -45,6 +45,7 @@ import Numeric.Natural (Natural)
 import qualified GHC.Generics as GHC
 import Generics.SOP (Generic, I (I))
 import Plutarch (
+  ClosedTerm,
   PDelayed,
   PType,
   PlutusType,
@@ -183,10 +184,12 @@ ptryIndex n xs = phead # (pdrop n xs)
   efficient in many circumstances.
 -}
 pdrop :: (PIsListLike list a) => Natural -> Term s (list a) -> Term s (list a)
-pdrop n xs = (phoistAcyclic $ plam $ \x -> pdrop' n x) # xs
+pdrop n xs = pdrop' n # xs
   where
-    pdrop' 0 xs' = xs'
-    pdrop' n' xs' = pdrop' (n' - 1) (ptail # xs')
+    pdrop' :: (PIsListLike list a) => Natural -> ClosedTerm (list a :--> list a)
+    pdrop' 0 = plam $ \x -> x
+    pdrop' 1 = ptail
+    pdrop' n' = phoistAcyclic $ plam $ \x -> ptail #$ pdrop' (n' - 1) # x
 
 --------------------------------------------------------------------------------
 

From 636d12b734aa76a70d95e5737f38a1a3fa2426b6 Mon Sep 17 00:00:00 2001
From: Las Safin <me@las.rs>
Date: Thu, 27 Jan 2022 17:16:13 +0000
Subject: [PATCH 6/6] Fix tests

---
 examples/Examples/Field.hs  | 12 ++++++------
 examples/Examples/LetRec.hs | 28 ++++++++++++++--------------
 2 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/examples/Examples/Field.hs b/examples/Examples/Field.hs
index 2589ef1e3..9a61b4e82 100644
--- a/examples/Examples/Field.hs
+++ b/examples/Examples/Field.hs
@@ -286,22 +286,22 @@ tests =
 
 tripSumComp :: String
 tripSumComp =
-  "(program 1.0.0 ((\\i0 -> (\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> (\\i0 -> addInteger (addInteger (unIData (i4 i2)) (unIData (i4 i1))) (unIData (i4 (i5 i1)))) (i4 i1)) ((\\i0 -> force (force sndPair) (unConstrData i1)) i1)) (force headList)) i1) (force tailList)))"
+  "(program 1.0.0 ((\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> (\\i0 -> addInteger (addInteger (unIData (i4 i2)) (unIData (i4 i1))) (unIData (i4 (i5 i1)))) (i4 i1)) (force (force sndPair) (unConstrData i1))) (force headList)) (force tailList)))"
 
 nFieldsComp :: String
 nFieldsComp = "(program 1.0.0 ((\\i0 -> \\i0 -> addInteger (unIData (i2 i1)) (unIData (i2 (force tailList i1)))) (force headList)))"
 
 dropFieldsComp :: String
-dropFieldsComp = "(program 1.0.0 ((\\i0 -> (\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> addInteger (unIData (i3 i1)) (unIData (i3 (i4 i1)))) (i3 (i3 (i3 (i3 (i3 (i3 (i3 (i3 i1))))))))) (force headList)) i1) (force tailList)))"
+dropFieldsComp = "(program 1.0.0 ((\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> addInteger (unIData (i3 i1)) (unIData (i3 (i4 i1)))) (i3 (i3 (i3 (i3 (i3 (i3 (i3 (i3 i1))))))))) (force headList)) (force tailList)))"
 
 rangeFieldsComp :: String
-rangeFieldsComp = "(program 1.0.0 ((\\i0 -> (\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> addInteger (unIData (i3 i1)) (unIData (i3 (i4 i1)))) (i3 (i3 (i3 (i3 (i3 i1)))))) (force headList)) i1) (force tailList)))"
+rangeFieldsComp = "(program 1.0.0 ((\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> addInteger (unIData (i3 i1)) (unIData (i3 (i4 i1)))) (i3 (i3 (i3 (i3 (i3 i1)))))) (force headList)) (force tailList)))"
 
 getYComp :: String
-getYComp = "(program 1.0.0 (\\i0 -> force headList (force tailList ((\\i0 -> force (force sndPair) (unConstrData i1)) i1))))"
+getYComp = "(program 1.0.0 (\\i0 -> force headList (force tailList (force (force sndPair) (unConstrData i1)))))"
 
 tripYZComp :: String
-tripYZComp = "(program 1.0.0 ((\\i0 -> (\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> addInteger (unIData (i3 i1)) (unIData (i3 (i4 i1)))) (i3 ((\\i0 -> force (force sndPair) (unConstrData i1)) i1))) (force headList)) i1) (force tailList)))"
+tripYZComp = "(program 1.0.0 ((\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> addInteger (unIData (i3 i1)) (unIData (i3 (i4 i1)))) (i3 (force (force sndPair) (unConstrData i1)))) (force headList)) (force tailList)))"
 
 letSomeFieldsComp :: String
-letSomeFieldsComp = "(program 1.0.0 ((\\i0 -> (\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> (\\i0 -> addInteger (addInteger (unIData (i4 i2)) (unIData (i4 i1))) (unIData (i4 (i5 (i5 (i5 i1)))))) (i4 i1)) (i3 (i3 (i3 i1)))) (force headList)) i1) (force tailList)))"
+letSomeFieldsComp = "(program 1.0.0 ((\\i0 -> (\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> (\\i0 -> addInteger (addInteger (unIData (i4 i2)) (unIData (i4 i1))) (unIData (i4 (i5 (i6 i1))))) (i5 i1)) (i4 (i3 i1))) (force headList)) (\\i0 -> i2 (i2 i1))) (force tailList)))"
diff --git a/examples/Examples/LetRec.hs b/examples/Examples/LetRec.hs
index 2dcfd32db..24574d77c 100644
--- a/examples/Examples/LetRec.hs
+++ b/examples/Examples/LetRec.hs
@@ -252,10 +252,10 @@ tests =
         "flat nested"
         [ testCase "record construction with rcon" $
             printTerm (sampleFlatOuter)
-              @?= "(program 1.0.0 (\\i0 -> i1 False False 6 \"Salut, Monde!\" 4 False 9 \"Salut, Monde!\" \"Hola, Mundo!\"))"
+              @?= "(program 1.0.0 ((\\i0 -> \\i0 -> i1 False False 6 i2 4 False 9 i2 \"Hola, Mundo!\") \"Salut, Monde!\"))"
         , testCase "nested field access" $
             printTerm (sampleFlatOuter # field (sampleInt . flatInner2))
-              @?= "(program 1.0.0 ((\\i0 -> i1 False False 6 \"Salut, Monde!\" 4 False 9 \"Salut, Monde!\" \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i3)))"
+              @?= "(program 1.0.0 ((\\i0 -> (\\i0 -> i1 False False 6 i2 4 False 9 i2 \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i3)) \"Salut, Monde!\"))"
         , testGroup "nested field value" $
             [ testCase "direct access" $
                 equal' (sampleFlatOuter # field (sampleInt . flatInner2)) "(program 1.0.0 9)"
@@ -268,7 +268,7 @@ tests =
             ]
         , testCase "reconstruct with pcon" $
             printTerm (pmatch' sampleFlatOuter (pcon @(PRecord FlatOuterRecord)))
-              @?= "(program 1.0.0 ((\\i0 -> i1 False False 6 \"Salut, Monde!\" 4 False 9 \"Salut, Monde!\" \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i1 i10 i9 i8 i7 i6 i5 i4 i3 i2)))"
+              @?= "(program 1.0.0 ((\\i0 -> (\\i0 -> i1 False False 6 i2 4 False 9 i2 \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i1 i10 i9 i8 i7 i6 i5 i4 i3 i2)) \"Salut, Monde!\"))"
         , testCase "reconstruction nested field value" $
             equal' (pto (pmatch' sampleFlatOuter (pcon @(PRecord FlatOuterRecord))) # field (sampleInt . flatInner2)) "(program 1.0.0 9)"
         , testCase "nested record access term" $
@@ -276,14 +276,14 @@ tests =
               ( pmatch' (rcon rawFlatOuter) $
                   \(PRecord FlatOuterRecord {flatInner1}) -> pcon $ PRecord flatInner1
               )
-              @?= "(program 1.0.0 ((\\i0 -> i1 False False 6 \"Salut, Monde!\" 4 False 9 \"Salut, Monde!\" \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i1 i9 i8 i7)))"
+              @?= "(program 1.0.0 ((\\i0 -> (\\i0 -> i1 False False 6 i2 4 False 9 i2 \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i1 i9 i8 i7)) \"Salut, Monde!\"))"
         , testCase "nested match term" $
             printTerm
               ( rmatch (rcon rawFlatOuter) $ \(FlatOuterRecord {flatInner2}) ->
                   rmatch (rcon flatInner2) $ \(SampleRecord {sampleString}) ->
                     sampleString
               )
-              @?= "(program 1.0.0 ((\\i0 -> i1 False False 6 \"Salut, Monde!\" 4 False 9 \"Salut, Monde!\" \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> (\\i0 -> i1 i5 i4 i3) (\\i0 -> \\i0 -> \\i0 -> i1))))"
+              @?= "(program 1.0.0 ((\\i0 -> (\\i0 -> i1 False False 6 i2 4 False 9 i2 \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> (\\i0 -> i1 i5 i4 i3) (\\i0 -> \\i0 -> \\i0 -> i1))) \"Salut, Monde!\"))"
         , testCase "nested match value" $
             equal'
               ( rmatch (rcon rawFlatOuter) $ \(FlatOuterRecord {flatInner2}) ->
@@ -296,10 +296,10 @@ tests =
         "shallow nested"
         [ testCase "record construction with rcon" $
             printTerm (sampleShallowOuter)
-              @?= "(program 1.0.0 (\\i0 -> i1 False (\\i0 -> i1 False 6 \"Salut, Monde!\") 4 (\\i0 -> i1 False 9 \"Salut, Monde!\") \"Hola, Mundo!\"))"
+              @?= "(program 1.0.0 ((\\i0 -> \\i0 -> i1 False (\\i0 -> i1 False 6 i3) 4 (\\i0 -> i1 False 9 i3) \"Hola, Mundo!\") \"Salut, Monde!\"))"
         , testCase "nested field access" $
             printTerm (pto (sampleShallowOuter # field shallowInner2) # field sampleInt)
-              @?= "(program 1.0.0 ((\\i0 -> i1 False (\\i0 -> i1 False 6 \"Salut, Monde!\") 4 (\\i0 -> i1 False 9 \"Salut, Monde!\") \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i2) (\\i0 -> \\i0 -> \\i0 -> i2)))"
+              @?= "(program 1.0.0 ((\\i0 -> (\\i0 -> i1 False (\\i0 -> i1 False 6 i3) 4 (\\i0 -> i1 False 9 i3) \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i2) (\\i0 -> \\i0 -> \\i0 -> i2)) \"Salut, Monde!\"))"
         , testGroup "nested field value" $
             [ testCase "direct access" $
                 equal' (pto (sampleShallowOuter # field shallowInner2) # field sampleInt) "(program 1.0.0 9)"
@@ -312,19 +312,19 @@ tests =
             ]
         , testCase "reconstruct with pcon" $
             printTerm (pmatch' sampleShallowOuter (pcon @(PRecord ShallowOuterRecord)))
-              @?= "(program 1.0.0 ((\\i0 -> i1 False (\\i0 -> i1 False 6 \"Salut, Monde!\") 4 (\\i0 -> i1 False 9 \"Salut, Monde!\") \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i1 i6 i5 i4 i3 i2)))"
+              @?= "(program 1.0.0 ((\\i0 -> (\\i0 -> i1 False (\\i0 -> i1 False 6 i3) 4 (\\i0 -> i1 False 9 i3) \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i1 i6 i5 i4 i3 i2)) \"Salut, Monde!\"))"
         , testCase "reconstruction nested field value" $
             equal' (pto (pto (pmatch' sampleShallowOuter (pcon @(PRecord ShallowOuterRecord))) # field shallowInner2) # field sampleInt) "(program 1.0.0 9)"
         , testCase "nested record access term" $
             printTerm (pmatch' sampleShallowOuter $ \(PRecord ShallowOuterRecord {shallowInner1}) -> shallowInner1)
-              @?= "(program 1.0.0 ((\\i0 -> i1 False (\\i0 -> i1 False 6 \"Salut, Monde!\") 4 (\\i0 -> i1 False 9 \"Salut, Monde!\") \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i4)))"
+              @?= "(program 1.0.0 ((\\i0 -> (\\i0 -> i1 False (\\i0 -> i1 False 6 i3) 4 (\\i0 -> i1 False 9 i3) \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i4)) \"Salut, Monde!\"))"
         , testCase "nested match term" $
             printTerm
               ( pmatch' sampleShallowOuter $ \(PRecord ShallowOuterRecord {shallowInner2}) ->
                   pmatch shallowInner2 $ \(PRecord SampleRecord {sampleString}) ->
                     sampleString
               )
-              @?= "(program 1.0.0 ((\\i0 -> i1 False (\\i0 -> i1 False 6 \"Salut, Monde!\") 4 (\\i0 -> i1 False 9 \"Salut, Monde!\") \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i2 (\\i0 -> \\i0 -> \\i0 -> i1))))"
+              @?= "(program 1.0.0 ((\\i0 -> (\\i0 -> i1 False (\\i0 -> i1 False 6 i3) 4 (\\i0 -> i1 False 9 i3) \"Hola, Mundo!\") (\\i0 -> \\i0 -> \\i0 -> \\i0 -> \\i0 -> i2 (\\i0 -> \\i0 -> \\i0 -> i1))) \"Salut, Monde!\"))"
         , testCase "nested match value" $
             equal'
               ( pmatch' sampleShallowOuter $ \(PRecord ShallowOuterRecord {shallowInner2}) ->
@@ -337,7 +337,7 @@ tests =
         "Data"
         [ testGroup
             "pdata"
-            [ testCase "simple" $ printTerm sampleData @?= "(program 1.0.0 ((\\i0 -> i1 False 6 \"Salut, Monde!\") (\\i0 -> \\i0 -> \\i0 -> constrData 0 (force mkCons ((\\i0 -> constrData (force ifThenElse i1 1 0) [  ]) i3) (force mkCons (iData i2) (force mkCons (bData (encodeUtf8 i1)) [  ]))))))"
+            [ testCase "simple" $ printTerm sampleData @?= "(program 1.0.0 ((\\i0 -> i1 False 6 \"Salut, Monde!\") (\\i0 -> \\i0 -> \\i0 -> constrData 0 (force mkCons (constrData (force ifThenElse i3 1 0) [  ]) (force mkCons (iData i2) (force mkCons (bData (encodeUtf8 i1)) [  ]))))))"
             , testCase "simple value deconstructed" $ equal' (pasConstr # pforgetData sampleData) "(program 1.0.0 (0, [#d87980, #06, #4d53616c75742c204d6f6e646521]))"
             , testCase "flat data deconstructed" $
                 equal'
@@ -382,7 +382,7 @@ result_fieldFromDataTerm'simpleRecord =
 #ifdef Development
   "(program 1.0.0 (\\i0 -> unIData ((\\i0 -> (\\i0 -> force (force ifThenElse (equalsInteger (force (force fstPair) i1) 0) (delay (force headList (force tailList (force (force sndPair) i1)))) (delay (force (force trace \"verifySoleConstructor failed\" (delay error)))))) (unConstrData i1)) i1)))"
 #else
-  "(program 1.0.0 (\\i0 -> unIData ((\\i0 -> (\\i0 -> force (force ifThenElse (equalsInteger (force (force fstPair) i1) 0) (delay (force headList (force tailList (force (force sndPair) i1)))) (delay error))) (unConstrData i1)) i1)))"
+  "(program 1.0.0 (\\i0 -> unIData ((\\i0 -> force (force ifThenElse (equalsInteger (force (force fstPair) i1) 0) (delay (force headList (force tailList (force (force sndPair) i1)))) (delay error))) (unConstrData i1))))"
 #endif
 
 result_fieldFromDataTerm'flatNested :: String
@@ -390,7 +390,7 @@ result_fieldFromDataTerm'flatNested =
 #ifdef Development
   "(program 1.0.0 ((\\i0 -> \\i0 -> unIData ((\\i0 -> (\\i0 -> force (force ifThenElse (equalsInteger (force (force fstPair) i1) 0) (delay (force headList (i4 (i4 (i4 (i4 (i4 (i4 (force (force sndPair) i1))))))))) (delay (force (force trace \"verifySoleConstructor failed\" (delay error)))))) (unConstrData i1)) i1)) (force tailList)))"
 #else
-  "(program 1.0.0 ((\\i0 -> \\i0 -> unIData ((\\i0 -> (\\i0 -> force (force ifThenElse (equalsInteger (force (force fstPair) i1) 0) (delay (force headList (i4 (i4 (i4 (i4 (i4 (i4 (force (force sndPair) i1))))))))) (delay error))) (unConstrData i1)) i1)) (force tailList)))"
+  "(program 1.0.0 ((\\i0 -> \\i0 -> unIData ((\\i0 -> force (force ifThenElse (equalsInteger (force (force fstPair) i1) 0) (delay (force headList (i3 (i3 (i3 (i3 (i3 (i3 (force (force sndPair) i1))))))))) (delay error))) (unConstrData i1))) (force tailList)))"
 #endif
 
 result_fieldFromDataTerm'shallowNested :: String
@@ -398,7 +398,7 @@ result_fieldFromDataTerm'shallowNested =
 #ifdef Development
   "(program 1.0.0 ((\\i0 -> (\\i0 -> (\\i0 -> (\\i0 -> (\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> (\\i0 -> force (i4 (equalsInteger (i5 i1) 0) (delay (\\i0 -> i1 ((\\i0 -> equalsInteger (i7 (unConstrData i1)) 1) (i7 (i9 i2))) (unIData (i7 (i8 (i9 i2)))) (decodeUtf8 (unBData (i7 (i8 (i8 (i9 i2)))))))) (delay (force (i9 \"verifySoleConstructor failed\" (delay error)))))) (unConstrData i1)) ((\\i0 -> (\\i0 -> force (i4 (equalsInteger (i5 i1) 0) (delay (i6 (i7 (i7 (i7 (i8 i1)))))) (delay (force (i9 \"verifySoleConstructor failed\" (delay error)))))) (unConstrData i1)) i1) (\\i0 -> \\i0 -> \\i0 -> i2)) (force ifThenElse)) (force (force fstPair))) (force headList)) (force tailList)) (force (force sndPair))) (force trace)))"
 #else
-  "(program 1.0.0 ((\\i0 -> (\\i0 -> (\\i0 -> (\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> (\\i0 -> force (i4 (equalsInteger (i5 i1) 0) (delay (\\i0 -> i1 ((\\i0 -> equalsInteger (i7 (unConstrData i1)) 1) (i7 (i9 i2))) (unIData (i7 (i8 (i9 i2)))) (decodeUtf8 (unBData (i7 (i8 (i8 (i9 i2)))))))) (delay error))) (unConstrData i1)) ((\\i0 -> (\\i0 -> force (i4 (equalsInteger (i5 i1) 0) (delay (i6 (i7 (i7 (i7 (i8 i1)))))) (delay error))) (unConstrData i1)) i1) (\\i0 -> \\i0 -> \\i0 -> i2)) (force ifThenElse)) (force (force fstPair))) (force headList)) (force tailList)) (force (force sndPair))))"
+  "(program 1.0.0 ((\\i0 -> (\\i0 -> (\\i0 -> (\\i0 -> (\\i0 -> \\i0 -> (\\i0 -> (\\i0 -> force (i4 (equalsInteger (i5 i1) 0) (delay (\\i0 -> i1 ((\\i0 -> equalsInteger (i7 (unConstrData i1)) 1) (i7 (i9 i2))) (unIData (i7 (i8 (i9 i2)))) (decodeUtf8 (unBData (i7 (i8 (i8 (i9 i2)))))))) (delay error))) (unConstrData i1)) ((\\i0 -> force (i3 (equalsInteger (i4 i1) 0) (delay (i5 (i6 (i6 (i6 (i7 i1)))))) (delay error))) (unConstrData i1)) (\\i0 -> \\i0 -> \\i0 -> i2)) (force ifThenElse)) (force (force fstPair))) (force headList)) (force tailList)) (force (force sndPair))))"
 #endif
 
 result_fieldFromDataValue'shallowNested :: String