Type equality constraints without signatures

[Tarmean]

The following code snippet

{-# 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

[goldfirere]

Yes, I think GHC can do much better in this regard. I think it's fair to submit your ticket to GHC directly.