Singletons/T78.hs:(0,0)-(0,0): Splicing declarations singletons [d| foo :: MaybeBool -> Bool foo (Just False) = False foo (Just True) = True foo Nothing = False |] ======> foo :: MaybeBool -> Bool foo (Just False) = False foo (Just True) = True foo Nothing = False type FooSym0 :: (~>) (Maybe Bool) Bool data FooSym0 :: (~>) (Maybe Bool) Bool where FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) => FooSym0 a0123456789876543210 type instance Apply FooSym0 a0123456789876543210 = Foo a0123456789876543210 instance SuppressUnusedWarnings FooSym0 where suppressUnusedWarnings = snd ((,) FooSym0KindInference ()) type FooSym1 :: Maybe Bool -> Bool type family FooSym1 (a0123456789876543210 :: Maybe Bool) :: Bool where FooSym1 a0123456789876543210 = Foo a0123456789876543210 type Foo :: Maybe Bool -> Bool type family Foo (a :: Maybe Bool) :: Bool where Foo ('Just 'False) = FalseSym0 Foo ('Just 'True) = TrueSym0 Foo 'Nothing = FalseSym0 sFoo :: (forall (t :: Maybe Bool). Sing t -> Sing (Apply FooSym0 t :: Bool) :: Type) sFoo (SJust SFalse) = SFalse sFoo (SJust STrue) = STrue sFoo SNothing = SFalse instance SingI (FooSym0 :: (~>) (Maybe Bool) Bool) where sing = singFun1 @FooSym0 sFoo