Hello Iavor,
One way to achieve the additional static checking is to use values of type `Sing (n :: Nat)` in the places where you've used `Integer` (and parameterize data structures by the `n`). If the code is fully polymorphic in the `n`, then you can use it with values whose types as not statically know by using an existential. Here is an example: […] I can elaborate more, just ask if this does not make sense.
Thanks for the example, it is very clear.
One issue at the moment is that you have to pass the explicit `Sing` values everywhere, and it is a lot more convenient to use the `SingI` class in GHC.TypeLits.
Right. Apart from the inconvenience, it seems this approach doesn't allow the 'Num' instance that I'm after: I can define a 'Num' instance for this type containing the 'Sing (n :: Nat)', but only when 'd' is an instance of 'SingI'.
Unfortunately at the moment this only works for types that are statically known at compile time. I think that we should be able to find a way to work around this, but we're not quite there yet.
OK. If there is progress in this area, I would be very interested! Thanks and regards, Arie