StaticEither accessors

[jorisdral]

Description

Closes #4232.

The StaticEither datatype encodes its "left-ness" or "right-ness" in a type-level Bool.

data StaticEither :: Bool -> Type -> Type -> Type where
  StaticLeft  :: l -> StaticEither False l r
  StaticRight :: r -> StaticEither True  l r

As a consequence, when the type-level Bool becomes concrete (i.e., 'True or 'False'), we can only match on one of the constructors.

case sl of StaticLeft x -> x
let StaticLeft x = sl
case sr of StaticRight x -> x
let StaticRight x = sr 

We add two helper functions, that are analogous to fromLeft and fromRight, but without the default value that fromLeft and fromRight require to be total functions.

fromStaticLeft :: StaticEither 'False l r -> l
fromStaticLeft = \case (StaticLeft x) -> x

fromStaticRight :: StaticEither 'True l r -> r
fromStaticRight = \case (StaticRight x) -> x

Checklist

• Branch
  • Commit sequence broadly makes sense
  • Commits have useful messages
  • New tests are added if needed and existing tests are updated
  • If this branch changes Consensus and has any consequences for downstream repositories or end users, said changes must be documented in interface-CHANGELOG.md
  • If this branch changes Network and has any consequences for downstream repositories or end users, said changes must be documented in interface-CHANGELOG.md
  • If serialization changes, user-facing consequences (e.g. replay from genesis) are confirmed to be intentional.
• Pull Request
  • Self-reviewed the diff
  • Useful pull request description at least containing the following information:
    • What does this PR change?
    • Why these changes were needed?
    • How does this affect downstream repositories and/or end-users?
    • Which ticket does this PR close (if any)? If it does, is it linked?
  • Reviewer requested

[jasagredo]

Looks good