From 6dbab1808bfbe484b3fb396aab1d105314f918d8 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simon.peytonjones@gmail.com>
Date: Tue, 7 Nov 2023 23:51:19 +0100
Subject: [PATCH] Add an extra check in kcCheckDeclHeader_sig
Fix #24083 by checking for a implicitly-scoped type variable that is not
actually bound. See Note [Disconnected type variables] in GHC.Tc.Gen.HsType
For some reason, on aarch64-darwin we saw a 2.8% decrease in compiler
allocations for MultiLayerModulesTH_Make; but 0.0% on other architectures.
Metric Decrease:
MultiLayerModulesTH_Make
---
compiler/GHC/Tc/Errors/Ppr.hs | 10 ++++
compiler/GHC/Tc/Errors/Types.hs | 7 +++
compiler/GHC/Tc/Gen/HsType.hs | 66 +++++++++++++++++++++++--
compiler/GHC/Types/Error/Codes.hs | 1 +
compiler/GHC/Types/Hint.hs | 4 ++
compiler/GHC/Types/Hint/Ppr.hs | 3 ++
testsuite/tests/polykinds/T24083.hs | 14 ++++++
testsuite/tests/polykinds/T24083.stderr | 6 +++
testsuite/tests/polykinds/all.T | 1 +
9 files changed, 107 insertions(+), 5 deletions(-)
create mode 100644 testsuite/tests/polykinds/T24083.hs
create mode 100644 testsuite/tests/polykinds/T24083.stderr
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index d47d3d100d5b..74587d877318 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -999,6 +999,12 @@ instance Diagnostic TcRnMessage where
-- Note [Swizzling the tyvars before generaliseTcTyCon]
= vcat [ quotes (ppr n1) <+> text "bound at" <+> ppr (getSrcLoc n1)
, quotes (ppr n2) <+> text "bound at" <+> ppr (getSrcLoc n2) ]
+
+ TcRnDisconnectedTyVar n
+ -> mkSimpleDecorated $
+ hang (text "Scoped type variable only appears non-injectively in declaration header:")
+ 2 (quotes (ppr n) <+> text "bound at" <+> ppr (getSrcLoc n))
+
TcRnInvalidReturnKind data_sort allowed_kind kind _suggested_ext
-> mkSimpleDecorated $
sep [ ppDataSort data_sort <+>
@@ -2201,6 +2207,8 @@ instance Diagnostic TcRnMessage where
-> ErrorWithoutFlag
TcRnDifferentNamesForTyVar{}
-> ErrorWithoutFlag
+ TcRnDisconnectedTyVar{}
+ -> ErrorWithoutFlag
TcRnInvalidReturnKind{}
-> ErrorWithoutFlag
TcRnClassKindNotConstraint{}
@@ -2842,6 +2850,8 @@ instance Diagnostic TcRnMessage where
-> noHints
TcRnDifferentNamesForTyVar{}
-> noHints
+ TcRnDisconnectedTyVar n
+ -> [SuggestBindTyVarExplicitly n]
TcRnInvalidReturnKind _ _ _ mb_suggest_unlifted_ext
-> case mb_suggest_unlifted_ext of
Nothing -> noHints
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 5ef90283e3ec..572b44b695c4 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -2276,6 +2276,13 @@ data TcRnMessage where
-}
TcRnDifferentNamesForTyVar :: !Name -> !Name -> TcRnMessage
+ {-| TcRnDisconnectedTyVar is an error for a data declaration that has a kind signature,
+ 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.
+ -}
+ TcRnDisconnectedTyVar :: !Name -> TcRnMessage
+
{-| TcRnInvalidReturnKind is an error for a data declaration that has a kind signature
with an invalid result kind.
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 5ffe4d35526e..7b0d838372b5 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2608,6 +2608,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 all_tcbs implicit_prs
-- Swizzle the Names so that the TyCon uses the user-declared implicit names
-- E.g type T :: k -> Type
@@ -2621,11 +2622,11 @@ kcCheckDeclHeader_sig sig_kind name flav
all_tv_prs = mkTyVarNamePairs (binderVars swizzled_tcbs)
; traceTc "kcCheckDeclHeader swizzle" $ vcat
- [ text "implicit_prs = " <+> ppr implicit_prs
- , text "implicit_nms = " <+> ppr implicit_nms
- , text "hs_tv_bndrs = " <+> ppr hs_tv_bndrs
- , text "all_tcbs = " <+> pprTyVars (binderVars all_tcbs)
- , text "swizzled_tcbs = " <+> pprTyVars (binderVars swizzled_tcbs)
+ [ text "sig_tcbs =" <+> ppr sig_tcbs
+ , text "implicit_prs =" <+> ppr implicit_prs
+ , text "hs_tv_bndrs =" <+> ppr hs_tv_bndrs
+ , text "all_tcbs =" <+> pprTyVars (binderVars all_tcbs)
+ , text "swizzled_tcbs =" <+> pprTyVars (binderVars swizzled_tcbs)
, text "tycon_res_kind =" <+> ppr tycon_res_kind
, text "swizzled_kind =" <+> ppr swizzled_kind ]
@@ -2963,6 +2964,22 @@ expectedKindInCtxt _ = OpenKind
* *
********************************************************************* -}
+checkForDisconnectedScopedTyVars :: [TcTyConBinder] -> [(Name,TcTyVar)] -> TcM ()
+-- See Note [Disconnected 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 sig_tcbs scoped_prs
+ = mapM_ report_disconnected (filterOut ok scoped_prs)
+ where
+ sig_tvs = mkVarSet (binderVars sig_tcbs)
+ ok (_, tc_tv) = tc_tv `elemVarSet` sig_tvs
+
+ report_disconnected :: (Name,TcTyVar) -> TcM ()
+ report_disconnected (nm, _)
+ = setSrcSpan (getSrcSpan nm) $
+ addErrTc $ TcRnDisconnectedTyVar nm
+
checkForDuplicateScopedTyVars :: [(Name,TcTyVar)] -> TcM ()
-- Check for duplicates
-- E.g. data SameKind (a::k) (b::k)
@@ -2993,6 +3010,45 @@ checkForDuplicateScopedTyVars scoped_prs
addErrTc $ TcRnDifferentNamesForTyVar n1 n2
+{- Note [Disconnected type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This note applies when kind-checking the header of a type/class decl that has
+a separate, standalone kind signature. See #24083.
+
+Consider:
+ type S a = Type
+
+ type C :: forall k. S k -> Constraint
+ class C (a :: S kk) where
+ op :: ...kk...
+
+Note that the class has a separate kind signature, so the elaborated decl should
+look like
+ class C @kk (a :: S kk) where ...
+
+But how can we "connect up" the scoped variable `kk` with the skolem kind from the
+standalone kind signature for `C`? In general we do this by unifying the two.
+For example
+ type T k = (k,Type)
+ type W :: forall k. T k -> Type
+ data W (a :: (x,Type)) = ..blah blah..
+
+When we encounter (a :: (x,Type)) we unify the kind (x,Type) with the kind (T k)
+from the standalone kind signature. Of course, unification looks through synonyms
+so we end up with the mapping [x :-> k] that connects the scoped type variable `x`
+with the kind from the signature.
+
+But in our earlier example this unification is ineffective -- because `S` is a
+phantom synonym that just discards its argument. So our plan is this:
+
+ if matchUpSigWithDecl fails to connect `kk with `k`, by unification,
+ we give up and complain about a "disconnected" type variable.
+
+See #24083 for dicussion of alternatives, none satisfactory. Also the fix is
+easy: just add an explicit `@kk` parameter to the declaration, to bind `kk`
+explicitly, rather than binding it implicitly via unification.
+-}
+
{- *********************************************************************
* *
Bringing type variables into scope
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index c7850e593e69..dc48b4313109 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -477,6 +477,7 @@ type family GhcDiagnosticCode c = n | n -> c where
GhcDiagnosticCode "TcRnInvalidVisibleKindArgument" = 20967
GhcDiagnosticCode "TcRnTooManyBinders" = 05989
GhcDiagnosticCode "TcRnDifferentNamesForTyVar" = 17370
+ GhcDiagnosticCode "TcRnDisconnectedTyVar" = 59738
GhcDiagnosticCode "TcRnInvalidReturnKind" = 55233
GhcDiagnosticCode "TcRnClassKindNotConstraint" = 80768
GhcDiagnosticCode "TcRnMatchesHaveDiffNumArgs" = 91938
diff --git a/compiler/GHC/Types/Hint.hs b/compiler/GHC/Types/Hint.hs
index 05b01884eedf..fe8882eb741f 100644
--- a/compiler/GHC/Types/Hint.hs
+++ b/compiler/GHC/Types/Hint.hs
@@ -480,6 +480,10 @@ data GhcHint
{-| Suggest explicitly quantifying a type variable instead of relying on implicit quantification -}
| SuggestExplicitQuantification RdrName
+
+ {-| Suggest binding explicitly; e.g data T @k (a :: F k) = .... -}
+ | SuggestBindTyVarExplicitly Name
+
-- | An 'InstantiationSuggestion' for a '.hsig' file. This is generated
-- by GHC in case of a 'DriverUnexpectedSignature' and suggests a way
-- to instantiate a particular signature, where the first argument is
diff --git a/compiler/GHC/Types/Hint/Ppr.hs b/compiler/GHC/Types/Hint/Ppr.hs
index dbe219a14e0c..48490b5f027b 100644
--- a/compiler/GHC/Types/Hint/Ppr.hs
+++ b/compiler/GHC/Types/Hint/Ppr.hs
@@ -271,6 +271,9 @@ instance Outputable GhcHint where
SuggestExplicitQuantification tv
-> hsep [ text "Use an explicit", quotes (text "forall")
, text "to quantify over", quotes (ppr tv) ]
+ SuggestBindTyVarExplicitly tv
+ -> text "bind" <+> quotes (ppr tv)
+ <+> text "explicitly with" <+> quotes (char '@' <> ppr tv)
perhapsAsPat :: SDoc
perhapsAsPat = text "Perhaps you meant an as-pattern, which must not be surrounded by whitespace"
diff --git a/testsuite/tests/polykinds/T24083.hs b/testsuite/tests/polykinds/T24083.hs
new file mode 100644
index 000000000000..e8e91d675e26
--- /dev/null
+++ b/testsuite/tests/polykinds/T24083.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T24083 where
+import Data.Kind (Constraint, Type)
+
+data family Pi t :: Type
+
+type FunctionSymbol :: Type -> Type
+type FunctionSymbol t = Type
+
+type IsSum :: forall s. FunctionSymbol s -> Constraint
+class IsSum (sumf :: FunctionSymbol t) where
+ sumConNames :: Pi t
diff --git a/testsuite/tests/polykinds/T24083.stderr b/testsuite/tests/polykinds/T24083.stderr
new file mode 100644
index 000000000000..a5a68dd164e1
--- /dev/null
+++ b/testsuite/tests/polykinds/T24083.stderr
@@ -0,0 +1,6 @@
+
+T24083.hs:13:14: error: [GHC-59738]
+ • Scoped type variable only appears non-injectively in declaration header:
+ ‘t’ bound at T24083.hs:13:14
+ • In the class declaration for ‘IsSum’
+ Suggested fix: bind ‘t’ explicitly with ‘@t’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index ab44471511af..c2b883809b80 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -243,3 +243,4 @@ test('T22379b', normal, compile, [''])
test('T22743', normal, compile_fail, [''])
test('T22742', normal, compile_fail, [''])
test('T22793', normal, compile_fail, [''])
+test('T24083', normal, compile_fail, [''])
--
GitLab