From faa30b41a6f941627ddeeba805815b2742d312d1 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simon.peytonjones@gmail.com>
Date: Fri, 29 Mar 2024 21:54:09 +0000
Subject: [PATCH] Deal with duplicate tyvars in type declarations
GHC was outright crashing before this fix: #24604
---
compiler/GHC/Tc/Gen/HsType.hs | 93 ++++++++++++++-----
.../tests/saks/should_compile/saks018.hs | 2 +-
.../tests/saks/should_compile/saks021.hs | 2 +-
testsuite/tests/saks/should_fail/all.T | 2 +
.../tests/saks/should_fail/saks018-fail.hs | 9 ++
.../saks/should_fail/saks018-fail.stderr | 4 +
.../tests/saks/should_fail/saks021-fail.hs | 9 ++
.../saks/should_fail/saks021-fail.stderr | 4 +
.../tests/typecheck/should_compile/T24470b.hs | 2 +-
testsuite/tests/vdq-rta/should_fail/T24604.hs | 7 ++
.../tests/vdq-rta/should_fail/T24604.stderr | 4 +
.../tests/vdq-rta/should_fail/T24604a.hs | 9 ++
.../tests/vdq-rta/should_fail/T24604a.stderr | 4 +
testsuite/tests/vdq-rta/should_fail/all.T | 4 +-
14 files changed, 129 insertions(+), 26 deletions(-)
create mode 100644 testsuite/tests/saks/should_fail/saks018-fail.hs
create mode 100644 testsuite/tests/saks/should_fail/saks018-fail.stderr
create mode 100644 testsuite/tests/saks/should_fail/saks021-fail.hs
create mode 100644 testsuite/tests/saks/should_fail/saks021-fail.stderr
create mode 100644 testsuite/tests/vdq-rta/should_fail/T24604.hs
create mode 100644 testsuite/tests/vdq-rta/should_fail/T24604.stderr
create mode 100644 testsuite/tests/vdq-rta/should_fail/T24604a.hs
create mode 100644 testsuite/tests/vdq-rta/should_fail/T24604a.stderr
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 70189387a9f0..90ff0f1ae04d 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2570,9 +2570,11 @@ kcCheckDeclHeader_sig sig_kind name flav
; traceTc "kcCheckDeclHeader_sig {" $
vcat [ text "sig_kind:" <+> ppr sig_kind
, text "sig_tcbs:" <+> ppr sig_tcbs
- , text "sig_res_kind:" <+> ppr sig_res_kind ]
+ , text "sig_res_kind:" <+> ppr sig_res_kind
+ , text "implict_nms:" <+> ppr implicit_nms
+ , text "hs_tv_bndrs:" <+> ppr hs_tv_bndrs ]
- ; (tclvl, wanted, (implicit_tvs, (skol_tcbs, (extra_tcbs, tycon_res_kind))))
+ ; (tclvl, wanted, (implicit_tvs, (skol_tcbs, skol_scoped_tvs, (extra_tcbs, tycon_res_kind))))
<- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_sig" $ -- #16687
bindImplicitTKBndrs_Q_Tv implicit_nms $ -- Q means don't clone
matchUpSigWithDecl name sig_tcbs sig_res_kind hs_tv_bndrs $ \ excess_sig_tcbs sig_res_kind ->
@@ -2615,9 +2617,18 @@ kcCheckDeclHeader_sig sig_kind name flav
-- Here p and q both map to the same kind variable k. We don't allow this
-- so we must check that they are distinct. A similar thing happens
-- in GHC.Tc.TyCl.swizzleTcTyConBinders during inference.
+ --
+ -- With visible dependent quantification, one of the binders involved
+ -- may be explicit. Consider #24604
+ -- type UF :: forall zk -> zk -> Constraint
+ -- class UF kk (xb :: k)
+ -- Here `k` and `kk` both denote the same variable; but only `k` is implicit
+ -- Hence we need to add skol_scoped_tvs
; implicit_tvs <- liftZonkM $ zonkTcTyVarsToTcTyVars implicit_tvs
; let implicit_prs = implicit_nms `zip` implicit_tvs
- ; checkForDuplicateScopedTyVars implicit_prs
+ dup_chk_prs = implicit_prs ++ mkTyVarNamePairs skol_scoped_tvs
+ ; unless (null implicit_nms) $ -- No need if no implicit tyvars
+ checkForDuplicateScopedTyVars dup_chk_prs
; checkForDisconnectedScopedTyVars name flav all_tcbs implicit_prs
-- Swizzle the Names so that the TyCon uses the user-declared implicit names
@@ -2686,6 +2697,7 @@ matchUpSigWithDecl
-> ([TcTyConBinder] -> TcKind -> TcM a) -- All user-written binders are in scope
-- Argument is excess TyConBinders and tail kind
-> TcM ( [TcTyConBinder] -- Skolemised binders, with TcTyVars
+ , [TcTyVar] -- Skolem tyvars brought into lexical scope by this matching-up
, a )
-- See Note [Matching a kind signature with a declaration]
-- Invariant: Length of returned TyConBinders + length of excess TyConBinders
@@ -2696,7 +2708,7 @@ matchUpSigWithDecl name sig_tcbs sig_res_kind hs_bndrs thing_inside
go subst tcbs []
= do { let (subst', tcbs') = substTyConBindersX subst tcbs
; res <- thing_inside tcbs' (substTy subst' sig_res_kind)
- ; return ([], res) }
+ ; return ([], [], res) }
go _ [] hs_bndrs
= failWithTc (TcRnTooManyBinders sig_res_kind hs_bndrs)
@@ -2712,17 +2724,22 @@ matchUpSigWithDecl name sig_tcbs sig_res_kind hs_bndrs thing_inside
-- that come from the type declaration, not the kind signature
subst' = extendTCvSubstWithClone subst tv tv'
; tc_hs_bndr (unLoc hs_bndr) (tyVarKind tv')
- ; (tcbs', res) <- tcExtendTyVarEnv [tv'] $
- go subst' tcbs' hs_bndrs'
- ; return (Bndr tv' vis : tcbs', res) }
+ ; traceTc "musd1" (ppr tcb $$ ppr hs_bndr $$ ppr tv')
+ ; (tcbs', tvs, res) <- tcExtendTyVarEnv [tv'] $
+ go subst' tcbs' hs_bndrs'
+ ; return (Bndr tv' vis : tcbs', tv':tvs, res) }
+ -- We do a tcExtendTyVarEnv [tv'], so we return tv' in
+ -- the list of lexically-scoped skolem type variables
| skippable (binderFlag tcb)
= -- Invisible TyConBinder, so do not consume one of the hs_bndrs
do { let (subst', tcb') = substTyConBinderX subst tcb
- ; (tcbs', res) <- go subst' tcbs' hs_bndrs
+ ; traceTc "musd2" (ppr tcb $$ ppr hs_bndr $$ ppr tcb')
+ ; (tcbs', tvs, res) <- go subst' tcbs' hs_bndrs
-- NB: pass on hs_bndrs unchanged; we do not consume a
-- HsTyVarBndr for an invisible TyConBinder
- ; return (tcb' : tcbs', res) }
+ ; return (tcb' : tcbs', tvs, res) }
+ -- Return `tvs`; no new lexically-scoped TyVars brought into scope
| otherwise =
-- At this point we conclude that:
@@ -2736,14 +2753,19 @@ matchUpSigWithDecl name sig_tcbs sig_res_kind hs_bndrs thing_inside
= return ()
tc_hs_bndr (KindedTyVar _ _ (L _ hs_nm) lhs_kind) expected_kind
= do { sig_kind <- tcLHsKindSig (TyVarBndrKindCtxt hs_nm) lhs_kind
+ ; traceTc "musd3:unifying" (ppr sig_kind $$ ppr expected_kind)
; discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
unifyKind (Just (NameThing hs_nm)) sig_kind expected_kind }
-- See GHC Proposal #425, section "Kind checking",
-- where zippable and skippable are defined.
+ -- In particular: we match up if
+ -- (a) HsBndr looks like @k, and TyCon binder is forall k. (NamedTCB Specified)
+ -- (b) HsBndr looks like a, and TyCon binder is forall k -> (NamedTCB Required)
+ -- or k -> (AnonTCB)
zippable :: TyConBndrVis -> HsBndrVis GhcRn -> Bool
- zippable vis (HsBndrRequired _) = isVisibleTcbVis vis
- zippable vis (HsBndrInvisible _) = isInvisSpecTcbVis vis
+ zippable vis (HsBndrInvisible _) = isInvisSpecTcbVis vis -- (a)
+ zippable vis (HsBndrRequired _) = isVisibleTcbVis vis -- (b)
-- See GHC Proposal #425, section "Kind checking",
-- where zippable and skippable are defined.
@@ -3007,15 +3029,7 @@ checkForDisconnectedScopedTyVars name flav all_tcbs scoped_prs
checkForDuplicateScopedTyVars :: [(Name,TcTyVar)] -> TcM ()
-- Check for duplicates
--- E.g. data SameKind (a::k) (b::k)
--- data T (a::k1) (b::k2) c = MkT (SameKind a b) c
--- Here k1 and k2 start as TyVarTvs, and get unified with each other
--- If this happens, things get very confused later, so fail fast
---
--- In the CUSK case k1 and k2 are skolems so they won't unify;
--- but in the inference case (see generaliseTcTyCon),
--- and the type-sig case (see kcCheckDeclHeader_sig), they are
--- TcTyVars, so we must check.
+-- See Note [Aliasing in type and class declarations]
checkForDuplicateScopedTyVars scoped_prs
= unless (null err_prs) $
do { mapM_ report_dup err_prs; failM }
@@ -3035,8 +3049,43 @@ checkForDuplicateScopedTyVars scoped_prs
addErrTc $ TcRnDifferentNamesForTyVar n1 n2
-{- Note [Disconnected type variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Aliasing in type and class declarations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data SameKind (a::k) (b::k)
+ data T1 (a::k1) (b::k2) c = MkT (SameKind a b) c
+We do not allow this, because `k1` and `k2` would both stand for the same type
+variable -- they are both aliases for `k`.
+
+Other examples
+ data T2 (a::k1) = MkT2 (SameKind a Int) -- k1 stands for Type
+ data T3 @k1 @k2 (a::k1) (b::k2) = MkT (SameKind a b) -- k1 and k2 are aliases
+
+ type UF :: forall zk. zk -> Constraint
+ class UF @kk (xb :: k) where -- kk and k are aliases
+ op :: (xs::kk) -> Bool
+
+See #24604 for an example that crashed GHC.
+
+There is a design choice here. It would be possible to allow implicit type variables
+like `k1` and `k2` in T1's declartion to stand for /abitrary kinds/. This is in fact
+the rule we use in /terms/ pattern signatures:
+ f :: [Int] -> Int
+ f ((x::a) : xs) = ...
+Here `a` stands for `Int`. But in type /signatures/ we make a different choice:
+ f1 :: forall (a::k1) (b::k2). SameKind a b -> blah
+ f2 :: forall (a::k). SameKind a Int -> blah
+
+Here f1's signature is rejected because `k1` and `k2` are aliased; and f2's is
+rejected because `k` stands for `Int`.
+
+Our current choice is that type and class declarations behave more like signatures;
+we do not allow aliasing. That is what `checkForDuplicateScopedTyVars` checks.
+See !12328 for some design discussion.
+
+
+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.
diff --git a/testsuite/tests/saks/should_compile/saks018.hs b/testsuite/tests/saks/should_compile/saks018.hs
index a24a19e117fd..63dfac1c9c6a 100644
--- a/testsuite/tests/saks/should_compile/saks018.hs
+++ b/testsuite/tests/saks/should_compile/saks018.hs
@@ -6,4 +6,4 @@ module SAKS_018 where
import Data.Kind (Type)
type T :: forall k -> k -> Type
-data T k (x :: hk)
+data T j (x :: j)
diff --git a/testsuite/tests/saks/should_compile/saks021.hs b/testsuite/tests/saks/should_compile/saks021.hs
index 00bf9f891895..929fef8a1af7 100644
--- a/testsuite/tests/saks/should_compile/saks021.hs
+++ b/testsuite/tests/saks/should_compile/saks021.hs
@@ -6,4 +6,4 @@ module SAKS_021 where
import Data.Kind (Type)
type T :: forall k -> forall (xx :: k) -> Type
-data T k (x :: hk)
+data T j (x :: j)
diff --git a/testsuite/tests/saks/should_fail/all.T b/testsuite/tests/saks/should_fail/all.T
index 5b29049fb601..798e287d9716 100644
--- a/testsuite/tests/saks/should_fail/all.T
+++ b/testsuite/tests/saks/should_fail/all.T
@@ -36,3 +36,5 @@ test('T18863b', normal, compile_fail, [''])
test('T18863c', normal, compile_fail, [''])
test('T18863d', normal, compile_fail, [''])
test('T20916', normal, compile_fail, [''])
+test('saks018-fail', normal, compile_fail, [''])
+test('saks021-fail', normal, compile_fail, [''])
diff --git a/testsuite/tests/saks/should_fail/saks018-fail.hs b/testsuite/tests/saks/should_fail/saks018-fail.hs
new file mode 100644
index 000000000000..a24a19e117fd
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/saks018-fail.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE PolyKinds, ExplicitForAll #-}
+
+module SAKS_018 where
+
+import Data.Kind (Type)
+
+type T :: forall k -> k -> Type
+data T k (x :: hk)
diff --git a/testsuite/tests/saks/should_fail/saks018-fail.stderr b/testsuite/tests/saks/should_fail/saks018-fail.stderr
new file mode 100644
index 000000000000..803486fcf214
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/saks018-fail.stderr
@@ -0,0 +1,4 @@
+
+saks018-fail.hs:9:8: error: [GHC-17370]
+ • Different names for the same type variable: ‘hk’ and ‘k’
+ • In the data type declaration for ‘T’
diff --git a/testsuite/tests/saks/should_fail/saks021-fail.hs b/testsuite/tests/saks/should_fail/saks021-fail.hs
new file mode 100644
index 000000000000..00bf9f891895
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/saks021-fail.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE PolyKinds, ExplicitForAll #-}
+
+module SAKS_021 where
+
+import Data.Kind (Type)
+
+type T :: forall k -> forall (xx :: k) -> Type
+data T k (x :: hk)
diff --git a/testsuite/tests/saks/should_fail/saks021-fail.stderr b/testsuite/tests/saks/should_fail/saks021-fail.stderr
new file mode 100644
index 000000000000..3b1fe73812f5
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/saks021-fail.stderr
@@ -0,0 +1,4 @@
+
+saks021-fail.hs:9:8: error: [GHC-17370]
+ • Different names for the same type variable: ‘hk’ and ‘k’
+ • In the data type declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_compile/T24470b.hs b/testsuite/tests/typecheck/should_compile/T24470b.hs
index 63d0757cf2c9..fbd93d36af66 100644
--- a/testsuite/tests/typecheck/should_compile/T24470b.hs
+++ b/testsuite/tests/typecheck/should_compile/T24470b.hs
@@ -7,4 +7,4 @@ import Data.Kind
import Data.Data
type SynOK :: forall k. k -> Type
-type SynOK @t = Proxy :: j -> Type
+type SynOK @j = Proxy :: j -> Type
diff --git a/testsuite/tests/vdq-rta/should_fail/T24604.hs b/testsuite/tests/vdq-rta/should_fail/T24604.hs
new file mode 100644
index 000000000000..1ada99903d04
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T24604.hs
@@ -0,0 +1,7 @@
+module T24604 where
+
+import Data.Kind
+
+type UF :: forall zk -> zk -> Constraint
+class UF kk (xb :: k) where
+ op :: (xs::kk) -> Bool
diff --git a/testsuite/tests/vdq-rta/should_fail/T24604.stderr b/testsuite/tests/vdq-rta/should_fail/T24604.stderr
new file mode 100644
index 000000000000..f791bc2ea9ae
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T24604.stderr
@@ -0,0 +1,4 @@
+
+T24604.hs:6:10: error: [GHC-17370]
+ • Different names for the same type variable: ‘k’ and ‘kk’
+ • In the class declaration for ‘UF’
diff --git a/testsuite/tests/vdq-rta/should_fail/T24604a.hs b/testsuite/tests/vdq-rta/should_fail/T24604a.hs
new file mode 100644
index 000000000000..03fcd009fbce
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T24604a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeAbstractions #-}
+
+module T24604a where
+
+import Data.Kind
+
+type UF :: forall zk. zk -> Constraint
+class UF @kk (xb :: k) where
+ op :: (xs::kk) -> Bool
diff --git a/testsuite/tests/vdq-rta/should_fail/T24604a.stderr b/testsuite/tests/vdq-rta/should_fail/T24604a.stderr
new file mode 100644
index 000000000000..c0a74a325dca
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T24604a.stderr
@@ -0,0 +1,4 @@
+
+T24604a.hs:8:11: error: [GHC-17370]
+ • Different names for the same type variable: ‘k’ and ‘kk’
+ • In the class declaration for ‘UF’
diff --git a/testsuite/tests/vdq-rta/should_fail/all.T b/testsuite/tests/vdq-rta/should_fail/all.T
index a0811d4de85b..197174430fb7 100644
--- a/testsuite/tests/vdq-rta/should_fail/all.T
+++ b/testsuite/tests/vdq-rta/should_fail/all.T
@@ -17,4 +17,6 @@ test('T23738_fail_implicit_tv', normal, compile_fail, [''])
test('T23738_fail_var', normal, compile_fail, [''])
test('T24176', normal, compile_fail, [''])
test('T23739_fail_ret', normal, compile_fail, [''])
-test('T23739_fail_case', normal, compile_fail, [''])
\ No newline at end of file
+test('T23739_fail_case', normal, compile_fail, [''])
+test('T24604', normal, compile_fail, [''])
+test('T24604a', normal, compile_fail, [''])
--
GitLab