Singletonize functions that already use singletons

[greatBigDot]

$(singletons [d|
  data Nat = Z | S Nat
  data Vec n a where
    VNil  :: Vec 'Z a
    (:::) :: a -> Vec n a -> Vec ('S n) a
|])

I frequently find myself wanting to singletonize functions that already use singletons, but since singletons can't do that I have to write it by hand. E.g., consider the vector version of replicate:

vReplicate :: SNat n -> a -> Vec n a
vReplicate SZ _ = VNil
vReplicate (SS n) x = x ::: vReplicate n x

It'd be nice if wrapping that in $(singletons [d| ... |]) automatically generated:

type family VReplicate (n :: Nat) (x :: a) :: Vec n a where
  VReplicate 'Z _ = 'VNil
  VReplicate ('S n) x = x '::: VReplicate n x

sVReplicate :: SNat n -> Sing (x :: a) -> SVec (VReplicate n x)
sVReplicate SZ _ = SVNil
sVReplicate (SS n) x = x :%:: sVReplicate n x

As well as all the defunctionalization symbols and whatnot.

Instead, it tries to generate things like sVReplicate :: Sing (n' :: SNat n) -> ...; as far as I'm aware, meta-singleton types like that are never actually useful.

I guess one problem would be in telling whether or not a type is a singleton, so you know when to prepend an S; would you need to add a typeclass to store the relationship between a type and its singleton type or something?

(My apologies if this idea doesn't generalize to more advanced stuff; I've only tried it on simple things like vReplicate, and so far there's always been a unique obvious way to singletonize everything manually.)

[RyanGlScott]

This idea seems tempting, but the more I think about it, the trickier it sounds. To see why, compare the types of vReplicate and VReplicate:

     vReplicate :: forall n a. SNat   n -> a -> Vec n a
type VReplicate :: forall   a. forall n -> a -> Vec n a

Note that in vReplicate, n is quantified invisibly, whereas in VReplicate, n is quantified visibly. This is a subtle but important distinction, and making this work in singletons would require some care to massage the foralls just right. That might be possible in this example, but I worry about more complicated examples. For example, consider this:

vTabulate :: forall n a. SNat n -> (Fin n -> a) -> Vec n a

This should promote to forall a. forall n -> (Fin n ~> a) -> Vec n a. But what if the arguments were reversed?

vTabulate' :: forall n a. (Fin n -> a) -> SNat n -> Vec n a

A naïve attempt at promoting this would yield forall a. (Fin n ~> a) -> forall n -> Vec n a. But this is ill scoped, as the n in Fin n is used before it is quantified!

Besides that, another complication is that this wouldn't work at all for data contructors. If you wrote:

newtype MySNat :: Nat -> Type where where
  MkMySNat :: SNat n -> MySNat n

Then there's no way to write a promoted version of this using a visible forall, as visible dependent quantification is not allowed in data constructors.