[Git][ghc/ghc][wip/T24604] Deal with duplicate tyvars in type declarations
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue Apr 2 15:20:25 UTC 2024
Simon Peyton Jones pushed to branch wip/T24604 at Glasgow Haskell Compiler / GHC
Commits:
60ad6eb6 by Simon Peyton Jones at 2024-04-02T16:20:01+01:00
Deal with duplicate tyvars in type declarations
GHC was outright crashing before this fix: #24604
- - - - -
9 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- testsuite/tests/saks/should_compile/all.T
- + testsuite/tests/saks/should_compile/saks018.stderr
- + testsuite/tests/saks/should_compile/saks021.stderr
- testsuite/tests/typecheck/should_compile/T24470b.hs
- testsuite/tests/vdq-rta/should_fail/T24604.hs
- + testsuite/tests/vdq-rta/should_fail/T24604a.hs
- + testsuite/tests/vdq-rta/should_fail/T24604a.stderr
- testsuite/tests/vdq-rta/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -2573,7 +2573,7 @@ kcCheckDeclHeader_sig sig_kind name flav
, 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 ->
@@ -2622,11 +2622,10 @@ kcCheckDeclHeader_sig sig_kind name flav
-- 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 the visible binders into dup_chk_prs
+ -- Hence we need to add skol_scoped_tvs
; implicit_tvs <- liftZonkM $ zonkTcTyVarsToTcTyVars implicit_tvs
; let implicit_prs = implicit_nms `zip` implicit_tvs
- dup_chk_prs = implicit_prs ++
- [ (tyVarName tv, tv) | Bndr tv vis <- skol_tcbs, isVisibleTcbVis vis ]
+ 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
@@ -2697,6 +2696,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
@@ -2707,7 +2707,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)
@@ -2724,18 +2724,21 @@ matchUpSigWithDecl name sig_tcbs sig_res_kind hs_bndrs thing_inside
subst' = extendTCvSubstWithClone subst tv tv'
; tc_hs_bndr (unLoc hs_bndr) (tyVarKind tv')
; traceTc "musd1" (ppr tcb $$ ppr hs_bndr $$ ppr tv')
- ; (tcbs', res) <- tcExtendTyVarEnv [tv'] $
- go subst' tcbs' hs_bndrs'
- ; return (Bndr tv' vis : tcbs', res) }
+ ; (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
; traceTc "musd2" (ppr tcb $$ ppr hs_bndr $$ ppr tcb')
- ; (tcbs', res) <- go subst' tcbs' hs_bndrs
+ ; (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:
@@ -2755,9 +2758,13 @@ matchUpSigWithDecl name sig_tcbs sig_res_kind hs_bndrs thing_inside
-- 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.
@@ -3021,15 +3028,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 }
@@ -3049,8 +3048,41 @@ 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.
+
+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.
=====================================
testsuite/tests/saks/should_compile/all.T
=====================================
@@ -13,10 +13,10 @@ test('saks014', normal, compile, [''])
test('saks015', normal, compile, [''])
test('saks016', normal, compile, [''])
test('saks017', normal, compile, [''])
-test('saks018', normal, compile, [''])
+test('saks018', normal, compile_fail, [''])
test('saks019', normal, compile, [''])
test('saks020', normal, compile, [''])
-test('saks021', normal, compile, [''])
+test('saks021', normal, compile_fail, [''])
test('saks023', normal, ghci_script, ['saks023.script'])
test('saks024', normal, compile, [''])
test('saks025', extra_files(['saks025.hs']), ghci_script, ['saks025.script'])
=====================================
testsuite/tests/saks/should_compile/saks018.stderr
=====================================
@@ -0,0 +1,4 @@
+
+saks018.hs:9:8: error: [GHC-17370]
+ • Different names for the same type variable: ‘hk’ and ‘k’
+ • In the data type declaration for ‘T’
=====================================
testsuite/tests/saks/should_compile/saks021.stderr
=====================================
@@ -0,0 +1,4 @@
+
+saks021.hs:9:8: error: [GHC-17370]
+ • Different names for the same type variable: ‘hk’ and ‘k’
+ • In the data type declaration for ‘T’
=====================================
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
=====================================
testsuite/tests/vdq-rta/should_fail/T24604.hs
=====================================
@@ -1,6 +1,6 @@
module T24604 where
-import Data.Kind (Constraint, Type)
+import Data.Kind
type UF :: forall zk -> zk -> Constraint
class UF kk (xb :: k) where
=====================================
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
=====================================
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’
=====================================
testsuite/tests/vdq-rta/should_fail/all.T
=====================================
@@ -19,3 +19,4 @@ test('T24176', normal, compile_fail, [''])
test('T23739_fail_ret', normal, compile_fail, [''])
test('T23739_fail_case', normal, compile_fail, [''])
test('T24604', normal, compile_fail, [''])
+test('T24604a', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/60ad6eb6b45a126f4c8f47173db40bed50ccba92
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/60ad6eb6b45a126f4c8f47173db40bed50ccba92
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/20240402/4f71621c/attachment-0001.html>
More information about the ghc-commits
mailing list