Inferring extra parameters

[goldfirere]

From singletons (see goldfirere/singletons#153):

-- | 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’

What's up with k and k1??