Swap type argument order of Index

This will make it possible to use it in combination with `NP`.

ouroboros-consensus-cardano-test/src/Test/Consensus/Cardano/Examples.hs

@@ -86,7 +86,7 @@ combineEras = mconcat . hcollapse . hap eraInjections
 
     injExamples ::
          String
-      -> Index blk (CardanoEras Crypto)
+      -> Index (CardanoEras Crypto) blk
       -> Examples blk
       -> Examples (CardanoBlock Crypto)
     injExamples eraName idx =
@@ -107,7 +107,7 @@ instance Inject SomeResult where
       SomeResult (QueryIfCurrent (injectQuery idx q)) (Right r)
 
 instance Inject Examples where
-  inject startBounds (idx :: Index x xs) Golden.Examples {..} = Golden.Examples {
+  inject startBounds (idx :: Index xs x) Golden.Examples {..} = Golden.Examples {
         exampleBlock            = inj (Proxy @I)                  exampleBlock
       , exampleSerialisedBlock  = inj (Proxy @Serialised)         exampleSerialisedBlock
       , exampleHeader           = inj (Proxy @Header)             exampleHeader

ouroboros-consensus/src/Ouroboros/Consensus/HardFork/Combinator/Nary.hs

@@ -41,7 +41,7 @@ class Inject f where
        forall x xs. CanHardFork xs
     => Exactly xs History.Bound
        -- ^ Start bound of each era
-    -> Index x xs
+    -> Index xs x
     -> f x
     -> f (HardForkBlock xs)
 
@@ -52,7 +52,7 @@ inject' ::
      , Coercible a (f x)
      , Coercible b (f (HardForkBlock xs))
      )
-  => Proxy f -> Exactly xs History.Bound -> Index x xs -> a -> b
+  => Proxy f -> Exactly xs History.Bound -> Index xs x -> a -> b
 inject' _ startBounds idx = coerce . inject @f startBounds idx . coerce
 
 {-------------------------------------------------------------------------------
@@ -61,7 +61,7 @@ inject' _ startBounds idx = coerce . inject @f startBounds idx . coerce
 
 injectNestedCtxt_ ::
      forall f x xs a.
-     Index x xs
+     Index xs x
   -> NestedCtxt_ x f a
   -> NestedCtxt_ (HardForkBlock xs) f a
 injectNestedCtxt_ idx nc = case idx of
@@ -70,7 +70,7 @@ injectNestedCtxt_ idx nc = case idx of
 
 injectQuery ::
      forall x xs result.
-     Index x xs
+     Index xs x
   -> Query x result
   -> QueryIfCurrent xs result
 injectQuery idx q = case idx of
@@ -81,15 +81,15 @@ injectHardForkState ::
      forall f x xs.
      Exactly xs History.Bound
      -- ^ Start bound of each era
-  -> Index x xs
+  -> Index xs x
   -> f x
   -> HardForkState f xs
 injectHardForkState startBounds idx x =
     HardForkState $ go startBounds idx
   where
     go ::
          Exactly xs' History.Bound
-      -> Index x xs'
+      -> Index xs' x
       -> Telescope (K State.Past) (State.Current f) xs'
     go (ExactlyCons start _) IZ =
         TZ (State.Current { currentStart = start, currentState = x })
@@ -115,7 +115,7 @@ instance Inject SerialisedHeader where
       . serialisedHeaderToPair
 
 instance Inject WrapHeaderHash where
-  inject _ (idx :: Index x xs) =
+  inject _ (idx :: Index xs x) =
     case dictIndexAll (Proxy @SingleEraBlock) idx of
       Dict ->
           WrapHeaderHash

ouroboros-consensus/src/Ouroboros/Consensus/Util/SOP.hs

@@ -181,25 +181,25 @@ checkIsNonEmpty _ = case sList @xs of
   Indexing SOP types
 -------------------------------------------------------------------------------}
 
-data Index x xs where
-  IZ ::               Index x (x ': xs)
-  IS :: Index x xs -> Index x (y ': xs)
+data Index xs x where
+  IZ ::               Index (x ': xs) x
+  IS :: Index xs x -> Index (y ': xs) x
 
-dictIndexAll :: All c xs => Proxy c -> Index x xs -> Dict c x
+dictIndexAll :: All c xs => Proxy c -> Index xs x -> Dict c x
 dictIndexAll p = \case
     IZ      -> Dict
     IS idx' -> dictIndexAll p idx'
 
-injectNS :: forall f x xs. Index x xs -> f x -> NS f xs
+injectNS :: forall f x xs. Index xs x -> f x -> NS f xs
 injectNS idx x = case idx of
     IZ      -> Z x
     IS idx' -> S (injectNS idx' x)
 
 injectNS' ::
      forall f a b x xs. (Coercible a (f x), Coercible b (NS f xs))
-  => Proxy f -> Index x xs -> a -> b
+  => Proxy f -> Index xs x -> a -> b
 injectNS' _ idx = coerce . injectNS @f idx . coerce
 
-projectNP :: Index x xs -> NP f xs -> f x
+projectNP :: Index xs x -> NP f xs -> f x
 projectNP IZ        (x :* _) = x
 projectNP (IS idx) (_ :* xs) = projectNP idx xs