Stuck type families can lead to lousy error messages

I first noticed this problem at the type level:

{-# language TypeFamilies, TypeInType, ScopedTypeVariables #-}

module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy

type family F (s :: Symbol) :: Type
type family G (s :: Symbol) :: F s
type instance G "Hi" = Maybe

This produces the error message

ArityError.hs:10:24: error:
    • Expecting one more argument to ‘Maybe’
      Expected kind ‘F "Hi"’, but ‘Maybe’ has kind ‘* -> *’
    • In the type ‘Maybe’
      In the type instance declaration for ‘G’
   |
10 | type instance G "Hi" = Maybe
   |                        ^^^^^

This looks utterly bogus: F "Hi" is stuck, so we have no idea what arity it indicates.

---

I just realized we have a similar problem at the term level:

f :: forall (s :: Symbol). Proxy s -> F s
f _ _ = undefined

produces

ArityError.hs:14:1: error:
    • Couldn't match expected type ‘F s’ with actual type ‘p0 -> a0’
      The type variables ‘p0’, ‘a0’ are ambiguous
    • The equation(s) for ‘f’ have two arguments,
      but its type ‘Proxy s -> F s’ has only one
    • Relevant bindings include
        f :: Proxy s -> F s (bound at ArityError.hs:14:1)
   |
14 | f _ _ = undefined
   | ^^^^^^^^^^^^^^^^^

The claim that Proxy s -> F s has only one argument is bogus; we only know that it has at least one argument. The fix (I imagine) is to refrain from reporting arity errors when we don't know enough about the relevant arities.