I think I prefer your suggestion of using Unsigned over the current pull-request. If we are going to have a safe indexing function, we might as well go all the way. Also, don't you think that maybe the Pow2 suffix is too much?

Ok, the only complication there is that Unsigned is not currently imported, but I hope it won't introduce a cycle. I figured I'd throw in the -Pow2 to differentiate from at which I hadn't heard of before, and which also is a "safe index", but I'm happy to chuck it.

A third idea that just occurred to me now is to make finite sets a la Agda, and rewrite at with it. Then the index given to at can be "dynamic", and we can make an Unsigned n -> Fin (n ^ 2) conversion.

Yeah, probably best to update at to work on Fin, and make the suggested conversion from Unsigned to Fin. I suggest putting Fin in it's own module: CLaSH.Sized.Fin.

That all sounds good.

One last thing, now that we have arbitrary sized naturals in base, we could use them to implement BitVector, Unsigned, and Fin. Also, index_int could be index_word, and the negative check could be moved to (!!). Then at could skip the < 0 check.

Also, if we made a class like https://hackage.haskell.org/package/nats-0.1/docs/Numeric-Natural-Internal.html#t:Whole (that didn't make it to base-4.8, unfortunately), there there would be some use for a power of 2 safe index again.

What module are these arbitrary size natural ins?

https://hackage.haskell.org/package/base-4.8.0.0/docs/Numeric-Natural.html and GHC.Natural