[Haskell-cafe] How to call hUpdateAtHNat with a value known only at runtime

[Phil Darnowsky]

Hello all,

I'm working on something that involves HLists where I'm making use of 
the hUpdateAtHNat function for array-like semantics, which works great 
if you know the index of the element you want at compile time:

Prelude> :module +Data.HList

Prelude Data.HList> let hl = hEnd $ hBuild "foobar" 123 True
Loading [a bunch of packages]

Prelude Data.HList> hl
H["foobar", 123, True]

Prelude Data.HList> hUpdateAtHNat hZero 90909 hl
H[90909, 123, True]

Prelude Data.HList> hUpdateAtHNat (hSucc hZero) 90909 hl
H["foobar", 90909, True]

Prelude Data.HList> hUpdateAtHNat (hSucc $ hSucc hZero) 90909 hl
H["foobar", 123, 90909]


So far so good. What's giving me trouble is figuring out how to update 
at an arbitrary index, where that index is only known at runtime, 
because hZero and hSucc are of different types:

Prelude Data.HList> :t hZero
hZero :: Proxy 'HZero

Prelude Data.HList> :t hSucc hZero
hSucc hZero :: Proxy ('HSucc 'HZero)


What I'd ideally like is some kind of function intToHNatProxy that would 
take an Int and return a Proxy of the appropriate type, but I so far 
only kinda sorta understand how proxies and lifted types work, so I 
haven't yet succeeded in constructing one. Any advice would be very welcome.

Thanks,
Phil