How to promote value into type with withKnownNat

I found functions withKnownNat and withSomeSNat in GHC.TypeNats. According to their signatures it is possible to apply function to a dynamic type parameter. If it is not possible then the purpose of having these functions? There is not many practical examples.

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

First attempt to combine these functions encounters a complain from the type checker.

 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 => [()]

Update

I found useful to wrap the pattern from the answer into following utility function for QuickCheck tests:

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)

Solution

The type signature for props leaves the type variable n ambiguous. One solution is to write something like:

dynat :: [()]
dynat = withSomeSNat 3 go
  where go :: forall n. SNat n -> [()]
        go s = withKnownNat s $ props @n

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

Note that if props has a non-ambiguous type, then your original approach works fine:

{-# LANGUAGE DataKinds #-}

module Nats where

import GHC.TypeNats

data Foo n = Foo

dynat :: Foo 3
dynat = withSomeSNat 3 (`withKnownNat` props)

props :: forall n. KnownNat n => Foo n
props = Foo