T297.golden

Singletons/T297.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| f MyProxy
            = let
                x = let
                      z :: MyProxy a
                      z = MyProxy
                    in z
              in x
          
          data MyProxy (a :: Type) = MyProxy |]
  ======>
    data MyProxy (a :: Type) = MyProxy
    f MyProxy
      = let
          x = let
                z :: MyProxy a
                z = MyProxy
              in z
        in x
    type MyProxySym0 :: forall (a :: Type). MyProxy (a :: Type)
    type family MyProxySym0 :: MyProxy (a :: Type) where
      MyProxySym0 = MyProxy
    type Let0123456789876543210ZSym0 :: MyProxy a
    type family Let0123456789876543210ZSym0 :: MyProxy a where
      Let0123456789876543210ZSym0 = Let0123456789876543210Z
    type Let0123456789876543210Z :: MyProxy a
    type family Let0123456789876543210Z :: MyProxy a where
      Let0123456789876543210Z = MyProxySym0
    type family Let0123456789876543210XSym0 where
      Let0123456789876543210XSym0 = Let0123456789876543210X
    type family Let0123456789876543210X where
      Let0123456789876543210X = Let0123456789876543210ZSym0
    data FSym0 a0123456789876543210
      where
        FSym0KindInference :: SameKind (Apply FSym0 arg) (FSym1 arg) =>
                              FSym0 a0123456789876543210
    type instance Apply FSym0 a0123456789876543210 = F a0123456789876543210
    instance SuppressUnusedWarnings FSym0 where
      suppressUnusedWarnings = snd ((,) FSym0KindInference ())
    type family FSym1 a0123456789876543210 where
      FSym1 a0123456789876543210 = F a0123456789876543210
    type family F a where
      F MyProxy = Let0123456789876543210XSym0
    sF :: forall arg. Sing arg -> Sing (Apply FSym0 arg)
    sF SMyProxy
      = let
          sX :: Sing @_ Let0123456789876543210XSym0
          sX
            = let
                sZ :: (Sing (Let0123456789876543210ZSym0 :: MyProxy a) :: Type)
                sZ = SMyProxy
              in sZ
        in sX
    instance SingI FSym0 where
      sing = singFun1 @FSym0 sF
    data SMyProxy :: forall (a :: Type). MyProxy a -> Type
      where
        SMyProxy :: forall (a :: Type).
                    SMyProxy (MyProxy :: MyProxy (a :: Type))
    type instance Sing @(MyProxy a) = SMyProxy
    instance SingKind a => SingKind (MyProxy a) where
      type Demote (MyProxy a) = MyProxy (Demote a)
      fromSing SMyProxy = MyProxy
      toSing MyProxy = SomeSing SMyProxy
    instance SingI MyProxy where
      sing = SMyProxy