Inference issue with RequiredTypeArguments, type equality

Summary

An expression involving visible type quantification does not compile without a type signature, when an analogous expression using proxies instead would not require one.

Steps to reproduce

(Adapted from this post)

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RequiredTypeArguments #-}

import GHC.TypeLits

showKnownChar :: forall c -> KnownChar c => IO ()
showKnownChar c = print (charSing @c)

withKnownChar_rta :: SChar c -> (forall c' -> c ~ c' => KnownChar c => r) -> r
withKnownChar_rta (SChar @c) r = r c

-- no type signature
example = withKnownChar_rta (SChar @'a') (\c -> showKnownChar c)

Resulting error:

Main.hs:13:49: error: [GHC-25897]
    • Could not deduce ‘r ~ IO ()’
      from the context: ('a' ~ c', KnownChar 'a')
        bound by a type expected by the context:
                   forall (c'1 :: Char) -> ('a' ~ c'1, KnownChar 'a') => r
        at Main.hs:13:43-63
      ‘r’ is a rigid type variable bound by
        the inferred type of example :: r
        at Main.hs:13:1-64
    • In the expression: showKnownChar c
      In the second argument of ‘withKnownChar_rta’, namely
        ‘(\ c -> showKnownChar c)’
      In the expression:
        withKnownChar_rta (SChar @'a') (\ c -> showKnownChar c)
    • Relevant bindings include example :: r (bound at Main.hs:13:1)
    Suggested fix: Consider giving ‘example’ a type signature
   |
13 | example = withKnownChar_rta (SChar @'a') (\c -> showKnownChar c)
   |                                                 ^^^^^^^^^^^^^^^

Expected behavior

I would expect r to be an unknown, not a rigid type variable, and for it to be inferred as IO ().

Environment

• GHC version used: 9.10.1 (play.haskell.org)