[Git][ghc/ghc][wip/sand-witch/fix-tysyn] Fix compiler crash caused by implicit RHS quantification in type synonyms (24470)
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Thu Mar 7 13:24:48 UTC 2024
Andrei Borzenkov pushed to branch wip/sand-witch/fix-tysyn at Glasgow Haskell Compiler / GHC
Commits:
26fa4a3a by Andrei Borzenkov at 2024-03-07T17:24:28+04:00
Fix compiler crash caused by implicit RHS quantification in type synonyms (24470)
- - - - -
9 changed files:
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Types/Error/Codes.hs
- + testsuite/tests/typecheck/should_compile/T24470b.hs
- testsuite/tests/typecheck/should_compile/all.T
- + testsuite/tests/typecheck/should_fail/T24470a.hs
- + testsuite/tests/typecheck/should_fail/T24470a.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -1911,6 +1911,11 @@ instance Diagnostic TcRnMessage where
, text "in a fixity signature"
]
+ TcRnOutOfArityTyVar ts_name tv_name -> mkSimpleDecorated $
+ text "Type variable" <+> quotes (ppr tv_name) <+>
+ text "in the right-hand side of type synonym" <+> quotes (ppr ts_name) <+>
+ text "is out of arity"
+
diagnosticReason :: TcRnMessage -> DiagnosticReason
diagnosticReason = \case
TcRnUnknownMessage m
@@ -2543,6 +2548,8 @@ instance Diagnostic TcRnMessage where
-> ErrorWithoutFlag
TcRnNamespacedFixitySigWithoutFlag{}
-> ErrorWithoutFlag
+ TcRnOutOfArityTyVar{}
+ -> ErrorWithoutFlag
diagnosticHints = \case
TcRnUnknownMessage m
@@ -3209,6 +3216,8 @@ instance Diagnostic TcRnMessage where
-> noHints
TcRnNamespacedFixitySigWithoutFlag{}
-> [suggestExtension LangExt.ExplicitNamespaces]
+ TcRnOutOfArityTyVar{}
+ -> noHints
diagnosticCode = constructorCode
=====================================
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
@@ -4263,6 +4265,23 @@ data TcRnMessage where
-}
TcRnNamespacedFixitySigWithoutFlag :: FixitySig GhcPs -> TcRnMessage
+ {-| TcRnOutOfArityTyVar is an error raised when an implicitly quantified
+ type variable on the RHS of a type synonym doesn't match the arity specified
+ by a user on the LHS of the 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
----
=====================================
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 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,52 @@ 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]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type signatures have special rule about scoping of the outmost kind signatures:
+
+ type P = Proxy :: k -> Type
+
+Here `k` isn't bind anywhere, however GHC performs implicit binding in this
+specific case, so the example above becomes equivalent to that declaration:
+
+ type P @k = Proxy :: k -> Type
+
+Doing so changes arity of type synonym declaration and could be observed e.g. when
+we use type synonym in high order position:
+
+ type T :: (forall k. k -> Type) -> Type
+
+ type P = Proxy
+
+ x :: T P -- Expected kind ‘forall k. k -> *’, but ‘P’ has kind ‘k0 -> *’
+
+To give user more control under arity of type declaration, we do not perform
+airty inference in check mode (i.e. when type synonym has standalone kind signature)
+starting from e89aa0721ca commit:
+
+ type T :: (forall k. k -> Type) -> Type
+
+ type P :: forall k. k -> Type
+ type P = Proxy
+
+ x :: T P -- OK
+
+However, renamer still adds type variables from outmost kind signature into
+scope (see #24470) because it doesn't have infromation about standalone kind
+signature in the context:
+
+ type P :: forall j. j -> Type
+ type P = Proxy :: k -> Type -- `k` is not in scope during type checking,
+ -- but it passed the renamer
+
+To handle this case, we add validation into `checkForDisconnectedScopedTyVars` function.
+Notice that an implicit binding isn't a problem itself, but becomes a problem when
+it's out of specified arity of type synonym, i.e. this code is fine:
+
+ type P :: forall j. j -> Type
+ type P @j = Proxy :: k -> Type
-}
{- *********************************************************************
=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -605,6 +605,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
=====================================
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
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -911,3 +911,4 @@ test('T22788', normal, compile, [''])
test('T21206', normal, compile, [''])
test('T17594a', req_th, compile, [''])
test('T17594f', normal, compile, [''])
+test('T24470b', normal, compile, [''])
=====================================
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
=====================================
testsuite/tests/typecheck/should_fail/T24470a.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T24470a.hs:7:24: error: [GHC-84925]
+ • Type variable ‘j’ in the right-hand side of type synonym ‘SynBad’ is out of arity
+ • In the type synonym declaration for ‘SynBad’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -721,3 +721,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, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/26fa4a3a8be8f2ab10d606670ba2980dcfd119e8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/26fa4a3a8be8f2ab10d606670ba2980dcfd119e8
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240307/f17ebd5b/attachment-0001.html>
More information about the ghc-commits
mailing list