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.