Hello, In your function, the type `n`, and thus also the value of the argument, would have to be known at compile time. I'm not sure if you could make it to work. However, you can use the reflection package (https://hackage.haskell.org/package/reflection) where you can find a `reifyNat` function ( https://hackage.haskell.org/package/reflection-2.1.2/docs/Data-Reflection.ht... ) that lets you create a "temporary" type that never escapes the callback you give to it, and so it doesn't have to be known at compile time: reifyNat :: forall r. Integer -> (forall n. KnownNat n => Proxy n -> r) -> r The only requirement is that type `r` doesn't depend in any way on `n` (but the computation itself can use it, it just has to return the same type every time). Best regards, Marcin Mrotek