How to construct a array indexed by my custom index

[oxinabox]

So for purposes of avoiding axis confusing i wanted to make a new index type.
So I could check at compile time my indexes were in agreement.

After some looking at the prelude i came up with

data HourIx k [Ix k] =
    AsHourIx i:k

instance {q:Type} [Ix q] Ix (HourIx q)
  getSize = \(). size q
  ordinal = \(AsHourIx j). ordinal j
  unsafeFromOrdinal = \j. AsHourIx $ unsafeFromOrdinal q j

Now I am trying to work out how to create something with that as it's index.

:p [1.4, 5.4, -2.3] : ((HourIx (Fin 3))=>Float32)

seemed vaguely promising.
But that errors with

Type error:
Expected: ((HourIx (Fin 3)) => Float32)
  Actual: ((Fin 3) => Float32)
If attempting to construct a fixed-size table not indexed by 'Fin n' for some n, this error may indicate there was not enough information to infer a concrete index set; try adding an explicit annotation.

:p [1.4, 5.4, -2.3] : ((HourIx (Fin 3))=>Float32)
   ^^^^^^^^^^^^^^^^^

reindex seems promising but i can't workout how to use that at all, it doesn;t hafve any docs or direct tests.

[apaszke]

Whoops, sorry for letting this slip! The good news is that I just tried this, and it seems to work now:

data HourIx k [Ix k] =
    AsHourIx i:k

instance {q:Type} [Ix q] Ix (HourIx q)
  size = size q
  ordinal = \(AsHourIx j). ordinal j
  unsafe_from_ordinal = \j. AsHourIx $ unsafe_from_ordinal q j

[1.4, 5.4, -2.3] :: ((HourIx (Fin 3))=>Float32)
> [1.4, 5.4, -2.3]@(HourIx (Fin 3))