Quantified constraint error should show more context

Motivation

QuantifiedConstraints sometimes leads to incomplete error message for which it is rather difficult to understand / locate the source of the error.

See the following example:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes, ScopedTypeVariables, QuantifiedConstraints, TypeApplications, DataKinds, ConstraintKinds, AllowAmbiguousTypes #-}
module QC2 where

import GHC.TypeLits
import Data.Proxy

data Array (n :: Nat) = Array

class IsEqual t

instance KnownNat n => IsEqual (Array n)

blork :: forall c.
  (forall k. {- KnownNat k => -} c (Array k)) => 
  (forall k. c k => k -> Bool) -> Bool
blork f = case someNatVal 10 of
    Nothing -> False
    Just (SomeNat (_ :: Proxy n)) -> f (Array @n)

blip :: Bool
blip = blork @IsEqual (\_ -> True)

The comment around KnownNat k => can be removed to fix the following error:

QC2.hs:22:8: error:
    • No instance for (KnownNat k) arising from a use of ‘blork’
      Possible fix:
        add (KnownNat k) to the context of a quantified context
    • In the expression: blork @IsEqual (\ _ -> True)
      In an equation for ‘blip’: blip = blork @IsEqual (\ _ -> True)
   |
22 | blip = blork @IsEqual (\_ -> True)
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^

This error show the call site and a "Possible fix". However it does not give any hint about the location of the erroneous quantified constraint. The developer must manually locate the blork function and, amongs the list of quantified constraints in its context, locate the erroneous one.

Note that GHC is smart enough to use the right name for the type variable k in the error message, this helps a bit. However, as depicted in my example, the constraint of blork may many quantified constraint using all the same type variable (because they are independent).

It took me a lot of time to first understand that the error was in the blork function. Now I'm used to this error, but locating the erroneous quantified constraint is still difficult.

Proposal

I'd like a more detailed error message, such as:

QC2.hs:22:8: error:
    • No instance for (KnownNat k) arising from a use of ‘blork’
      Possible fix:
        add (KnownNat k) to the context of a quantified context
        in the `blork` function context:

         15  |  blork :: forall c.
             |  (forall k. c (Array k)) => 
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^
    • In the expression: blork @IsEqual (\ _ -> True)
        In an equation for ‘blip’: blip = blork @IsEqual (\ _ -> True)
   |
22 | blip = blork @IsEqual (\_ -> True)
   |      

I'd like something similar to the hint associated with missing constraint in this context:

foo :: t -> String
foo = show

    • No instance for (Show t) arising from a use of ‘show’
      Possible fix:
        add (Show t) to the context of
          the type signature for:
            foo :: forall t. t -> String
    • In the expression: show
      In an equation for ‘foo’: foo = show