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