Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Builtins] Make 'toBuiltinRuntime' a class method #4419

Conversation

effectfully
Copy link
Contributor

Same as #4418 except doesn't contain fancy unfolding stuff, which deserves a separate PR.

Don't look here yet.

@effectfully effectfully changed the title Effectfully/builtins/to builtin runtime as a class method no unfold eq [Builtins] Make 'toBuiltinRuntime' a class method Feb 19, 2022
@effectfully
Copy link
Contributor Author

/benchmark plutus-benchmark:validation

@iohk-devops
Copy link

Comparing benchmark results of 'plutus-benchmark:validation' on '0397f83b8' (base) and '307cbbdb7' (PR)

Script 0397f83 307cbbd Change
auction_1-1 279.8 μs 264.3 μs -5.5%
auction_1-2 940.9 μs 908.9 μs -3.4%
auction_1-3 936.9 μs 902.6 μs -3.7%
auction_1-4 364.9 μs 344.6 μs -5.6%
auction_2-1 279.9 μs 264.1 μs -5.6%
auction_2-2 938.3 μs 907.3 μs -3.3%
auction_2-3 1.188 ms 1.158 ms -2.5%
auction_2-4 930.7 μs 904.0 μs -2.9%
auction_2-5 363.7 μs 347.0 μs -4.6%
crowdfunding-success-1 330.5 μs 311.5 μs -5.7%
crowdfunding-success-2 330.7 μs 310.8 μs -6.0%
crowdfunding-success-3 330.4 μs 310.5 μs -6.0%
currency-1 366.6 μs 352.1 μs -4.0%
escrow-redeem_1-1 535.0 μs 512.0 μs -4.3%
escrow-redeem_1-2 536.9 μs 511.4 μs -4.7%
escrow-redeem_2-1 629.3 μs 597.7 μs -5.0%
escrow-redeem_2-2 627.3 μs 597.6 μs -4.7%
escrow-redeem_2-3 627.8 μs 595.6 μs -5.1%
escrow-refund-1 246.0 μs 231.3 μs -6.0%
future-increase-margin-1 368.4 μs 352.1 μs -4.4%
future-increase-margin-2 815.1 μs 784.0 μs -3.8%
future-increase-margin-3 812.1 μs 785.1 μs -3.3%
future-increase-margin-4 751.1 μs 721.6 μs -3.9%
future-increase-margin-5 1.150 ms 1.108 ms -3.7%
future-pay-out-1 368.7 μs 351.7 μs -4.6%
future-pay-out-2 810.2 μs 785.5 μs -3.0%
future-pay-out-3 812.6 μs 785.7 μs -3.3%
future-pay-out-4 1.149 ms 1.113 ms -3.1%
future-settle-early-1 368.4 μs 353.5 μs -4.0%
future-settle-early-2 816.6 μs 787.5 μs -3.6%
future-settle-early-3 814.5 μs 788.6 μs -3.2%
future-settle-early-4 889.7 μs 858.3 μs -3.5%
game-sm-success_1-1 598.9 μs 572.4 μs -4.4%
game-sm-success_1-2 311.0 μs 291.9 μs -6.1%
game-sm-success_1-3 936.5 μs 904.4 μs -3.4%
game-sm-success_1-4 362.5 μs 340.9 μs -6.0%
game-sm-success_2-1 601.3 μs 573.7 μs -4.6%
game-sm-success_2-2 311.3 μs 291.0 μs -6.5%
game-sm-success_2-3 938.6 μs 903.2 μs -3.8%
game-sm-success_2-4 363.3 μs 340.6 μs -6.2%
game-sm-success_2-5 941.4 μs 904.2 μs -4.0%
game-sm-success_2-6 364.7 μs 340.3 μs -6.7%
multisig-sm-1 608.6 μs 579.1 μs -4.8%
multisig-sm-2 596.8 μs 566.5 μs -5.1%
multisig-sm-3 602.3 μs 575.1 μs -4.5%
multisig-sm-4 609.5 μs 583.2 μs -4.3%
multisig-sm-5 835.0 μs 802.6 μs -3.9%
multisig-sm-6 608.3 μs 580.2 μs -4.6%
multisig-sm-7 595.2 μs 568.1 μs -4.6%
multisig-sm-8 601.2 μs 574.9 μs -4.4%
multisig-sm-9 607.7 μs 582.8 μs -4.1%
multisig-sm-10 833.6 μs 803.6 μs -3.6%
ping-pong-1 499.9 μs 480.8 μs -3.8%
ping-pong-2 499.4 μs 480.3 μs -3.8%
ping-pong_2-1 308.9 μs 293.1 μs -5.1%
prism-1 260.3 μs 242.0 μs -7.0%
prism-2 650.0 μs 619.6 μs -4.7%
prism-3 555.1 μs 531.4 μs -4.3%
pubkey-1 220.6 μs 207.8 μs -5.8%
stablecoin_1-1 1.307 ms 1.267 ms -3.1%
stablecoin_1-2 304.2 μs 284.6 μs -6.4%
stablecoin_1-3 1.500 ms 1.448 ms -3.5%
stablecoin_1-4 324.5 μs 301.7 μs -7.0%
stablecoin_1-5 1.911 ms 1.838 ms -3.8%
stablecoin_1-6 404.1 μs 375.5 μs -7.1%
stablecoin_2-1 1.315 ms 1.265 ms -3.8%
stablecoin_2-2 304.9 μs 283.9 μs -6.9%
stablecoin_2-3 1.504 ms 1.448 ms -3.7%
stablecoin_2-4 324.9 μs 302.2 μs -7.0%
token-account-1 285.4 μs 271.0 μs -5.0%
token-account-2 497.8 μs 476.2 μs -4.3%
uniswap-1 592.5 μs 576.1 μs -2.8%
uniswap-2 340.5 μs 324.1 μs -4.8%
uniswap-3 2.441 ms 2.337 ms -4.3%
uniswap-4 530.7 μs 497.8 μs -6.2%
uniswap-5 1.713 ms 1.623 ms -5.3%
uniswap-6 505.7 μs 477.3 μs -5.6%
vesting-1 521.1 μs 495.6 μs -4.9%

@effectfully
Copy link
Contributor Author

/benchmark plutus-benchmark:validation

@iohk-devops
Copy link

Comparing benchmark results of 'plutus-benchmark:validation' on '0397f83b8' (base) and '799d9fc5b' (PR)

Script 0397f83 799d9fc Change
auction_1-1 278.6 μs 266.6 μs -4.3%
auction_1-2 938.3 μs 911.2 μs -2.9%
auction_1-3 932.6 μs 909.0 μs -2.5%
auction_1-4 363.5 μs 346.8 μs -4.6%
auction_2-1 279.2 μs 265.5 μs -4.9%
auction_2-2 935.2 μs 910.6 μs -2.6%
auction_2-3 1.191 ms 1.158 ms -2.8%
auction_2-4 936.9 μs 908.0 μs -3.1%
auction_2-5 365.4 μs 347.3 μs -5.0%
crowdfunding-success-1 330.8 μs 312.4 μs -5.6%
crowdfunding-success-2 331.6 μs 312.8 μs -5.7%
crowdfunding-success-3 331.3 μs 311.9 μs -5.9%
currency-1 367.7 μs 353.5 μs -3.9%
escrow-redeem_1-1 534.7 μs 514.0 μs -3.9%
escrow-redeem_1-2 534.5 μs 513.8 μs -3.9%
escrow-redeem_2-1 623.4 μs 602.8 μs -3.3%
escrow-redeem_2-2 625.7 μs 604.3 μs -3.4%
escrow-redeem_2-3 626.1 μs 604.9 μs -3.4%
escrow-refund-1 246.2 μs 231.0 μs -6.2%
future-increase-margin-1 366.6 μs 355.4 μs -3.1%
future-increase-margin-2 809.4 μs 789.3 μs -2.5%
future-increase-margin-3 815.3 μs 788.6 μs -3.3%
future-increase-margin-4 757.5 μs 729.2 μs -3.7%
future-increase-margin-5 1.154 ms 1.119 ms -3.0%
future-pay-out-1 368.0 μs 353.7 μs -3.9%
future-pay-out-2 812.8 μs 787.9 μs -3.1%
future-pay-out-3 811.3 μs 787.5 μs -2.9%
future-pay-out-4 1.143 ms 1.117 ms -2.3%
future-settle-early-1 367.6 μs 353.1 μs -3.9%
future-settle-early-2 812.2 μs 787.4 μs -3.1%
future-settle-early-3 811.5 μs 787.3 μs -3.0%
future-settle-early-4 885.8 μs 863.7 μs -2.5%
game-sm-success_1-1 599.2 μs 574.1 μs -4.2%
game-sm-success_1-2 312.3 μs 293.2 μs -6.1%
game-sm-success_1-3 940.7 μs 905.4 μs -3.8%
game-sm-success_1-4 364.1 μs 343.8 μs -5.6%
game-sm-success_2-1 599.0 μs 575.0 μs -4.0%
game-sm-success_2-2 311.3 μs 295.5 μs -5.1%
game-sm-success_2-3 938.3 μs 908.9 μs -3.1%
game-sm-success_2-4 362.4 μs 345.3 μs -4.7%
game-sm-success_2-5 936.3 μs 911.8 μs -2.6%
game-sm-success_2-6 362.4 μs 344.5 μs -4.9%
multisig-sm-1 606.5 μs 583.9 μs -3.7%
multisig-sm-2 594.1 μs 572.0 μs -3.7%
multisig-sm-3 601.7 μs 576.1 μs -4.3%
multisig-sm-4 608.4 μs 583.1 μs -4.2%
multisig-sm-5 832.3 μs 804.3 μs -3.4%
multisig-sm-6 604.5 μs 580.6 μs -4.0%
multisig-sm-7 594.8 μs 569.7 μs -4.2%
multisig-sm-8 602.5 μs 577.0 μs -4.2%
multisig-sm-9 610.0 μs 583.4 μs -4.4%
multisig-sm-10 837.5 μs 806.1 μs -3.7%
ping-pong-1 502.5 μs 480.1 μs -4.5%
ping-pong-2 500.7 μs 479.8 μs -4.2%
ping-pong_2-1 310.3 μs 295.2 μs -4.9%
prism-1 260.1 μs 244.3 μs -6.1%
prism-2 647.8 μs 621.4 μs -4.1%
prism-3 555.1 μs 534.7 μs -3.7%
pubkey-1 221.1 μs 209.1 μs -5.4%
stablecoin_1-1 1.306 ms 1.269 ms -2.8%
stablecoin_1-2 304.2 μs 286.8 μs -5.7%
stablecoin_1-3 1.493 ms 1.451 ms -2.8%
stablecoin_1-4 322.6 μs 305.5 μs -5.3%
stablecoin_1-5 1.896 ms 1.831 ms -3.4%
stablecoin_1-6 401.7 μs 377.6 μs -6.0%
stablecoin_2-1 1.305 ms 1.261 ms -3.4%
stablecoin_2-2 303.9 μs 285.1 μs -6.2%
stablecoin_2-3 1.491 ms 1.446 ms -3.0%
stablecoin_2-4 323.8 μs 305.2 μs -5.7%
token-account-1 282.9 μs 272.2 μs -3.8%
token-account-2 496.8 μs 476.0 μs -4.2%
uniswap-1 593.9 μs 574.6 μs -3.2%
uniswap-2 341.3 μs 324.9 μs -4.8%
uniswap-3 2.453 ms 2.327 ms -5.1%
uniswap-4 533.1 μs 501.0 μs -6.0%
uniswap-5 1.720 ms 1.630 ms -5.2%
uniswap-6 506.9 μs 480.7 μs -5.2%
vesting-1 520.1 μs 499.7 μs -3.9%

@effectfully
Copy link
Contributor Author

/benchmark plutus-benchmark:validation

@iohk-devops
Copy link

Comparing benchmark results of 'plutus-benchmark:validation' on '0397f83b8' (base) and '695c053ee' (PR)

Script 0397f83 695c053 Change
auction_1-1 279.0 μs 265.6 μs -4.8%
auction_1-2 937.7 μs 920.0 μs -1.9%
auction_1-3 932.2 μs 911.7 μs -2.2%
auction_1-4 364.1 μs 345.7 μs -5.1%
auction_2-1 279.5 μs 265.6 μs -5.0%
auction_2-2 940.7 μs 917.8 μs -2.4%
auction_2-3 1.192 ms 1.163 ms -2.4%
auction_2-4 935.2 μs 908.8 μs -2.8%
auction_2-5 364.3 μs 344.4 μs -5.5%
crowdfunding-success-1 329.8 μs 311.4 μs -5.6%
crowdfunding-success-2 330.6 μs 310.8 μs -6.0%
crowdfunding-success-3 330.8 μs 310.5 μs -6.1%
currency-1 366.4 μs 351.8 μs -4.0%
escrow-redeem_1-1 534.6 μs 513.6 μs -3.9%
escrow-redeem_1-2 534.8 μs 513.3 μs -4.0%
escrow-redeem_2-1 626.4 μs 599.0 μs -4.4%
escrow-redeem_2-2 625.0 μs 601.3 μs -3.8%
escrow-redeem_2-3 624.5 μs 604.0 μs -3.3%
escrow-refund-1 244.6 μs 231.0 μs -5.6%
future-increase-margin-1 366.7 μs 353.6 μs -3.6%
future-increase-margin-2 812.3 μs 785.7 μs -3.3%
future-increase-margin-3 814.2 μs 787.0 μs -3.3%
future-increase-margin-4 755.6 μs 725.8 μs -3.9%
future-increase-margin-5 1.150 ms 1.116 ms -3.0%
future-pay-out-1 367.6 μs 352.3 μs -4.2%
future-pay-out-2 809.6 μs 784.4 μs -3.1%
future-pay-out-3 810.6 μs 783.5 μs -3.3%
future-pay-out-4 1.149 ms 1.111 ms -3.3%
future-settle-early-1 366.9 μs 352.1 μs -4.0%
future-settle-early-2 812.8 μs 787.1 μs -3.2%
future-settle-early-3 811.1 μs 787.2 μs -2.9%
future-settle-early-4 891.3 μs 860.4 μs -3.5%
game-sm-success_1-1 602.1 μs 575.7 μs -4.4%
game-sm-success_1-2 311.7 μs 293.3 μs -5.9%
game-sm-success_1-3 940.1 μs 906.0 μs -3.6%
game-sm-success_1-4 363.4 μs 342.4 μs -5.8%
game-sm-success_2-1 599.3 μs 578.9 μs -3.4%
game-sm-success_2-2 310.6 μs 294.5 μs -5.2%
game-sm-success_2-3 936.4 μs 912.3 μs -2.6%
game-sm-success_2-4 362.2 μs 344.7 μs -4.8%
game-sm-success_2-5 936.9 μs 913.3 μs -2.5%
game-sm-success_2-6 362.5 μs 343.6 μs -5.2%
multisig-sm-1 605.2 μs 587.4 μs -2.9%
multisig-sm-2 593.8 μs 573.7 μs -3.4%
multisig-sm-3 599.0 μs 579.0 μs -3.3%
multisig-sm-4 607.1 μs 586.1 μs -3.5%
multisig-sm-5 834.9 μs 808.3 μs -3.2%
multisig-sm-6 608.2 μs 584.2 μs -3.9%
multisig-sm-7 595.7 μs 570.9 μs -4.2%
multisig-sm-8 601.1 μs 575.8 μs -4.2%
multisig-sm-9 609.2 μs 585.1 μs -4.0%
multisig-sm-10 835.2 μs 808.5 μs -3.2%
ping-pong-1 500.6 μs 483.5 μs -3.4%
ping-pong-2 500.1 μs 483.5 μs -3.3%
ping-pong_2-1 309.6 μs 294.1 μs -5.0%
prism-1 259.9 μs 244.3 μs -6.0%
prism-2 647.2 μs 623.8 μs -3.6%
prism-3 552.8 μs 534.6 μs -3.3%
pubkey-1 220.3 μs 209.3 μs -5.0%
stablecoin_1-1 1.304 ms 1.272 ms -2.5%
stablecoin_1-2 304.2 μs 286.5 μs -5.8%
stablecoin_1-3 1.499 ms 1.455 ms -2.9%
stablecoin_1-4 323.9 μs 304.1 μs -6.1%
stablecoin_1-5 1.903 ms 1.839 ms -3.4%
stablecoin_1-6 400.0 μs 377.7 μs -5.6%
stablecoin_2-1 1.304 ms 1.266 ms -2.9%
stablecoin_2-2 303.1 μs 285.9 μs -5.7%
stablecoin_2-3 1.497 ms 1.452 ms -3.0%
stablecoin_2-4 323.4 μs 304.1 μs -6.0%
token-account-1 285.0 μs 271.1 μs -4.9%
token-account-2 499.3 μs 476.6 μs -4.5%
uniswap-1 595.0 μs 572.0 μs -3.9%
uniswap-2 340.7 μs 325.0 μs -4.6%
uniswap-3 2.446 ms 2.342 ms -4.3%
uniswap-4 530.3 μs 504.7 μs -4.8%
uniswap-5 1.704 ms 1.645 ms -3.5%
uniswap-6 505.8 μs 482.9 μs -4.5%
vesting-1 519.2 μs 502.2 μs -3.3%

@effectfully
Copy link
Contributor Author

This is a big one. Not because of the small speedup, but because it finally allows us to look into the builtins machinery as a whole instead of contemplating the multiple specific parts of it trying to guess how they interact with each other. It also lets us inline way more than what was possible before and allows us to exactly pinpoint inefficiencies.

Here's the 2.5k lines of Core of the builtins machinery in its full glory:

Core

==================== Tidy Core ====================

Result size of Tidy Core
  = {terms: 2,607, types: 13,630, coercions: 11,679, joins: 2/86}

-- RHS size: {terms: 15, types: 9, coercions: 0, joins: 0/0}
$sverifySignature
  = \ w1_i14cz w2_i14cA w3_i14cB ->
      case w1_i14cz of { PS ww7_i14cP ww8_i14cQ ww9_i14cR ww10_i14cS ->
      $wverifySignature
        $fApplicativeEvaluationResult
        EvaluationFailure
        ww7_i14cP
        ww8_i14cQ
        ww9_i14cR
        ww10_i14cS
        w2_i14cA
        w3_i14cB
      }

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$s$WTypeSchemeAll_$dKnownNat = 0

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$s$WTypeSchemeAll3 = "a"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$s$WTypeSchemeAll_$dKnownSymbol = unpackCString# $s$WTypeSchemeAll3

-- RHS size: {terms: 1, types: 6, coercions: 6, joins: 0/0}
$dContains4_r3npp = DefaultUniProtoList @~ <Co:6>

-- RHS size: {terms: 1, types: 4, coercions: 4, joins: 0/0}
$dContains1_r3npq = DefaultUniData @~ <Co:4>

-- RHS size: {terms: 3, types: 11, coercions: 5, joins: 0/0}
$dContains2_r3npr
  = DefaultUniApply @~ <Co:5> $dContains4_r3npp $dContains1_r3npq

-- RHS size: {terms: 1, types: 8, coercions: 8, joins: 0/0}
dt_r3nps = DefaultUniProtoPair @~ <Co:8>

-- RHS size: {terms: 3, types: 15, coercions: 7, joins: 0/0}
$dContains5_r3npt
  = DefaultUniApply @~ <Co:7> dt_r3nps $dContains1_r3npq

-- RHS size: {terms: 3, types: 13, coercions: 6, joins: 0/0}
$dContains3_r3npu
  = DefaultUniApply @~ <Co:6> $dContains5_r3npt $dContains1_r3npq

-- RHS size: {terms: 3, types: 15, coercions: 7, joins: 0/0}
$dContains6_r3npv
  = DefaultUniApply @~ <Co:7> $dContains4_r3npp $dContains3_r3npu

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$s$WTypeSchemeAll_$dKnownNat1 = 1

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$s$WTypeSchemeAll1 = "b"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$s$WTypeSchemeAll_$dKnownSymbol1
  = unpackCString# $s$WTypeSchemeAll1

-- RHS size: {terms: 6, types: 29, coercions: 0, joins: 0/0}
lvl_r3npw = \ @ cause_afoV @ val_a10Qq _ eta_Xo -> Right eta_Xo

-- RHS size: {terms: 3, types: 14, coercions: 15, joins: 0/0}
poly_$dKnownTypeAst_r3npx
  = \ @ val_a10Qq ->
      $fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst
        ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniOpaque_$ctoTypeAst1
         `cast` <Co:15>)

-- RHS size: {terms: 3, types: 14, coercions: 15, joins: 0/0}
poly_$dKnownTypeAst1_r3npy
  = \ @ val_a10Qq ->
      $fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst
        ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniOpaque_$ctoTypeAst2
         `cast` <Co:15>)

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
lvl1_r3npz = 9223372036854775807

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
lvl2_r3npA = -9223372036854775808

-- RHS size: {terms: 3, types: 14, coercions: 15, joins: 0/0}
lvl3_r3npB
  = \ @ val_a10Qq ->
      $fKnownTypeAstTYPEuniEmitter_$ctoTypeAst
        ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniOpaque_$ctoTypeAst2
         `cast` <Co:15>)

-- RHS size: {terms: 6, types: 29, coercions: 0, joins: 0/0}
lvl4_r3npC = \ @ cause_Xgg8 @ val_a10Qq _ eta_X1s -> Right eta_X1s

-- RHS size: {terms: 3, types: 15, coercions: 16, joins: 0/0}
lvl5_r3npD
  = \ @ val_a10Qq ->
      $fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst
        ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniOpaque_$ctoTypeAst
         `cast` <Co:16>)

-- RHS size: {terms: 1, types: 4, coercions: 4, joins: 0/0}
dt1_r3npE = DefaultUniInteger @~ <Co:4>

-- RHS size: {terms: 3, types: 15, coercions: 7, joins: 0/0}
lvl6_r3npF = DefaultUniApply @~ <Co:7> dt_r3nps dt1_r3npE

-- RHS size: {terms: 3, types: 15, coercions: 7, joins: 0/0}
lvl7_r3npG = DefaultUniApply @~ <Co:7> lvl6_r3npF $dContains2_r3npr

-- RHS size: {terms: 13, types: 5, coercions: 0, joins: 0/0}
lvl8_r3npH
  = \ ds1_d13IL ds2_d13IM ->
      case eqInteger# ds2_d13IM $fToBuiltinMeaninguniDefaultFun1 of {
        __DEFAULT ->
          EvaluationSuccess ($fIntegralInteger_$cdiv ds1_d13IL ds2_d13IM);
        1# -> EvaluationFailure
      }

-- RHS size: {terms: 13, types: 5, coercions: 0, joins: 0/0}
lvl9_r3npI
  = \ ds1_d13IL ds2_d13IM ->
      case eqInteger# ds2_d13IM $fToBuiltinMeaninguniDefaultFun1 of {
        __DEFAULT ->
          EvaluationSuccess ($fIntegralInteger_$cquot ds1_d13IL ds2_d13IM);
        1# -> EvaluationFailure
      }

-- RHS size: {terms: 13, types: 5, coercions: 0, joins: 0/0}
lvl10_r3npJ
  = \ ds1_d13IL ds2_d13IM ->
      case eqInteger# ds2_d13IM $fToBuiltinMeaninguniDefaultFun1 of {
        __DEFAULT ->
          EvaluationSuccess ($fIntegralInteger_$crem ds1_d13IL ds2_d13IM);
        1# -> EvaluationFailure
      }

-- RHS size: {terms: 13, types: 5, coercions: 0, joins: 0/0}
lvl11_r3npK
  = \ ds1_d13IL ds2_d13IM ->
      case eqInteger# ds2_d13IM $fToBuiltinMeaninguniDefaultFun1 of {
        __DEFAULT ->
          EvaluationSuccess ($fIntegralInteger_$cmod ds1_d13IL ds2_d13IM);
        1# -> EvaluationFailure
      }

-- RHS size: {terms: 2, types: 1, coercions: 0, joins: 0/0}
lvl12_r3npL = mappend $fMonoidByteString

-- RHS size: {terms: 74, types: 90, coercions: 5, joins: 0/3}
$wlvl_r3npM
  = \ w_s3mgk ww_s3mgo ww1_s3mgp ww2_s3mgq ww3_s3mgr ->
      case runRW#
             (\ s_i1475 ->
                let { x_s3l0T = +# ww3_s3mgr 1# } in
                case <# x_s3l0T 0# of {
                  __DEFAULT ->
                    case newPinnedByteArray# x_s3l0T s_i1475 of
                    { (# ipv_i147f, ipv1_i147g #) ->
                    case integerToWord w_s3mgk of wild_i1jdn { __DEFAULT ->
                    let {
                      ipv2_s3l0S = byteArrayContents# (ipv1_i147g `cast` <Co:5>) } in
                    case writeWord8OffAddr#
                           ipv2_s3l0S 0# (narrow8Word# wild_i1jdn) ipv_i147f
                    of s2_i148r
                    { __DEFAULT ->
                    case {__pkg_ccall bytestring-0.10.12.0 Addr#
                                  -> Addr#
                                  -> Word#
                                  -> State# RealWorld
                                  -> (# State# RealWorld, Addr# #)}_i148s
                           (plusAddr# ipv2_s3l0S 1#)
                           (plusAddr# ww_s3mgo ww2_s3mgq)
                           (int2Word# ww3_s3mgr)
                           s2_i148r
                    of
                    { (# ds4_i148u, ds5_i148v #) ->
                    case touch# ww1_s3mgp ds4_i148u of s'_i148x { __DEFAULT ->
                    let { ipv3_s3l0R = PlainPtr ipv1_i147g } in
                    case touch# ipv3_s3l0R s'_i148x of s'1_i148y { __DEFAULT ->
                    (# s'1_i148y, PS ipv2_s3l0S ipv3_s3l0R 0# x_s3l0T #)
                    }
                    }
                    }
                    }
                    }
                    };
                  1# -> case mallocPlainForeignPtrBytes2 of wild_00 { }
                })
      of
      { (# ipv_i148B, ipv1_i148C #) ->
      ipv1_i148C
      }

-- RHS size: {terms: 11, types: 7, coercions: 0, joins: 0/0}
lvl13_r3npN
  = \ w_s3mgk w1_s3mgl ->
      case w1_s3mgl of { PS ww1_s3mgo ww2_s3mgp ww3_s3mgq ww4_s3mgr ->
      $wlvl_r3npM w_s3mgk ww1_s3mgo ww2_s3mgp ww3_s3mgq ww4_s3mgr
      }

-- RHS size: {terms: 5, types: 0, coercions: 0, joins: 0/0}
lvl14_r3npO = PS __NULL $fMonoidByteString1 0# 0#

-- RHS size: {terms: 93, types: 21, coercions: 0, joins: 0/1}
lvl15_r3npP
  = \ w_s3mgu w1_s3mgv w2_s3mgw ->
      case w_s3mgu of { I# ww1_s3mgz ->
      case w1_s3mgv of { I# ww3_s3mgD ->
      case w2_s3mgw of ww4_s3mgG
      { PS ww5_s3mgH ww6_s3mgI ww7_s3mgJ ww8_s3mgK ->
      case <=# ww1_s3mgz 0# of {
        __DEFAULT ->
          case >=# ww1_s3mgz ww8_s3mgK of {
            __DEFAULT ->
              case <=# ww3_s3mgD 0# of {
                __DEFAULT ->
                  let { dt32_s3l2e = -# ww8_s3mgK ww1_s3mgz } in
                  case >=# ww3_s3mgD dt32_s3l2e of {
                    __DEFAULT ->
                      PS ww5_s3mgH ww6_s3mgI (+# ww7_s3mgJ ww1_s3mgz) ww3_s3mgD;
                    1# -> PS ww5_s3mgH ww6_s3mgI (+# ww7_s3mgJ ww1_s3mgz) dt32_s3l2e
                  };
                1# -> lvl14_r3npO
              };
            1# ->
              case <=# ww3_s3mgD 0# of {
                __DEFAULT ->
                  case >=# ww3_s3mgD 0# of {
                    __DEFAULT -> PS __NULL $fMonoidByteString1 0# ww3_s3mgD;
                    1# -> lvl14_r3npO
                  };
                1# -> lvl14_r3npO
              }
          };
        1# ->
          case <=# ww3_s3mgD 0# of {
            __DEFAULT ->
              case >=# ww3_s3mgD ww8_s3mgK of {
                __DEFAULT -> PS ww5_s3mgH ww6_s3mgI ww7_s3mgJ ww3_s3mgD;
                1# -> ww4_s3mgG
              };
            1# -> lvl14_r3npO
          }
      }
      }
      }
      }

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
lvl16_r3npQ = "index"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
lvl17_r3npR = unpackCString# lvl16_r3npQ

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
lvl18_r3npS = "index too large: "#

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
lvl19_r3npT = ", length = "#

-- RHS size: {terms: 26, types: 25, coercions: 0, joins: 0/0}
$wlvl1_r3npU
  = \ ww_s3mgU w_s3mgR ->
      moduleError
        lvl17_r3npR
        (unpackAppendCString#
           lvl18_r3npS
           (case $wshowSignedInt 0# ww_s3mgU [] of
            { (# ww5_ika4, ww6_ika5 #) ->
            ++_$s++
              (unpackAppendCString#
                 lvl19_r3npT
                 (case $wshowSignedInt 0# w_s3mgR [] of
                  { (# ww2_Xkdr, ww3_Xkdt #) ->
                  : ww2_Xkdr ww3_Xkdt
                  }))
              ww5_ika4
              ww6_ika5
            }))

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
lvl20_r3npV = "negative index: "#

-- RHS size: {terms: 14, types: 13, coercions: 0, joins: 0/0}
$wlvl2_r3npW
  = \ ww_s3mh0 ->
      moduleError
        lvl17_r3npR
        (unpackAppendCString#
           lvl20_r3npV
           (case $wshowSignedInt 0# ww_s3mh0 [] of
            { (# ww5_ika4, ww6_ika5 #) ->
            : ww5_ika4 ww6_ika5
            }))

-- RHS size: {terms: 57, types: 32, coercions: 0, joins: 0/0}
$wlvl3_r3npX
  = \ w_s3mh3 ww_s3mh7 ->
      case >=# ww_s3mh7 0# of {
        __DEFAULT -> EvaluationFailure;
        1# ->
          case w_s3mh3 of { PS dt32_i149F dt33_i149G dt34_i149H dt35_i149I ->
          case <# ww_s3mh7 dt35_i149I of {
            __DEFAULT -> EvaluationFailure;
            1# ->
              EvaluationSuccess
                (case <# ww_s3mh7 0# of {
                   __DEFAULT ->
                     case >=# ww_s3mh7 dt35_i149I of {
                       __DEFAULT ->
                         case readWord8OffAddr#
                                (plusAddr# dt32_i149F (+# dt34_i149H ww_s3mh7)) 0# realWorld#
                         of
                         { (# ipv_i14ag, ipv1_i14ah #) ->
                         case touch# dt33_i149G ipv_i14ag of { __DEFAULT ->
                         smallInteger (word2Int# ipv1_i14ah)
                         }
                         };
                       1# -> case $wlvl1_r3npU ww_s3mh7 dt35_i149I of wild_00 { }
                     };
                   1# -> case $wlvl2_r3npW ww_s3mh7 of wild_00 { }
                 })
          }
          }
      }

-- RHS size: {terms: 8, types: 4, coercions: 0, joins: 0/0}
lvl21_r3npY
  = \ w_s3mh3 w1_s3mh4 ->
      case w1_s3mh4 of { I# ww1_s3mh7 -> $wlvl3_r3npX w_s3mh3 ww1_s3mh7 }

-- RHS size: {terms: 19, types: 32, coercions: 8, joins: 0/0}
lvl22_r3npZ
  = \ e1_a14eW eta1_a14eX ->
      case e1_a14eW of wild1_a14eY
      { SomeException @ e2_a14eZ $dException1_a14f2 e3_a14f3 ->
      case sameTypeRep
             (($p1Exception $dException1_a14f2) `cast` <Co:4>)
             $fExceptionUnicodeException8
      of {
        False -> raiseIO# wild1_a14eY eta1_a14eX;
        True -> (# eta1_a14eX, Left (e3_a14f3 `cast` <Co:4>) #)
      }
      }

-- RHS size: {terms: 33, types: 81, coercions: 0, joins: 0/0}
lvl23_r3nq0
  = \ x_XkZj ->
      case runRW#
             (\ eta_a14eQ ->
                catch#
                  (\ s_a14eR ->
                     case seq#
                            (case x_XkZj of { PS ww1_a1hpu ww2_a1hpv ww3_a1hpw ww4_a1hpx ->
                             $wdecodeUtf8With
                               strictDecode ww1_a1hpu ww2_a1hpv ww3_a1hpw ww4_a1hpx
                             })
                            s_a14eR
                     of
                     { (# ipv_a14eT, ipv1_a14eU #) ->
                     (# ipv_a14eT, Right ipv1_a14eU #)
                     })
                  lvl22_r3npZ
                  eta_a14eQ)
      of
      { (# ipv_a14f9, ipv1_a14fa #) ->
      case ipv1_a14fa of {
        Left ds2_i1jdy -> EvaluationFailure;
        Right y_i1jdA -> EvaluationSuccess y_i1jdA
      }
      }

-- RHS size: {terms: 10, types: 24, coercions: 0, joins: 0/0}
lvl24_r3nq1
  = \ @ val_a10Qq b_aY7V x_aY7W y_aY7X ->
      case b_aY7V of {
        False -> y_aY7X;
        True -> x_aY7W
      }

-- RHS size: {terms: 7, types: 14, coercions: 0, joins: 0/0}
lvl25_r3nq2
  = \ @ val_a10Qq ds1_d14fI a_aY7Y ->
      case ds1_d14fI of { () -> a_aY7Y }

-- RHS size: {terms: 13, types: 36, coercions: 0, joins: 0/0}
lvl26_r3nq3
  = \ @ val_a10Qq
      text_aY7Z
      a_aY80
      @ m_i1hrm
      $dMonad_i1hrn
      eta_i1hro ->
      <$
        ($p1Applicative ($p1Monad $dMonad_i1hrn))
        a_aY80
        (eta_i1hro text_aY7Z)

-- RHS size: {terms: 25, types: 88, coercions: 41, joins: 0/0}
choosePlc_r3nq4
  = \ @ a_a115c @ b_a115d ds1_d17Rl a1_aY8i b1_aY8j ->
      case ds1_d17Rl `cast` <Co:9> of { ValueOf uniListA_aY8g xs_aY8h ->
      case uniListA_aY8g of {
        __DEFAULT -> EvaluationFailure;
        DefaultUniApply @ k_apmg @ k1_apmh @ f_apmi @ a2_apmj co5_apmk
                        ds2_dqqc uniA_apjC ->
          case ds2_dqqc of {
            __DEFAULT -> EvaluationFailure;
            DefaultUniProtoList co6_apml ->
              EvaluationSuccess
                (case xs_aY8h `cast` <Co:32> of {
                   [] -> a1_aY8i;
                   : ds3_d17Tv ds4_d17Tw -> b1_aY8j
                 })
          }
      }
      }

-- RHS size: {terms: 22, types: 84, coercions: 41, joins: 0/0}
nullPlc_r3nq5
  = \ @ a_a11b6 ds1_d1fdk ->
      case ds1_d1fdk `cast` <Co:9> of { ValueOf uniListA_aY8E xs_aY8F ->
      case uniListA_aY8E of {
        __DEFAULT -> EvaluationFailure;
        DefaultUniApply @ k_apmg @ k1_apmh @ f_apmi @ a1_apmj co5_apmk
                        ds2_dqqc uniA_apjC ->
          case ds2_dqqc of {
            __DEFAULT -> EvaluationFailure;
            DefaultUniProtoList co6_apml ->
              EvaluationSuccess
                (case xs_aY8F `cast` <Co:32> of {
                   [] -> True;
                   : ds3_i1ht3 ds4_i1ht4 -> False
                 })
          }
      }
      }

-- RHS size: {terms: 19, types: 65, coercions: 0, joins: 0/0}
lvl27_r3nq6
  = \ @ val_a10Qq
      d_aY8G
      xConstr_aY8H
      xMap_aY8I
      xList_aY8J
      xI_aY8K
      xB_aY8L ->
      case d_aY8G of {
        Constr ds1_d14kV ds2_d14kW -> xConstr_aY8H;
        Map ds1_d14kX -> xMap_aY8I;
        List ds1_d14kY -> xList_aY8J;
        I ds1_d14kZ -> xI_aY8K;
        B ds1_d14l0 -> xB_aY8L
      }

-- RHS size: {terms: 10, types: 16, coercions: 0, joins: 0/0}
lvl28_r3nq7
  = \ ds1_d14mz ->
      case ds1_d14mz of {
        __DEFAULT -> EvaluationFailure;
        Constr i_aY8M ds2_aY8N -> EvaluationSuccess (i_aY8M, ds2_aY8N)
      }

-- RHS size: {terms: 8, types: 14, coercions: 0, joins: 0/0}
lvl29_r3nq8
  = \ ds1_d14nF ->
      case ds1_d14nF of {
        __DEFAULT -> EvaluationFailure;
        Map es_aY8O -> EvaluationSuccess es_aY8O
      }

-- RHS size: {terms: 8, types: 8, coercions: 0, joins: 0/0}
lvl30_r3nq9
  = \ ds1_d14oM ->
      case ds1_d14oM of {
        __DEFAULT -> EvaluationFailure;
        List ds2_aY8P -> EvaluationSuccess ds2_aY8P
      }

-- RHS size: {terms: 8, types: 5, coercions: 0, joins: 0/0}
lvl31_r3nqa
  = \ ds1_d14pT ->
      case ds1_d14pT of {
        __DEFAULT -> EvaluationFailure;
        I i_aY8Q -> EvaluationSuccess i_aY8Q
      }

-- RHS size: {terms: 8, types: 5, coercions: 0, joins: 0/0}
lvl32_r3nqb
  = \ ds1_d14r0 ->
      case ds1_d14r0 of {
        __DEFAULT -> EvaluationFailure;
        B b_aY8R -> EvaluationSuccess b_aY8R
      }

-- RHS size: {terms: 5, types: 3, coercions: 0, joins: 0/0}
lvl33_r3nqc = \ ds1_d14sD -> case ds1_d14sD of { () -> [] }

-- RHS size: {terms: 5, types: 5, coercions: 0, joins: 0/0}
lvl34_r3nqd = \ ds1_d14tG -> case ds1_d14tG of { () -> [] }

-- RHS size: {terms: 1, types: 4, coercions: 1, joins: 0/0}
lvl35_r3nqe = Eq# @~ <Co:1>

-- RHS size: {terms: 3, types: 12, coercions: 23, joins: 0/0}
lvl36_r3nqf
  = ($fAsConstantCekValue_$casConstant `cast` <Co:5>,
     $WVCon `cast` <Co:18>)

-- RHS size: {terms: 3, types: 9, coercions: 0, joins: 0/0}
lvl37_r3nqg = (lvl35_r3nqe, lvl36_r3nqf)

-- RHS size: {terms: 3, types: 6, coercions: 29, joins: 0/0}
$dKnownTypeIn16_r3nqh
  = $fKnownTypeInDefaultUniterm[]
      (lvl37_r3nqg `cast` <Co:20>) ($dContains6_r3npv `cast` <Co:9>)

-- RHS size: {terms: 3, types: 17, coercions: 9, joins: 0/0}
$d(%,%)17_r3nqi
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEDefaultUni[]_$ctoTypeAst
     `cast` <Co:9>,
     $dKnownTypeIn16_r3nqh)

-- RHS size: {terms: 2, types: 9, coercions: 26, joins: 0/0}
$dKnownMonotype38_r3nqj
  = TypeSchemeResult @~ <Co:2> ($d(%,%)17_r3nqi `cast` <Co:24>)

-- RHS size: {terms: 2, types: 0, coercions: 2, joins: 0/0}
lvl38_r3nqk
  = ReadKnownUnliftingError ($fAsConstantTerm1 `cast` <Co:2>)

-- RHS size: {terms: 33, types: 105, coercions: 38, joins: 0/0}
dt2_r3nql
  = \ @ cause_XfDd mayCause_iEmp val1_iEmq ->
      case val1_iEmq of {
        __DEFAULT -> Left (ErrorWithCause lvl38_r3nqk mayCause_iEmp);
        VCon val_a2W7W ->
          case val_a2W7W `cast` <Co:8> of { ValueOf uniAct_s3mJY x_s3mJZ ->
          case $fGCompareTYPEDefaultUni_$cgeq
                 $WDefaultUniUnit (uniAct_s3mJY `cast` <Co:8>)
          of {
            Nothing ->
              Left
                (ErrorWithCause
                   (ReadKnownUnliftingError
                      (typeMismatchError
                         ($fGShowTYPEDefaultUni_$cshowsPrec `cast` <Co:6>)
                         ($WDefaultUniUnit `cast` <Co:9>)
                         uniAct_s3mJY))
                   mayCause_iEmp);
            Just ds_iEmC ->
              case ds_iEmC of { Refl co8_iEmF -> (Right x_s3mJZ) `cast` <Co:7> }
          }
          }
      }

-- RHS size: {terms: 2, types: 3, coercions: 20, joins: 0/0}
$dKnownTypeIn17_r3nqm
  = $fKnownTypeInDefaultUniterm() (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 3, types: 11, coercions: 6, joins: 0/0}
$d(%,%)18_r3nqn
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEDefaultUni()_$ctoTypeAst
     `cast` <Co:6>,
     $dKnownTypeIn17_r3nqm)

-- RHS size: {terms: 4, types: 16, coercions: 24, joins: 0/0}
$dKnownMonotype1_r3nqo
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)18_r3nqn `cast` <Co:18>)
      dt2_r3nql
      $dKnownMonotype38_r3nqj

-- RHS size: {terms: 3, types: 4, coercions: 27, joins: 0/0}
$dKnownTypeIn14_r3nqp
  = $fKnownTypeInDefaultUniterm[]
      (lvl37_r3nqg `cast` <Co:20>) ($dContains2_r3npr `cast` <Co:7>)

-- RHS size: {terms: 3, types: 13, coercions: 7, joins: 0/0}
$d(%,%)15_r3nqq
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEDefaultUni[]_$ctoTypeAst1
     `cast` <Co:7>,
     $dKnownTypeIn14_r3nqp)

-- RHS size: {terms: 2, types: 7, coercions: 22, joins: 0/0}
$dKnownMonotype37_r3nqr
  = TypeSchemeResult @~ <Co:2> ($d(%,%)15_r3nqq `cast` <Co:20>)

-- RHS size: {terms: 4, types: 14, coercions: 24, joins: 0/0}
$dKnownMonotype2_r3nqs
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)18_r3nqn `cast` <Co:18>)
      dt2_r3nql
      $dKnownMonotype37_r3nqr

-- RHS size: {terms: 3, types: 5, coercions: 28, joins: 0/0}
dt3_r3nqt
  = $fKnownTypeInDefaultUniterm(,)
      (lvl37_r3nqg `cast` <Co:20>) ($dContains3_r3npu `cast` <Co:8>)

-- RHS size: {terms: 3, types: 15, coercions: 8, joins: 0/0}
dt4_r3nqu
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEDefaultUni(,)_$ctoTypeAst
     `cast` <Co:8>,
     dt3_r3nqt)

-- RHS size: {terms: 2, types: 8, coercions: 24, joins: 0/0}
dt5_r3nqv = TypeSchemeResult @~ <Co:2> (dt4_r3nqu `cast` <Co:22>)

-- RHS size: {terms: 33, types: 105, coercions: 38, joins: 0/0}
dt6_r3nqw
  = \ @ cause_XggU mayCause_iEmp val1_iEmq ->
      case val1_iEmq of {
        __DEFAULT -> Left (ErrorWithCause lvl38_r3nqk mayCause_iEmp);
        VCon val_a2W7W ->
          case val_a2W7W `cast` <Co:8> of { ValueOf uniAct_s3mKw x_s3mKx ->
          case $fGCompareTYPEDefaultUni_$cgeq
                 $WDefaultUniData (uniAct_s3mKw `cast` <Co:8>)
          of {
            Nothing ->
              Left
                (ErrorWithCause
                   (ReadKnownUnliftingError
                      (typeMismatchError
                         ($fGShowTYPEDefaultUni_$cshowsPrec `cast` <Co:6>)
                         ($WDefaultUniData `cast` <Co:9>)
                         uniAct_s3mKw))
                   mayCause_iEmp);
            Just ds_iEmC ->
              case ds_iEmC of { Refl co8_iEmF -> (Right x_s3mKx) `cast` <Co:7> }
          }
          }
      }

-- RHS size: {terms: 2, types: 3, coercions: 20, joins: 0/0}
$dKnownTypeIn15_r3nqx
  = $fKnownTypeInDefaultUnitermData (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 3, types: 11, coercions: 6, joins: 0/0}
$d(%,%)16_r3nqy
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEDefaultUniData_$ctoTypeAst
     `cast` <Co:6>,
     $dKnownTypeIn15_r3nqx)

-- RHS size: {terms: 4, types: 15, coercions: 24, joins: 0/0}
$dKnownMonotype36_r3nqz
  = TypeSchemeArrow
      @~ <Co:6> ($d(%,%)16_r3nqy `cast` <Co:18>) dt6_r3nqw dt5_r3nqv

-- RHS size: {terms: 4, types: 23, coercions: 28, joins: 0/0}
$dKnownMonotype3_r3nqA
  = TypeSchemeArrow
      @~ <Co:10>
      ($d(%,%)16_r3nqy `cast` <Co:18>)
      dt6_r3nqw
      $dKnownMonotype36_r3nqz

-- RHS size: {terms: 2, types: 3, coercions: 20, joins: 0/0}
$dKnownTypeIn3_r3nqB
  = $fKnownTypeInDefaultUnitermBool (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 3, types: 11, coercions: 6, joins: 0/0}
$d(%,%)5_r3nqC
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEDefaultUniBool_$ctoTypeAst
     `cast` <Co:6>,
     $dKnownTypeIn3_r3nqB)

-- RHS size: {terms: 2, types: 6, coercions: 20, joins: 0/0}
dt7_r3nqD
  = TypeSchemeResult @~ <Co:2> ($d(%,%)5_r3nqC `cast` <Co:18>)

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype35_r3nqE
  = TypeSchemeArrow
      @~ <Co:6> ($d(%,%)16_r3nqy `cast` <Co:18>) dt6_r3nqw dt7_r3nqD

-- RHS size: {terms: 4, types: 21, coercions: 28, joins: 0/0}
$dKnownMonotype4_r3nqF
  = TypeSchemeArrow
      @~ <Co:10>
      ($d(%,%)16_r3nqy `cast` <Co:18>)
      dt6_r3nqw
      $dKnownMonotype35_r3nqE

-- RHS size: {terms: 2, types: 3, coercions: 20, joins: 0/0}
$dKnownTypeIn5_r3nqG
  = $fKnownTypeInDefaultUnitermByteString
      (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 2, types: 5, coercions: 0, joins: 0/0}
dt8_r3nqH
  = $fKnownTypeInunivalEvaluationResult $dKnownTypeIn5_r3nqG

-- RHS size: {terms: 3, types: 13, coercions: 7, joins: 0/0}
dt9_r3nqI
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst
     `cast` <Co:7>,
     dt8_r3nqH)

-- RHS size: {terms: 2, types: 7, coercions: 22, joins: 0/0}
$dKnownMonotype34_r3nqJ
  = TypeSchemeResult @~ <Co:2> (dt9_r3nqI `cast` <Co:20>)

-- RHS size: {terms: 4, types: 14, coercions: 24, joins: 0/0}
$dKnownMonotype5_r3nqK
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)16_r3nqy `cast` <Co:18>)
      dt6_r3nqw
      $dKnownMonotype34_r3nqJ

-- RHS size: {terms: 2, types: 3, coercions: 20, joins: 0/0}
$dKnownTypeIn1_r3nqL
  = $fKnownTypeInDefaultUnitermInteger (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 2, types: 5, coercions: 0, joins: 0/0}
$dKnownTypeIn2_r3nqM
  = $fKnownTypeInunivalEvaluationResult $dKnownTypeIn1_r3nqL

-- RHS size: {terms: 3, types: 13, coercions: 7, joins: 0/0}
$d(%,%)4_r3nqN
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst6
     `cast` <Co:7>,
     $dKnownTypeIn2_r3nqM)

-- RHS size: {terms: 2, types: 7, coercions: 22, joins: 0/0}
$dKnownMonotype33_r3nqO
  = TypeSchemeResult @~ <Co:2> ($d(%,%)4_r3nqN `cast` <Co:20>)

-- RHS size: {terms: 4, types: 14, coercions: 24, joins: 0/0}
$dKnownMonotype6_r3nqP
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)16_r3nqy `cast` <Co:18>)
      dt6_r3nqw
      $dKnownMonotype33_r3nqO

-- RHS size: {terms: 2, types: 6, coercions: 0, joins: 0/0}
dt10_r3nqQ
  = $fKnownTypeInunivalEvaluationResult $dKnownTypeIn14_r3nqp

-- RHS size: {terms: 3, types: 15, coercions: 8, joins: 0/0}
dt11_r3nqR
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst1
     `cast` <Co:8>,
     dt10_r3nqQ)

-- RHS size: {terms: 2, types: 8, coercions: 24, joins: 0/0}
$dKnownMonotype32_r3nqS
  = TypeSchemeResult @~ <Co:2> (dt11_r3nqR `cast` <Co:22>)

-- RHS size: {terms: 4, types: 15, coercions: 24, joins: 0/0}
$dKnownMonotype7_r3nqT
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)16_r3nqy `cast` <Co:18>)
      dt6_r3nqw
      $dKnownMonotype32_r3nqS

-- RHS size: {terms: 2, types: 8, coercions: 0, joins: 0/0}
dt12_r3nqU
  = $fKnownTypeInunivalEvaluationResult $dKnownTypeIn16_r3nqh

-- RHS size: {terms: 3, types: 19, coercions: 10, joins: 0/0}
dt13_r3nqV
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst2
     `cast` <Co:10>,
     dt12_r3nqU)

-- RHS size: {terms: 2, types: 10, coercions: 28, joins: 0/0}
$dKnownMonotype31_r3nqW
  = TypeSchemeResult @~ <Co:2> (dt13_r3nqV `cast` <Co:26>)

-- RHS size: {terms: 4, types: 17, coercions: 24, joins: 0/0}
$dKnownMonotype8_r3nqX
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)16_r3nqy `cast` <Co:18>)
      dt6_r3nqw
      $dKnownMonotype31_r3nqW

-- RHS size: {terms: 3, types: 6, coercions: 29, joins: 0/0}
dt14_r3nqY
  = $fKnownTypeInDefaultUniterm(,)
      (lvl37_r3nqg `cast` <Co:20>) (lvl7_r3npG `cast` <Co:9>)

-- RHS size: {terms: 2, types: 8, coercions: 0, joins: 0/0}
dt15_r3nqZ = $fKnownTypeInunivalEvaluationResult dt14_r3nqY

-- RHS size: {terms: 3, types: 19, coercions: 10, joins: 0/0}
dt16_r3nr0
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst3
     `cast` <Co:10>,
     dt15_r3nqZ)

-- RHS size: {terms: 2, types: 10, coercions: 28, joins: 0/0}
$dKnownMonotype30_r3nr1
  = TypeSchemeResult @~ <Co:2> (dt16_r3nr0 `cast` <Co:26>)

-- RHS size: {terms: 4, types: 17, coercions: 24, joins: 0/0}
$dKnownMonotype9_r3nr2
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)16_r3nqy `cast` <Co:18>)
      dt6_r3nqw
      $dKnownMonotype30_r3nr1

-- RHS size: {terms: 2, types: 6, coercions: 20, joins: 0/0}
$dKnownMonotype29_r3nr3
  = TypeSchemeResult @~ <Co:2> ($d(%,%)16_r3nqy `cast` <Co:18>)

-- RHS size: {terms: 33, types: 105, coercions: 38, joins: 0/0}
dt17_r3nr4
  = \ @ cause_XfBw mayCause_iEmp val1_iEmq ->
      case val1_iEmq of {
        __DEFAULT -> Left (ErrorWithCause lvl38_r3nqk mayCause_iEmp);
        VCon val_a2W7W ->
          case val_a2W7W `cast` <Co:8> of { ValueOf uniAct_s3mMB x_s3mMC ->
          case $fGCompareTYPEDefaultUni_$cgeq
                 $WDefaultUniByteString (uniAct_s3mMB `cast` <Co:8>)
          of {
            Nothing ->
              Left
                (ErrorWithCause
                   (ReadKnownUnliftingError
                      (typeMismatchError
                         ($fGShowTYPEDefaultUni_$cshowsPrec `cast` <Co:6>)
                         ($WDefaultUniByteString `cast` <Co:9>)
                         uniAct_s3mMB))
                   mayCause_iEmp);
            Just ds_iEmC ->
              case ds_iEmC of { Refl co8_iEmF -> (Right x_s3mMC) `cast` <Co:7> }
          }
          }
      }

-- RHS size: {terms: 3, types: 11, coercions: 6, joins: 0/0}
$d(%,%)7_r3nr5
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEDefaultUniByteString_$ctoTypeAst
     `cast` <Co:6>,
     $dKnownTypeIn5_r3nqG)

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype10_r3nr6
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)7_r3nr5 `cast` <Co:18>)
      dt17_r3nr4
      $dKnownMonotype29_r3nr3

-- RHS size: {terms: 33, types: 105, coercions: 38, joins: 0/0}
dt18_r3nr7
  = \ @ cause_XfBm mayCause_iEmp val1_iEmq ->
      case val1_iEmq of {
        __DEFAULT -> Left (ErrorWithCause lvl38_r3nqk mayCause_iEmp);
        VCon val_a2W7W ->
          case val_a2W7W `cast` <Co:8> of { ValueOf uniAct_s3mMO x_s3mMP ->
          case $fGCompareTYPEDefaultUni_$cgeq
                 $WDefaultUniInteger (uniAct_s3mMO `cast` <Co:8>)
          of {
            Nothing ->
              Left
                (ErrorWithCause
                   (ReadKnownUnliftingError
                      (typeMismatchError
                         ($fGShowTYPEDefaultUni_$cshowsPrec `cast` <Co:6>)
                         ($WDefaultUniInteger `cast` <Co:9>)
                         uniAct_s3mMO))
                   mayCause_iEmp);
            Just ds_iEmC ->
              case ds_iEmC of { Refl co8_iEmF -> (Right x_s3mMP) `cast` <Co:7> }
          }
          }
      }

-- RHS size: {terms: 3, types: 11, coercions: 6, joins: 0/0}
$d(%,%)3_r3nr8
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEDefaultUniInteger_$ctoTypeAst
     `cast` <Co:6>,
     $dKnownTypeIn1_r3nqL)

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype28_r3nr9
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)3_r3nr8 `cast` <Co:18>)
      dt18_r3nr7
      $dKnownMonotype29_r3nr3

-- RHS size: {terms: 33, types: 129, coercions: 41, joins: 0/0}
dt19_r3nra
  = \ @ cause_XfBc mayCause_iEmp val1_iEmq ->
      case val1_iEmq of {
        __DEFAULT -> Left (ErrorWithCause lvl38_r3nqk mayCause_iEmp);
        VCon val_a2W7W ->
          case val_a2W7W `cast` <Co:8> of { ValueOf uniAct_s3mN1 x_s3mN2 ->
          case $fGCompareTYPEDefaultUni_$cgeq
                 $dContains6_r3npv (uniAct_s3mN1 `cast` <Co:8>)
          of {
            Nothing ->
              Left
                (ErrorWithCause
                   (ReadKnownUnliftingError
                      (typeMismatchError
                         ($fGShowTYPEDefaultUni_$cshowsPrec `cast` <Co:6>)
                         ($dContains6_r3npv `cast` <Co:12>)
                         uniAct_s3mN1))
                   mayCause_iEmp);
            Just ds_iEmC ->
              case ds_iEmC of { Refl co8_iEmF -> (Right x_s3mN2) `cast` <Co:7> }
          }
          }
      }

-- RHS size: {terms: 4, types: 19, coercions: 33, joins: 0/0}
$dKnownMonotype27_r3nrb
  = TypeSchemeArrow
      @~ <Co:9>
      ($d(%,%)17_r3nqi `cast` <Co:24>)
      dt19_r3nra
      $dKnownMonotype29_r3nr3

-- RHS size: {terms: 33, types: 113, coercions: 39, joins: 0/0}
dt20_r3nrc
  = \ @ cause_XfAQ mayCause_iEmp val1_iEmq ->
      case val1_iEmq of {
        __DEFAULT -> Left (ErrorWithCause lvl38_r3nqk mayCause_iEmp);
        VCon val_a2W7W ->
          case val_a2W7W `cast` <Co:8> of { ValueOf uniAct_s3mNc x_s3mNd ->
          case $fGCompareTYPEDefaultUni_$cgeq
                 $dContains2_r3npr (uniAct_s3mNc `cast` <Co:8>)
          of {
            Nothing ->
              Left
                (ErrorWithCause
                   (ReadKnownUnliftingError
                      (typeMismatchError
                         ($fGShowTYPEDefaultUni_$cshowsPrec `cast` <Co:6>)
                         ($dContains2_r3npr `cast` <Co:10>)
                         uniAct_s3mNc))
                   mayCause_iEmp);
            Just ds_iEmC ->
              case ds_iEmC of { Refl co8_iEmF -> (Right x_s3mNd) `cast` <Co:7> }
          }
          }
      }

-- RHS size: {terms: 4, types: 15, coercions: 27, joins: 0/0}
$dKnownMonotype26_r3nrd
  = TypeSchemeArrow
      @~ <Co:7>
      ($d(%,%)15_r3nqq `cast` <Co:20>)
      dt20_r3nrc
      $dKnownMonotype29_r3nr3

-- RHS size: {terms: 4, types: 23, coercions: 29, joins: 0/0}
$dKnownMonotype11_r3nre
  = TypeSchemeArrow
      @~ <Co:11>
      ($d(%,%)3_r3nr8 `cast` <Co:18>)
      dt18_r3nr7
      $dKnownMonotype26_r3nrd

-- RHS size: {terms: 2, types: 5, coercions: 0, joins: 0/0}
$dKnownTypeIn4_r3nrf
  = $fKnownTypeInunivalEvaluationResult $dKnownTypeIn3_r3nqB

-- RHS size: {terms: 3, types: 13, coercions: 7, joins: 0/0}
$d(%,%)6_r3nrg
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst5
     `cast` <Co:7>,
     $dKnownTypeIn4_r3nrf)

-- RHS size: {terms: 2, types: 7, coercions: 22, joins: 0/0}
dt21_r3nrh
  = TypeSchemeResult @~ <Co:2> ($d(%,%)6_r3nrg `cast` <Co:20>)

-- RHS size: {terms: 13, types: 30, coercions: 25, joins: 0/0}
dt22_r3nri
  = \ @ cause_XfAC mayCause_a2W7V ds_d36oj ->
      case ds_d36oj of {
        __DEFAULT ->
          (Left (ErrorWithCause lvl38_r3nqk mayCause_a2W7V)) `cast` <Co:13>;
        VCon val_a2W7W -> (Right val_a2W7W) `cast` <Co:12>
      }

-- RHS size: {terms: 2, types: 13, coercions: 20, joins: 0/0}
$dKnownTypeIn13_r3nrj
  = $fKnownTypeInunivalSomeConstant (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 3, types: 31, coercions: 16, joins: 0/0}
$d(%,%)14_r3nrk
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniSomeConstant_$ctoTypeAst1
     `cast` <Co:16>,
     $dKnownTypeIn13_r3nrj)

-- RHS size: {terms: 4, types: 34, coercions: 88, joins: 0/0}
$dKnownPolytype10_r3nrl
  = TypeSchemeArrow
      @~ <Co:16>
      ($d(%,%)14_r3nrk `cast` <Co:38>)
      (dt22_r3nri `cast` <Co:34>)
      dt21_r3nrh

-- RHS size: {terms: 5, types: 25, coercions: 18, joins: 0/0}
$dKnownPolytype1_r3nrm
  = TypeSchemeAll
      ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
      ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
      ($WSingType `cast` <Co:4>)
      $dKnownPolytype10_r3nrl

-- RHS size: {terms: 28, types: 112, coercions: 73, joins: 0/0}
headPlc_r3nrn
  = \ @ a_a118a ds1_d1cck ->
      case ds1_d1cck `cast` <Co:9> of { ValueOf uniListA_aY8t xs_aY8u ->
      case uniListA_aY8t of {
        __DEFAULT -> EvaluationFailure;
        DefaultUniApply @ k_apmg @ k1_apmh @ f_apmi @ a1_apmj co5_apmk
                        ds2_dqqc uniA_apjC ->
          case ds2_dqqc of {
            __DEFAULT -> EvaluationFailure;
            DefaultUniProtoList co6_apml ->
              case xs_aY8u `cast` <Co:32> of {
                [] -> EvaluationFailure;
                : x_aY8w ds3_d1ce4 ->
                  EvaluationSuccess
                    (case x_aY8w of dt32_Xi5x { __DEFAULT ->
                     (VCon
                        ((ValueOf (uniA_apjC `cast` <Co:10>) dt32_Xi5x) `cast` <Co:16>))
                     `cast` <Co:6>
                     })
              }
          }
      }
      }

-- RHS size: {terms: 28, types: 112, coercions: 89, joins: 0/0}
tailPlc_r3nro
  = \ @ a_a119E ds1_d1dHO ->
      case ds1_d1dHO `cast` <Co:9> of { ValueOf uniListA_aY8z xs_aY8A ->
      case uniListA_aY8z of wild2_X3E {
        __DEFAULT -> EvaluationFailure;
        DefaultUniApply @ k_apmg @ k1_apmh @ f_apmi @ a1_apmj co5_apmk
                        ds2_dqqc uniA_apjC ->
          case ds2_dqqc of {
            __DEFAULT -> EvaluationFailure;
            DefaultUniProtoList co6_apml ->
              case xs_aY8A `cast` <Co:32> of {
                [] -> EvaluationFailure;
                : ds3_d1dJy xs'_aY8B ->
                  EvaluationSuccess
                    (case xs'_aY8B `cast` <Co:36> of dt32_Xi5x { __DEFAULT ->
                     (VCon ((ValueOf wild2_X3E dt32_Xi5x) `cast` <Co:5>)) `cast` <Co:7>
                     })
              }
          }
      }
      }

-- RHS size: {terms: 36, types: 156, coercions: 113, joins: 0/0}
consPlc_r3nrp
  = \ @ a_a116p ds1_d19ng ds2_d19nh ->
      case ds1_d19ng `cast` <Co:8> of { ValueOf uniA_aY8m x_aY8n ->
      case ds2_d19nh `cast` <Co:9> of { ValueOf uniListA_aY8o xs_aY8p ->
      case uniListA_aY8o of wild3_X3E {
        __DEFAULT -> EvaluationFailure;
        DefaultUniApply @ k_apmg @ k1_apmh @ f_apmi @ a1_apmj co5_apmk
                        ds3_dqqc uniA1_apjC ->
          case ds3_dqqc of {
            __DEFAULT -> EvaluationFailure;
            DefaultUniProtoList co6_apml ->
              case $fGCompareTYPEDefaultUni_$cgeq uniA_aY8m uniA1_apjC of {
                Nothing -> EvaluationFailure;
                Just ds4_d19Hz ->
                  case ds4_d19Hz of { Refl co7_a1179 ->
                  EvaluationSuccess
                    ((VCon
                        ((ValueOf
                            wild3_X3E ((: x_aY8n (xs_aY8p `cast` <Co:39>)) `cast` <Co:45>))
                         `cast` <Co:5>))
                     `cast` <Co:7>)
                  }
              }
          }
      }
      }
      }

-- RHS size: {terms: 2, types: 12, coercions: 20, joins: 0/0}
dt23_r3nrq
  = $fKnownTypeInunivalSomeConstant (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 3, types: 29, coercions: 15, joins: 0/0}
dt24_r3nrr
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniSomeConstant_$ctoTypeAst
     `cast` <Co:15>,
     dt23_r3nrq)

-- RHS size: {terms: 32, types: 188, coercions: 266, joins: 0/0}
sndPlc_r3nrs
  = \ @ a_a113C @ b_a113D ds1_d16bc ->
      case ds1_d16bc `cast` <Co:10> of
      { ValueOf uniPairAB_aY8a xy_aY8b ->
      case uniPairAB_aY8a of {
        __DEFAULT -> EvaluationFailure;
        DefaultUniApply @ k_aplA @ k1_aplB @ f_aplC @ a1_aplD co5_aplE
                        ds2_dqq7 uniB_apjE ->
          case ds2_dqq7 of {
            __DEFAULT -> EvaluationFailure;
            DefaultUniApply @ k2_aplF @ k3_aplG @ f1_aplH @ a2_aplI co6_aplJ
                            ds3_dqq8 uniA_apjD ->
              case ds3_dqq8 of {
                __DEFAULT -> EvaluationFailure;
                DefaultUniProtoPair co7_aplK ->
                  case xy_aY8b `cast` <Co:181> of { (ds4_s3mOa, y_s3mOb) ->
                  EvaluationSuccess
                    (case y_s3mOb of dt32_Xi5x { __DEFAULT ->
                     (VCon
                        ((ValueOf (uniB_apjE `cast` <Co:44>) dt32_Xi5x) `cast` <Co:25>))
                     `cast` <Co:6>
                     })
                  }
              }
          }
      }
      }

-- RHS size: {terms: 2, types: 21, coercions: 20, joins: 0/0}
$dKnownTypeIn10_r3nrt
  = $fKnownTypeInunivalSomeConstant (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 3, types: 47, coercions: 24, joins: 0/0}
$d(%,%)11_r3nru
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniSomeConstant_$ctoTypeAst2
     `cast` <Co:24>,
     $dKnownTypeIn10_r3nrt)

-- RHS size: {terms: 32, types: 170, coercions: 228, joins: 0/0}
fstPlc_r3nrv
  = \ @ a_a1124 @ b_a1125 ds1_d14uZ ->
      case ds1_d14uZ `cast` <Co:10> of
      { ValueOf uniPairAB_aY84 xy_aY85 ->
      case uniPairAB_aY84 of {
        __DEFAULT -> EvaluationFailure;
        DefaultUniApply @ k_aplA @ k1_aplB @ f_aplC @ a1_aplD co5_aplE
                        ds2_dqq7 uniB_apjE ->
          case ds2_dqq7 of {
            __DEFAULT -> EvaluationFailure;
            DefaultUniApply @ k2_aplF @ k3_aplG @ f1_aplH @ a2_aplI co6_aplJ
                            ds3_dqq8 uniA_apjD ->
              case ds3_dqq8 of {
                __DEFAULT -> EvaluationFailure;
                DefaultUniProtoPair co7_aplK ->
                  case xy_aY85 `cast` <Co:181> of { (x_s3mOn, ds4_s3mOo) ->
                  EvaluationSuccess
                    (case x_s3mOn of dt32_Xi5x { __DEFAULT ->
                     (VCon
                        ((ValueOf (uniA_apjD `cast` <Co:15>) dt32_Xi5x) `cast` <Co:16>))
                     `cast` <Co:6>
                     })
                  }
              }
          }
      }
      }

-- RHS size: {terms: 2, types: 3, coercions: 20, joins: 0/0}
$dKnownTypeIn7_r3nrw
  = $fKnownTypeInDefaultUnitermText (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 3, types: 11, coercions: 6, joins: 0/0}
$d(%,%)9_r3nrx
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEDefaultUniText_$ctoTypeAst
     `cast` <Co:6>,
     $dKnownTypeIn7_r3nrw)

-- RHS size: {terms: 33, types: 105, coercions: 38, joins: 0/0}
$dKnownPolytype3_r3nry
  = \ @ cause_XfyZ mayCause_iEmp val1_iEmq ->
      case val1_iEmq of {
        __DEFAULT -> Left (ErrorWithCause lvl38_r3nqk mayCause_iEmp);
        VCon val_a2W7W ->
          case val_a2W7W `cast` <Co:8> of { ValueOf uniAct_s3mOB x_s3mOC ->
          case $fGCompareTYPEDefaultUni_$cgeq
                 $WDefaultUniString (uniAct_s3mOB `cast` <Co:8>)
          of {
            Nothing ->
              Left
                (ErrorWithCause
                   (ReadKnownUnliftingError
                      (typeMismatchError
                         ($fGShowTYPEDefaultUni_$cshowsPrec `cast` <Co:6>)
                         ($WDefaultUniString `cast` <Co:9>)
                         uniAct_s3mOB))
                   mayCause_iEmp);
            Just ds_iEmC ->
              case ds_iEmC of { Refl co8_iEmF -> (Right x_s3mOC) `cast` <Co:7> }
          }
          }
      }

-- RHS size: {terms: 2, types: 5, coercions: 0, joins: 0/0}
dt25_r3nrz
  = $fKnownTypeInunivalEvaluationResult $dKnownTypeIn7_r3nrw

-- RHS size: {terms: 3, types: 13, coercions: 7, joins: 0/0}
dt26_r3nrA
  = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniEvaluationResult_$ctoTypeAst4
     `cast` <Co:7>,
     dt25_r3nrz)

-- RHS size: {terms: 2, types: 7, coercions: 22, joins: 0/0}
$dKnownMonotype20_r3nrB
  = TypeSchemeResult @~ <Co:2> (dt26_r3nrA `cast` <Co:20>)

-- RHS size: {terms: 4, types: 14, coercions: 24, joins: 0/0}
$dKnownMonotype12_r3nrC
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)7_r3nr5 `cast` <Co:18>)
      dt17_r3nr4
      $dKnownMonotype20_r3nrB

-- RHS size: {terms: 2, types: 6, coercions: 20, joins: 0/0}
$dKnownMonotype19_r3nrD
  = TypeSchemeResult @~ <Co:2> ($d(%,%)7_r3nr5 `cast` <Co:18>)

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype13_r3nrE
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)9_r3nrx `cast` <Co:18>)
      $dKnownPolytype3_r3nry
      $dKnownMonotype19_r3nrD

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype18_r3nrF
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)9_r3nrx `cast` <Co:18>)
      $dKnownPolytype3_r3nry
      dt7_r3nqD

-- RHS size: {terms: 4, types: 21, coercions: 28, joins: 0/0}
$dKnownMonotype14_r3nrG
  = TypeSchemeArrow
      @~ <Co:10>
      ($d(%,%)9_r3nrx `cast` <Co:18>)
      $dKnownPolytype3_r3nry
      $dKnownMonotype18_r3nrF

-- RHS size: {terms: 2, types: 6, coercions: 20, joins: 0/0}
dt27_r3nrH
  = TypeSchemeResult @~ <Co:2> ($d(%,%)9_r3nrx `cast` <Co:18>)

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype17_r3nrI
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)9_r3nrx `cast` <Co:18>)
      $dKnownPolytype3_r3nry
      dt27_r3nrH

-- RHS size: {terms: 4, types: 21, coercions: 28, joins: 0/0}
$dKnownMonotype15_r3nrJ
  = TypeSchemeArrow
      @~ <Co:10>
      ($d(%,%)9_r3nrx `cast` <Co:18>)
      $dKnownPolytype3_r3nry
      $dKnownMonotype17_r3nrI

-- RHS size: {terms: 4, types: 14, coercions: 24, joins: 0/0}
dt28_r3nrK
  = TypeSchemeArrow
      @~ <Co:6> ($d(%,%)7_r3nr5 `cast` <Co:18>) dt17_r3nr4 dt21_r3nrh

-- RHS size: {terms: 4, types: 22, coercions: 28, joins: 0/0}
$dKnownMonotype16_r3nrL
  = TypeSchemeArrow
      @~ <Co:10> ($d(%,%)7_r3nr5 `cast` <Co:18>) dt17_r3nr4 dt28_r3nrK

-- RHS size: {terms: 4, types: 30, coercions: 32, joins: 0/0}
$dKnownMonotype22_r3nrM
  = TypeSchemeArrow
      @~ <Co:14>
      ($d(%,%)7_r3nr5 `cast` <Co:18>)
      dt17_r3nr4
      $dKnownMonotype16_r3nrL

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype23_r3nrN
  = TypeSchemeArrow
      @~ <Co:6> ($d(%,%)7_r3nr5 `cast` <Co:18>) dt17_r3nr4 dt7_r3nqD

-- RHS size: {terms: 4, types: 21, coercions: 28, joins: 0/0}
$dKnownMonotype24_r3nrO
  = TypeSchemeArrow
      @~ <Co:10>
      ($d(%,%)7_r3nr5 `cast` <Co:18>)
      dt17_r3nr4
      $dKnownMonotype23_r3nrN

-- RHS size: {terms: 58, types: 119, coercions: 40, joins: 0/0}
dt29_r3nrP
  = \ @ cause_Xgfi mayCause_Xpzo term1_Xpzq ->
      case term1_Xpzq of {
        __DEFAULT -> Left (ErrorWithCause lvl38_r3nqk mayCause_Xpzo);
        VCon val_a2W7W ->
          case val_a2W7W `cast` <Co:8> of { ValueOf uniAct_s3mQC x_s3mQD ->
          case $fGCompareTYPEDefaultUni_$cgeq
                 $WDefaultUniInteger (uniAct_s3mQC `cast` <Co:8>)
          of {
            Nothing ->
              Left
                (ErrorWithCause
                   (ReadKnownUnliftingError
                      (typeMismatchError
                         ($fGShowTYPEDefaultUni_$cshowsPrec `cast` <Co:6>)
                         ($WDefaultUniInteger `cast` <Co:9>)
                         uniAct_s3mQC))
                   mayCause_Xpzo);
            Just ds_iEk9 ->
              case ds_iEk9 of { Refl co6_iEkc ->
              case leInteger# lvl2_r3npA (x_s3mQD `cast` <Co:3>) of {
                __DEFAULT ->
                  Left (ErrorWithCause ReadKnownEvaluationFailure mayCause_Xpzo);
                1# ->
                  case leInteger# (x_s3mQD `cast` <Co:3>) lvl1_r3npz of {
                    __DEFAULT ->
                      Left (ErrorWithCause ReadKnownEvaluationFailure mayCause_Xpzo);
                    1# ->
                      Right
                        (case integerToInt (x_s3mQD `cast` <Co:3>) of wild7_iNda
                         { __DEFAULT ->
                         I# wild7_iNda
                         })
                  }
              }
              }
          }
          }
      }

-- RHS size: {terms: 2, types: 3, coercions: 20, joins: 0/0}
$dKnownTypeIn6_r3nrQ
  = $fKnownTypeInDefaultUnitermInt (lvl37_r3nqg `cast` <Co:20>)

-- RHS size: {terms: 3, types: 11, coercions: 6, joins: 0/0}
$d(%,%)8_r3nrR
  = ($fKnownTypeAstTYPEDefaultUniInt_$ctoTypeAst `cast` <Co:6>,
     $dKnownTypeIn6_r3nrQ)

-- RHS size: {terms: 4, types: 14, coercions: 24, joins: 0/0}
$dKnownMonotype25_r3nrS
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)8_r3nrR `cast` <Co:18>)
      dt29_r3nrP
      $dKnownMonotype33_r3nqO

-- RHS size: {terms: 4, types: 22, coercions: 28, joins: 0/0}
$dKnownMonotype41_r3nrT
  = TypeSchemeArrow
      @~ <Co:10>
      ($d(%,%)7_r3nr5 `cast` <Co:18>)
      dt17_r3nr4
      $dKnownMonotype25_r3nrS

-- RHS size: {terms: 2, types: 6, coercions: 20, joins: 0/0}
$dKnownMonotype42_r3nrU
  = TypeSchemeResult @~ <Co:2> ($d(%,%)8_r3nrR `cast` <Co:18>)

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype43_r3nrV
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)7_r3nr5 `cast` <Co:18>)
      dt17_r3nr4
      $dKnownMonotype42_r3nrU

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
dt30_r3nrW
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)7_r3nr5 `cast` <Co:18>)
      dt17_r3nr4
      $dKnownMonotype19_r3nrD

-- RHS size: {terms: 4, types: 21, coercions: 28, joins: 0/0}
$dKnownMonotype44_r3nrX
  = TypeSchemeArrow
      @~ <Co:10> ($d(%,%)8_r3nrR `cast` <Co:18>) dt29_r3nrP dt30_r3nrW

-- RHS size: {terms: 4, types: 29, coercions: 32, joins: 0/0}
$dKnownMonotype45_r3nrY
  = TypeSchemeArrow
      @~ <Co:14>
      ($d(%,%)8_r3nrR `cast` <Co:18>)
      dt29_r3nrP
      $dKnownMonotype44_r3nrX

-- RHS size: {terms: 4, types: 21, coercions: 28, joins: 0/0}
$dKnownMonotype46_r3nrZ
  = TypeSchemeArrow
      @~ <Co:10> ($d(%,%)3_r3nr8 `cast` <Co:18>) dt18_r3nr7 dt30_r3nrW

-- RHS size: {terms: 4, types: 21, coercions: 28, joins: 0/0}
$dKnownMonotype47_r3ns0
  = TypeSchemeArrow
      @~ <Co:10> ($d(%,%)7_r3nr5 `cast` <Co:18>) dt17_r3nr4 dt30_r3nrW

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype48_r3ns1
  = TypeSchemeArrow
      @~ <Co:6> ($d(%,%)3_r3nr8 `cast` <Co:18>) dt18_r3nr7 dt7_r3nqD

-- RHS size: {terms: 4, types: 21, coercions: 28, joins: 0/0}
$dKnownMonotype49_r3ns2
  = TypeSchemeArrow
      @~ <Co:10>
      ($d(%,%)3_r3nr8 `cast` <Co:18>)
      dt18_r3nr7
      $dKnownMonotype48_r3ns1

-- RHS size: {terms: 4, types: 14, coercions: 24, joins: 0/0}
$dKnownMonotype50_r3ns3
  = TypeSchemeArrow
      @~ <Co:6>
      ($d(%,%)3_r3nr8 `cast` <Co:18>)
      dt18_r3nr7
      $dKnownMonotype33_r3nqO

-- RHS size: {terms: 4, types: 22, coercions: 28, joins: 0/0}
$dKnownMonotype51_r3ns4
  = TypeSchemeArrow
      @~ <Co:10>
      ($d(%,%)3_r3nr8 `cast` <Co:18>)
      dt18_r3nr7
      $dKnownMonotype50_r3ns3

-- RHS size: {terms: 2, types: 6, coercions: 20, joins: 0/0}
dt31_r3ns5
  = TypeSchemeResult @~ <Co:2> ($d(%,%)3_r3nr8 `cast` <Co:18>)

-- RHS size: {terms: 4, types: 13, coercions: 24, joins: 0/0}
$dKnownMonotype52_r3ns6
  = TypeSchemeArrow
      @~ <Co:6> ($d(%,%)3_r3nr8 `cast` <Co:18>) dt18_r3nr7 dt31_r3ns5

-- RHS size: {terms: 4, types: 21, coercions: 28, joins: 0/0}
$dKnownMonotype53_r3ns7
  = TypeSchemeArrow
      @~ <Co:10>
      ($d(%,%)3_r3nr8 `cast` <Co:18>)
      dt18_r3nr7
      $dKnownMonotype52_r3ns6

-- RHS size: {terms: 33, types: 105, coercions: 38, joins: 0/0}
$dKnownPolytype2_r3ns8
  = \ @ cause_XfCm mayCause_iEmp val1_iEmq ->
      case val1_iEmq of {
        __DEFAULT -> Left (ErrorWithCause lvl38_r3nqk mayCause_iEmp);
        VCon val_a2W7W ->
          case val_a2W7W `cast` <Co:8> of { ValueOf uniAct_s3mTf x_s3mTg ->
          case $fGCompareTYPEDefaultUni_$cgeq
                 $WDefaultUniBool (uniAct_s3mTf `cast` <Co:8>)
          of {
            Nothing ->
              Left
                (ErrorWithCause
                   (ReadKnownUnliftingError
                      (typeMismatchError
                         ($fGShowTYPEDefaultUni_$cshowsPrec `cast` <Co:6>)
                         ($WDefaultUniBool `cast` <Co:9>)
                         uniAct_s3mTf))
                   mayCause_iEmp);
            Just ds_iEmC ->
              case ds_iEmC of { Refl co7_iEmF -> (Right x_s3mTg) `cast` <Co:7> }
          }
          }
      }

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl39_r3ns9 = typeSchemeToRuntimeScheme $dKnownMonotype53_r3ns7

-- RHS size: {terms: 2, types: 15, coercions: 0, joins: 0/0}
lvl40_r3nsa = typeSchemeToRuntimeScheme $dKnownMonotype51_r3ns4

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl41_r3nsb = typeSchemeToRuntimeScheme $dKnownMonotype49_r3ns2

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl42_r3nsc = typeSchemeToRuntimeScheme $dKnownMonotype47_r3ns0

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl43_r3nsd = typeSchemeToRuntimeScheme $dKnownMonotype46_r3nrZ

-- RHS size: {terms: 2, types: 18, coercions: 0, joins: 0/0}
lvl44_r3nse = typeSchemeToRuntimeScheme $dKnownMonotype45_r3nrY

-- RHS size: {terms: 2, types: 10, coercions: 0, joins: 0/0}
lvl45_r3nsf = typeSchemeToRuntimeScheme $dKnownMonotype43_r3nrV

-- RHS size: {terms: 2, types: 15, coercions: 0, joins: 0/0}
lvl46_r3nsg = typeSchemeToRuntimeScheme $dKnownMonotype41_r3nrT

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl47_r3nsh = typeSchemeToRuntimeScheme $dKnownMonotype24_r3nrO

-- RHS size: {terms: 2, types: 10, coercions: 0, joins: 0/0}
lvl48_r3nsi = typeSchemeToRuntimeScheme dt30_r3nrW

-- RHS size: {terms: 2, types: 19, coercions: 0, joins: 0/0}
lvl49_r3nsj = typeSchemeToRuntimeScheme $dKnownMonotype22_r3nrM

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl50_r3nsk = typeSchemeToRuntimeScheme $dKnownMonotype15_r3nrJ

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl51_r3nsl = typeSchemeToRuntimeScheme $dKnownMonotype14_r3nrG

-- RHS size: {terms: 2, types: 10, coercions: 0, joins: 0/0}
lvl52_r3nsm = typeSchemeToRuntimeScheme $dKnownMonotype13_r3nrE

-- RHS size: {terms: 2, types: 11, coercions: 0, joins: 0/0}
lvl53_r3nsn = typeSchemeToRuntimeScheme $dKnownMonotype12_r3nrC

-- RHS size: {terms: 2, types: 21, coercions: 0, joins: 0/0}
lvl54_r3nso = typeSchemeToRuntimeScheme $dKnownPolytype1_r3nrm

-- RHS size: {terms: 2, types: 15, coercions: 0, joins: 0/0}
lvl55_r3nsp = typeSchemeToRuntimeScheme $dKnownMonotype11_r3nre

-- RHS size: {terms: 2, types: 13, coercions: 0, joins: 0/0}
lvl56_r3nsq = typeSchemeToRuntimeScheme $dKnownMonotype27_r3nrb

-- RHS size: {terms: 2, types: 11, coercions: 0, joins: 0/0}
lvl57_r3nsr = typeSchemeToRuntimeScheme $dKnownMonotype26_r3nrd

-- RHS size: {terms: 2, types: 10, coercions: 0, joins: 0/0}
lvl58_r3nss = typeSchemeToRuntimeScheme $dKnownMonotype28_r3nr9

-- RHS size: {terms: 2, types: 10, coercions: 0, joins: 0/0}
lvl59_r3nst = typeSchemeToRuntimeScheme $dKnownMonotype10_r3nr6

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl60_r3nsu = typeSchemeToRuntimeScheme $dKnownMonotype9_r3nr2

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl61_r3nsv = typeSchemeToRuntimeScheme $dKnownMonotype8_r3nqX

-- RHS size: {terms: 2, types: 12, coercions: 0, joins: 0/0}
lvl62_r3nsw = typeSchemeToRuntimeScheme $dKnownMonotype7_r3nqT

-- RHS size: {terms: 2, types: 11, coercions: 0, joins: 0/0}
lvl63_r3nsx = typeSchemeToRuntimeScheme $dKnownMonotype6_r3nqP

-- RHS size: {terms: 2, types: 11, coercions: 0, joins: 0/0}
lvl64_r3nsy = typeSchemeToRuntimeScheme $dKnownMonotype5_r3nqK

-- RHS size: {terms: 2, types: 14, coercions: 0, joins: 0/0}
lvl65_r3nsz = typeSchemeToRuntimeScheme $dKnownMonotype4_r3nqF

-- RHS size: {terms: 2, types: 16, coercions: 0, joins: 0/0}
lvl66_r3nsA = typeSchemeToRuntimeScheme $dKnownMonotype3_r3nqA

-- RHS size: {terms: 2, types: 11, coercions: 0, joins: 0/0}
lvl67_r3nsB = typeSchemeToRuntimeScheme $dKnownMonotype2_r3nqs

-- RHS size: {terms: 2, types: 13, coercions: 0, joins: 0/0}
lvl68_r3nsC = typeSchemeToRuntimeScheme $dKnownMonotype1_r3nqo

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
lvl69_r3nsD
  = $fEnumDefaultFun_$cenumFromTo AddInteger MkNilPairData

-- RHS size: {terms: 880,
              types: 6,651,
              coercions: 8,262,
              joins: 2/82}
$w$ctoBuiltinsRuntime
  = \ @ uni_s3mjc ww_s3mjh w_s3mje ->
      case runRW#
             (\ s1#_i2CtT ->
                case newArray# 51# arrEleBottom s1#_i2CtT of
                { (# ipv_i2Cu1, ipv1_i2Cu2 #) ->
                let { $d~_a3kve = Eq# @~ <Co:1> } in
                let {
                  $dKnownTypeIn8_s3l1C
                    = $fKnownTypeInunivalOpaque ($d~_a3kve `cast` <Co:14>) } in
                let {
                  $dKnownPolytype4_s3mnB
                    = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniOpaque_$ctoTypeAst2
                       `cast` <Co:17>,
                       $dKnownTypeIn8_s3l1C) } in
                let {
                  $dKnownMonotype_s3mps
                    = TypeSchemeResult
                        @~ <Co:2> ($dKnownPolytype4_s3mnB `cast` <Co:40>) } in
                let {
                  $dKnownPolytype5_s3mpA
                    = TypeSchemeArrow
                        @~ <Co:17>
                        ($dKnownPolytype4_s3mnB `cast` <Co:40>)
                        ((\ @ cause_Xgpl -> lvl_r3npw) `cast` <Co:35>)
                        $dKnownMonotype_s3mps } in
                let {
                  $dKnownPolytype6_s3mpK
                    = TypeSchemeArrow
                        @~ <Co:32>
                        ($dKnownPolytype4_s3mnB `cast` <Co:40>)
                        ((\ @ cause_Xgpl -> lvl_r3npw) `cast` <Co:35>)
                        $dKnownPolytype5_s3mpA } in
                let {
                  lvl70_s3mUJ
                    = typeSchemeToRuntimeScheme
                        ((TypeSchemeAll
                            ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                            ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                            ($WSingType `cast` <Co:4>)
                            (TypeSchemeArrow
                               @~ <Co:81>
                               ($d(%,%)16_r3nqy `cast` <Co:18>)
                               dt6_r3nqw
                               (TypeSchemeArrow
                                  @~ <Co:77>
                                  ($dKnownPolytype4_s3mnB `cast` <Co:40>)
                                  ((\ @ cause_Xgpl -> lvl_r3npw) `cast` <Co:35>)
                                  (TypeSchemeArrow
                                     @~ <Co:62>
                                     ($dKnownPolytype4_s3mnB `cast` <Co:40>)
                                     ((\ @ cause_Xgpl -> lvl_r3npw) `cast` <Co:35>)
                                     (TypeSchemeArrow
                                        @~ <Co:47>
                                        ($dKnownPolytype4_s3mnB `cast` <Co:40>)
                                        ((\ @ cause_Xgpl -> lvl_r3npw) `cast` <Co:35>)
                                        $dKnownPolytype6_s3mpK)))))
                         `cast` <Co:364>) } in
                let {
                  lvl71_s3mUp
                    = typeSchemeToRuntimeScheme
                        ((TypeSchemeAll
                            ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                            ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                            ($WSingType `cast` <Co:4>)
                            (TypeSchemeArrow
                               @~ <Co:36>
                               ($d(%,%)5_r3nqC `cast` <Co:18>)
                               $dKnownPolytype2_r3ns8
                               $dKnownPolytype6_s3mpK))
                         `cast` <Co:130>) } in
                let {
                  lvl72_s3mUr
                    = typeSchemeToRuntimeScheme
                        ((TypeSchemeAll
                            ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                            ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                            ($WSingType `cast` <Co:4>)
                            (TypeSchemeArrow
                               @~ <Co:21>
                               ($d(%,%)18_r3nqn `cast` <Co:18>)
                               dt2_r3nql
                               $dKnownPolytype5_s3mpA))
                         `cast` <Co:76>) } in
                let {
                  lvl73_s3mUt
                    = typeSchemeToRuntimeScheme
                        (TypeSchemeAll
                           ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                           ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                           ($WSingType `cast` <Co:4>)
                           (TypeSchemeArrow
                              @~ <Co:21>
                              ($d(%,%)9_r3nrx `cast` <Co:18>)
                              $dKnownPolytype3_r3nry
                              (TypeSchemeArrow
                                 @~ <Co:17>
                                 ($dKnownPolytype4_s3mnB `cast` <Co:40>)
                                 ((\ @ cause_Xgpl -> lvl_r3npw) `cast` <Co:35>)
                                 (TypeSchemeResult
                                    @~ <Co:2>
                                    ((lvl3_r3npB `cast` <Co:18>,
                                      $fKnownTypeInunivalEmitter $dKnownTypeIn8_s3l1C)
                                     `cast` <Co:42>))))) } in
                let {
                  $dKnownTypeIn9_s3l1B
                    = $fKnownTypeInunivalEvaluationResult $dKnownTypeIn8_s3l1C } in
                let {
                  $d(%,%)10_s3l1A
                    = (poly_$dKnownTypeAst1_r3npy `cast` <Co:18>,
                       $dKnownTypeIn9_s3l1B) } in
                let {
                  dt32_s3lRB
                    = TypeSchemeResult @~ <Co:2> ($d(%,%)10_s3l1A `cast` <Co:42>) } in
                let {
                  lvl74_s3mUv
                    = typeSchemeToRuntimeScheme
                        (TypeSchemeAll
                           ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                           ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                           ($WSingType `cast` <Co:4>)
                           (TypeSchemeAll
                              ($s$WTypeSchemeAll_$dKnownSymbol1 `cast` <Co:7>)
                              ($s$WTypeSchemeAll_$dKnownNat1 `cast` <Co:7>)
                              ($WSingType `cast` <Co:4>)
                              (TypeSchemeArrow
                                 @~ <Co:24>
                                 ($d(%,%)11_r3nru `cast` <Co:54>)
                                 (dt22_r3nri `cast` <Co:42>)
                                 dt32_s3lRB))) } in
                let {
                  $dKnownTypeIn11_s3l1u
                    = $fKnownTypeInunivalOpaque ($d~_a3kve `cast` <Co:14>) } in
                let {
                  $dKnownTypeIn12_s3l1t
                    = $fKnownTypeInunivalEvaluationResult $dKnownTypeIn11_s3l1u } in
                let {
                  $d(%,%)12_s3l1s
                    = (poly_$dKnownTypeAst_r3npx `cast` <Co:18>,
                       $dKnownTypeIn12_s3l1t) } in
                let {
                  $dKnownPolytype7_s3mn3
                    = TypeSchemeResult @~ <Co:2> ($d(%,%)12_s3l1s `cast` <Co:42>) } in
                let {
                  lvl75_s3mUx
                    = typeSchemeToRuntimeScheme
                        (TypeSchemeAll
                           ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                           ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                           ($WSingType `cast` <Co:4>)
                           (TypeSchemeAll
                              ($s$WTypeSchemeAll_$dKnownSymbol1 `cast` <Co:7>)
                              ($s$WTypeSchemeAll_$dKnownNat1 `cast` <Co:7>)
                              ($WSingType `cast` <Co:4>)
                              (TypeSchemeArrow
                                 @~ <Co:24>
                                 ($d(%,%)11_r3nru `cast` <Co:54>)
                                 (dt22_r3nri `cast` <Co:42>)
                                 $dKnownPolytype7_s3mn3))) } in
                let {
                  lvl76_s3mUz
                    = let {
                        $d(%,%)13_s3l1p
                          = ($fToBuiltinMeaninguniDefaultFun_$s$fKnownTypeAstTYPEuniOpaque_$ctoTypeAst1
                             `cast` <Co:17>,
                             $dKnownTypeIn11_s3l1u) } in
                      typeSchemeToRuntimeScheme
                        (TypeSchemeAll
                           ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                           ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                           ($WSingType `cast` <Co:4>)
                           (TypeSchemeAll
                              ($s$WTypeSchemeAll_$dKnownSymbol1 `cast` <Co:7>)
                              ($s$WTypeSchemeAll_$dKnownNat1 `cast` <Co:7>)
                              ($WSingType `cast` <Co:4>)
                              (TypeSchemeArrow
                                 @~ <Co:46>
                                 ($d(%,%)14_r3nrk `cast` <Co:38>)
                                 (dt22_r3nri `cast` <Co:34>)
                                 (TypeSchemeArrow
                                    @~ <Co:32>
                                    ($d(%,%)13_s3l1p `cast` <Co:40>)
                                    ((\ @ cause_Xgp0 -> lvl4_r3npC) `cast` <Co:35>)
                                    (TypeSchemeArrow
                                       @~ <Co:17>
                                       ($d(%,%)13_s3l1p `cast` <Co:40>)
                                       ((\ @ cause_Xgp0 -> lvl4_r3npC) `cast` <Co:35>)
                                       $dKnownPolytype7_s3mn3))))) } in
                let {
                  dt33_s3lQY
                    = $fKnownTypeInunivalOpaque ($d~_a3kve `cast` <Co:14>) } in
                let {
                  dt34_s3lQZ = $fKnownTypeInunivalEvaluationResult dt33_s3lQY } in
                let { dt35_s3lR0 = (lvl5_r3npD `cast` <Co:19>, dt34_s3lQZ) } in
                let {
                  $dKnownMonotype54_s3lR1
                    = TypeSchemeResult @~ <Co:2> (dt35_s3lR0 `cast` <Co:44>) } in
                let {
                  $dKnownPolytype8_s3lRn
                    = TypeSchemeArrow
                        @~ <Co:16>
                        ($d(%,%)14_r3nrk `cast` <Co:38>)
                        (dt22_r3nri `cast` <Co:34>)
                        $dKnownMonotype54_s3lR1 } in
                let {
                  lvl77_s3mUB
                    = typeSchemeToRuntimeScheme
                        (TypeSchemeAll
                           ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                           ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                           ($WSingType `cast` <Co:4>)
                           (TypeSchemeArrow
                              @~ <Co:29>
                              (dt24_r3nrr `cast` <Co:36>)
                              (dt22_r3nri `cast` <Co:33>)
                              $dKnownPolytype8_s3lRn)) } in
                let {
                  lvl78_s3mUF
                    = typeSchemeToRuntimeScheme
                        (TypeSchemeAll
                           ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                           ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                           ($WSingType `cast` <Co:4>)
                           $dKnownPolytype8_s3lRn) } in
                let {
                  lvl79_s3mUD
                    = typeSchemeToRuntimeScheme
                        (TypeSchemeAll
                           ($s$WTypeSchemeAll_$dKnownSymbol `cast` <Co:7>)
                           ($s$WTypeSchemeAll_$dKnownNat `cast` <Co:7>)
                           ($WSingType `cast` <Co:4>)
                           (TypeSchemeArrow
                              @~ <Co:16>
                              ($d(%,%)14_r3nrk `cast` <Co:38>)
                              (dt22_r3nri `cast` <Co:34>)
                              dt32_s3lRB)) } in
                let {
                  lvl80_s3mVc
                    = runCostingFunOneArgument
                        (paramMkNilPairData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl81_s3mVa
                    = runCostingFunOneArgument
                        (paramMkNilData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl82_s3mV8
                    = runCostingFunTwoArguments
                        (paramMkPairData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl83_s3mV6
                    = runCostingFunTwoArguments
                        (paramEqualsData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl84_s3mV4
                    = runCostingFunOneArgument
                        (paramUnBData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl85_s3mV2
                    = runCostingFunOneArgument
                        (paramUnIData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl86_s3mV0
                    = runCostingFunOneArgument
                        (paramUnListData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl87_s3mUY
                    = runCostingFunOneArgument
                        (paramUnMapData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl88_s3mUW
                    = runCostingFunOneArgument
                        (paramUnConstrData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl89_s3mUU
                    = runCostingFunOneArgument
                        (paramBData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl90_s3mUS
                    = runCostingFunOneArgument
                        (paramIData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl91_s3mUQ
                    = runCostingFunOneArgument
                        (paramListData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl92_s3mUO
                    = runCostingFunOneArgument
                        (paramMapData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl93_s3mUM
                    = runCostingFunTwoArguments
                        (paramConstrData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl94_s3mUK
                    = runCostingFunSixArguments
                        (paramChooseData (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl95_s3mUI
                    = runCostingFunOneArgument
                        (paramNullList (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl96_s3mUG
                    = runCostingFunOneArgument
                        (paramTailList (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl97_s3mUE
                    = runCostingFunOneArgument
                        (paramHeadList (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl98_s3mUC
                    = runCostingFunTwoArguments
                        (paramMkCons (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl99_s3mUA
                    = runCostingFunThreeArguments
                        (paramChooseList (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl100_s3mUy
                    = runCostingFunOneArgument
                        (paramSndPair (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl101_s3mUw
                    = runCostingFunOneArgument
                        (paramFstPair (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl102_s3mUu
                    = runCostingFunTwoArguments
                        (paramTrace (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl103_s3mUs
                    = runCostingFunTwoArguments
                        (paramChooseUnit (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl104_s3mUq
                    = runCostingFunThreeArguments
                        (paramIfThenElse (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl105_s3mUo
                    = runCostingFunOneArgument
                        (paramDecodeUtf8 (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl106_s3mUm
                    = runCostingFunOneArgument
                        (paramEncodeUtf8 (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl107_s3mUk
                    = runCostingFunTwoArguments
                        (paramEqualsString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl108_s3mUi
                    = runCostingFunTwoArguments
                        (paramAppendString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl109_s3mUg
                    = runCostingFunThreeArguments
                        (paramVerifySignature (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl110_s3mUe
                    = runCostingFunOneArgument
                        (paramBlake2b (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl111_s3mUc
                    = runCostingFunOneArgument
                        (paramSha3_256 (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl112_s3mUa
                    = runCostingFunOneArgument
                        (paramSha2_256 (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl113_s3mU8
                    = runCostingFunTwoArguments
                        (paramLessThanEqualsByteString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl114_s3mU6
                    = runCostingFunTwoArguments
                        (paramLessThanByteString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl115_s3mU4
                    = runCostingFunTwoArguments
                        (paramEqualsByteString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl116_s3mU2
                    = runCostingFunTwoArguments
                        (paramIndexByteString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl117_s3mU0
                    = runCostingFunOneArgument
                        (paramLengthOfByteString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl118_s3mTY
                    = runCostingFunThreeArguments
                        (paramSliceByteString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl119_s3mTW
                    = runCostingFunTwoArguments
                        (paramConsByteString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl120_s3mTU
                    = runCostingFunTwoArguments
                        (paramAppendByteString (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl121_s3mTS
                    = runCostingFunTwoArguments
                        (paramLessThanEqualsInteger (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl122_s3mTQ
                    = runCostingFunTwoArguments
                        (paramLessThanInteger (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl123_s3mTO
                    = runCostingFunTwoArguments
                        (paramEqualsInteger (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl124_s3mTM
                    = runCostingFunTwoArguments
                        (paramModInteger (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl125_s3mTK
                    = runCostingFunTwoArguments
                        (paramRemainderInteger (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl126_s3mTI
                    = runCostingFunTwoArguments
                        (paramQuotientInteger (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl127_s3mTG
                    = runCostingFunTwoArguments
                        (paramDivideInteger (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl128_s3mTE
                    = runCostingFunTwoArguments
                        (paramMultiplyInteger (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl129_s3mTC
                    = runCostingFunTwoArguments
                        (paramSubtractInteger (w_s3mje `cast` <Co:3>)) } in
                let {
                  lvl130_s3mTA
                    = runCostingFunTwoArguments
                        (paramAddInteger (w_s3mje `cast` <Co:3>)) } in
                join {
                  $j_i2Cu5 wild4_i2Cu6
                    = case unsafeFreezeArray# ipv1_i2Cu2 wild4_i2Cu6 of
                      { (# ipv2_i2Cu8, ipv3_i2Cu9 #) ->
                      (# ipv2_i2Cu8, Array AddInteger MkNilPairData 51# ipv3_i2Cu9 #)
                      } } in
                joinrec {
                  go1_i2Cud ds_i2Cue eta_i2Cuf eta1_i2Cug
                    = case ds_i2Cue of {
                        [] -> jump $j_i2Cu5 eta1_i2Cug;
                        : y_i2Cuj ys_i2Cuk ->
                          case writeArray#
                                 ipv1_i2Cu2
                                 eta_i2Cuf
                                 (case y_i2Cuj of {
                                    AddInteger ->
                                      case lvl39_r3ns9 of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (plusInteger `cast` <Co:28>)
                                        (lvl130_s3mTA `cast` <Co:25>)
                                      };
                                    SubtractInteger ->
                                      case lvl39_r3ns9 of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (minusInteger `cast` <Co:28>)
                                        (lvl129_s3mTC `cast` <Co:25>)
                                      };
                                    MultiplyInteger ->
                                      case lvl39_r3ns9 of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (timesInteger `cast` <Co:28>)
                                        (lvl128_s3mTE `cast` <Co:25>)
                                      };
                                    DivideInteger ->
                                      case lvl40_r3nsa of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl8_r3npH `cast` <Co:31>)
                                        (lvl127_s3mTG `cast` <Co:25>)
                                      };
                                    QuotientInteger ->
                                      case lvl40_r3nsa of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl9_r3npI `cast` <Co:31>)
                                        (lvl126_s3mTI `cast` <Co:25>)
                                      };
                                    RemainderInteger ->
                                      case lvl40_r3nsa of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl10_r3npJ `cast` <Co:31>)
                                        (lvl125_s3mTK `cast` <Co:25>)
                                      };
                                    ModInteger ->
                                      case lvl40_r3nsa of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl11_r3npK `cast` <Co:31>)
                                        (lvl124_s3mTM `cast` <Co:25>)
                                      };
                                    EqualsInteger ->
                                      case lvl41_r3nsb of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (eqInteger `cast` <Co:28>)
                                        (lvl123_s3mTO `cast` <Co:25>)
                                      };
                                    LessThanInteger ->
                                      case lvl41_r3nsb of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (ltInteger `cast` <Co:28>)
                                        (lvl122_s3mTQ `cast` <Co:25>)
                                      };
                                    LessThanEqualsInteger ->
                                      case lvl41_r3nsb of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (leInteger `cast` <Co:28>)
                                        (lvl121_s3mTS `cast` <Co:25>)
                                      };
                                    AppendByteString ->
                                      case lvl42_r3nsc of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl12_r3npL `cast` <Co:28>)
                                        (lvl120_s3mTU `cast` <Co:25>)
                                      };
                                    ConsByteString ->
                                      case lvl43_r3nsd of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl13_r3npN `cast` <Co:28>)
                                        (lvl119_s3mTW `cast` <Co:25>)
                                      };
                                    SliceByteString ->
                                      case lvl44_r3nse of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl15_r3npP `cast` <Co:46>)
                                        (lvl118_s3mTY `cast` <Co:42>)
                                      };
                                    LengthOfByteString ->
                                      case lvl45_r3nsf of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (length `cast` <Co:14>)
                                        (lvl117_s3mU0 `cast` <Co:12>)
                                      };
                                    IndexByteString ->
                                      case lvl46_r3nsg of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl21_r3npY `cast` <Co:31>)
                                        (lvl116_s3mU2 `cast` <Co:25>)
                                      };
                                    EqualsByteString ->
                                      case lvl47_r3nsh of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV (eq `cast` <Co:28>) (lvl115_s3mU4 `cast` <Co:25>)
                                      };
                                    LessThanByteString ->
                                      case lvl47_r3nsh of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        ($fOrdByteString_$c< `cast` <Co:28>)
                                        (lvl114_s3mU6 `cast` <Co:25>)
                                      };
                                    LessThanEqualsByteString ->
                                      case lvl47_r3nsh of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        ($fOrdByteString_$c<= `cast` <Co:28>)
                                        (lvl113_s3mU8 `cast` <Co:25>)
                                      };
                                    Sha2_256 ->
                                      case lvl48_r3nsi of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (sha256_libsodium `cast` <Co:14>)
                                        (lvl112_s3mUa `cast` <Co:12>)
                                      };
                                    Sha3_256 ->
                                      case lvl48_r3nsi of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        ($w$cdigest `cast` <Co:14>)
                                        (lvl111_s3mUc `cast` <Co:12>)
                                      };
                                    Blake2b_256 ->
                                      case lvl48_r3nsi of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (blake2b `cast` <Co:14>)
                                        (lvl110_s3mUe `cast` <Co:12>)
                                      };
                                    VerifySignature ->
                                      case lvl49_r3nsj of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        ($sverifySignature `cast` <Co:50>)
                                        (lvl109_s3mUg `cast` <Co:42>)
                                      };
                                    AppendString ->
                                      case lvl50_r3nsk of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (append `cast` <Co:28>)
                                        (lvl108_s3mUi `cast` <Co:25>)
                                      };
                                    EqualsString ->
                                      case lvl51_r3nsl of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        ($fEqText_$c== `cast` <Co:28>)
                                        (lvl107_s3mUk `cast` <Co:25>)
                                      };
                                    EncodeUtf8 ->
                                      case lvl52_r3nsm of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (encodeUtf8 `cast` <Co:14>)
                                        (lvl106_s3mUm `cast` <Co:12>)
                                      };
                                    DecodeUtf8 ->
                                      case lvl53_r3nsn of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl23_r3nq0 `cast` <Co:16>)
                                        (lvl105_s3mUo `cast` <Co:12>)
                                      };
                                    IfThenElse ->
                                      case lvl71_s3mUp of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl24_r3nq1 `cast` <Co:296>)
                                        (lvl104_s3mUq `cast` <Co:214>)
                                      };
                                    ChooseUnit ->
                                      case lvl72_s3mUr of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl25_r3nq2 `cast` <Co:172>)
                                        (lvl103_s3mUs `cast` <Co:113>)
                                      };
                                    Trace ->
                                      case lvl73_s3mUt of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl26_r3nq3 `cast` <Co:112>)
                                        (lvl102_s3mUu `cast` <Co:47>)
                                      };
                                    FstPair ->
                                      case lvl74_s3mUv of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (fstPlc_r3nrv `cast` <Co:74>)
                                        (lvl101_s3mUw `cast` <Co:30>)
                                      };
                                    SndPair ->
                                      case lvl75_s3mUx of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (sndPlc_r3nrs `cast` <Co:74>)
                                        (lvl100_s3mUy `cast` <Co:30>)
                                      };
                                    ChooseList ->
                                      case lvl76_s3mUz of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (choosePlc_r3nq4 `cast` <Co:191>)
                                        (lvl99_s3mUA `cast` <Co:107>)
                                      };
                                    MkCons ->
                                      case lvl77_s3mUB of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (consPlc_r3nrp `cast` <Co:115>)
                                        (lvl98_s3mUC `cast` <Co:54>)
                                      };
                                    HeadList ->
                                      case lvl79_s3mUD of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (headPlc_r3nrn `cast` <Co:58>)
                                        (lvl97_s3mUE `cast` <Co:22>)
                                      };
                                    TailList ->
                                      case lvl78_s3mUF of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (tailPlc_r3nro `cast` <Co:60>)
                                        (lvl96_s3mUG `cast` <Co:22>)
                                      };
                                    NullList ->
                                      case lvl54_r3nso of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (nullPlc_r3nq5 `cast` <Co:36>)
                                        (lvl95_s3mUI `cast` <Co:22>)
                                      };
                                    ChooseData ->
                                      case lvl70_s3mUJ of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl27_r3nq6 `cast` <Co:830>)
                                        (lvl94_s3mUK `cast` <Co:679>)
                                      };
                                    ConstrData ->
                                      case lvl55_r3nsp of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (Constr `cast` <Co:31>)
                                        (lvl93_s3mUM `cast` <Co:27>)
                                      };
                                    MapData ->
                                      case lvl56_r3nsq of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV (Map `cast` <Co:20>) (lvl92_s3mUO `cast` <Co:15>)
                                      };
                                    ListData ->
                                      case lvl57_r3nsr of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (List `cast` <Co:16>)
                                        (lvl91_s3mUQ `cast` <Co:13>)
                                      };
                                    IData ->
                                      case lvl58_r3nss of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV (I `cast` <Co:14>) (lvl90_s3mUS `cast` <Co:12>)
                                      };
                                    BData ->
                                      case lvl59_r3nst of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV (B `cast` <Co:14>) (lvl89_s3mUU `cast` <Co:12>)
                                      };
                                    UnConstrData ->
                                      case lvl60_r3nsu of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl28_r3nq7 `cast` <Co:22>)
                                        (lvl88_s3mUW `cast` <Co:12>)
                                      };
                                    UnMapData ->
                                      case lvl61_r3nsv of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl29_r3nq8 `cast` <Co:22>)
                                        (lvl87_s3mUY `cast` <Co:12>)
                                      };
                                    UnListData ->
                                      case lvl62_r3nsw of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl30_r3nq9 `cast` <Co:18>)
                                        (lvl86_s3mV0 `cast` <Co:12>)
                                      };
                                    UnIData ->
                                      case lvl63_r3nsx of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl31_r3nqa `cast` <Co:16>)
                                        (lvl85_s3mV2 `cast` <Co:12>)
                                      };
                                    UnBData ->
                                      case lvl64_r3nsy of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl32_r3nqb `cast` <Co:16>)
                                        (lvl84_s3mV4 `cast` <Co:12>)
                                      };
                                    EqualsData ->
                                      case lvl65_r3nsz of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        ($fEqData_$c== `cast` <Co:28>)
                                        (lvl83_s3mV6 `cast` <Co:25>)
                                      };
                                    MkPairData ->
                                      case lvl66_r3nsA of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV ((,) `cast` <Co:34>) (lvl82_s3mV8 `cast` <Co:25>)
                                      };
                                    MkNilData ->
                                      case lvl67_r3nsB of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl33_r3nqc `cast` <Co:16>)
                                        (lvl81_s3mVa `cast` <Co:12>)
                                      };
                                    MkNilPairData ->
                                      case lvl68_r3nsC of dt36_X2AsV { __DEFAULT ->
                                      BuiltinRuntime
                                        dt36_X2AsV
                                        (lvl34_r3nqd `cast` <Co:20>)
                                        (lvl80_s3mVc `cast` <Co:12>)
                                      }
                                  })
                                 eta1_i2Cug
                          of s4#_i2Cum
                          { __DEFAULT ->
                          case eta_i2Cuf of wild_Xek {
                            __DEFAULT -> jump go1_i2Cud ys_i2Cuk (+# wild_Xek 1#) s4#_i2Cum;
                            50# -> jump $j_i2Cu5 s4#_i2Cum
                          }
                          }
                      }; } in
                jump go1_i2Cud lvl69_r3nsD 0# ipv_i2Cu1
                })
      of
      { (# ipv_i2Cuv, ipv1_i2Cuw #) ->
      ipv1_i2Cuw `cast` <Co:6>
      }

-- RHS size: {terms: 8, types: 32, coercions: 1, joins: 0/0}
$fToBuiltinsRuntimeDefaultFunCekValue_$ctoBuiltinsRuntime
  = \ @ uni_s3mjc w_s3mjd w1_s3mje ->
      case w_s3mjd of { Eq# ww1_s3mjh ->
      $w$ctoBuiltinsRuntime @~ <Co:1> w1_s3mje
      }

-- RHS size: {terms: 1, types: 0, coercions: 6, joins: 0/0}
$fToBuiltinsRuntimeDefaultFunCekValue
  = $fToBuiltinsRuntimeDefaultFunCekValue_$ctoBuiltinsRuntime
    `cast` <Co:6>

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$trModule4 = "plutus-core-0.1.0.0-3WAHA0CT4bW16woblwUZPf"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$trModule3 = TrNameS $trModule4

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
$trModule2 = "UntypedPlutusCore.Evaluation.Machine.Cek.Default"#

-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
$trModule1 = TrNameS $trModule2

-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$trModule = Module $trModule3 $trModule1


------ Local rules for imported ids --------
"SPEC/UntypedPlutusCore.Evaluation.Machine.Cek.Default verifySignature @ EvaluationResult" [2]
    forall w_s3l6C. verifySignature w_s3l6C = $sverifySignature

Ready for review.

@effectfully
Copy link
Contributor Author

effectfully commented Feb 21, 2022

Ah, yeah, I also inlined readKnown in TypeScheme and RuntimeScheme to check how well they can get optimized because of that and it turned out to work really well. You can see in the Core output above that asConstant calls get inlined and we have explicit pattern matching on VCon, which improves not only performance, but also readability of Core. I haven't done the same for makeKnown yet, but I plan to.

@effectfully effectfully force-pushed the effectfully/builtins/toBuiltinRuntime-as-a-class-method-no-UnfoldEq branch from 7f38422 to d537941 Compare February 21, 2022 04:43
@effectfully
Copy link
Contributor Author

@michaelpj yup, git commit --amend -a; git push -f <...> breaks CI.

@michaelpj
Copy link
Contributor

Re: CI, I don't think it can be that simple, I do that all the time!

@michaelpj
Copy link
Contributor

Will have a look in a bit. I wonder whether we'd be better off asking the ledger to cache this for us. We're planning to ask them to cache the rehydration of the cost model, perhaps we could bundle this in too...

@@ -1,6 +1,7 @@
-- GHC doesn't like the definition of 'makeBuiltinMeaning'.
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}

{-# LANGUAGE AllowAmbiguousTypes #-}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do we need this?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see, it's because we dropped the Proxy args. Does that matter? Perhaps this change should be done separately so we can see if it matters.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does that matter?

Probably not. I did it to see if it could change Core output, but couldn't tell if there was a difference in the end. I left it in the code, because AllowAmbiguousTypes looks better to my taste than those stupid proxies.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I actually did see it affect things in one of the previous PRs. Even with INLINE pragmas everywhere, stuff still wasn't inlining properly because of that Proxy. I don't think we care about that here though, since the Core output is pretty chaotic anyway: some of TypeScheme are inlined and some are not and we're fine in both the cases, because we really only care about TypeSchemes being outside of the loop that computes BuiltinsRuntime, so that all BuiltinRuntimes are shared and never recomputed.


-- | Same as 'TypeScheme' except this one doesn't contain any evaluation-irrelevant types stuff.
data RuntimeScheme val (args :: [GHC.Type]) res where
RuntimeSchemeResult
:: KnownTypeIn (UniOf val) val res
=> RuntimeScheme val '[] res
RuntimeSchemeArrow
:: KnownTypeIn (UniOf val) val arg
=> RuntimeScheme val args res
-- 'readKnown' inlined for optimization purposes.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So I guess the idea is that this is better than passing the class dictionary. What would happen if you split KnownTypeIn in two? Then you'd have single-method classes, which get represented directly as the underlying function. Perhaps that would also inline and specialize well.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Then you could do the same trick for RuntimeSchemeResult, which I guess is also packing a dictionary instead of just taking the makeKnown function.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see, you explain this in the note below. Maybe we should investigate what goes wrong with the split more thoroughly.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Then you'd have single-method classes, which get represented directly as the underlying function. Perhaps that would also inline and specialize well.

According to my experiments, it's not necessarily the case, but I'll make sure to check once we perform the split (I really hope we'll do that in the end).

--
-- For performance-critical code both @fun@ and @val@ need to be specified as concrete data types
-- for inlining to happen. In other places it's fine to only specify one of them.
class ToBuiltinsRuntime fun val where
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let me try and write down what I think this is doing.

We want to specialize toBuiltinsRuntime to specific choices of fun and val. It's not enough to inline toBuiltinsRuntime, because then we will only optimize the generic generated code at the call site, rather than generating specialized code (is this true?). Requiring a type class instance for each combination of fun and val creates a definition site which can be individually optimized, and then inlined.

That suggests the following question: does this basically amount to a SPECIALIZE pragma? Note that SPECIALIZE pragmas can be given for imported functions so long as they're INLINABLE.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm also genuinely quite unclear why inlining toBuiltinsRuntime doesn't do the job more simply.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably also need to inline toMachineParameters.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not enough to inline toBuiltinsRuntime, because then we will only optimize the generic generated code at the call site, rather than generating specialized code (is this true?).

Yes, unless the call site has uni and fun specialized. If it doesn't, we'll also need to inline the call site of the call site. And so on until we reach a call site with uni and fun specialized. With the class approach we're just passing around a dictionary with specialized and optimized stuff in it and don't need to worry about chains of call sites, they can do whatever they want.

Note that we're running the CEK machine from different places, so we'd need to track all of them. How would we even do that? inspection-testing? Let's-occasionally-dump-Core-and-check-if-it's-fine-at-every-call-site?

Using a class just seems more reliable than hoping a SPECIALIZE pragma will fire or a chain of calls won't have a missing INLINE somewhere in the middle. And INLINE is sometimes not enough, an explicit call to inline is needed and all of that can change from one GHC version to another. Having a single place where we need to worry about checking if things still get optimized properly is much less of a headache.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, except this is only for the call to toBuiltinsRuntime. Which isn't called in that many places. From a quick grep, about 2.

Note that we're running the CEK machine from different places, so we'd need to track all of them. How would we even do that?

This is why we have benchmarking, no? We've done all kinds of things that we might accidentally break.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I want to have a little try and see if I can make a version with SPECIALIZE work also, just for comparison.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd really like going in the opposite direction and testing the performance of the builtin machinery via a dedicated benchmark instead of shoving everything into a single huge run and then trying to separate actual changes from noise.

We kind of have that in the cost model benchmarks for the builtins, if you're willing to wait 12 hours or so. I'm not suggesting that seriously because (a) it takes too long, and (b) it tells us far more than we need to know. Maybe we could do something like extracting some small subset for checking the performance of the machinery though? I'm already trying to make some attempt to do that with some extra Nop benchmarks that are supposed to give some measure of the overhead of calling a builtin so that we can just model the cost of running the denotation.

I suppose that an advantage of having some separate benchmarks would be that it'd make it easier to spot regressions in the efficiency of the builtin machinery. That makes me a bit nervous because a lot of it depends on delicate implementation choices and I can imagine things going backwards if something changes in GHC.

Copy link
Contributor Author

@effectfully effectfully Mar 4, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@michaelpj

Yes, although the other way to look at that is that we shouldn't necessarily spend as much time trying to optimize the builtin machinery if the overall effect is small!

What do you consider small? Here's a breakdown of how much speedup we got from builtins-related PRs affecting performance that are already merged. A speedup of 31.22% seems to be quite a decent one. Add to that the monomorphic makeKnown PR giving us another 4.87% and the inlined toBuiltinsRuntime PR giving us another 4.03% (my version, yours is even faster), plus subsequent inlining of makeKnown like we did with readKnown, plus I also have a couple of competing branches for inlining matching on type tags. We're approaching cutting evaluation time in half by just tweaking the builtins machinery. All of that working a few hours per week (I've been also spending time on performance-irrelevant things like refactorings, improving the interface of the builtins machinery and documentation writing). I feel like this is quite a success and I should continue doing it.

@kwxm

I can imagine things going backwards if something changes in GHC.

I'm almost sure it will. Which is one of the reasons why I want the toBuiltinsRuntime-as-a-class alignment. Only one place to look it, no irrelevant things in there and the optimized version is guaranteed to be picked up unlike with INLINE or SPECIALIZE.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A speedup of 31.22% seems to be quite a decent one.

I can't of course just add up those individual changes, I'm cutting some corners here.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add to that the monomorphic makeKnown PR giving us another 4.87% and the inlined toBuiltinsRuntime PR giving us another 4.03%

My rusty math skills suggest that with these two PRs we'll get a total of 34% speedup, which I think is not bad at all.

@@ -59,6 +59,8 @@ data CkValue uni fun =
| VBuiltin (Term TyName Name uni fun ()) (BuiltinRuntime (CkValue uni fun))
deriving (Show)

instance ToBuiltinsRuntime DefaultFun (CkValue DefaultUni DefaultFun)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't love the fact that now the functions exported from this module claim to work on any uni and fun, but you would need to add these instances to make it work in practice.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Err, it should be a general instance in the CK machine, because we don't care about performance there. I originally did experiments in this module and then forgot to fix it. I'll do that.

The CEK machine is different though, there we do need the specialization. However note that Cek.Internal is not lying: it can handle absolutely any uni and fun, because it asks the caller to provide a BuiltinsRuntime for them and doesn't need anything else. The Cek module does expose general functions while only working on DefaultUni and DefaultFun out of the box though. Maybe we need a module that only exports specialized functions, so that there's no confusion, not sure.

Copy link
Contributor Author

@effectfully effectfully Feb 27, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Err, not so fast, a general instance conflicts with the one for Either...

@michaelpj
Copy link
Contributor

Hmm also, the changes to include readKnown in TypeScheme is orthogonal to making toBuiltinsRuntime a class method, right? So should we try those separately?

@effectfully
Copy link
Contributor Author

Hmm also, the changes to include readKnown in TypeScheme is orthogonal to making toBuiltinsRuntime a class method, right?

Yep.

So should we try those separately?

Meh, ok.

@michaelpj
Copy link
Contributor

Oh, also I lost a comment here.

I wanted to say: we could also improve the situation here by getting the ledger to cache this. We already want them to cache the cost model, if we can get them to cache the "evaluator" i.e. all the constant stuff across multiple executions, then that could potentially include this. Then I think we don't really care about the performance of toBuiltinRuntime any more!

Copy link
Contributor

@kwxm kwxm left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've not got much to say here, although seeing that you can get gains of 5% or so makes me wonder exactly how much time builtin evaluation is taking. I thought it was taking about 15% of the total time for the validation scripts, but if that was true then a 5% would be relatively huge. Maybe I should try some profiling to see what the situation is these days.

@effectfully
Copy link
Contributor Author

@michaelpj

I wanted to say: we could also improve the situation here by getting the ledger to cache this.

That would improve very little compared to master, probably negligibly so (might be still worth doing though). I'm not optimizing toBuiltinsRuntime in this PR! That function gets called only once, right before evaluation starts and it can't be a bottleneck. What I'm doing in this PR is optimizing functions stored inside of a BuiltinRuntime (makeKnown, readKnown, the denotation of each builtin, HasConstant stuff inside of all of that etc). Caching does not allow you to optimize stuff under a lambda -- inlining does. Hence

Then I think we don't really care about the performance of toBuiltinRuntime any more!

we still care about optimizing the internals of toBuiltinsRuntime.

@kwxm

I've not got much to say here, although seeing that you can get gains of 5% or so makes me wonder exactly how much time builtin evaluation is taking. I thought it was taking about 15% of the total time for the validation scripts, but if that was true then a 5% would be relatively huge. Maybe I should try some profiling to see what the situation is these days.

I feel like I've already optimized evaluation by 20+% only by tweaking the builtins machinery. It would be interesting to check.

Were there any performance improvements in the evaluator in ~six months apart from builtins and De Bruijn indices?

effectfully and others added 5 commits February 27, 2022 21:10
…to effectfully/builtins/toBuiltinRuntime-as-a-class-method-no-UnfoldEq
Co-authored-by: Kenneth MacKenzie <kwxm@inf.ed.ac.uk>
…-no-UnfoldEq' of https://github.com/input-output-hk/plutus into effectfully/builtins/toBuiltinRuntime-as-a-class-method-no-UnfoldEq
@effectfully
Copy link
Contributor Author

/benchmark plutus-benchmark:validation

@iohk-devops
Copy link

Comparing benchmark results of 'plutus-benchmark:validation' on '61a9a0fbe' (base) and 'aea09528d' (PR)

Script 61a9a0f aea0952 Change
auction_1-1 281.6 μs 277.0 μs -1.6%
auction_1-2 934.6 μs 930.2 μs -0.5%
auction_1-3 933.8 μs 927.3 μs -0.7%
auction_1-4 367.1 μs 363.7 μs -0.9%
auction_2-1 282.8 μs 279.2 μs -1.3%
auction_2-2 939.2 μs 933.8 μs -0.6%
auction_2-3 1.187 ms 1.181 ms -0.5%
auction_2-4 935.3 μs 923.5 μs -1.3%
auction_2-5 368.5 μs 362.0 μs -1.8%
crowdfunding-success-1 332.9 μs 327.2 μs -1.7%
crowdfunding-success-2 334.0 μs 327.8 μs -1.9%
crowdfunding-success-3 333.5 μs 328.3 μs -1.6%
currency-1 365.1 μs 364.6 μs -0.1%
escrow-redeem_1-1 536.5 μs 534.0 μs -0.5%
escrow-redeem_1-2 535.8 μs 533.6 μs -0.4%
escrow-redeem_2-1 624.8 μs 621.0 μs -0.6%
escrow-redeem_2-2 627.3 μs 621.2 μs -1.0%
escrow-redeem_2-3 628.8 μs 621.9 μs -1.1%
escrow-refund-1 247.1 μs 243.5 μs -1.5%
future-increase-margin-1 365.5 μs 365.0 μs -0.1%
future-increase-margin-2 814.6 μs 806.6 μs -1.0%
future-increase-margin-3 816.2 μs 810.1 μs -0.7%
future-increase-margin-4 752.2 μs 747.5 μs -0.6%
future-increase-margin-5 1.147 ms 1.142 ms -0.4%
future-pay-out-1 366.6 μs 364.4 μs -0.6%
future-pay-out-2 811.6 μs 812.6 μs +0.1%
future-pay-out-3 811.3 μs 813.7 μs +0.3%
future-pay-out-4 1.139 ms 1.146 ms +0.6%
future-settle-early-1 365.7 μs 366.5 μs +0.2%
future-settle-early-2 815.7 μs 812.4 μs -0.4%
future-settle-early-3 814.0 μs 811.9 μs -0.3%
future-settle-early-4 883.9 μs 883.4 μs -0.1%
game-sm-success_1-1 597.8 μs 595.4 μs -0.4%
game-sm-success_1-2 314.1 μs 306.9 μs -2.3%
game-sm-success_1-3 938.3 μs 938.6 μs +0.0%
game-sm-success_1-4 367.3 μs 361.2 μs -1.7%
game-sm-success_2-1 599.8 μs 594.1 μs -1.0%
game-sm-success_2-2 313.8 μs 308.1 μs -1.8%
game-sm-success_2-3 935.8 μs 935.4 μs -0.0%
game-sm-success_2-4 366.0 μs 360.2 μs -1.6%
game-sm-success_2-5 934.5 μs 936.2 μs +0.2%
game-sm-success_2-6 365.7 μs 362.1 μs -1.0%
multisig-sm-1 605.7 μs 600.2 μs -0.9%
multisig-sm-2 592.8 μs 590.6 μs -0.4%
multisig-sm-3 598.5 μs 597.0 μs -0.3%
multisig-sm-4 604.1 μs 603.9 μs -0.0%
multisig-sm-5 828.0 μs 825.3 μs -0.3%
multisig-sm-6 605.0 μs 597.3 μs -1.3%
multisig-sm-7 596.0 μs 588.3 μs -1.3%
multisig-sm-8 601.6 μs 593.7 μs -1.3%
multisig-sm-9 607.0 μs 602.6 μs -0.7%
multisig-sm-10 829.5 μs 825.9 μs -0.4%
ping-pong-1 500.0 μs 496.7 μs -0.7%
ping-pong-2 499.4 μs 495.8 μs -0.7%
ping-pong_2-1 309.6 μs 304.6 μs -1.6%
prism-1 261.3 μs 257.0 μs -1.6%
prism-2 645.3 μs 646.8 μs +0.2%
prism-3 555.5 μs 556.4 μs +0.2%
pubkey-1 221.8 μs 219.2 μs -1.2%
stablecoin_1-1 1.315 ms 1.312 ms -0.2%
stablecoin_1-2 308.4 μs 302.0 μs -2.1%
stablecoin_1-3 1.506 ms 1.491 ms -1.0%
stablecoin_1-4 327.1 μs 321.3 μs -1.8%
stablecoin_1-5 1.913 ms 1.903 ms -0.5%
stablecoin_1-6 404.7 μs 396.5 μs -2.0%
stablecoin_2-1 1.313 ms 1.300 ms -1.0%
stablecoin_2-2 307.6 μs 300.8 μs -2.2%
stablecoin_2-3 1.512 ms 1.488 ms -1.6%
stablecoin_2-4 328.2 μs 320.7 μs -2.3%
token-account-1 285.5 μs 280.1 μs -1.9%
token-account-2 498.1 μs 493.4 μs -0.9%
uniswap-1 590.7 μs 587.8 μs -0.5%
uniswap-2 340.5 μs 338.3 μs -0.6%
uniswap-3 2.430 ms 2.428 ms -0.1%
uniswap-4 535.2 μs 527.0 μs -1.5%
uniswap-5 1.709 ms 1.700 ms -0.5%
uniswap-6 510.1 μs 504.0 μs -1.2%
vesting-1 516.1 μs 516.2 μs +0.0%

@effectfully
Copy link
Contributor Author

effectfully commented Feb 27, 2022

^ @michaelpj it's noise without inlining readKnown. Which makes sense: very little additional stuff gets optimized if we don't inline readKnown. Should we merge this PR without the readKnown part and add it as a follow-up?

In any case, comments addressed (almost, there's one left), ready for another review.

@michaelpj
Copy link
Contributor

Caching does not allow you to optimize stuff under a lambda -- inlining does.

Okay, let me try and state my revised understanding. The issue is not that computing BuiltinsRuntime is expensive, but that the functions inside it will not be optimized. To do better requires GHC to see the context it needs for optimizing those functions at the point at which they're defined, which realistically means doing enough inlining.

Sorry for being slow, this stuff is confusing!

Which makes sense: very little additional stuff gets optimized if we don't inline readKnown. Should we merge this PR without the readKnown part and add it as a follow-up?

Or maybe we should do it the other way around? I don't know.

@michaelpj
Copy link
Contributor

Here's an ugly attempt at just putting lots of INLINE everywhere. I put the inlining of readKnown back in so we can see if the performance actually holds up.

@michaelpj
Copy link
Contributor

Uh, actual link here: #4435

Seems to perform even better?

@effectfully
Copy link
Contributor Author

@michaelpj

Okay, let me try and state my revised understanding. The issue is not that computing BuiltinsRuntime is expensive, but that the functions inside it will not be optimized. To do better requires GHC to see the context it needs for optimizing those functions at the point at which they're defined, which realistically means doing enough inlining.

Correct.

Sorry for being slow, this stuff is confusing!

No problem, it is confusing.

Seems to perform even better?

Yes, by ~2.5%. I haven't looked into it yet, but I suspect it's due to costing stuff getting inlined, which is something I wanted to look into later.

I still believe it's worth using the class until we're sure that we can't achieve the same performance with it compared to what we can get from explicit inlining (which very well can be the case, although maybe we just need to move that class abstraction up the pipeline a bit). Inlining is very unreliable, we have multiple call sites, GHC changes its optimization strategies all the time, there are too many moving parts and that makes me uncomfortable. When you know that you only need to look into a single instance, that alleviates plenty of uncertainty.

But it's not a hill I want to die on. If you believe we should use your version, we can close this PR and I'll update yours (or the other way around). But if it ever bites us, I'm gonna be very annoying with my "I told you so". Consider yourself warned!

Either way, I'd like this PR to be merged soon, ideally somewhere next week.

@michaelpj
Copy link
Contributor

We did #4481 instead.

@michaelpj michaelpj closed this Mar 21, 2022
@effectfully effectfully deleted the effectfully/builtins/toBuiltinRuntime-as-a-class-method-no-UnfoldEq branch November 10, 2022 22:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants