Typed Holes, GADTs and residual constraints

The error messages when using typed holes on the RHS of a pattern match on GADT constructors are not optimal, since type equality constraints are left unresolved and not applied as substitutions. (Tested with GHC 8.6, 8.10 and 9.2.1).
Understanding the error message requires understanding both GADTs and the implementation of GADTs with the help of type equality constraints.

## Example

Consider the following snippet:

```haskell
{-# LANGUAGE GADTs #-}

data Expr a where
ExprInt :: Int -> Expr Int
ExprBool :: Bool -> Expr Bool

foo :: Expr a -> Bool
foo x = case x of
ExprInt _ -> True
ExprBool _ -> _
```

The error message I get (shortened):

```
example.hs:10:17: error:
• Found hole: _ :: Bool
• In the expression: _
In a case alternative: ExprBool _ -> _
In the expression:
case x of
ExprInt _ -> True
ExprBool _ -> _
• Relevant bindings include
x :: Expr a (bound at example.hs:8:5)
foo :: Expr a -> Bool (bound at example.hs:8:1)
Constraints include a ~ Bool (from example.hs:10:3-12)
```
This error message correctly identifies the constraint `a ~ Bool` which came into context by pattern matching on the GADT constructor `ExprBool`. But understanding this error message requires understanding how GADT constructors are desugared internally (into `ExprBool :: forall a. a ~ Bool => Bool -> Expr a`)

The error message I would ideally expect would turn this constraint into a substitution and apply it:

```
example.hs:10:17: error:
• Found hole: _ :: Bool
• In the expression: _
In a case alternative: ExprBool _ -> _
In the expression:
case x of
ExprInt _ -> True
ExprBool _ -> _
• Relevant bindings include
x :: Expr Bool (bound at example.hs:8:5)
foo :: Expr a -> Bool (bound at example.hs:8:1)
```

I am not very familiar with GHC internals, in particular how closely GHC follows the implementation described in the OutsideIn paper, but the problem is probably that `a` is considered an untouchable unification variable within the implication constraint generated for the RHS of the pattern match. But for the typed hole, the unification variable `a` should probably be allowed to unify with Bool. (Except for the occurrence in `foo`, of course).