T567.golden

Singletons/T567.hs:(0,0)-(0,0): Splicing declarations
    withOptions defaultOptions {genSingKindInsts = False}
      $ singletons
          [d| type D1 :: forall k. forall (a :: k) -> Proxy a -> Type
              type D2 :: forall k. forall (a :: k) -> Proxy a -> Type
              type D3 :: forall k. forall (a :: k) -> Proxy a -> Type
              type D4 :: forall k. forall (a :: k) -> Proxy a -> Type
              
              data D1 x p = MkD1
              data D2 (x :: j) p = MkD2
              data D3 x (p :: Proxy x) = MkD3
              data D4 (x :: j) (p :: Proxy x) = MkD4 |]
  ======>
    type D1 :: forall k. forall (a :: k) -> Proxy a -> Type
    data D1 x p = MkD1
    type D2 :: forall k. forall (a :: k) -> Proxy a -> Type
    data D2 (x :: j) p = MkD2
    type D3 :: forall k. forall (a :: k) -> Proxy a -> Type
    data D3 x (p :: Proxy x) = MkD3
    type D4 :: forall k. forall (a :: k) -> Proxy a -> Type
    data D4 (x :: j) (p :: Proxy x) = MkD4
    type MkD1Sym0 :: forall x p. D1 x p
    type family MkD1Sym0 @x @p :: D1 x p where
      MkD1Sym0 = MkD1
    type MkD2Sym0 :: forall j (x :: j) p. D2 x p
    type family MkD2Sym0 @j @(x :: j) @p :: D2 x p where
      MkD2Sym0 = MkD2
    type MkD3Sym0 :: forall x (p :: Proxy x). D3 x p
    type family MkD3Sym0 @x @(p :: Proxy x) :: D3 x p where
      MkD3Sym0 = MkD3
    type MkD4Sym0 :: forall j (x :: j) (p :: Proxy x). D4 x p
    type family MkD4Sym0 @j @(x :: j) @(p :: Proxy x) :: D4 x p where
      MkD4Sym0 = MkD4
    type SD1 :: forall k (x :: k) (p :: Proxy x). D1 x p -> Type
    data SD1 :: forall k (x :: k) (p :: Proxy x). D1 x p -> Type
      where SMkD1 :: forall x p. SD1 (MkD1 :: D1 x p)
    type instance Sing @(D1 x p) = SD1
    type SD2 :: forall j (x :: j) (p :: Proxy x). D2 x p -> Type
    data SD2 :: forall j (x :: j) (p :: Proxy x). D2 x p -> Type
      where SMkD2 :: forall j (x :: j) p. SD2 (MkD2 :: D2 x p)
    type instance Sing @(D2 x p) = SD2
    type SD3 :: forall k (x :: k) (p :: Proxy x). D3 x p -> Type
    data SD3 :: forall k (x :: k) (p :: Proxy x). D3 x p -> Type
      where SMkD3 :: forall x (p :: Proxy x). SD3 (MkD3 :: D3 x p)
    type instance Sing @(D3 x p) = SD3
    type SD4 :: forall j (x :: j) (p :: Proxy x). D4 x p -> Type
    data SD4 :: forall j (x :: j) (p :: Proxy x). D4 x p -> Type
      where
        SMkD4 :: forall j (x :: j) (p :: Proxy x). SD4 (MkD4 :: D4 x p)
    type instance Sing @(D4 x p) = SD4
    instance SingI MkD1 where
      sing = SMkD1
    instance SingI MkD2 where
      sing = SMkD2
    instance SingI MkD3 where
      sing = SMkD3
    instance SingI MkD4 where
      sing = SMkD4