Typecasting using type application syntax

I created #11350 (closed) to allow visible (static) type applications in patterns. I had a thought about translating non-parametric type applications in patterns as a runtime type check (Typeable) and decided to create a ticket in case it made any sense. Example:

doubleWhenInt :: forall a. Typeable a => a -> a
doubleWhenInt x =
  case eqT @Int @a of
    Just Refl -> x + x
    Nothing   -> x

-- Becomes…
doubleWhenInt :: Typeable a => a -> a
doubleWhenInt @Int n = n + n
doubleWhenInt @_   x = x

Thoughts?

Trac metadata

Trac field	Value
Version
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture