Singletons/Contains.hs:(0,0)-(0,0): Splicing declarations singletons [d| contains :: Eq a => a -> [a] -> Bool contains _ [] = False contains elt (h : t) = (elt == h) || (contains elt t) |] ======> contains :: Eq a => a -> [a] -> Bool contains _ GHC.Types.[] = False contains elt (h GHC.Types.: t) = ((elt == h) || ((contains elt) t)) type ContainsSym2 (t :: a0123456789876543210) (t :: [a0123456789876543210]) = Contains t t instance SuppressUnusedWarnings ContainsSym1 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) ContainsSym1KindInference) GHC.Tuple.()) data ContainsSym1 (l :: a0123456789876543210) (l :: TyFun [a0123456789876543210] Bool) = forall arg. SameKind (Apply (ContainsSym1 l) arg) (ContainsSym2 l arg) => ContainsSym1KindInference type instance Apply (ContainsSym1 l) l = Contains l l instance SuppressUnusedWarnings ContainsSym0 where suppressUnusedWarnings _ = snd ((GHC.Tuple.(,) ContainsSym0KindInference) GHC.Tuple.()) data ContainsSym0 (l :: TyFun a0123456789876543210 (TyFun [a0123456789876543210] Bool -> GHC.Types.Type)) = forall arg. SameKind (Apply ContainsSym0 arg) (ContainsSym1 arg) => ContainsSym0KindInference type instance Apply ContainsSym0 l = ContainsSym1 l type family Contains (a :: a) (a :: [a]) :: Bool where Contains _z_0123456789876543210 '[] = FalseSym0 Contains elt ((:) h t) = Apply (Apply (:||$) (Apply (Apply (:==$) elt) h)) (Apply (Apply ContainsSym0 elt) t) sContains :: forall (t :: a) (t :: [a]). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ContainsSym0 t) t :: Bool) sContains _ SNil = SFalse sContains (sElt :: Sing elt) (SCons (sH :: Sing h) (sT :: Sing t)) = (applySing ((applySing ((singFun2 @(:||$)) (%:||))) ((applySing ((applySing ((singFun2 @(:==$)) (%:==))) sElt)) sH))) ((applySing ((applySing ((singFun2 @ContainsSym0) sContains)) sElt)) sT)