Type equality constraints without signatures

The following code snippet

```haskell
{-# LANGUAGE GADTs #-}
import Data.Type.Equality

foo Refl = ()
```
produces the type error

```
• Could not deduce: p ~ ()
from the context: b ~ a
bound by a pattern with constructor:
Refl :: forall {k} (a :: k). a :~: a,
in an equation for ‘foo’
‘p’ is a rigid type variable bound by
the inferred type of foo :: (a :~: b) -> p
```

This makes sort of sense because there may be no unique most general type. We could have the sane `foo :: a :~: b -> ()`, or `foo :: a :~: () -> a`, or even `foo :: a :~: Int -> SomeTypeFamily a`.
If I understand the OutsideIn paper correctly this failure is intentional. Currently, GHC could guess `foo :: ()` but future extension may break this behaviour.

But many variants of this error crop up when using GADTs. Ideally, GHC would detect cases where the result type may be insufficiently constrained for OutsideIn and say so where a type signature is missing. I have no ideas yet how to implement this, though.

But I think a default note for generic rigid type errors may still be useful? Maybe something like

```
• Note: Perhaps you can give an explicit type signature
```