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:
{-# LANGUAGE DataKinds, KindSignatures, ExistentialQuantification #-}
import GHC.TypeLits
data SomeNat = forall (n :: Nat). SomeNat (Sing n)
getSomeNat :: IO SomeNat
getSomeNat =
do x <- getLine
case reads x of
-- The use of `unsafeSingNat` is OK here because it is wrapped in `SomeNat`
-- so we are not assuming anything about the actual number.
[(n,_)] | n >= 0 -> return $ SomeNat $ unsafeSingNat n
_ -> putStrLn "Invalid number, try again." >> getSomeNat
main :: IO ()
main =
do x <- getSomeNat
case x of
SomeNat s -> polyFun s s
-- The argument of this function are always going to be the same.
-- (just an example, one could probably get more interesting properties)
polyFun :: Sing (n :: Nat) -> Sing n -> IO ()
polyFun x y = print (x,y)
I can elaborate more, just ask if this does not make sense. 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. 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.