Show constraints in ``Found hole...''

Currently it is not clear when types are known equal. Consider writing castWith:

{-# LANGUAGE GADTs , TypeOperators #-}
import Data.Type.Equality hiding (castWith)

castWith :: a :~: b -> a -> b
castWith Refl x = _

which results in

TypeEq.hs:5:19: error:
    Found hole: _ :: b
    Where: ‘b’ is a rigid type variable bound by
               the type signature for: castWith :: a :~: b -> a -> b
               at TypeEq.hs:4:13
    Relevant bindings include
      x :: a (bound at TypeEq.hs:5:15)
      castWith :: a :~: b -> a -> b (bound at TypeEq.hs:5:1)
    In the expression: _
    In an equation for ‘castWith’: castWith Refl x = _

Filling the hole with x is correct, but it is not clear from the message that GHC knows this. It would be useful to have a section "Constraints include" e.g.

TypeEq.hs:5:19: error:
    Found hole: _ :: b
    Where: ‘b’ is a rigid type variable bound by
               the type signature for: castWith :: a :~: b -> a -> b
               at TypeEq.hs:4:13
    Relevant bindings include
      x :: a (bound at TypeEq.hs:5:15)
      castWith :: a :~: b -> a -> b (bound at TypeEq.hs:5:1)
    Constraints include                                        <------ NEW LINE
      a ~ b (from Refl :: a :~: a at TypeEq.hs:5:10)           <------ NEW LINE
    In the expression: _
    In an equation for ‘castWith’: castWith Refl x = _

And show class constraints (Show a etc.) similarly

Trac metadata

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