Singletons/Undef.hs:(0,0)-(0,0): Splicing declarations singletons [d| foo :: Bool -> Bool foo = undefined bar :: Bool -> Bool bar = error "urk" |] ======> foo :: Bool -> Bool foo = undefined bar :: Bool -> Bool bar = error "urk" type BarSym0 :: (~>) Bool Bool data BarSym0 :: (~>) Bool Bool where BarSym0KindInference :: SameKind (Apply BarSym0 arg) (BarSym1 arg) => BarSym0 a0123456789876543210 type instance Apply BarSym0 a0123456789876543210 = Bar a0123456789876543210 instance SuppressUnusedWarnings BarSym0 where suppressUnusedWarnings = snd ((,) BarSym0KindInference ()) type BarSym1 :: Bool -> Bool type family BarSym1 (a0123456789876543210 :: Bool) :: Bool where BarSym1 a0123456789876543210 = Bar a0123456789876543210 type FooSym0 :: (~>) Bool Bool data FooSym0 :: (~>) 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 :: Bool -> Bool type family FooSym1 (a0123456789876543210 :: Bool) :: Bool where FooSym1 a0123456789876543210 = Foo a0123456789876543210 type Bar :: Bool -> Bool type family Bar (a :: Bool) :: Bool where Bar a_0123456789876543210 = Apply (Apply ErrorSym0 "urk") a_0123456789876543210 type Foo :: Bool -> Bool type family Foo (a :: Bool) :: Bool where Foo a_0123456789876543210 = Apply UndefinedSym0 a_0123456789876543210 sBar :: (forall (t :: Bool). Sing t -> Sing (Apply BarSym0 t :: Bool) :: Type) sFoo :: (forall (t :: Bool). Sing t -> Sing (Apply FooSym0 t :: Bool) :: Type) sBar (sA_0123456789876543210 :: Sing a_0123456789876543210) = sError (sing :: Sing "urk") sA_0123456789876543210 sFoo (sA_0123456789876543210 :: Sing a_0123456789876543210) = sUndefined sA_0123456789876543210 instance SingI (BarSym0 :: (~>) Bool Bool) where sing = singFun1 @BarSym0 sBar instance SingI (FooSym0 :: (~>) Bool Bool) where sing = singFun1 @FooSym0 sFoo