Sigma types in Haskell

SigmaExample.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PackageImports #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module SigmaExample where

import                  Data.Kind
import "singleton-nats" Data.Nat
import "singletons"     Data.Singletons.Prelude
import "singletons"     Data.Singletons.TH

data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t
infixr 4 :&:

data Vec :: Type -> Nat -> Type where
  VNil :: Vec a Z
  (:>) :: a -> Vec a n -> Vec a (S n)
infixr 5 :>

$(singletons
    [d| len :: [a] -> Nat
        len []     = Z
        len (_:xs) = S (len xs) |])

slistToVec :: forall (a :: Type) (z :: [a]). SingKind a
           => SList z -> Vec (Demote a) (Len z)
slistToVec SNil           = VNil
slistToVec (x `SCons` xs) = fromSing x :> slistToVec xs

listToVec :: SingKind a => [Demote a] -> Sigma Nat (TyCon1 (Vec (Demote a)))
listToVec x = withSomeSing x $ \sX -> sLen sX :&: slistToVec sX