T296.golden

Singletons/T296.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| f :: forall a. MyProxy a -> MyProxy a
          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 :: forall a. MyProxy a -> MyProxy a
    f MyProxy
      = let
          x = let
                z :: MyProxy a
                z = MyProxy
              in z
        in x
    type MyProxySym0 = MyProxy :: MyProxy (a :: Type)
    type Let0123456789876543210ZSym0 =
        Let0123456789876543210Z :: MyProxy a
    type Let0123456789876543210Z :: MyProxy a
    type family Let0123456789876543210Z where
      Let0123456789876543210Z = MyProxySym0
    type Let0123456789876543210XSym0 = Let0123456789876543210X
    type family Let0123456789876543210X where
      Let0123456789876543210X = Let0123456789876543210ZSym0
    type FSym0 :: forall a. (~>) (MyProxy a) (MyProxy a)
    data FSym0 a0123456789876543210
      where
        FSym0KindInference :: SameKind (Apply FSym0 arg) (FSym1 arg) =>
                              FSym0 a0123456789876543210
    type instance Apply FSym0 a0123456789876543210 = FSym1 a0123456789876543210
    instance SuppressUnusedWarnings FSym0 where
      suppressUnusedWarnings = snd (((,) FSym0KindInference) ())
    type FSym1 (a0123456789876543210 :: MyProxy a) =
        F a0123456789876543210 :: MyProxy a
    type F :: forall a. MyProxy a -> MyProxy a
    type family F a where
      F MyProxy = Let0123456789876543210XSym0
    sF ::
      forall a (t :: MyProxy a).
      Sing t -> Sing (Apply FSym0 t :: MyProxy a)
    sF SMyProxy
      = let
          sX :: Sing @_ Let0123456789876543210XSym0
          sX
            = let
                sZ :: Sing (Let0123456789876543210ZSym0 :: MyProxy a)
                sZ = SMyProxy
              in sZ
        in sX
    instance SingI (FSym0 :: (~>) (MyProxy a) (MyProxy a)) where
      sing = (singFun1 @FSym0) sF
    data SMyProxy :: forall a. MyProxy (a :: Type) -> 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