Singletons/EqInstances.hs:0:0: Splicing declarations singEqInstances [''Foo, ''Empty] ======> Singletons/EqInstances.hs:0:0: instance SEq (KProxy :: KProxy Foo) where (%:==) SFLeaf SFLeaf = STrue (%:==) SFLeaf ((:%+:) _ _) = SFalse (%:==) ((:%+:) _ _) SFLeaf = SFalse (%:==) ((:%+:) a a) ((:%+:) b b) = (%:&&) ((%:==) a b) ((%:==) a b) type family Equals_0123456789 (a :: Foo) (b :: Foo) :: Bool where Equals_0123456789 FLeaf FLeaf = TrueSym0 Equals_0123456789 ((:+:) a a) ((:+:) b b) = (:&&) ((:==) a b) ((:==) a b) Equals_0123456789 (a :: Foo) (b :: Foo) = FalseSym0 instance PEq (KProxy :: KProxy Foo) where type (:==) (a :: Foo) (b :: Foo) = Equals_0123456789 a b instance SEq (KProxy :: KProxy Empty) where (%:==) a _ = case a of { _ -> error "Empty case reached -- this should be impossible" } type family Equals_0123456789 (a :: Empty) (b :: Empty) :: Bool where Equals_0123456789 (a :: Empty) (b :: Empty) = FalseSym0 instance PEq (KProxy :: KProxy Empty) where type (:==) (a :: Empty) (b :: Empty) = Equals_0123456789 a b