How to create Arbitrary instance for dependent types?

Learn
5

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

{-# 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
4 Likes