Singletons/T150.hs:(0,0)-(0,0): Splicing declarations
    withOptions defaultOptions {genSingKindInsts = False}
      $ singletons
          $ lift
              [d| headVec :: Vec (Succ n) a -> a
                  headVec (VCons x _) = x
                  tailVec :: Vec (Succ n) a -> Vec n a
                  tailVec (VCons _ xs) = xs
                  (!) :: Vec n a -> Fin n -> a
                  VCons x _ ! FZ = x
                  VCons _ xs ! FS n = xs ! n
                  VNil ! n = case n of {}
                  mapVec :: (a -> b) -> Vec n a -> Vec n b
                  mapVec _ VNil = VNil
                  mapVec f (VCons x xs) = VCons (f x) (mapVec f xs)
                  symmetry :: Equal a b -> Equal b a
                  symmetry Reflexive = Reflexive
                  transitivity :: Equal a b -> Equal b c -> Equal a c
                  transitivity Reflexive Reflexive = Reflexive
                  
                  data Fin :: Nat -> Type
                    where
                      FZ :: Fin (Succ n)
                      FS :: Fin n -> Fin (Succ n)
                  data Foo :: Type -> Type
                    where
                      MkFoo1 :: Foo Bool
                      MkFoo2 :: Foo Ordering
                  data Vec :: Nat -> Type -> Type
                    where
                      VNil :: Vec Zero a
                      VCons :: a -> Vec n a -> Vec (Succ n) a
                  data Equal :: Type -> Type -> Type where Reflexive :: Equal a a
                  data HList :: [Type] -> Type
                    where
                      HNil :: HList '[]
                      HCons :: x -> HList xs -> HList (x : xs)
                  data Obj :: Type where Obj :: a -> Obj |]
  ======>
    data Fin :: Nat -> Type
      where
        FZ :: Fin ('Succ n)
        FS :: (Fin n) -> Fin ('Succ n)
    data Foo :: Type -> Type
      where
        MkFoo1 :: Foo Bool
        MkFoo2 :: Foo Ordering
    data Vec :: Nat -> Type -> Type
      where
        VNil :: Vec 'Zero a
        VCons :: a -> (Vec n a) -> Vec ('Succ n) a
    headVec :: Vec ('Succ n) a -> a
    headVec (VCons x _) = x
    tailVec :: Vec ('Succ n) a -> Vec n a
    tailVec (VCons _ xs) = xs
    (!) :: Vec n a -> Fin n -> a
    (!) (VCons x _) FZ = x
    (!) (VCons _ xs) (FS n) = (xs ! n)
    (!) VNil n = case n of {}
    mapVec :: (a -> b) -> Vec n a -> Vec n b
    mapVec _ VNil = VNil
    mapVec f (VCons x xs) = VCons (f x) (mapVec f xs)
    data Equal :: Type -> Type -> Type where Reflexive :: Equal a a
    symmetry :: Equal a b -> Equal b a
    symmetry Reflexive = Reflexive
    transitivity :: Equal a b -> Equal b c -> Equal a c
    transitivity Reflexive Reflexive = Reflexive
    data HList :: [Type] -> Type
      where
        HNil :: HList '[]
        HCons :: x -> (HList xs) -> HList ('(:) x xs)
    data Obj :: Type where Obj :: a -> Obj
    type FZSym0 :: Fin ('Succ n)
    type family FZSym0 :: Fin ('Succ n) where
      FZSym0 = FZ
    type FSSym0 :: (~>) (Fin n) (Fin ('Succ n))
    data FSSym0 :: (~>) (Fin n) (Fin ('Succ n))
      where
        FSSym0KindInference :: SameKind (Apply FSSym0 arg) (FSSym1 arg) =>
                               FSSym0 a0123456789876543210
    type instance Apply FSSym0 a0123456789876543210 = FS a0123456789876543210
    instance SuppressUnusedWarnings FSSym0 where
      suppressUnusedWarnings = snd ((,) FSSym0KindInference ())
    type FSSym1 :: Fin n -> Fin ('Succ n)
    type family FSSym1 (a0123456789876543210 :: Fin n) :: Fin ('Succ n) where
      FSSym1 a0123456789876543210 = FS a0123456789876543210
    type MkFoo1Sym0 :: Foo Bool
    type family MkFoo1Sym0 :: Foo Bool where
      MkFoo1Sym0 = MkFoo1
    type MkFoo2Sym0 :: Foo Ordering
    type family MkFoo2Sym0 :: Foo Ordering where
      MkFoo2Sym0 = MkFoo2
    type VNilSym0 :: Vec 'Zero a
    type family VNilSym0 :: Vec 'Zero a where
      VNilSym0 = VNil
    type VConsSym0 :: (~>) a ((~>) (Vec n a) (Vec ('Succ n) a))
    data VConsSym0 :: (~>) a ((~>) (Vec n a) (Vec ('Succ n) a))
      where
        VConsSym0KindInference :: SameKind (Apply VConsSym0 arg) (VConsSym1 arg) =>
                                  VConsSym0 a0123456789876543210
    type instance Apply VConsSym0 a0123456789876543210 = VConsSym1 a0123456789876543210
    instance SuppressUnusedWarnings VConsSym0 where
      suppressUnusedWarnings = snd ((,) VConsSym0KindInference ())
    type VConsSym1 :: a -> (~>) (Vec n a) (Vec ('Succ n) a)
    data VConsSym1 (a0123456789876543210 :: a) :: (~>) (Vec n a) (Vec ('Succ n) a)
      where
        VConsSym1KindInference :: SameKind (Apply (VConsSym1 a0123456789876543210) arg) (VConsSym2 a0123456789876543210 arg) =>
                                  VConsSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (VConsSym1 a0123456789876543210) a0123456789876543210 = VCons a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (VConsSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) VConsSym1KindInference ())
    type VConsSym2 :: a -> Vec n a -> Vec ('Succ n) a
    type family VConsSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Vec n a) :: Vec ('Succ n) a where
      VConsSym2 a0123456789876543210 a0123456789876543210 = VCons a0123456789876543210 a0123456789876543210
    type ReflexiveSym0 :: Equal a a
    type family ReflexiveSym0 :: Equal a a where
      ReflexiveSym0 = Reflexive
    type HNilSym0 :: HList '[]
    type family HNilSym0 :: HList '[] where
      HNilSym0 = HNil
    type HConsSym0 :: (~>) x ((~>) (HList xs) (HList ('(:) x xs)))
    data HConsSym0 :: (~>) x ((~>) (HList xs) (HList ('(:) x xs)))
      where
        HConsSym0KindInference :: SameKind (Apply HConsSym0 arg) (HConsSym1 arg) =>
                                  HConsSym0 a0123456789876543210
    type instance Apply HConsSym0 a0123456789876543210 = HConsSym1 a0123456789876543210
    instance SuppressUnusedWarnings HConsSym0 where
      suppressUnusedWarnings = snd ((,) HConsSym0KindInference ())
    type HConsSym1 :: x -> (~>) (HList xs) (HList ('(:) x xs))
    data HConsSym1 (a0123456789876543210 :: x) :: (~>) (HList xs) (HList ('(:) x xs))
      where
        HConsSym1KindInference :: SameKind (Apply (HConsSym1 a0123456789876543210) arg) (HConsSym2 a0123456789876543210 arg) =>
                                  HConsSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (HConsSym1 a0123456789876543210) a0123456789876543210 = HCons a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (HConsSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) HConsSym1KindInference ())
    type HConsSym2 :: x -> HList xs -> HList ('(:) x xs)
    type family HConsSym2 (a0123456789876543210 :: x) (a0123456789876543210 :: HList xs) :: HList ('(:) x xs) where
      HConsSym2 a0123456789876543210 a0123456789876543210 = HCons a0123456789876543210 a0123456789876543210
    type ObjSym0 :: (~>) a Obj
    data ObjSym0 :: (~>) a Obj
      where
        ObjSym0KindInference :: SameKind (Apply ObjSym0 arg) (ObjSym1 arg) =>
                                ObjSym0 a0123456789876543210
    type instance Apply ObjSym0 a0123456789876543210 = Obj a0123456789876543210
    instance SuppressUnusedWarnings ObjSym0 where
      suppressUnusedWarnings = snd ((,) ObjSym0KindInference ())
    type ObjSym1 :: a -> Obj
    type family ObjSym1 (a0123456789876543210 :: a) :: Obj where
      ObjSym1 a0123456789876543210 = Obj a0123456789876543210
    type family Case_0123456789876543210 n t where
    type TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c))
    data TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c))
      where
        TransitivitySym0KindInference :: SameKind (Apply TransitivitySym0 arg) (TransitivitySym1 arg) =>
                                         TransitivitySym0 a0123456789876543210
    type instance Apply TransitivitySym0 a0123456789876543210 = TransitivitySym1 a0123456789876543210
    instance SuppressUnusedWarnings TransitivitySym0 where
      suppressUnusedWarnings = snd ((,) TransitivitySym0KindInference ())
    type TransitivitySym1 :: Equal a b -> (~>) (Equal b c) (Equal a c)
    data TransitivitySym1 (a0123456789876543210 :: Equal a b) :: (~>) (Equal b c) (Equal a c)
      where
        TransitivitySym1KindInference :: SameKind (Apply (TransitivitySym1 a0123456789876543210) arg) (TransitivitySym2 a0123456789876543210 arg) =>
                                         TransitivitySym1 a0123456789876543210 a0123456789876543210
    type instance Apply (TransitivitySym1 a0123456789876543210) a0123456789876543210 = Transitivity a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (TransitivitySym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) TransitivitySym1KindInference ())
    type TransitivitySym2 :: Equal a b -> Equal b c -> Equal a c
    type family TransitivitySym2 (a0123456789876543210 :: Equal a b) (a0123456789876543210 :: Equal b c) :: Equal a c where
      TransitivitySym2 a0123456789876543210 a0123456789876543210 = Transitivity a0123456789876543210 a0123456789876543210
    type SymmetrySym0 :: (~>) (Equal a b) (Equal b a)
    data SymmetrySym0 :: (~>) (Equal a b) (Equal b a)
      where
        SymmetrySym0KindInference :: SameKind (Apply SymmetrySym0 arg) (SymmetrySym1 arg) =>
                                     SymmetrySym0 a0123456789876543210
    type instance Apply SymmetrySym0 a0123456789876543210 = Symmetry a0123456789876543210
    instance SuppressUnusedWarnings SymmetrySym0 where
      suppressUnusedWarnings = snd ((,) SymmetrySym0KindInference ())
    type SymmetrySym1 :: Equal a b -> Equal b a
    type family SymmetrySym1 (a0123456789876543210 :: Equal a b) :: Equal b a where
      SymmetrySym1 a0123456789876543210 = Symmetry a0123456789876543210
    type MapVecSym0 :: (~>) ((~>) a b) ((~>) (Vec n a) (Vec n b))
    data MapVecSym0 :: (~>) ((~>) a b) ((~>) (Vec n a) (Vec n b))
      where
        MapVecSym0KindInference :: SameKind (Apply MapVecSym0 arg) (MapVecSym1 arg) =>
                                   MapVecSym0 a0123456789876543210
    type instance Apply MapVecSym0 a0123456789876543210 = MapVecSym1 a0123456789876543210
    instance SuppressUnusedWarnings MapVecSym0 where
      suppressUnusedWarnings = snd ((,) MapVecSym0KindInference ())
    type MapVecSym1 :: (~>) a b -> (~>) (Vec n a) (Vec n b)
    data MapVecSym1 (a0123456789876543210 :: (~>) a b) :: (~>) (Vec n a) (Vec n b)
      where
        MapVecSym1KindInference :: SameKind (Apply (MapVecSym1 a0123456789876543210) arg) (MapVecSym2 a0123456789876543210 arg) =>
                                   MapVecSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (MapVecSym1 a0123456789876543210) a0123456789876543210 = MapVec a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (MapVecSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) MapVecSym1KindInference ())
    type MapVecSym2 :: (~>) a b -> Vec n a -> Vec n b
    type family MapVecSym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Vec n a) :: Vec n b where
      MapVecSym2 a0123456789876543210 a0123456789876543210 = MapVec a0123456789876543210 a0123456789876543210
    type (!@#@$) :: (~>) (Vec n a) ((~>) (Fin n) a)
    data (!@#@$) :: (~>) (Vec n a) ((~>) (Fin n) a)
      where
        (:!@#@$###) :: SameKind (Apply (!@#@$) arg) ((!@#@$$) arg) =>
                       (!@#@$) a0123456789876543210
    type instance Apply (!@#@$) a0123456789876543210 = (!@#@$$) a0123456789876543210
    instance SuppressUnusedWarnings (!@#@$) where
      suppressUnusedWarnings = snd ((,) (:!@#@$###) ())
    type (!@#@$$) :: Vec n a -> (~>) (Fin n) a
    data (!@#@$$) (a0123456789876543210 :: Vec n a) :: (~>) (Fin n) a
      where
        (:!@#@$$###) :: SameKind (Apply ((!@#@$$) a0123456789876543210) arg) ((!@#@$$$) a0123456789876543210 arg) =>
                        (!@#@$$) a0123456789876543210 a0123456789876543210
    type instance Apply ((!@#@$$) a0123456789876543210) a0123456789876543210 = (!) a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings ((!@#@$$) a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) (:!@#@$$###) ())
    type (!@#@$$$) :: Vec n a -> Fin n -> a
    type family (!@#@$$$) (a0123456789876543210 :: Vec n a) (a0123456789876543210 :: Fin n) :: a where
      (!@#@$$$) a0123456789876543210 a0123456789876543210 = (!) a0123456789876543210 a0123456789876543210
    type TailVecSym0 :: (~>) (Vec ('Succ n) a) (Vec n a)
    data TailVecSym0 :: (~>) (Vec ('Succ n) a) (Vec n a)
      where
        TailVecSym0KindInference :: SameKind (Apply TailVecSym0 arg) (TailVecSym1 arg) =>
                                    TailVecSym0 a0123456789876543210
    type instance Apply TailVecSym0 a0123456789876543210 = TailVec a0123456789876543210
    instance SuppressUnusedWarnings TailVecSym0 where
      suppressUnusedWarnings = snd ((,) TailVecSym0KindInference ())
    type TailVecSym1 :: Vec ('Succ n) a -> Vec n a
    type family TailVecSym1 (a0123456789876543210 :: Vec ('Succ n) a) :: Vec n a where
      TailVecSym1 a0123456789876543210 = TailVec a0123456789876543210
    type HeadVecSym0 :: (~>) (Vec ('Succ n) a) a
    data HeadVecSym0 :: (~>) (Vec ('Succ n) a) a
      where
        HeadVecSym0KindInference :: SameKind (Apply HeadVecSym0 arg) (HeadVecSym1 arg) =>
                                    HeadVecSym0 a0123456789876543210
    type instance Apply HeadVecSym0 a0123456789876543210 = HeadVec a0123456789876543210
    instance SuppressUnusedWarnings HeadVecSym0 where
      suppressUnusedWarnings = snd ((,) HeadVecSym0KindInference ())
    type HeadVecSym1 :: Vec ('Succ n) a -> a
    type family HeadVecSym1 (a0123456789876543210 :: Vec ('Succ n) a) :: a where
      HeadVecSym1 a0123456789876543210 = HeadVec a0123456789876543210
    type Transitivity :: Equal a b -> Equal b c -> Equal a c
    type family Transitivity (a :: Equal a b) (a :: Equal b c) :: Equal a c where
      Transitivity Reflexive Reflexive = ReflexiveSym0
    type Symmetry :: Equal a b -> Equal b a
    type family Symmetry (a :: Equal a b) :: Equal b a where
      Symmetry Reflexive = ReflexiveSym0
    type MapVec :: (~>) a b -> Vec n a -> Vec n b
    type family MapVec (a :: (~>) a b) (a :: Vec n a) :: Vec n b where
      MapVec _ VNil = VNilSym0
      MapVec f (VCons x xs) = Apply (Apply VConsSym0 (Apply f x)) (Apply (Apply MapVecSym0 f) xs)
    type (!) :: Vec n a -> Fin n -> a
    type family (!) (a :: Vec n a) (a :: Fin n) :: a where
      (!) (VCons x _) FZ = x
      (!) (VCons _ xs) (FS n) = Apply (Apply (!@#@$) xs) n
      (!) VNil n = Case_0123456789876543210 n n
    type TailVec :: Vec ('Succ n) a -> Vec n a
    type family TailVec (a :: Vec ('Succ n) a) :: Vec n a where
      TailVec (VCons _ xs) = xs
    type HeadVec :: Vec ('Succ n) a -> a
    type family HeadVec (a :: Vec ('Succ n) a) :: a where
      HeadVec (VCons x _) = x
    sTransitivity ::
      (forall (t :: Equal a b) (t :: Equal b c).
       Sing t
       -> Sing t
          -> Sing (Apply (Apply TransitivitySym0 t) t :: Equal a c) :: Type)
    sSymmetry ::
      (forall (t :: Equal a b).
       Sing t -> Sing (Apply SymmetrySym0 t :: Equal b a) :: Type)
    sMapVec ::
      (forall (t :: (~>) a b) (t :: Vec n a).
       Sing t
       -> Sing t
          -> Sing (Apply (Apply MapVecSym0 t) t :: Vec n b) :: Type)
    (%!) ::
      (forall (t :: Vec n a) (t :: Fin n).
       Sing t -> Sing t -> Sing (Apply (Apply (!@#@$) t) t :: a) :: Type)
    sTailVec ::
      (forall (t :: Vec ('Succ n) a).
       Sing t -> Sing (Apply TailVecSym0 t :: Vec n a) :: Type)
    sHeadVec ::
      (forall (t :: Vec ('Succ n) a).
       Sing t -> Sing (Apply HeadVecSym0 t :: a) :: Type)
    sTransitivity SReflexive SReflexive = SReflexive
    sSymmetry SReflexive = SReflexive
    sMapVec _ SVNil = SVNil
    sMapVec (sF :: Sing f) (SVCons (sX :: Sing x) (sXs :: Sing xs))
      = applySing
          (applySing (singFun2 @VConsSym0 SVCons) (applySing sF sX))
          (applySing (applySing (singFun2 @MapVecSym0 sMapVec) sF) sXs)
    (%!) (SVCons (sX :: Sing x) _) SFZ = sX
    (%!) (SVCons _ (sXs :: Sing xs)) (SFS (sN :: Sing n))
      = applySing (applySing (singFun2 @(!@#@$) (%!)) sXs) sN
    (%!) SVNil (sN :: Sing n)
      = id @(Sing (Case_0123456789876543210 n n)) (case sN of {})
    sTailVec (SVCons _ (sXs :: Sing xs)) = sXs
    sHeadVec (SVCons (sX :: Sing x) _) = sX
    instance SingI (TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c))) where
      sing = singFun2 @TransitivitySym0 sTransitivity
    instance SingI d =>
             SingI (TransitivitySym1 (d :: Equal a b) :: (~>) (Equal b c) (Equal a c)) where
      sing
        = singFun1
            @(TransitivitySym1 (d :: Equal a b)) (sTransitivity (sing @d))
    instance SingI1 (TransitivitySym1 :: Equal a b
                                         -> (~>) (Equal b c) (Equal a c)) where
      liftSing (s :: Sing (d :: Equal a b))
        = singFun1 @(TransitivitySym1 (d :: Equal a b)) (sTransitivity s)
    instance SingI (SymmetrySym0 :: (~>) (Equal a b) (Equal b a)) where
      sing = singFun1 @SymmetrySym0 sSymmetry
    instance SingI (MapVecSym0 :: (~>) ((~>) a b) ((~>) (Vec n a) (Vec n b))) where
      sing = singFun2 @MapVecSym0 sMapVec
    instance SingI d =>
             SingI (MapVecSym1 (d :: (~>) a b) :: (~>) (Vec n a) (Vec n b)) where
      sing = singFun1 @(MapVecSym1 (d :: (~>) a b)) (sMapVec (sing @d))
    instance SingI1 (MapVecSym1 :: (~>) a b
                                   -> (~>) (Vec n a) (Vec n b)) where
      liftSing (s :: Sing (d :: (~>) a b))
        = singFun1 @(MapVecSym1 (d :: (~>) a b)) (sMapVec s)
    instance SingI ((!@#@$) :: (~>) (Vec n a) ((~>) (Fin n) a)) where
      sing = singFun2 @(!@#@$) (%!)
    instance SingI d =>
             SingI ((!@#@$$) (d :: Vec n a) :: (~>) (Fin n) a) where
      sing = singFun1 @((!@#@$$) (d :: Vec n a)) ((%!) (sing @d))
    instance SingI1 ((!@#@$$) :: Vec n a -> (~>) (Fin n) a) where
      liftSing (s :: Sing (d :: Vec n a))
        = singFun1 @((!@#@$$) (d :: Vec n a)) ((%!) s)
    instance SingI (TailVecSym0 :: (~>) (Vec ('Succ n) a) (Vec n a)) where
      sing = singFun1 @TailVecSym0 sTailVec
    instance SingI (HeadVecSym0 :: (~>) (Vec ('Succ n) a) a) where
      sing = singFun1 @HeadVecSym0 sHeadVec
    data SFin :: forall (a :: Nat). Fin a -> Type
      where
        SFZ :: forall n. SFin (FZ :: Fin ('Succ n))
        SFS :: forall n (n :: Fin n).
               (Sing n) -> SFin (FS n :: Fin ('Succ n))
    type instance Sing @(Fin a) = SFin
    data SFoo :: forall (a :: Type). Foo a -> Type
      where
        SMkFoo1 :: SFoo (MkFoo1 :: Foo Bool)
        SMkFoo2 :: SFoo (MkFoo2 :: Foo Ordering)
    type instance Sing @(Foo a) = SFoo
    data SVec :: forall (a :: Nat) (a :: Type). Vec a a -> Type
      where
        SVNil :: forall a. SVec (VNil :: Vec 'Zero a)
        SVCons :: forall a n (n :: a) (n :: Vec n a).
                  (Sing n) -> (Sing n) -> SVec (VCons n n :: Vec ('Succ n) a)
    type instance Sing @(Vec a a) = SVec
    data SEqual :: forall (a :: Type) (a :: Type). Equal a a -> Type
      where SReflexive :: forall a. SEqual (Reflexive :: Equal a a)
    type instance Sing @(Equal a a) = SEqual
    data SHList :: forall (a :: [Type]). HList a -> Type
      where
        SHNil :: SHList (HNil :: HList '[])
        SHCons :: forall x xs (n :: x) (n :: HList xs).
                  (Sing n) -> (Sing n) -> SHList (HCons n n :: HList ('(:) x xs))
    type instance Sing @(HList a) = SHList
    data SObj :: Obj -> Type
      where SObj :: forall a (n :: a). (Sing n) -> SObj (Obj n :: Obj)
    type instance Sing @Obj = SObj
    instance SingI FZ where
      sing = SFZ
    instance SingI n => SingI (FS (n :: Fin n)) where
      sing = SFS sing
    instance SingI1 FS where
      liftSing = SFS
    instance SingI (FSSym0 :: (~>) (Fin n) (Fin ('Succ n))) where
      sing = singFun1 @FSSym0 SFS
    instance SingI MkFoo1 where
      sing = SMkFoo1
    instance SingI MkFoo2 where
      sing = SMkFoo2
    instance SingI VNil where
      sing = SVNil
    instance (SingI n, SingI n) =>
             SingI (VCons (n :: a) (n :: Vec n a)) where
      sing = SVCons sing sing
    instance SingI n => SingI1 (VCons (n :: a)) where
      liftSing = SVCons sing
    instance SingI2 VCons where
      liftSing2 = SVCons
    instance SingI (VConsSym0 :: (~>) a ((~>) (Vec n a) (Vec ('Succ n) a))) where
      sing = singFun2 @VConsSym0 SVCons
    instance SingI d =>
             SingI (VConsSym1 (d :: a) :: (~>) (Vec n a) (Vec ('Succ n) a)) where
      sing = singFun1 @(VConsSym1 (d :: a)) (SVCons (sing @d))
    instance SingI1 (VConsSym1 :: a
                                  -> (~>) (Vec n a) (Vec ('Succ n) a)) where
      liftSing (s :: Sing (d :: a))
        = singFun1 @(VConsSym1 (d :: a)) (SVCons s)
    instance SingI Reflexive where
      sing = SReflexive
    instance SingI HNil where
      sing = SHNil
    instance (SingI n, SingI n) =>
             SingI (HCons (n :: x) (n :: HList xs)) where
      sing = SHCons sing sing
    instance SingI n => SingI1 (HCons (n :: x)) where
      liftSing = SHCons sing
    instance SingI2 HCons where
      liftSing2 = SHCons
    instance SingI (HConsSym0 :: (~>) x ((~>) (HList xs) (HList ('(:) x xs)))) where
      sing = singFun2 @HConsSym0 SHCons
    instance SingI d =>
             SingI (HConsSym1 (d :: x) :: (~>) (HList xs) (HList ('(:) x xs))) where
      sing = singFun1 @(HConsSym1 (d :: x)) (SHCons (sing @d))
    instance SingI1 (HConsSym1 :: x
                                  -> (~>) (HList xs) (HList ('(:) x xs))) where
      liftSing (s :: Sing (d :: x))
        = singFun1 @(HConsSym1 (d :: x)) (SHCons s)
    instance SingI n => SingI (Obj (n :: a)) where
      sing = SObj sing
    instance SingI1 Obj where
      liftSing = SObj
    instance SingI (ObjSym0 :: (~>) a Obj) where
      sing = singFun1 @ObjSym0 SObj