{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-- | Infrastructure for doing chain selection across eras
module Ouroboros.Consensus.HardFork.Combinator.Protocol.ChainSel
  ( AcrossEraMode (..)
  , AcrossEraTiebreaker (..)
  , acrossEraSelection
  , SwitchOutput (..)
  , OneEraReasonForSwitch (..)
  , ConstOutput (..)
  ) where

import Data.Kind (Type)
import Data.SOP.Constraint
import Data.SOP.Strict
import Data.SOP.Tails (Tails (..))
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.HardFork.Combinator.Abstract.SingleEraBlock
import Ouroboros.Consensus.Protocol.Abstract
import Ouroboros.Consensus.TypeFamilyWrappers

{-------------------------------------------------------------------------------
  Configuration
-------------------------------------------------------------------------------}

-- | How to compare chains of equal length across eras.
data AcrossEraTiebreaker :: Type -> Type -> Type where
  -- | No preference.
  NoTiebreakerAcrossEras :: AcrossEraTiebreaker x y
  -- | Two eras using the same 'TiebreakerView', so use the corresponding
  -- (identical) tiebreaker.
  --
  -- We use the 'ChainOrderConfig' of the 'TiebreakerView' in the newer era
  -- (with the intuition that newer eras are generally "preferred") when
  -- invoking 'compareChains'. However, this choice is arbitrary; we could also
  -- make it configurable here.
  SameTiebreakerAcrossEras ::
    TiebreakerView (BlockProtocol x) ~ TiebreakerView (BlockProtocol y) =>
    AcrossEraTiebreaker x y

{-------------------------------------------------------------------------------
  Compare two eras
-------------------------------------------------------------------------------}

-- | GADT indicating whether we are lifting 'compare' or 'preferCandidate' to
-- the HFC, together with the type of configuration we need for that and the
-- result type. The result type indicates whether we expect something that
-- changes between eras or some constant output.
data AcrossEraMode cfg (f :: [Type] -> Type) where
  AcrossEraCompare :: AcrossEraMode Proxy (ConstOutput Ordering)
  AcrossEraPreferCandidate :: AcrossEraMode WrapChainOrderConfig SwitchOutput

newtype OneEraReasonForSwitch xs = OneEraReasonForSwitch {forall (xs :: [*]).
OneEraReasonForSwitch xs -> NS WrapReasonForSwitch xs
getOneEraReasonForSwitch :: NS WrapReasonForSwitch xs}

-- | Abstract the result of chain selection so we can handle both
-- invariant results (Ordering) and covariant results (ShouldSwitch).
class AcrossEraOutput (f :: [Type] -> Type) where
  type SingleEraOutput f (x :: Type) :: Type

  liftHead :: SingleEraOutput f x -> f (x ': xs)
  liftTail :: f xs -> f (x ': xs)

  -- | Lift a result from (x : zs) to (x : y : zs).
  -- Keeps index 0 (x) as is, shifts indices >= 1 (zs) by one.
  -- This is needed when comparing 'x' against a list and skipping the head of the list.
  liftSkip :: f (x ': zs) -> f (x ': y ': zs)

-- | 1. Ordering Instance (Invariant)
newtype ConstOutput a xs = ConstOutput {forall {k} a (xs :: k). ConstOutput a xs -> a
getConstOutput :: a}

instance AcrossEraOutput (ConstOutput a) where
  type SingleEraOutput (ConstOutput a) x = a
  liftHead :: forall x (xs :: [*]).
SingleEraOutput (ConstOutput a) x -> ConstOutput a (x : xs)
liftHead = a -> ConstOutput a (x : xs)
SingleEraOutput (ConstOutput a) x -> ConstOutput a (x : xs)
forall {k} a (xs :: k). a -> ConstOutput a xs
ConstOutput
  liftTail :: forall (xs :: [*]) x. ConstOutput a xs -> ConstOutput a (x : xs)
liftTail = a -> ConstOutput a (x : xs)
forall {k} a (xs :: k). a -> ConstOutput a xs
ConstOutput (a -> ConstOutput a (x : xs))
-> (ConstOutput a xs -> a)
-> ConstOutput a xs
-> ConstOutput a (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstOutput a xs -> a
forall {k} a (xs :: k). ConstOutput a xs -> a
getConstOutput
  liftSkip :: forall x (zs :: [*]) y.
ConstOutput a (x : zs) -> ConstOutput a (x : y : zs)
liftSkip = a -> ConstOutput a (x : y : zs)
forall {k} a (xs :: k). a -> ConstOutput a xs
ConstOutput (a -> ConstOutput a (x : y : zs))
-> (ConstOutput a (x : zs) -> a)
-> ConstOutput a (x : zs)
-> ConstOutput a (x : y : zs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstOutput a (x : zs) -> a
forall {k} a (xs :: k). ConstOutput a xs -> a
getConstOutput

-- | 2. Switch Instance (Covariant)
newtype SwitchOutput xs = SwitchOutput
  { forall (xs :: [*]).
SwitchOutput xs -> ShouldSwitch (OneEraReasonForSwitch xs)
getSwitchOutput :: ShouldSwitch (OneEraReasonForSwitch xs)
  }

instance AcrossEraOutput SwitchOutput where
  -- The leaf result corresponds to one era's wrapped reason
  type SingleEraOutput SwitchOutput x = ShouldSwitch (WrapReasonForSwitch x)

  liftHead :: forall x (xs :: [*]).
SingleEraOutput SwitchOutput x -> SwitchOutput (x : xs)
liftHead = \case
    ShouldNotSwitch Ordering
o -> ShouldSwitch (OneEraReasonForSwitch (x : xs))
-> SwitchOutput (x : xs)
forall (xs :: [*]).
ShouldSwitch (OneEraReasonForSwitch xs) -> SwitchOutput xs
SwitchOutput (Ordering -> ShouldSwitch (OneEraReasonForSwitch (x : xs))
forall reason. Ordering -> ShouldSwitch reason
ShouldNotSwitch Ordering
o)
    ShouldSwitch WrapReasonForSwitch x
r -> ShouldSwitch (OneEraReasonForSwitch (x : xs))
-> SwitchOutput (x : xs)
forall (xs :: [*]).
ShouldSwitch (OneEraReasonForSwitch xs) -> SwitchOutput xs
SwitchOutput (ShouldSwitch (OneEraReasonForSwitch (x : xs))
 -> SwitchOutput (x : xs))
-> ShouldSwitch (OneEraReasonForSwitch (x : xs))
-> SwitchOutput (x : xs)
forall a b. (a -> b) -> a -> b
$ OneEraReasonForSwitch (x : xs)
-> ShouldSwitch (OneEraReasonForSwitch (x : xs))
forall reason. reason -> ShouldSwitch reason
ShouldSwitch (OneEraReasonForSwitch (x : xs)
 -> ShouldSwitch (OneEraReasonForSwitch (x : xs)))
-> OneEraReasonForSwitch (x : xs)
-> ShouldSwitch (OneEraReasonForSwitch (x : xs))
forall a b. (a -> b) -> a -> b
$ NS WrapReasonForSwitch (x : xs) -> OneEraReasonForSwitch (x : xs)
forall (xs :: [*]).
NS WrapReasonForSwitch xs -> OneEraReasonForSwitch xs
OneEraReasonForSwitch (WrapReasonForSwitch x -> NS WrapReasonForSwitch (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NS f (x : xs1)
Z WrapReasonForSwitch x
r)

  liftTail :: forall (xs :: [*]) x. SwitchOutput xs -> SwitchOutput (x : xs)
liftTail (SwitchOutput ShouldSwitch (OneEraReasonForSwitch xs)
s) = ShouldSwitch (OneEraReasonForSwitch (x : xs))
-> SwitchOutput (x : xs)
forall (xs :: [*]).
ShouldSwitch (OneEraReasonForSwitch xs) -> SwitchOutput xs
SwitchOutput (ShouldSwitch (OneEraReasonForSwitch (x : xs))
 -> SwitchOutput (x : xs))
-> ShouldSwitch (OneEraReasonForSwitch (x : xs))
-> SwitchOutput (x : xs)
forall a b. (a -> b) -> a -> b
$ case ShouldSwitch (OneEraReasonForSwitch xs)
s of
    ShouldNotSwitch Ordering
o -> Ordering -> ShouldSwitch (OneEraReasonForSwitch (x : xs))
forall reason. Ordering -> ShouldSwitch reason
ShouldNotSwitch Ordering
o
    ShouldSwitch OneEraReasonForSwitch xs
rs -> OneEraReasonForSwitch (x : xs)
-> ShouldSwitch (OneEraReasonForSwitch (x : xs))
forall reason. reason -> ShouldSwitch reason
ShouldSwitch (OneEraReasonForSwitch (x : xs)
 -> ShouldSwitch (OneEraReasonForSwitch (x : xs)))
-> OneEraReasonForSwitch (x : xs)
-> ShouldSwitch (OneEraReasonForSwitch (x : xs))
forall a b. (a -> b) -> a -> b
$ NS WrapReasonForSwitch (x : xs) -> OneEraReasonForSwitch (x : xs)
forall (xs :: [*]).
NS WrapReasonForSwitch xs -> OneEraReasonForSwitch xs
OneEraReasonForSwitch (NS WrapReasonForSwitch xs -> NS WrapReasonForSwitch (x : xs)
forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k).
NS f xs1 -> NS f (x : xs1)
S (OneEraReasonForSwitch xs -> NS WrapReasonForSwitch xs
forall (xs :: [*]).
OneEraReasonForSwitch xs -> NS WrapReasonForSwitch xs
getOneEraReasonForSwitch OneEraReasonForSwitch xs
rs))

  liftSkip :: forall x (zs :: [*]) y.
SwitchOutput (x : zs) -> SwitchOutput (x : y : zs)
liftSkip (SwitchOutput ShouldSwitch (OneEraReasonForSwitch (x : zs))
s) = ShouldSwitch (OneEraReasonForSwitch (x : y : zs))
-> SwitchOutput (x : y : zs)
forall (xs :: [*]).
ShouldSwitch (OneEraReasonForSwitch xs) -> SwitchOutput xs
SwitchOutput (ShouldSwitch (OneEraReasonForSwitch (x : y : zs))
 -> SwitchOutput (x : y : zs))
-> ShouldSwitch (OneEraReasonForSwitch (x : y : zs))
-> SwitchOutput (x : y : zs)
forall a b. (a -> b) -> a -> b
$ case ShouldSwitch (OneEraReasonForSwitch (x : zs))
s of
    ShouldNotSwitch Ordering
o -> Ordering -> ShouldSwitch (OneEraReasonForSwitch (x : y : zs))
forall reason. Ordering -> ShouldSwitch reason
ShouldNotSwitch Ordering
o
    ShouldSwitch (OneEraReasonForSwitch NS WrapReasonForSwitch (x : zs)
ns) ->
      OneEraReasonForSwitch (x : y : zs)
-> ShouldSwitch (OneEraReasonForSwitch (x : y : zs))
forall reason. reason -> ShouldSwitch reason
ShouldSwitch (OneEraReasonForSwitch (x : y : zs)
 -> ShouldSwitch (OneEraReasonForSwitch (x : y : zs)))
-> OneEraReasonForSwitch (x : y : zs)
-> ShouldSwitch (OneEraReasonForSwitch (x : y : zs))
forall a b. (a -> b) -> a -> b
$ NS WrapReasonForSwitch (x : y : zs)
-> OneEraReasonForSwitch (x : y : zs)
forall (xs :: [*]).
NS WrapReasonForSwitch xs -> OneEraReasonForSwitch xs
OneEraReasonForSwitch (NS WrapReasonForSwitch (x : y : zs)
 -> OneEraReasonForSwitch (x : y : zs))
-> NS WrapReasonForSwitch (x : y : zs)
-> OneEraReasonForSwitch (x : y : zs)
forall a b. (a -> b) -> a -> b
$ case NS WrapReasonForSwitch (x : zs)
ns of
        Z WrapReasonForSwitch x
r -> WrapReasonForSwitch x -> NS WrapReasonForSwitch (x : y : zs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NS f (x : xs1)
Z WrapReasonForSwitch x
WrapReasonForSwitch x
r -- The reason was 'x' (index 0), keep it at index 0
        S NS WrapReasonForSwitch xs1
rs -> NS WrapReasonForSwitch (y : zs)
-> NS WrapReasonForSwitch (x : y : zs)
forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k).
NS f xs1 -> NS f (x : xs1)
S (NS WrapReasonForSwitch zs -> NS WrapReasonForSwitch (y : zs)
forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k).
NS f xs1 -> NS f (x : xs1)
S NS WrapReasonForSwitch zs
NS WrapReasonForSwitch xs1
rs) -- The reason was in 'zs' (index 1+), shift to index 2+

applyAcrossEraMode ::
  ChainOrder (WrapTiebreakerView blk) =>
  cfg blk ->
  (WrapChainOrderConfig blk -> ChainOrderConfig (WrapTiebreakerView blk)) ->
  AcrossEraMode cfg f ->
  WrapTiebreakerView blk ->
  WrapTiebreakerView blk ->
  SingleEraOutput f blk
applyAcrossEraMode :: forall blk (cfg :: * -> *) (f :: [*] -> *).
ChainOrder (WrapTiebreakerView blk) =>
cfg blk
-> (WrapChainOrderConfig blk
    -> ChainOrderConfig (WrapTiebreakerView blk))
-> AcrossEraMode cfg f
-> WrapTiebreakerView blk
-> WrapTiebreakerView blk
-> SingleEraOutput f blk
applyAcrossEraMode cfg blk
cfg WrapChainOrderConfig blk
-> ChainOrderConfig (WrapTiebreakerView blk)
f = \case
  AcrossEraMode cfg f
AcrossEraCompare -> WrapTiebreakerView blk -> WrapTiebreakerView blk -> Ordering
WrapTiebreakerView blk
-> WrapTiebreakerView blk -> SingleEraOutput f blk
forall a. Ord a => a -> a -> Ordering
compare
  AcrossEraMode cfg f
AcrossEraPreferCandidate -> \WrapTiebreakerView blk
ours WrapTiebreakerView blk
cand ->
    case ChainOrderConfig (WrapTiebreakerView blk)
-> WrapTiebreakerView blk
-> WrapTiebreakerView blk
-> ShouldSwitch (ReasonForSwitch (WrapTiebreakerView blk))
forall sv.
ChainOrder sv =>
ChainOrderConfig sv
-> sv -> sv -> ShouldSwitch (ReasonForSwitch sv)
preferCandidate (WrapChainOrderConfig blk
-> ChainOrderConfig (WrapTiebreakerView blk)
f cfg blk
WrapChainOrderConfig blk
cfg) WrapTiebreakerView blk
ours WrapTiebreakerView blk
cand of
      ShouldNotSwitch Ordering
o -> Ordering -> ShouldSwitch (WrapReasonForSwitch blk)
forall reason. Ordering -> ShouldSwitch reason
ShouldNotSwitch Ordering
o
      ShouldSwitch ReasonForSwitch (WrapTiebreakerView blk)
r -> WrapReasonForSwitch blk -> ShouldSwitch (WrapReasonForSwitch blk)
forall reason. reason -> ShouldSwitch reason
ShouldSwitch (ReasonForSwitch (WrapTiebreakerView blk) -> WrapReasonForSwitch blk
forall blk.
ReasonForSwitch (WrapTiebreakerView blk) -> WrapReasonForSwitch blk
WrapReasonForSwitch ReasonForSwitch (WrapTiebreakerView blk)
r)

data FlipArgs = KeepArgs | FlipArgs

acrossEras ::
  forall blk blk' cfg f.
  SingleEraBlock blk =>
  FlipArgs ->
  AcrossEraMode cfg f ->
  -- | The configuration corresponding to the later block/era, also see
  -- 'SameTiebreakerAcrossEras'.
  cfg blk' ->
  WrapTiebreakerView blk ->
  WrapTiebreakerView blk' ->
  AcrossEraTiebreaker blk blk' ->
  SingleEraOutput f blk'
acrossEras :: forall blk blk' (cfg :: * -> *) (f :: [*] -> *).
SingleEraBlock blk =>
FlipArgs
-> AcrossEraMode cfg f
-> cfg blk'
-> WrapTiebreakerView blk
-> WrapTiebreakerView blk'
-> AcrossEraTiebreaker blk blk'
-> SingleEraOutput f blk'
acrossEras
  FlipArgs
flipArgs
  AcrossEraMode cfg f
mode
  cfg blk'
cfg
  (WrapTiebreakerView TiebreakerView (BlockProtocol blk)
l)
  (WrapTiebreakerView TiebreakerView (BlockProtocol blk')
r) = \case
    AcrossEraTiebreaker blk blk'
NoTiebreakerAcrossEras ->
      -- We would compare NoTiebreak vs NoTiebreak but this will always result
      -- in EQ and ShouldNotSwitch
      case AcrossEraMode cfg f
mode of
        AcrossEraMode cfg f
AcrossEraCompare -> Ordering
SingleEraOutput f blk'
EQ
        AcrossEraMode cfg f
AcrossEraPreferCandidate -> Ordering -> ShouldSwitch (WrapReasonForSwitch blk')
forall reason. Ordering -> ShouldSwitch reason
ShouldNotSwitch Ordering
EQ
    AcrossEraTiebreaker blk blk'
SameTiebreakerAcrossEras -> (WrapTiebreakerView blk'
 -> WrapTiebreakerView blk' -> SingleEraOutput f blk')
-> WrapTiebreakerView blk'
-> WrapTiebreakerView blk'
-> SingleEraOutput f blk'
forall b r. (b -> b -> r) -> b -> b -> r
maybeFlip WrapTiebreakerView blk'
-> WrapTiebreakerView blk' -> SingleEraOutput f blk'
cmp WrapTiebreakerView blk'
l' WrapTiebreakerView blk'
r'
     where
      -- We must re-wrap the inner tiebreakers into the type expected by 'cfg' (blk')
      -- The GADT equality ensures this is type-safe.
      l' :: WrapTiebreakerView blk'
l' = TiebreakerView (BlockProtocol blk') -> WrapTiebreakerView blk'
forall blk.
TiebreakerView (BlockProtocol blk) -> WrapTiebreakerView blk
WrapTiebreakerView TiebreakerView (BlockProtocol blk)
TiebreakerView (BlockProtocol blk')
l :: WrapTiebreakerView blk'
      r' :: WrapTiebreakerView blk'
r' = TiebreakerView (BlockProtocol blk') -> WrapTiebreakerView blk'
forall blk.
TiebreakerView (BlockProtocol blk) -> WrapTiebreakerView blk
WrapTiebreakerView TiebreakerView (BlockProtocol blk')
r :: WrapTiebreakerView blk'

      cmp :: WrapTiebreakerView blk'
-> WrapTiebreakerView blk' -> SingleEraOutput f blk'
cmp = cfg blk'
-> (WrapChainOrderConfig blk'
    -> ChainOrderConfig (WrapTiebreakerView blk'))
-> AcrossEraMode cfg f
-> WrapTiebreakerView blk'
-> WrapTiebreakerView blk'
-> SingleEraOutput f blk'
forall blk (cfg :: * -> *) (f :: [*] -> *).
ChainOrder (WrapTiebreakerView blk) =>
cfg blk
-> (WrapChainOrderConfig blk
    -> ChainOrderConfig (WrapTiebreakerView blk))
-> AcrossEraMode cfg f
-> WrapTiebreakerView blk
-> WrapTiebreakerView blk
-> SingleEraOutput f blk
applyAcrossEraMode cfg blk'
cfg WrapChainOrderConfig blk'
-> ChainOrderConfig (TiebreakerView (BlockProtocol blk'))
WrapChainOrderConfig blk'
-> ChainOrderConfig (WrapTiebreakerView blk')
forall blk.
WrapChainOrderConfig blk
-> ChainOrderConfig (TiebreakerView (BlockProtocol blk))
unwrapChainOrderConfig AcrossEraMode cfg f
mode
   where
    maybeFlip :: (b -> b -> r) -> b -> b -> r
    maybeFlip :: forall b r. (b -> b -> r) -> b -> b -> r
maybeFlip = case FlipArgs
flipArgs of
      FlipArgs
KeepArgs -> (b -> b -> r) -> b -> b -> r
forall a. a -> a
id
      FlipArgs
FlipArgs -> (b -> b -> r) -> b -> b -> r
forall a b c. (a -> b -> c) -> b -> a -> c
flip

acrossEraSelection ::
  forall xs cfg f.
  (All SingleEraBlock xs, AcrossEraOutput f) =>
  AcrossEraMode cfg f ->
  NP cfg xs ->
  Tails AcrossEraTiebreaker xs ->
  NS WrapTiebreakerView xs ->
  NS WrapTiebreakerView xs ->
  f xs
acrossEraSelection :: forall (xs :: [*]) (cfg :: * -> *) (f :: [*] -> *).
(All SingleEraBlock xs, AcrossEraOutput f) =>
AcrossEraMode cfg f
-> NP cfg xs
-> Tails AcrossEraTiebreaker xs
-> NS WrapTiebreakerView xs
-> NS WrapTiebreakerView xs
-> f xs
acrossEraSelection AcrossEraMode cfg f
mode = \NP cfg xs
cfg Tails AcrossEraTiebreaker xs
ffs NS WrapTiebreakerView xs
l NS WrapTiebreakerView xs
r ->
  NP cfg xs
-> Tails AcrossEraTiebreaker xs
-> (NS WrapTiebreakerView xs, NS WrapTiebreakerView xs)
-> f xs
forall (xs' :: [*]).
All SingleEraBlock xs' =>
NP cfg xs'
-> Tails AcrossEraTiebreaker xs'
-> (NS WrapTiebreakerView xs', NS WrapTiebreakerView xs')
-> f xs'
goBoth NP cfg xs
cfg Tails AcrossEraTiebreaker xs
ffs (NS WrapTiebreakerView xs
l, NS WrapTiebreakerView xs
r)
 where
  goBoth ::
    forall xs'.
    All SingleEraBlock xs' =>
    NP cfg xs' ->
    Tails AcrossEraTiebreaker xs' ->
    (NS WrapTiebreakerView xs', NS WrapTiebreakerView xs') ->
    f xs'
  goBoth :: forall (xs' :: [*]).
All SingleEraBlock xs' =>
NP cfg xs'
-> Tails AcrossEraTiebreaker xs'
-> (NS WrapTiebreakerView xs', NS WrapTiebreakerView xs')
-> f xs'
goBoth NP cfg xs'
_ Tails AcrossEraTiebreaker xs'
TNil = \(NS WrapTiebreakerView xs'
a, NS WrapTiebreakerView xs'
_) -> case NS WrapTiebreakerView xs'
a of {}
  goBoth (cfg x
cfg :* NP cfg xs1
cfgs) (TCons NP (AcrossEraTiebreaker x) xs1
fs Tails AcrossEraTiebreaker xs1
ffs') = \case
    (Z WrapTiebreakerView x
a, Z WrapTiebreakerView x
b) ->
      SingleEraOutput f x -> f (x : xs1)
forall x (xs :: [*]). SingleEraOutput f x -> f (x : xs)
forall (f :: [*] -> *) x (xs :: [*]).
AcrossEraOutput f =>
SingleEraOutput f x -> f (x : xs)
liftHead (SingleEraOutput f x -> f (x : xs1))
-> SingleEraOutput f x -> f (x : xs1)
forall a b. (a -> b) -> a -> b
$
        cfg x
-> (WrapChainOrderConfig x
    -> ChainOrderConfig (WrapTiebreakerView x))
-> AcrossEraMode cfg f
-> WrapTiebreakerView x
-> WrapTiebreakerView x
-> SingleEraOutput f x
forall blk (cfg :: * -> *) (f :: [*] -> *).
ChainOrder (WrapTiebreakerView blk) =>
cfg blk
-> (WrapChainOrderConfig blk
    -> ChainOrderConfig (WrapTiebreakerView blk))
-> AcrossEraMode cfg f
-> WrapTiebreakerView blk
-> WrapTiebreakerView blk
-> SingleEraOutput f blk
applyAcrossEraMode cfg x
cfg WrapChainOrderConfig x
-> ChainOrderConfig (TiebreakerView (BlockProtocol x))
WrapChainOrderConfig x -> ChainOrderConfig (WrapTiebreakerView x)
forall blk.
WrapChainOrderConfig blk
-> ChainOrderConfig (TiebreakerView (BlockProtocol blk))
unwrapChainOrderConfig AcrossEraMode cfg f
mode WrapTiebreakerView x
WrapTiebreakerView x
a WrapTiebreakerView x
WrapTiebreakerView x
b
    (Z WrapTiebreakerView x
a, S NS WrapTiebreakerView xs1
b) -> FlipArgs
-> WrapTiebreakerView x
-> NP cfg xs1
-> NP (AcrossEraTiebreaker x) xs1
-> NS WrapTiebreakerView xs1
-> f (x : xs1)
forall x (xs' :: [*]).
(SingleEraBlock x, All SingleEraBlock xs') =>
FlipArgs
-> WrapTiebreakerView x
-> NP cfg xs'
-> NP (AcrossEraTiebreaker x) xs'
-> NS WrapTiebreakerView xs'
-> f (x : xs')
goOne FlipArgs
KeepArgs WrapTiebreakerView x
a NP cfg xs1
cfgs NP (AcrossEraTiebreaker x) xs1
NP (AcrossEraTiebreaker x) xs1
fs NS WrapTiebreakerView xs1
NS WrapTiebreakerView xs1
b
    (S NS WrapTiebreakerView xs1
a, Z WrapTiebreakerView x
b) -> FlipArgs
-> WrapTiebreakerView x
-> NP cfg xs1
-> NP (AcrossEraTiebreaker x) xs1
-> NS WrapTiebreakerView xs1
-> f (x : xs1)
forall x (xs' :: [*]).
(SingleEraBlock x, All SingleEraBlock xs') =>
FlipArgs
-> WrapTiebreakerView x
-> NP cfg xs'
-> NP (AcrossEraTiebreaker x) xs'
-> NS WrapTiebreakerView xs'
-> f (x : xs')
goOne FlipArgs
FlipArgs WrapTiebreakerView x
b NP cfg xs1
cfgs NP (AcrossEraTiebreaker x) xs1
NP (AcrossEraTiebreaker x) xs1
fs NS WrapTiebreakerView xs1
NS WrapTiebreakerView xs1
a
    (S NS WrapTiebreakerView xs1
a, S NS WrapTiebreakerView xs1
b) ->
      f xs1 -> f (x : xs1)
forall (xs :: [*]) x. f xs -> f (x : xs)
forall (f :: [*] -> *) (xs :: [*]) x.
AcrossEraOutput f =>
f xs -> f (x : xs)
liftTail (f xs1 -> f (x : xs1)) -> f xs1 -> f (x : xs1)
forall a b. (a -> b) -> a -> b
$ NP cfg xs1
-> Tails AcrossEraTiebreaker xs1
-> (NS WrapTiebreakerView xs1, NS WrapTiebreakerView xs1)
-> f xs1
forall (xs' :: [*]).
All SingleEraBlock xs' =>
NP cfg xs'
-> Tails AcrossEraTiebreaker xs'
-> (NS WrapTiebreakerView xs', NS WrapTiebreakerView xs')
-> f xs'
goBoth NP cfg xs1
cfgs Tails AcrossEraTiebreaker xs1
Tails AcrossEraTiebreaker xs1
ffs' (NS WrapTiebreakerView xs1
NS WrapTiebreakerView xs1
a, NS WrapTiebreakerView xs1
NS WrapTiebreakerView xs1
b)

  goOne ::
    forall x xs'.
    (SingleEraBlock x, All SingleEraBlock xs') =>
    FlipArgs ->
    WrapTiebreakerView x ->
    NP cfg xs' ->
    NP (AcrossEraTiebreaker x) xs' ->
    NS WrapTiebreakerView xs' ->
    f (x ': xs')
  goOne :: forall x (xs' :: [*]).
(SingleEraBlock x, All SingleEraBlock xs') =>
FlipArgs
-> WrapTiebreakerView x
-> NP cfg xs'
-> NP (AcrossEraTiebreaker x) xs'
-> NS WrapTiebreakerView xs'
-> f (x : xs')
goOne FlipArgs
flipArgs WrapTiebreakerView x
a = NP cfg xs'
-> NP (AcrossEraTiebreaker x) xs'
-> NS WrapTiebreakerView xs'
-> f (x : xs')
forall (xs'' :: [*]).
All SingleEraBlock xs'' =>
NP cfg xs''
-> NP (AcrossEraTiebreaker x) xs''
-> NS WrapTiebreakerView xs''
-> f (x : xs'')
go
   where
    go ::
      forall xs''.
      All SingleEraBlock xs'' =>
      NP cfg xs'' ->
      NP (AcrossEraTiebreaker x) xs'' ->
      NS WrapTiebreakerView xs'' ->
      f (x ': xs'')
    go :: forall (xs'' :: [*]).
All SingleEraBlock xs'' =>
NP cfg xs''
-> NP (AcrossEraTiebreaker x) xs''
-> NS WrapTiebreakerView xs''
-> f (x : xs'')
go NP cfg xs''
_ NP (AcrossEraTiebreaker x) xs''
Nil NS WrapTiebreakerView xs''
b = case NS WrapTiebreakerView xs''
b of {}
    go (cfg x
cfg :* NP cfg xs1
_) (AcrossEraTiebreaker x x
f :* NP (AcrossEraTiebreaker x) xs1
_) (Z WrapTiebreakerView x
b) =
      f xs'' -> f (x : xs'')
forall (xs :: [*]) x. f xs -> f (x : xs)
forall (f :: [*] -> *) (xs :: [*]) x.
AcrossEraOutput f =>
f xs -> f (x : xs)
liftTail (f xs'' -> f (x : xs'')) -> f xs'' -> f (x : xs'')
forall a b. (a -> b) -> a -> b
$ SingleEraOutput f x -> f (x : xs1)
forall x (xs :: [*]). SingleEraOutput f x -> f (x : xs)
forall (f :: [*] -> *) x (xs :: [*]).
AcrossEraOutput f =>
SingleEraOutput f x -> f (x : xs)
liftHead (SingleEraOutput f x -> f (x : xs1))
-> SingleEraOutput f x -> f (x : xs1)
forall a b. (a -> b) -> a -> b
$ FlipArgs
-> AcrossEraMode cfg f
-> cfg x
-> WrapTiebreakerView x
-> WrapTiebreakerView x
-> AcrossEraTiebreaker x x
-> SingleEraOutput f x
forall blk blk' (cfg :: * -> *) (f :: [*] -> *).
SingleEraBlock blk =>
FlipArgs
-> AcrossEraMode cfg f
-> cfg blk'
-> WrapTiebreakerView blk
-> WrapTiebreakerView blk'
-> AcrossEraTiebreaker blk blk'
-> SingleEraOutput f blk'
acrossEras FlipArgs
flipArgs AcrossEraMode cfg f
mode cfg x
cfg WrapTiebreakerView x
a WrapTiebreakerView x
WrapTiebreakerView x
b AcrossEraTiebreaker x x
AcrossEraTiebreaker x x
f
    go (cfg x
_ :* NP cfg xs1
cfgs) (AcrossEraTiebreaker x x
_ :* NP (AcrossEraTiebreaker x) xs1
fs) (S NS WrapTiebreakerView xs1
b) =
      f (x : xs1) -> f (x : x : xs1)
forall x (zs :: [*]) y. f (x : zs) -> f (x : y : zs)
forall (f :: [*] -> *) x (zs :: [*]) y.
AcrossEraOutput f =>
f (x : zs) -> f (x : y : zs)
liftSkip (f (x : xs1) -> f (x : x : xs1)) -> f (x : xs1) -> f (x : x : xs1)
forall a b. (a -> b) -> a -> b
$ NP cfg xs1
-> NP (AcrossEraTiebreaker x) xs1
-> NS WrapTiebreakerView xs1
-> f (x : xs1)
forall (xs'' :: [*]).
All SingleEraBlock xs'' =>
NP cfg xs''
-> NP (AcrossEraTiebreaker x) xs''
-> NS WrapTiebreakerView xs''
-> f (x : xs'')
go NP cfg xs1
cfgs NP (AcrossEraTiebreaker x) xs1
NP (AcrossEraTiebreaker x) xs1
fs NS WrapTiebreakerView xs1
NS WrapTiebreakerView xs1
b