Mention existential type variables in 'relevant bindings'

[zarakshR]

For this example code --

{-# LANGUAGE GADTs #-}

data T where
  X :: T
  Y :: a -> T

f :: T -> ()
f X = ()
f (Y a) = _

The error message (ghc 9.0.2) reads -

example.hs:9:11: error:
    • Found hole: _ :: ()
    • In the expression: _
      In an equation for ‘f’: f (Y a) = _
    • Relevant bindings include
        a :: a (bound at example.hs:9:6)
        f :: T -> () (bound at example.hs:8:1)
      Valid hole fits include
      .....

The type of a is just a. Would it be possible for GHC to do something like this? -

    • Relevant bindings include
        a :: a (bound at example.hs:9:6)
        f :: T -> () (bound at example.hs:8:1)
    • Where                                                                                  <------
        a is an existential type variable                                          <------

Additionally, would it be possible to annotate a with the location where it is introduced (so, for the above example, it could read a is an existential type variable introduced at example.hs:5:9) and any constraints on it? I believe the error messages for escaping skolem variables already do something similar -

data Any where
  Any :: a -> Any

Any True                    :: Any
Any (show :: Int -> String) :: Any

f (Any a) = a

• Couldn't match expected type ‘t’ with actual type ‘a’ because type variable ‘a’ would escape its scope
  This (rigid, skolem) type variable is bound by a pattern with constructor: Any :: forall a. a -> Any,