Singletons/TopLevelPatterns.hs:0:0: Splicing declarations
    singletons
      [d| data Bool = False | True
          data Foo = Bar Bool Bool |]
  ======>
    Singletons/TopLevelPatterns.hs:(0,0)-(0,0)
    data Bool = False | True
    data Foo = Bar Bool Bool
    type FalseSym0 = False
    type TrueSym0 = True
    type BarSym2 (t :: Bool) (t :: Bool) = Bar t t
    instance SuppressUnusedWarnings BarSym1 where
      suppressUnusedWarnings _
        = Data.Tuple.snd (GHC.Tuple.(,) BarSym1KindInference GHC.Tuple.())
    data BarSym1 (l :: Bool) (l :: TyFun Bool Foo)
      = forall arg. KindOf (Apply (BarSym1 l) arg) ~ KindOf (BarSym2 l arg) =>
        BarSym1KindInference
    type instance Apply (BarSym1 l) l = BarSym2 l l
    instance SuppressUnusedWarnings BarSym0 where
      suppressUnusedWarnings _
        = Data.Tuple.snd (GHC.Tuple.(,) BarSym0KindInference GHC.Tuple.())
    data BarSym0 (l :: TyFun Bool (TyFun Bool Foo -> *))
      = forall arg. KindOf (Apply BarSym0 arg) ~ KindOf (BarSym1 arg) =>
        BarSym0KindInference
    type instance Apply BarSym0 l = BarSym1 l
    data instance Sing (z :: Bool)
      = z ~ False => SFalse | z ~ True => STrue
    type SBool (z :: Bool) = Sing z
    instance SingKind (KProxy :: KProxy Bool) where
      type DemoteRep (KProxy :: KProxy Bool) = Bool
      fromSing SFalse = False
      fromSing STrue = True
      toSing False = SomeSing SFalse
      toSing True = SomeSing STrue
    data instance Sing (z :: Foo)
      = forall (n :: Bool) (n :: Bool). z ~ Bar n n =>
        SBar (Sing n) (Sing n)
    type SFoo (z :: Foo) = Sing z
    instance SingKind (KProxy :: KProxy Foo) where
      type DemoteRep (KProxy :: KProxy Foo) = Foo
      fromSing (SBar b b) = Bar (fromSing b) (fromSing b)
      toSing (Bar b b)
        = case
              GHC.Tuple.(,)
                (toSing b :: SomeSing (KProxy :: KProxy Bool))
                (toSing b :: SomeSing (KProxy :: KProxy Bool))
          of {
            GHC.Tuple.(,) (SomeSing c) (SomeSing c) -> SomeSing (SBar c c) }
    instance SingI False where
      sing = SFalse
    instance SingI True where
      sing = STrue
    instance (SingI n, SingI n) =>
             SingI (Bar (n :: Bool) (n :: Bool)) where
      sing = SBar sing sing
Singletons/TopLevelPatterns.hs:0:0: Splicing declarations
    singletons
      [d| otherwise :: Bool
          otherwise = True
          id :: a -> a
          id x = x
          not :: Bool -> Bool
          not True = False
          not False = True
          false_ = False |]
  ======>
    Singletons/TopLevelPatterns.hs:(0,0)-(0,0)
    otherwise :: Bool
    otherwise = True
    id :: forall a. a -> a
    id x = x
    not :: Bool -> Bool
    not True = False
    not False = True
    false_ = False
    type False_Sym0 = False_
    type NotSym1 (t :: Bool) = Not t
    instance SuppressUnusedWarnings NotSym0 where
      suppressUnusedWarnings _
        = Data.Tuple.snd (GHC.Tuple.(,) NotSym0KindInference GHC.Tuple.())
    data NotSym0 (l :: TyFun Bool Bool)
      = forall arg. KindOf (Apply NotSym0 arg) ~ KindOf (NotSym1 arg) =>
        NotSym0KindInference
    type instance Apply NotSym0 l = NotSym1 l
    type IdSym1 (t :: a) = Id t
    instance SuppressUnusedWarnings IdSym0 where
      suppressUnusedWarnings _
        = Data.Tuple.snd (GHC.Tuple.(,) IdSym0KindInference GHC.Tuple.())
    data IdSym0 (l :: TyFun a a)
      = forall arg. KindOf (Apply IdSym0 arg) ~ KindOf (IdSym1 arg) =>
        IdSym0KindInference
    type instance Apply IdSym0 l = IdSym1 l
    type OtherwiseSym0 = Otherwise
    type False_ = FalseSym0
    type family Not (a :: Bool) :: Bool where
      Not True = FalseSym0
      Not False = TrueSym0
    type family Id (a :: a) :: a where
      Id x = x
    type Otherwise = (TrueSym0 :: Bool)
    sFalse_ :: Sing False_Sym0
    sNot :: forall (t :: Bool). Sing t -> Sing (Apply NotSym0 t)
    sId :: forall (t :: a). Sing t -> Sing (Apply IdSym0 t)
    sOtherwise :: Sing OtherwiseSym0
    sFalse_ = SFalse
    sNot STrue
      = let
          lambda :: t ~ TrueSym0 => Sing (Apply NotSym0 TrueSym0)
          lambda = SFalse
        in lambda
    sNot SFalse
      = let
          lambda :: t ~ FalseSym0 => Sing (Apply NotSym0 FalseSym0)
          lambda = STrue
        in lambda
    sId sX
      = let
          lambda :: forall x. t ~ x => Sing x -> Sing (Apply IdSym0 x)
          lambda x = x
        in lambda sX
    sOtherwise = STrue