Simplify constraints when showing errors / typed holes

Motivation

I'm doing some type-level programming with typed holes, and often I will see constraints of the form x ~ (y : ys) or (x : xs) ~ (y : ys). There can be several such constraints that form a "chain", and it would be an immense help if they were simplified, such that redundant variables wouldn't be shown, e.g. x :: a when we have the constraint a ~ Int.

Proposal

Apply constraints before showing the information.

Example

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fno-show-valid-hole-fits #-}

data IsInt a where
  IsInt :: IsInt Int

f :: IsInt a -> a -> Int
f IsInt x = _

This currently shows (with GHC 9.2.4)

X.hs:9:13: error:
    • Found hole: _ :: Int
    • In an equation for ‘f’: f IsInt x = _
    • Relevant bindings include
        x :: a (bound at X.hs:9:9)
        f :: IsInt a -> a -> Int (bound at X.hs:9:1)
      Constraints include a ~ Int (from X.hs:9:3-7)
  |
9 | f IsInt x = _
  |             ^

It should show

X.hs:9:13: error:
    • Found hole: _ :: Int
    • In an equation for ‘f’: f IsInt x = _
    • Relevant bindings include
        x :: Int (bound at X.hs:9:9)
        f :: IsInt a -> a -> Int (bound at X.hs:9:1)
  |
9 | f IsInt x = _
  |             ^