Singletons/T33.hs:(0,0)-(0,0): Splicing declarations singletons [d| foo :: (Bool, Bool) -> () foo ~(_, _) = () |] ======> foo :: (Bool, Bool) -> () foo ~(_, _) = () type FooSym1 (a0123456789876543210 :: (Bool, Bool)) = Foo a0123456789876543210 instance SuppressUnusedWarnings FooSym0 where suppressUnusedWarnings = snd (((,) FooSym0KindInference) ()) data FooSym0 :: (~>) (Bool, Bool) () where FooSym0KindInference :: forall a0123456789876543210 arg. SameKind (Apply FooSym0 arg) (FooSym1 arg) => FooSym0 a0123456789876543210 type instance Apply FooSym0 a0123456789876543210 = Foo a0123456789876543210 type family Foo (a :: (Bool, Bool)) :: () where Foo '(_, _) = Tuple0Sym0 sFoo :: forall (t :: (Bool, Bool)). Sing t -> Sing (Apply FooSym0 t :: ()) sFoo (STuple2 _ _) = STuple0 instance SingI (FooSym0 :: (~>) (Bool, Bool) ()) where sing = (singFun1 @FooSym0) sFoo Singletons/T33.hs:0:0: warning: Lazy pattern converted into regular pattern in promotion | 6 | $(singletons [d| | ^^^^^^^^^^^^^^... Singletons/T33.hs:0:0: warning: Lazy pattern converted into regular pattern during singleton generation. | 6 | $(singletons [d| | ^^^^^^^^^^^^^^...