PatternSynonyms problems with provided constraints

Using the newly added TypeRep pattern synonym (#19691 (closed))

pattern TypeRep :: forall (k :: Type) (a :: k). () => Typeable a => TypeRep a

it is possible to define this

pattern TFalse :: TypeRep False
pattern TFalse = TypeRep

but not

-- • Couldn't match type ‘bool’ with ‘'False’
--     arising from the "provided" constraints claimed by
--       the signature of ‘TFalse’
--   ‘bool’ is a rigid type variable bound by
--     the signature for pattern synonym ‘TFalse’
--     at /home/baldur/hs/5456.hs:15:1-52
-- • In the declaration for pattern synonym ‘TFalse’
pattern TFalse :: () => bool ~ False => TypeRep bool
pattern TFalse = TypeRep

I was thinking it could be used to quickly define singletons, is this not expected to work?

which :: TypeRep bool -> If bool Double (Int, Int)
which TTrue  = pi
which TFalse = (20, 30)