When wren's email moved this thread to the top of my inbox, I noticed that I never sent this draft I wrote. It gives some concrete code along the line of Wren's suggestion.
-----
The included code uses a little of this (singleton types) and a little of that (implicit configurations).
As is so often the case with Haskell discussions, I'm not sure if this is overkill for your actual needs. There might be simpler possible solutions, but this idea at least matches my rather literal interpretation of your email.
Also, I apologize if this approach is what you meant by "(Or, more or less equivalently, one can't write dependently typed functions, and trying to fake it at the type-level leads to the original problem.)"
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE Rank2Types #-}
> module STandIC where
A data type for naturals; I'm assuming you have something like a useful Arbitrary instance for these.
> data Nat = Z | S Nat
The corresponding singleton type.
> data Nat1 :: Nat -> * where
> Z1 :: Nat1 Z
> S1 :: Nat1 n -> Nat1 (S n)
Reification of a Nat; cf implicit configurations (ie prepose.pdf).
> reifyNat :: Nat -> (forall n. Nat1 n -> a) -> a
> reifyNat Z k = k Z1
> reifyNat (S n) k = reifyNat n $ k . S1
Here's my questionable assumption:
If the code you want to use arbitrary type-level naturals with
works for all type-level naturals, then it should be possible to
wrap it in a function that fits as the second argument to reifyNat.
That may be tricky to do. I'm not sure it's necessarily always possible in general; hence "questionable assumption". But maybe it'll work for you.
HTH. And I apologize if it's overkill; as Pedro was suggesting, there might be simpler ways.