Fix try-catch scoping bug in daml-script

[akrmn]

Fixes #16132, see #16190 (comment) for explanation

[akrmn]

we can simplify this to

- act : () -> Free ScriptF (Free ScriptF LedgerValue, ())
+ act : () -> Free ScriptF LedgerValue

but I'd rather do that separately so the fix is easier to understand

[akrmn]

The type argument a no longer appears in fields act and handle; now it's been replaced by Free ScriptF LedgerValue. This matches the type when used inside Script x, namely a ~ Free ScriptF x, except x is wrapped into a LedgerValue.

This means that instance Functor CatchPayload now only maps over the new field continue, which is only evaluated and run after act (and after handle if act threw an exception). The old behaviour, namely mapping over act and handle was the root of the problem; it meant that all actions after the try-catch block were added to both fields, and if one of the actions was a bare error/fail/abort, the outer Free ScriptF in act would crash while trying to construct the inner Free ScriptF. This last part explains why the bug didn't happen when using throw, since the inner Free ScriptF could be constructed with a ScriptF.Throw to be evaluated in the following runner iteration.

[akrmn]

Another fix would have been to change the type of act,

- act : () -> Free ScriptF (a, ())
+ act : () -> Free ScriptF (() -> a, ())

recall that inside Script x a ~ Free ScriptF x, giving us

- act : () -> Free ScriptF (Free ScriptF x, ())
+ act : () -> Free ScriptF (() -> Free ScriptF x, ())

with that change, the inner computation in act doesn't need to be constructed until applied to (), so the exception cannot be caught. However, that approach would still duplicate all the actions after the try-catch block into both act and handle, so i opted against it.

[nickchapman-da]

Awesome fix!
LGTM (to the extent I understand it)

My only comment is a question regarding why we now need to manufacture LedgerValue from within the Daml code side. (using toLedgerVaue)

Previously LedgerValues only came from the scala side, and we used fromLedgerValue because in the Daml we know what the a is.

[nickchapman-da]

I'm slightly puzzled why we need this.

[akrmn]

I needed this to write the CatchPayload in instance ActionCatch Script. Since it's inside lift $ Free $ Catch $ _, it needs to have type CatchPayload (Free ScriptF t) (where t is the return type of the Script). For context this is what the datatype looks like (in this PR):

data CatchPayload a = CatchPayload
  with
    act : () -> Free ScriptF (Free ScriptF LedgerValue, ())
    handle : AnyException -> Optional (Free ScriptF LedgerValue)
    continue : Free ScriptF LedgerValue -> a

really, we would like to say that the LedgerValue returned by act, the LedgerValue possibly returned by handle, and the LedgerValue consumed by continue are all the same type, let's call it x, for something like

data CatchPayload x a = CatchPayload
  with
    act : () -> Free ScriptF (Free ScriptF x, ())
    handle : AnyException -> Optional (Free ScriptF x)
    continue : Free ScriptF x -> a

the problem with that is that then it's not clear what to put in for x in the Catch constructor of ScriptF:

data ScriptF a 
  = Submit (SubmitCmd a)
  | {- ... -}
  | Catch (CatchPayload (???) a)

what we would want here is to say any type is fine, since what really matters is that all three fields agree on what it is. In Haskell we could use an existential type for exactly that, but those aren't allowed in Daml. However we do have LedgerValue, a fake type representing a value of some type, which is pretty close to what we want. Since we're the ones constructing the CatchPayload, we can make sure that they agree, and then toLedgerValue lets us convince the typechecker.

[akrmn]

prompted by this I've changed the encoding a bit. Now CatchPayload is defined as above with the x argument, and instead of constructing it by using {from,to}LedgerValue in each field, we construct it with type CatchPayload t (Free ScriptF t) and then cast it to CatchPayload LedgerValue (Free ScriptF t) using a new fake function castCatchPayload : CatchPayload x a -> CatchPayload LedgerValue a (using the same id trick). This removes the need for toLedgerValue and gives us a bit more confidence that the types make sense before the cast.

[remyhaemmerle-da]

This look good for me, however I would like @cocreature to have a look at it. (let him few days before merging)

[cocreature]

Nice! Thanks for tracking this down