Как преобразовать значение в тип с помощью withKnownNat

Я нашел функции withKnownNat и withSomeSNat в GHC.TypeNats. По их сигнатурам можно применить функцию к параметру динамического типа. Если это невозможно, то для чего нужны эти функции? Практических примеров не так много.

withSomeSNat :: Natural -> (forall (n :: Nat). SNat n -> r) -> r 
withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r 

Первая попытка объединить эти функции сталкивается с жалобой от средства проверки типов.

 dynat :: [()]
 dynat = withSomeSNat 3 (`withKnownNat` props)

 props :: forall n. KnownNat n => [()]
 props = []

Could not deduce ‘KnownNat n0’ arising from a use of ‘props'’
from the context: KnownNat n
    bound by a type expected by the context:
               KnownNat n => [()]

Обновлять

Мне показалось полезным обернуть шаблон из ответа в следующую служебную функцию для тестов QuickCheck:

applyAsNatType :: 
  forall a. 
  (forall n. KnownNat n => SNat n -> a) -> Natural -> a
applyAsNatType f x = x `withSomeSNat` go
  where
    go :: forall n. SNat n -> a
    go n = n `withKnownNat` f n

foo :: forall n. KnownNat n => SNat n -> Property
foo _ = monadicIO $ do
  ps :: Foo n <- liftIO (generate arbitrary)
  liftIO (putStrLn $ "ps = " <> show ps)

test_Tree = testProperty "foo" (applyAsNatType foo)