{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- |
--
--
-- The Leios node must relay EbAnnouncements promptly.
-- CIP-0164 is designed around the idea that an EbAnnouncement at an honest stake pool will have propagated to all other honest stake pools within L_hdr, and suggests a value of 1 second.
-- On a network that spans the globe, that's a very tight window.
-- But each EbAnnouncement is slightly less than 1 kB, so it does seem plausible.
--
-- In the current design of CIP-0164, the existing Praos header (aka RbHeader) was extended with new fields.
-- One of those fields is an optional tuple: EbBody hash and EbBody size.
-- That's the announcement.
-- As part of the RbHeader, it is adjacent to the election proof that justifies the EbAnnouncement and it is signed by the electee.
-- Because that election proof necessarily includes the slot of the election, every EbAnnouncement has an age.
-- In particular, that age is used to evict too-old announcements so that the existing stochastic bound on the number of elections younger than some age also bounds the number of in-memory EbAnnouncements: zero (no announcement), one (unequivocal announcement), or two (equivocal announcements) per sufficiently-young election.
--
-- The LeiosNotify mini protocol in CIP-0164 already includes a notification MsgLeiosAnnouncement, whose payload is the RbHeader.
-- It is sent as one of the possible responses to the generic MsgLeiosNotificationRequestNext message.
-- The healthy honest node tries to maintain ~hundreds of those requests outstanding at all times, so that the upstream peer can always enqueue a notification immediately.
-- The intended timeline one a single connection from an honest node X to an honest node Y is as follows.
--
-- - X either receives or itself issues a new valid EbAnnouncement.
-- - If that's the first or second announcement X has seen for that election, then X tries to relay that announcement to its downstream peers, including Y.
-- - X will be able to send to Y, because X should have received at least one more MsgLeiosNotificationRequestNext message from Y than X has already replied to.
--
-- TO BE IMPORTED QUALIFIED
module Ouroboros.Consensus.MiniProtocol.LeiosNotify.Client.Announcements
  ( module Ouroboros.Consensus.MiniProtocol.LeiosNotify.Client.Announcements
  ) where

import Cardano.Slotting.Slot (SlotNo)
import Data.Foldable (toList)
import qualified Data.Map.Strict as Map
import qualified Data.Map.Strict as Strict (Map)
import GHC.Generics (Generic)
import NoThunks.Class (NoThunks)
import Ouroboros.Consensus.Leios.Types (ElectionId (..))

-----
-- The state of each LeiosNotify client
-----

-- | What a single LeiosNotify upstream peer has announced, per election: the
-- announcements part of the client's per-peer state
newtype State anc = MkState {forall anc. State anc -> Map ElectionId (SeenAnnouncements anc)
live :: Strict.Map ElectionId (SeenAnnouncements anc)}
  deriving stock (forall x. State anc -> Rep (State anc) x)
-> (forall x. Rep (State anc) x -> State anc)
-> Generic (State anc)
forall x. Rep (State anc) x -> State anc
forall x. State anc -> Rep (State anc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall anc x. Rep (State anc) x -> State anc
forall anc x. State anc -> Rep (State anc) x
$cfrom :: forall anc x. State anc -> Rep (State anc) x
from :: forall x. State anc -> Rep (State anc) x
$cto :: forall anc x. Rep (State anc) x -> State anc
to :: forall x. Rep (State anc) x -> State anc
Generic
  deriving anyclass Context -> State anc -> IO (Maybe ThunkInfo)
Proxy (State anc) -> String
(Context -> State anc -> IO (Maybe ThunkInfo))
-> (Context -> State anc -> IO (Maybe ThunkInfo))
-> (Proxy (State anc) -> String)
-> NoThunks (State anc)
forall anc.
NoThunks anc =>
Context -> State anc -> IO (Maybe ThunkInfo)
forall anc. NoThunks anc => Proxy (State anc) -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: forall anc.
NoThunks anc =>
Context -> State anc -> IO (Maybe ThunkInfo)
noThunks :: Context -> State anc -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall anc.
NoThunks anc =>
Context -> State anc -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> State anc -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall anc. NoThunks anc => Proxy (State anc) -> String
showTypeOf :: Proxy (State anc) -> String
NoThunks

empty :: State anc
empty :: forall anc. State anc
empty = Map ElectionId (SeenAnnouncements anc) -> State anc
forall anc. Map ElectionId (SeenAnnouncements anc) -> State anc
MkState Map ElectionId (SeenAnnouncements anc)
forall k a. Map k a
Map.empty

-- | The announcements the peer has sent for one election
data SeenAnnouncements anc
  = -- | The peer has sent one announcement
    --
    -- INVARIANT: has valid signature and election proof
    OneAnnouncement !anc
  | -- | The peer has sent two announcements
    --
    -- INVARIANT: the left announcement was received first
    --
    -- INVARIANT: both have valid signature and election proof
    --
    -- INVARIANT: they are different announcements
    TwoAnnouncements !anc !anc
  deriving stock ((forall x. SeenAnnouncements anc -> Rep (SeenAnnouncements anc) x)
-> (forall x.
    Rep (SeenAnnouncements anc) x -> SeenAnnouncements anc)
-> Generic (SeenAnnouncements anc)
forall x. Rep (SeenAnnouncements anc) x -> SeenAnnouncements anc
forall x. SeenAnnouncements anc -> Rep (SeenAnnouncements anc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall anc x.
Rep (SeenAnnouncements anc) x -> SeenAnnouncements anc
forall anc x.
SeenAnnouncements anc -> Rep (SeenAnnouncements anc) x
$cfrom :: forall anc x.
SeenAnnouncements anc -> Rep (SeenAnnouncements anc) x
from :: forall x. SeenAnnouncements anc -> Rep (SeenAnnouncements anc) x
$cto :: forall anc x.
Rep (SeenAnnouncements anc) x -> SeenAnnouncements anc
to :: forall x. Rep (SeenAnnouncements anc) x -> SeenAnnouncements anc
Generic, (forall m. Monoid m => SeenAnnouncements m -> m)
-> (forall m a. Monoid m => (a -> m) -> SeenAnnouncements a -> m)
-> (forall m a. Monoid m => (a -> m) -> SeenAnnouncements a -> m)
-> (forall a b. (a -> b -> b) -> b -> SeenAnnouncements a -> b)
-> (forall a b. (a -> b -> b) -> b -> SeenAnnouncements a -> b)
-> (forall b a. (b -> a -> b) -> b -> SeenAnnouncements a -> b)
-> (forall b a. (b -> a -> b) -> b -> SeenAnnouncements a -> b)
-> (forall a. (a -> a -> a) -> SeenAnnouncements a -> a)
-> (forall a. (a -> a -> a) -> SeenAnnouncements a -> a)
-> (forall a. SeenAnnouncements a -> [a])
-> (forall a. SeenAnnouncements a -> Bool)
-> (forall a. SeenAnnouncements a -> Int)
-> (forall a. Eq a => a -> SeenAnnouncements a -> Bool)
-> (forall a. Ord a => SeenAnnouncements a -> a)
-> (forall a. Ord a => SeenAnnouncements a -> a)
-> (forall a. Num a => SeenAnnouncements a -> a)
-> (forall a. Num a => SeenAnnouncements a -> a)
-> Foldable SeenAnnouncements
forall a. Eq a => a -> SeenAnnouncements a -> Bool
forall a. Num a => SeenAnnouncements a -> a
forall a. Ord a => SeenAnnouncements a -> a
forall m. Monoid m => SeenAnnouncements m -> m
forall a. SeenAnnouncements a -> Bool
forall a. SeenAnnouncements a -> Int
forall a. SeenAnnouncements a -> [a]
forall a. (a -> a -> a) -> SeenAnnouncements a -> a
forall m a. Monoid m => (a -> m) -> SeenAnnouncements a -> m
forall b a. (b -> a -> b) -> b -> SeenAnnouncements a -> b
forall a b. (a -> b -> b) -> b -> SeenAnnouncements a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => SeenAnnouncements m -> m
fold :: forall m. Monoid m => SeenAnnouncements m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SeenAnnouncements a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> SeenAnnouncements a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SeenAnnouncements a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> SeenAnnouncements a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> SeenAnnouncements a -> b
foldr :: forall a b. (a -> b -> b) -> b -> SeenAnnouncements a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SeenAnnouncements a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> SeenAnnouncements a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SeenAnnouncements a -> b
foldl :: forall b a. (b -> a -> b) -> b -> SeenAnnouncements a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SeenAnnouncements a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> SeenAnnouncements a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> SeenAnnouncements a -> a
foldr1 :: forall a. (a -> a -> a) -> SeenAnnouncements a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SeenAnnouncements a -> a
foldl1 :: forall a. (a -> a -> a) -> SeenAnnouncements a -> a
$ctoList :: forall a. SeenAnnouncements a -> [a]
toList :: forall a. SeenAnnouncements a -> [a]
$cnull :: forall a. SeenAnnouncements a -> Bool
null :: forall a. SeenAnnouncements a -> Bool
$clength :: forall a. SeenAnnouncements a -> Int
length :: forall a. SeenAnnouncements a -> Int
$celem :: forall a. Eq a => a -> SeenAnnouncements a -> Bool
elem :: forall a. Eq a => a -> SeenAnnouncements a -> Bool
$cmaximum :: forall a. Ord a => SeenAnnouncements a -> a
maximum :: forall a. Ord a => SeenAnnouncements a -> a
$cminimum :: forall a. Ord a => SeenAnnouncements a -> a
minimum :: forall a. Ord a => SeenAnnouncements a -> a
$csum :: forall a. Num a => SeenAnnouncements a -> a
sum :: forall a. Num a => SeenAnnouncements a -> a
$cproduct :: forall a. Num a => SeenAnnouncements a -> a
product :: forall a. Num a => SeenAnnouncements a -> a
Foldable)
  deriving anyclass Context -> SeenAnnouncements anc -> IO (Maybe ThunkInfo)
Proxy (SeenAnnouncements anc) -> String
(Context -> SeenAnnouncements anc -> IO (Maybe ThunkInfo))
-> (Context -> SeenAnnouncements anc -> IO (Maybe ThunkInfo))
-> (Proxy (SeenAnnouncements anc) -> String)
-> NoThunks (SeenAnnouncements anc)
forall anc.
NoThunks anc =>
Context -> SeenAnnouncements anc -> IO (Maybe ThunkInfo)
forall anc. NoThunks anc => Proxy (SeenAnnouncements anc) -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: forall anc.
NoThunks anc =>
Context -> SeenAnnouncements anc -> IO (Maybe ThunkInfo)
noThunks :: Context -> SeenAnnouncements anc -> IO (Maybe ThunkInfo)
$cwNoThunks :: forall anc.
NoThunks anc =>
Context -> SeenAnnouncements anc -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> SeenAnnouncements anc -> IO (Maybe ThunkInfo)
$cshowTypeOf :: forall anc. NoThunks anc => Proxy (SeenAnnouncements anc) -> String
showTypeOf :: Proxy (SeenAnnouncements anc) -> String
NoThunks

-- | Everything this peer has announced for elections in the given slot.
--
-- 'ElectionId' orders slot-first, so those elections are a contiguous range. An
-- endorser block's own slot is its election's slot, so this is what an offer
-- of that endorser block has to be backed by.
inSlot :: SlotNo -> State anc -> [anc]
inSlot :: forall anc. SlotNo -> State anc -> [anc]
inSlot SlotNo
slot State anc
st =
  (SeenAnnouncements anc -> [anc])
-> [SeenAnnouncements anc] -> [anc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SeenAnnouncements anc -> [anc]
forall a. SeenAnnouncements a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Map ElectionId (SeenAnnouncements anc) -> [SeenAnnouncements anc]
forall k a. Map k a -> [a]
Map.elems Map ElectionId (SeenAnnouncements anc)
atSlot)
 where
  (Map ElectionId (SeenAnnouncements anc)
_below, Map ElectionId (SeenAnnouncements anc)
atOrAbove) =
    (ElectionId -> Bool)
-> Map ElectionId (SeenAnnouncements anc)
-> (Map ElectionId (SeenAnnouncements anc),
    Map ElectionId (SeenAnnouncements anc))
forall k a. (k -> Bool) -> Map k a -> (Map k a, Map k a)
Map.spanAntitone (\(ElectionId SlotNo
elSlot KeyHash BlockIssuer
_poolId) -> SlotNo
elSlot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
slot) (State anc -> Map ElectionId (SeenAnnouncements anc)
forall anc. State anc -> Map ElectionId (SeenAnnouncements anc)
live State anc
st)
  (Map ElectionId (SeenAnnouncements anc)
atSlot, Map ElectionId (SeenAnnouncements anc)
_above) =
    (ElectionId -> Bool)
-> Map ElectionId (SeenAnnouncements anc)
-> (Map ElectionId (SeenAnnouncements anc),
    Map ElectionId (SeenAnnouncements anc))
forall k a. (k -> Bool) -> Map k a -> (Map k a, Map k a)
Map.spanAntitone (\(ElectionId SlotNo
elSlot KeyHash BlockIssuer
_poolId) -> SlotNo
elSlot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<= SlotNo
slot) Map ElectionId (SeenAnnouncements anc)
atOrAbove

-- | Called whenever the ChainDB's immutable tip advances to a new slot. Also
-- returns the announcements it forgets.
--
-- NOTE this pruning should happen ~60 s after the immutable tip
-- advances.  That accommodates clock skew, transmission time, etc
-- with only an insignificant increase in the stochastic bound on
-- election count
prune :: SlotNo -> State anc -> ([anc], State anc)
prune :: forall anc. SlotNo -> State anc -> ([anc], State anc)
prune SlotNo
immTipSlot State anc
st =
  ((SeenAnnouncements anc -> [anc])
-> [SeenAnnouncements anc] -> [anc]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SeenAnnouncements anc -> [anc]
forall a. SeenAnnouncements a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Map ElectionId (SeenAnnouncements anc) -> [SeenAnnouncements anc]
forall k a. Map k a -> [a]
Map.elems Map ElectionId (SeenAnnouncements anc)
pruned), Map ElectionId (SeenAnnouncements anc) -> State anc
forall anc. Map ElectionId (SeenAnnouncements anc) -> State anc
MkState Map ElectionId (SeenAnnouncements anc)
live')
 where
  (Map ElectionId (SeenAnnouncements anc)
pruned, Map ElectionId (SeenAnnouncements anc)
live') = (ElectionId -> Bool)
-> Map ElectionId (SeenAnnouncements anc)
-> (Map ElectionId (SeenAnnouncements anc),
    Map ElectionId (SeenAnnouncements anc))
forall k a. (k -> Bool) -> Map k a -> (Map k a, Map k a)
Map.spanAntitone ElectionId -> Bool
tooOld (State anc -> Map ElectionId (SeenAnnouncements anc)
forall anc. State anc -> Map ElectionId (SeenAnnouncements anc)
live State anc
st)

  -- NB strict comparison, so that the immtip's own announcement is
  -- not pruned
  tooOld :: ElectionId -> Bool
tooOld (ElectionId SlotNo
elSlot KeyHash BlockIssuer
_poolId) = SlotNo
elSlot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
immTipSlot

-- | Behaviors of a LeiosNotify upstream peer's announcement stream
-- that an honest node rejects
data Error invalidity
  = -- | The peer had already sent this same announcement before
    ErrRepeat
  | -- | The peer had already sent two announcements for this election
    ErrThird
  | -- | This announcement is invalid
    ErrInvalid !invalidity
  | -- | This announcement's election is too old (its wall-clock age exceeds
    -- what a client tolerates from an upstream peer). Unlike 'ErrInvalid', this
    -- verdict depends on the wall clock rather than on the announcement itself.
    ErrTooOld
  deriving Int -> Error invalidity -> ShowS
[Error invalidity] -> ShowS
Error invalidity -> String
(Int -> Error invalidity -> ShowS)
-> (Error invalidity -> String)
-> ([Error invalidity] -> ShowS)
-> Show (Error invalidity)
forall invalidity.
Show invalidity =>
Int -> Error invalidity -> ShowS
forall invalidity. Show invalidity => [Error invalidity] -> ShowS
forall invalidity. Show invalidity => Error invalidity -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall invalidity.
Show invalidity =>
Int -> Error invalidity -> ShowS
showsPrec :: Int -> Error invalidity -> ShowS
$cshow :: forall invalidity. Show invalidity => Error invalidity -> String
show :: Error invalidity -> String
$cshowList :: forall invalidity. Show invalidity => [Error invalidity] -> ShowS
showList :: [Error invalidity] -> ShowS
Show

-- | Fails if this election was already 'TwoAnnouncements' or if this
-- announcement was already received
insert ::
  forall anc invalidity.
  Eq anc =>
  ElectionId ->
  anc ->
  State anc ->
  Either (Error invalidity) (State anc)
insert :: forall anc invalidity.
Eq anc =>
ElectionId
-> anc -> State anc -> Either (Error invalidity) (State anc)
insert ElectionId
elId anc
anc State anc
st =
  Map ElectionId (SeenAnnouncements anc) -> State anc
forall anc. Map ElectionId (SeenAnnouncements anc) -> State anc
MkState (Map ElectionId (SeenAnnouncements anc) -> State anc)
-> Either
     (Error invalidity) (Map ElectionId (SeenAnnouncements anc))
-> Either (Error invalidity) (State anc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe (SeenAnnouncements anc)
 -> Either (Error invalidity) (Maybe (SeenAnnouncements anc)))
-> ElectionId
-> Map ElectionId (SeenAnnouncements anc)
-> Either
     (Error invalidity) (Map ElectionId (SeenAnnouncements anc))
forall (f :: * -> *) k a.
(Functor f, Ord k) =>
(Maybe a -> f (Maybe a)) -> k -> Map k a -> f (Map k a)
Map.alterF ((SeenAnnouncements anc -> Maybe (SeenAnnouncements anc))
-> Either (Error invalidity) (SeenAnnouncements anc)
-> Either (Error invalidity) (Maybe (SeenAnnouncements anc))
forall a b.
(a -> b)
-> Either (Error invalidity) a -> Either (Error invalidity) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SeenAnnouncements anc -> Maybe (SeenAnnouncements anc)
forall a. a -> Maybe a
Just (Either (Error invalidity) (SeenAnnouncements anc)
 -> Either (Error invalidity) (Maybe (SeenAnnouncements anc)))
-> (Maybe (SeenAnnouncements anc)
    -> Either (Error invalidity) (SeenAnnouncements anc))
-> Maybe (SeenAnnouncements anc)
-> Either (Error invalidity) (Maybe (SeenAnnouncements anc))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (SeenAnnouncements anc)
-> Either (Error invalidity) (SeenAnnouncements anc)
upd) ElectionId
elId (State anc -> Map ElectionId (SeenAnnouncements anc)
forall anc. State anc -> Map ElectionId (SeenAnnouncements anc)
live State anc
st)
 where
  -- 0 -> 1 ok
  -- 1 -> 2 ok when unequal
  -- 2 -> 3 not ok
  upd :: Maybe (SeenAnnouncements anc) -> Either (Error invalidity) (SeenAnnouncements anc)
  upd :: Maybe (SeenAnnouncements anc)
-> Either (Error invalidity) (SeenAnnouncements anc)
upd = \case
    Maybe (SeenAnnouncements anc)
Nothing -> SeenAnnouncements anc
-> Either (Error invalidity) (SeenAnnouncements anc)
forall a b. b -> Either a b
Right (SeenAnnouncements anc
 -> Either (Error invalidity) (SeenAnnouncements anc))
-> SeenAnnouncements anc
-> Either (Error invalidity) (SeenAnnouncements anc)
forall a b. (a -> b) -> a -> b
$ anc -> SeenAnnouncements anc
forall anc. anc -> SeenAnnouncements anc
OneAnnouncement anc
anc
    Just (OneAnnouncement anc
x) ->
      if anc
x anc -> anc -> Bool
forall a. Eq a => a -> a -> Bool
== anc
anc
        then Error invalidity
-> Either (Error invalidity) (SeenAnnouncements anc)
forall a b. a -> Either a b
Left Error invalidity
forall invalidity. Error invalidity
ErrRepeat
        else
          SeenAnnouncements anc
-> Either (Error invalidity) (SeenAnnouncements anc)
forall a b. b -> Either a b
Right (SeenAnnouncements anc
 -> Either (Error invalidity) (SeenAnnouncements anc))
-> SeenAnnouncements anc
-> Either (Error invalidity) (SeenAnnouncements anc)
forall a b. (a -> b) -> a -> b
$ anc -> anc -> SeenAnnouncements anc
forall anc. anc -> anc -> SeenAnnouncements anc
TwoAnnouncements anc
x anc
anc
    Just TwoAnnouncements{} -> Error invalidity
-> Either (Error invalidity) (SeenAnnouncements anc)
forall a b. a -> Either a b
Left Error invalidity
forall invalidity. Error invalidity
ErrThird