T376.golden

Singletons/T376.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| f :: (() -> ()) -> (() -> ())
          f g = g :: () -> () |]
  ======>
    f :: (() -> ()) -> () -> ()
    f g = g :: () -> ()
    type FSym0 :: (~>) ((~>) () ()) ((~>) () ())
    data FSym0 :: (~>) ((~>) () ()) ((~>) () ())
      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 :: (~>) () () -> (~>) () ()
    data FSym1 (a0123456789876543210 :: (~>) () ()) :: (~>) () ()
      where
        FSym1KindInference :: SameKind (Apply (FSym1 a0123456789876543210) arg) (FSym2 a0123456789876543210 arg) =>
                              FSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (FSym1 a0123456789876543210) a0123456789876543210 = F a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (FSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) FSym1KindInference ())
    type FSym2 :: (~>) () () -> () -> ()
    type family FSym2 (a0123456789876543210 :: (~>) () ()) (a0123456789876543210 :: ()) :: () where
      FSym2 a0123456789876543210 a0123456789876543210 = F a0123456789876543210 a0123456789876543210
    type F :: (~>) () () -> () -> ()
    type family F (a :: (~>) () ()) (a :: ()) :: () where
      F g a_0123456789876543210 = Apply (g :: (~>) () ()) a_0123456789876543210
    sF ::
      (forall (t :: (~>) () ()) (t :: ()).
       Sing t -> Sing t -> Sing (Apply (Apply FSym0 t) t :: ()) :: Type)
    sF
      (sG :: Sing g)
      (sA_0123456789876543210 :: Sing a_0123456789876543210)
      = applySing (sG :: Sing (g :: (~>) () ())) sA_0123456789876543210
    instance SingI (FSym0 :: (~>) ((~>) () ()) ((~>) () ())) where
      sing = singFun2 @FSym0 sF
    instance SingI d =>
             SingI (FSym1 (d :: (~>) () ()) :: (~>) () ()) where
      sing = singFun1 @(FSym1 (d :: (~>) () ())) (sF (sing @d))
    instance SingI1 (FSym1 :: (~>) () () -> (~>) () ()) where
      liftSing (s :: Sing (d :: (~>) () ()))
        = singFun1 @(FSym1 (d :: (~>) () ())) (sF s)