# How to create Arbitrary instance for dependent types?

**URL:** <https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990>\
**Category:** Learn\
**Created:** [July 13, 2023, 9:19am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990 "2023-07-13T09:19:42Z")\
**Posts on this page:** 1\
**Showing post:** 5

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [July 13, 2023, 10:11am UTC](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/5 "2023-07-13T10:11:08Z")

</div>

Here’s a more complete solution. Does it do what you want?

```haskell
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}

import Test.QuickCheck
import Data.Reflection
import GHC.TypeLits
import Data.Kind
import Data.Proxy

data SomeVect a where
    SomeVect :: KnownNat n => Vect n a -> SomeVect a

example :: Arbitrary a => Gen (SomeVect a)
example = do
  i <- arbitrary
  reifyNat i $ \(_ :: Proxy n) -> do
    v <- replicateV @n arbitrary
    pure (SomeVect v)

----

data Vect (n :: Nat) (a :: Type) where

replicateV :: forall n m a. Monad m => m a -> m (Vect n a)
replicateV = undefined

```

---

_[View the full topic](https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990)._