Get rid of `delay`s in `case` branches

[effectfully]

Currently the compiler puts delays into branches, i.e. this Haskell code:

case xs of
    []    -> z
    x:xs' -> f x xs'

becomes this PIR code (this needs to be verified):

let matchList = \b1 b2 -> case xs of
        []    -> b1
        x:xs' -> b2 x xs'
in force (matchList xs (delay z) (\x xs' -> delay (f x xs')))

The reason for that is that the compiler turns Haskell pattern matching into calls of match* functions (a.k.a. matchers) and those are regular functions, meaning they're strict and so we have to put delays in the arguments in order to prevent them from being computed prematurely.

But case is lazy and so we'd really like to inline the matcher function and get rid of the delays. Unfortunately, we can't do that in PIR, quoting Michael:

The thing that tipped me over is realising that there is at least one thing we always want to inline: data type matchers. Why? Because: a) calls to them are always saturated (we always provide all the case branches!), b) they reduce well because the body is just a function application. The thing that's really annoying is that we basically can't inline them in PIR. The types get in the way because of the way we abstract out the complex types for data types. So we can't inline them without making the program type incorrect. Now, we could inline all the types... but then we'd massively (exponentially!) increase the program size and type checking time. No such problem in UPLC.

But doing that in UPLC isn't going to cut it either! OK, we've inlined the matcher, now we have

force (case xs
        (delay z)
        (\x xs' -> delay (f x xs'))

but we can't put force into the branches, because at that point we've lost all type information and don't know how many lambdas to skip for each branch, see this for details.

So is it the case that there's no way we can get rid of delays generated in case branches? That's quite some overhead and it's entirely unnecessary. Maybe we should compile PIR to untyped PIR and then UPLC bypassing TPLC entirely.

Or maybe we should have transparent type lets allowing one to use case on a data type, here's for example how that works in Agda:

open import Data.Unit.Base using (tt)
open import Function using (case_of_)

test =
    let EvenSecreterData = SecretData
    in (λ (secretData′ : EvenSecreterData) -> case secretData′ of λ { secretData -> tt })
       secretData
  where
    data SecretData : Set where
      secretData : SecretData

Could that allow us to get rid of the matchers entirely?