This example is accepted by GHC 9.8 but crashes GHC HEAD: ```haskell 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: ```haskell 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 e89aa0721ca5c594f6811f2108d49cd051488ce1, 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.