Add Type-level Nat-sized version of Block (BlockN)

[tekul]

This will be analogous to SList (which should probably be renamed to ListN).

[tekul]

I'm trying to write some tests and having doubts about the usability of the code. For example if I try to write a simple test using cons followed by uncons, the compiler complains (for uncons) that Natural (n+1) is out of bounds for Int. I have to add both NatWithinBound Int n and NatWithinBound Int (n+1)) to the test function. It then complains about CmpNat 0 (n+1) ~ 'LT and so on. It seems to all be part of the problem that ghc can't really add numbers in types, but I'm not sure how to get round this.

[vincenthz]

I think you're hitting the normal problem of current nats. at the moment the only way is the plugin: https://github.com/yav/type-nat-solver

If the code is ready it's probably fine to start pushing even without tests, we can probably already use for just simple constraint like hardcoded value for API like 16 for block size.

[tekul]

OK, thanks. I'll make a PR tomorrow. Have to go to Biel just now :).

On 15 Jun 2017 3:57 pm, "Vincent Hanquez" [email protected] wrote:

I think you're hitting the normal problem of current nats. at the moment the only way is the plugin: https://github.com/yav/type-nat-solver

If the code is ready it's probably fine to start pushing even without tests, we can probably already use for just simple constraint like hardcoded value for API like 16 for block size.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/haskell-foundation/foundation/issues/298#issuecomment-308735890, or mute the thread https://github.com/notifications/unsubscribe-auth/AALs6DVBqopwYw9f47m8uQnhKjWvu7wIks5sETeZgaJpZM4N1e8F .