[Git][ghc/ghc][wip/T24604] Improvements: handle @a binders too

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Mon Apr 1 16:26:17 UTC 2024



Simon Peyton Jones pushed to branch wip/T24604 at Glasgow Haskell Compiler / GHC


Commits:
bf5e0858 by Simon Peyton Jones at 2024-04-01T17:25:44+01:00
Improvements: handle @a binders too

- - - - -


5 changed files:

- compiler/GHC/Tc/Gen/HsType.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 ->
@@ -2625,8 +2625,7 @@ kcCheckDeclHeader_sig sig_kind name flav
         -- Hence we need to add the visible binders into dup_chk_prs
         ; 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]             -- Tyvar 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,19 @@ 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) }
 
       | 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 +2756,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.


=====================================
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/bf5e08589e240d49c50b695959d0382c4fbae47f

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bf5e08589e240d49c50b695959d0382c4fbae47f
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/20240401/9402f58c/attachment-0001.html>


More information about the ghc-commits mailing list