Implicit RHS quantification in type synonyms crashes GHC

This example is accepted by GHC 9.8 but crashes GHC HEAD:

type SynBad :: forall k. k -> Type
type SynBad = Proxy :: j -> Type

Test.hs:7:24: error: [GHC-76329]
    • GHC internal error: ‘j’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [rDP :-> ATcTyCon SynBad :: forall k.
                                                          k -> *]
    • In the kind ‘j -> Type’
      In the type ‘Proxy :: j -> Type’
      In the type declaration for ‘SynBad’
  |
7 | type SynBad = Proxy :: j -> Type
  |  

While this one is accepted by both compilers:

type SynOK :: forall k. k -> Type
type SynOK @t = Proxy :: j -> Type

The difference between SynBad and SynOK is the arity. Adding the @t binder changes the arity of SynOK so that it includes j (in fact, j=t=k.)

This is an example of rather exotic interaction between SAKS, arity, and implicit RHS quantification in type synonyms.

Long-term, both examples should be rejected, as implicit RHS quantification in type synonyms is deprecated anyway

Test.hs:8:24: warning: [GHC-16382] [-Wimplicit-rhs-quantification]
    The variable ‘j’ occurs free on the RHS of the type declaration
    In the future GHC will no longer implicitly quantify over such variables
    Suggested fix: Bind ‘j’ on the LHS of the type declaration
  |
8 | type SynBad = Proxy :: j -> Type
  |                        ^

Test.hs:11:26: warning: [GHC-16382] [-Wimplicit-rhs-quantification]
    The variable ‘j’ occurs free on the RHS of the type declaration
    In the future GHC will no longer implicitly quantify over such variables
    Suggested fix: Bind ‘j’ on the LHS of the type declaration
   |
11 | type SynOK @t = Proxy :: j -> Type
   |                          ^
Ok, one module loaded.

Short-term (for the next few releases while we still supported implicit RHS quantification in type synonyms), we probably want a proper error message for SynBad. Arity inference has been removed in e89aa072, so that rules out accepting SynBad. And if we reject it, it's much better to do so with a proper error message rather than a compiler panic.