-- | Convert a normal datatype (like 'Bool') to a singleton for that datatype,
-- passing it into a continuation.
withSomeSing :: SingKind k
=> DemoteRep k -- ^ The original datatype
-> (forall (a :: k). Sing a -> r) -- ^ Function expecting a singleton
-> r
withSomeSing x f =
case toSing x of
SomeSing x' -> f x'
GHC gives it this sig, as reported by :info:
withSomeSing ::
forall {k} (k1 :: k) k2 r.
SingKind k2 =>
DemoteRep k2 -> (forall (a :: k2). Sing a -> r) -> r
-- Defined in ‘Data.Singletons’
From
singletons
(see goldfirere/singletons#153):GHC gives it this sig, as reported by
:info
:What's up with
k
andk1
??