From 7ea971d314c4eba59e12e94bf3eb8edb95fbfac5 Mon Sep 17 00:00:00 2001
From: Andrei Borzenkov <andreyborzenkov2002@gmail.com>
Date: Thu, 7 Mar 2024 17:11:00 +0400
Subject: [PATCH] Fix compiler crash caused by implicit RHS quantification in
type synonyms (#24470)
---
compiler/GHC/Tc/Errors/Ppr.hs | 16 ++++
compiler/GHC/Tc/Errors/Types.hs | 20 +++++
compiler/GHC/Tc/Gen/HsType.hs | 78 +++++++++++++++++--
compiler/GHC/Types/Error/Codes.hs | 1 +
.../tests/typecheck/should_compile/T24470b.hs | 10 +++
.../tests/typecheck/should_compile/all.T | 1 +
.../tests/typecheck/should_fail/T24470a.hs | 7 ++
.../typecheck/should_fail/T24470a.stderr | 6 ++
testsuite/tests/typecheck/should_fail/all.T | 2 +
9 files changed, 134 insertions(+), 7 deletions(-)
create mode 100644 testsuite/tests/typecheck/should_compile/T24470b.hs
create mode 100644 testsuite/tests/typecheck/should_fail/T24470a.hs
create mode 100644 testsuite/tests/typecheck/should_fail/T24470a.stderr
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index ef4fe07f8818..08646816eb1d 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -1922,6 +1922,18 @@ instance Diagnostic TcRnMessage where
, text "in a fixity signature"
]
+ TcRnOutOfArityTyVar ts_name tv_name -> mkDecorated
+ [ vcat [ text "The arity of" <+> quotes (ppr ts_name) <+> text "is insufficiently high to accommodate"
+ , text "an implicit binding for the" <+> quotes (ppr tv_name) <+> text "type variable." ]
+ , suggestion ]
+ where
+ suggestion =
+ text "Use" <+> quotes at_bndr <+> text "on the LHS" <+>
+ text "or" <+> quotes forall_bndr <+> text "on the RHS" <+>
+ text "to bring it into scope."
+ at_bndr = char '@' <> ppr tv_name
+ forall_bndr = text "forall" <+> ppr tv_name <> text "."
+
diagnosticReason :: TcRnMessage -> DiagnosticReason
diagnosticReason = \case
TcRnUnknownMessage m
@@ -2556,6 +2568,8 @@ instance Diagnostic TcRnMessage where
-> ErrorWithoutFlag
TcRnNamespacedFixitySigWithoutFlag{}
-> ErrorWithoutFlag
+ TcRnOutOfArityTyVar{}
+ -> ErrorWithoutFlag
diagnosticHints = \case
TcRnUnknownMessage m
@@ -3224,6 +3238,8 @@ instance Diagnostic TcRnMessage where
-> noHints
TcRnNamespacedFixitySigWithoutFlag{}
-> [suggestExtension LangExt.ExplicitNamespaces]
+ TcRnOutOfArityTyVar{}
+ -> noHints
diagnosticCode = constructorCode
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 79bf0be072aa..55f08237624f 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -2272,6 +2272,8 @@ data TcRnMessage where
where the implicitly-bound type type variables can't be matched up unambiguously
with the ones from the signature. See Note [Disconnected type variables] in
GHC.Tc.Gen.HsType.
+
+ Test cases: T24083
-}
TcRnDisconnectedTyVar :: !Name -> TcRnMessage
@@ -4267,6 +4269,24 @@ data TcRnMessage where
-}
TcRnDefaultedExceptionContext :: CtLoc -> TcRnMessage
+ {-| TcRnOutOfArityTyVar is an error raised when the arity of a type synonym
+ (as determined by the SAKS and the LHS) is insufficiently high to
+ accommodate an implicit binding for a free variable that occurs in the
+ outermost kind signature on the RHS of the said type synonym.
+
+ Example:
+
+ type SynBad :: forall k. k -> Type
+ type SynBad = Proxy :: j -> Type
+
+ Test cases:
+ T24770a
+ -}
+ TcRnOutOfArityTyVar
+ :: Name -- ^ Type synonym's name
+ -> Name -- ^ Type variable's name
+ -> TcRnMessage
+
deriving Generic
----
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 573f086f5223..ceb3fd1a1bdd 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2617,7 +2617,7 @@ kcCheckDeclHeader_sig sig_kind name flav
; implicit_tvs <- liftZonkM $ zonkTcTyVarsToTcTyVars implicit_tvs
; let implicit_prs = implicit_nms `zip` implicit_tvs
; checkForDuplicateScopedTyVars implicit_prs
- ; checkForDisconnectedScopedTyVars flav all_tcbs implicit_prs
+ ; checkForDisconnectedScopedTyVars name flav all_tcbs implicit_prs
-- Swizzle the Names so that the TyCon uses the user-declared implicit names
-- E.g type T :: k -> Type
@@ -2978,25 +2978,32 @@ expectedKindInCtxt _ = OpenKind
* *
********************************************************************* -}
-checkForDisconnectedScopedTyVars :: TyConFlavour TyCon -> [TcTyConBinder]
+checkForDisconnectedScopedTyVars :: Name -> TyConFlavour TyCon -> [TcTyConBinder]
-> [(Name,TcTyVar)] -> TcM ()
-- See Note [Disconnected type variables]
+-- For the type synonym case see Note [Out of arity type variables]
-- `scoped_prs` is the mapping gotten by unifying
-- - the standalone kind signature for T, with
-- - the header of the type/class declaration for T
-checkForDisconnectedScopedTyVars flav sig_tcbs scoped_prs
- = when (needsEtaExpansion flav) $
+checkForDisconnectedScopedTyVars name flav all_tcbs scoped_prs
-- needsEtaExpansion: see wrinkle (DTV1) in Note [Disconnected type variables]
- mapM_ report_disconnected (filterOut ok scoped_prs)
+ | needsEtaExpansion flav = mapM_ report_disconnected (filterOut ok scoped_prs)
+ | flav == TypeSynonymFlavour = mapM_ report_out_of_arity (filterOut ok scoped_prs)
+ | otherwise = pure ()
where
- sig_tvs = mkVarSet (binderVars sig_tcbs)
- ok (_, tc_tv) = tc_tv `elemVarSet` sig_tvs
+ all_tvs = mkVarSet (binderVars all_tcbs)
+ ok (_, tc_tv) = tc_tv `elemVarSet` all_tvs
report_disconnected :: (Name,TcTyVar) -> TcM ()
report_disconnected (nm, _)
= setSrcSpan (getSrcSpan nm) $
addErrTc $ TcRnDisconnectedTyVar nm
+ report_out_of_arity :: (Name,TcTyVar) -> TcM ()
+ report_out_of_arity (tv_nm, _)
+ = setSrcSpan (getSrcSpan tv_nm) $
+ addErrTc $ TcRnOutOfArityTyVar name tv_nm
+
checkForDuplicateScopedTyVars :: [(Name,TcTyVar)] -> TcM ()
-- Check for duplicates
-- E.g. data SameKind (a::k) (b::k)
@@ -3083,6 +3090,63 @@ explicitly, rather than binding it implicitly via unification.
The scoped-tyvar stuff is needed precisely for data/class/newtype declarations,
where needsEtaExpansion is True.
+
+Note [Out of arity type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(Relevant ticket: #24470)
+Type synonyms have a special scoping rule that allows implicit quantification in
+the outermost kind signature:
+
+ type P_e :: k -> Type
+ type P_e @k = Proxy :: k -> Type -- explicit binding
+
+ type P_i = Proxy :: k -> Type -- implicit binding (relies on the special rule)
+
+This is a deprecated feature (warning flag: -Wimplicit-rhs-quantification) but
+we have to support it for a couple more releases. It is explained in more detail
+in Note [Implicit quantification in type synonyms] in GHC.Rename.HsType.
+
+Type synonyms `P_e` and `P_i` are equivalent. Both of them have kind
+`forall k. k -> Type` and arity 1. (Recall that the arity of a type synonym is
+the number of arguments it requires at use sites; the arity matter because
+unsaturated application of type families and type synonyms is not allowed).
+
+We start to see problems when implicit RHS quantification (as in `P_i`) is
+combined with a standalone king signature (like the one that `P_e` has).
+That is:
+
+ type P_i_sig :: k -> Type
+ type P_i_sig = Proxy :: k -> Type
+
+Per GHC Proposal #425, the arity of `P_i_sig` is determined /by the LHS only/,
+which has no binders. So the arity of `P_i_sig` is 0.
+At the same time, the legacy implicit quantification rule dictates that `k` is
+brought into scope, as if there was a binder `@k` on the LHS.
+
+We end up with a `k` that is in scope on the RHS but cannot be bound implicitly
+on the LHS without affecting the arity. This led to #24470 (a compiler crash)
+
+ GHC internal error: ‘k’ is not in scope during type checking,
+ but it passed the renamer
+
+This problem occurs only if the arity of the type synonym is insufficiently
+high to accommodate an implicit binding. It can be worked around by adding an
+unused binder on the LHS:
+
+ type P_w :: k -> Type
+ type P_w @_w = Proxy :: k -> Type
+
+The variable `_w` is unused. The only effect of the `@_w` binder is that the
+arity of `P_w` is changed from 0 to 1. However, bumping the arity is exactly
+what's needed to make the implicit binding of `k` possible.
+
+All this is a rather unfortunate bit of accidental complexity that will go away
+when GHC drops support for implicit RHS quantification. In the meantime, we
+ought to produce a proper error message instead of a compiler panic, and we do
+that with a check in checkForDisconnectedScopedTyVars:
+
+ | flav == TypeSynonymFlavour = mapM_ report_out_of_arity (filterOut ok scoped_prs)
+
-}
{- *********************************************************************
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index f45cf0fdfb81..e72753677f36 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -606,6 +606,7 @@ type family GhcDiagnosticCode c = n | n -> c where
GhcDiagnosticCode "TcRnInvisPatWithNoForAll" = 14964
GhcDiagnosticCode "TcRnIllegalInvisibleTypePattern" = 78249
GhcDiagnosticCode "TcRnNamespacedFixitySigWithoutFlag" = 78534
+ GhcDiagnosticCode "TcRnOutOfArityTyVar" = 84925
-- TcRnTypeApplicationsDisabled
GhcDiagnosticCode "TypeApplication" = 23482
diff --git a/testsuite/tests/typecheck/should_compile/T24470b.hs b/testsuite/tests/typecheck/should_compile/T24470b.hs
new file mode 100644
index 000000000000..63d0757cf2c9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T24470b.hs
@@ -0,0 +1,10 @@
+{-# OPTIONS_GHC -Wno-implicit-rhs-quantification #-}
+{-# LANGUAGE TypeAbstractions #-}
+
+module T24470b where
+
+import Data.Kind
+import Data.Data
+
+type SynOK :: forall k. k -> Type
+type SynOK @t = Proxy :: j -> Type
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 0d3ff57dbeca..824bf93c5f83 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -912,3 +912,4 @@ test('T21206', normal, compile, [''])
test('T17594a', req_th, compile, [''])
test('T17594f', normal, compile, [''])
test('WarnDefaultedExceptionContext', normal, compile, ['-Wdefaulted-exception-context'])
+test('T24470b', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T24470a.hs b/testsuite/tests/typecheck/should_fail/T24470a.hs
new file mode 100644
index 000000000000..7b96b5b3d7af
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T24470a.hs
@@ -0,0 +1,7 @@
+module T24470a where
+
+import Data.Data
+import Data.Kind
+
+type SynBad :: forall k. k -> Type
+type SynBad = Proxy :: j -> Type
diff --git a/testsuite/tests/typecheck/should_fail/T24470a.stderr b/testsuite/tests/typecheck/should_fail/T24470a.stderr
new file mode 100644
index 000000000000..068c61c8cde1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T24470a.stderr
@@ -0,0 +1,6 @@
+
+T24470a.hs:7:24: error: [GHC-84925]
+ • The arity of ‘SynBad’ is insufficiently high to accommodate
+ an implicit binding for the ‘j’ type variable.
+ • Use ‘@j’ on the LHS or ‘forall j.’ on the RHS to bring it into scope.
+ • In the type synonym declaration for ‘SynBad’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 1c782f971df7..f593052d4a5e 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -722,3 +722,5 @@ test('DoExpansion3', normal, compile, ['-fdefer-type-errors'])
test('T17594c', normal, compile_fail, [''])
test('T17594d', normal, compile_fail, [''])
test('T17594g', normal, compile_fail, [''])
+
+test('T24470a', normal, compile_fail, [''])
--
GitLab