[Git][ghc/ghc][wip/sand-witch/pattern- at a-binders] Add more notes and comments to the patch

Andrei Borzenkov (@sand-witch) gitlab at gitlab.haskell.org
Wed Jun 28 12:22:59 UTC 2023



Andrei Borzenkov pushed to branch wip/sand-witch/pattern- at a-binders at Glasgow Haskell Compiler / GHC


Commits:
94791a61 by Andrei Borzenkov at 2023-06-28T16:22:39+04:00
Add more notes and comments to the patch

- - - - -


10 changed files:

- compiler/GHC/Hs/Type.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Rename/Pat.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/HsType.hs
- testsuite/tests/gadt/T18191.stderr
- testsuite/tests/rename/should_fail/T22478b.stderr
- testsuite/tests/rename/should_fail/T7943.stderr
- testsuite/tests/rename/should_fail/T9077.stderr


Changes:

=====================================
compiler/GHC/Hs/Type.hs
=====================================
@@ -37,7 +37,7 @@ module GHC.Hs.Type (
         HsOuterTyVarBndrs(..), HsOuterFamEqnTyVarBndrs, HsOuterSigTyVarBndrs,
         HsWildCardBndrs(..),
         HsPatSigType(..), HsPSRn(..),
-        HsTyPat(..), HsTyPatRn(..), isTyPatBndr,
+        HsTyPat(..), HsTyPatRn(..), tyPatToBndr,
         HsSigType(..), LHsSigType, LHsSigWcType, LHsWcType,
         HsTupleSort(..),
         HsContext, LHsContext, fromMaybeContext,
@@ -222,7 +222,7 @@ type instance XHsPS GhcTc = HsPSRn
 
 type instance XHsTP GhcPs = EpAnnCO
 type instance XHsTP GhcRn = HsTyPatRn
-type instance XHsTP GhcTc = HsTyPatRn
+type instance XHsTP GhcTc = DataConCantHappen
 
 -- | The extension field for 'HsPatSigType', which is only used in the
 -- renamer onwards. See @Note [Pattern signature binders and scoping]@.
@@ -240,8 +240,8 @@ data HsTyPatRn = HsTPRn
   deriving Data
 
 -- See Note [Type patterns: binders and unifiers]
-isTyPatBndr :: HsTyPat GhcRn -> Maybe (HsTyVarBndr () GhcRn)
-isTyPatBndr HsTP{hstp_body = (L _ hs_ty)} = go hs_ty where
+tyPatToBndr :: HsTyPat GhcRn -> Maybe (HsTyVarBndr () GhcRn)
+tyPatToBndr HsTP{hstp_body = (L _ hs_ty)} = go hs_ty where
   go :: HsType GhcRn -> Maybe (HsTyVarBndr () GhcRn)
   go (HsParTy _ (L _ ty)) = go ty
   go (HsTyVar an _ name)


=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -555,7 +555,9 @@ rnHsTyKi env ty@(HsRecTy _ flds)
     get_fields ctxt = err ctxt
 
     err ctxt =
-      do { addErr $ TcRnIllegalRecordSyntax (Just ctxt) (Left ty)
+      do { addErr $
+            TcRnWithHsDocContext ctxt $
+            TcRnIllegalRecordSyntax (Left ty)
          ; return [] }
 
 rnHsTyKi env (HsFunTy u mult ty1 ty2)


=====================================
compiler/GHC/Rename/Pat.hs
=====================================
@@ -1109,6 +1109,10 @@ rnHsTyPat ctxt sigType = case sigType of
           , hstp_ext = buildHsTyPatRn tpb
           }
 
+-- | Type pattern renaming monad
+-- For the OccSet in the ReaderT, see Note [Locally bound names in type patterns]
+-- For the HsTyPatRnBuilderRn in the WriterT, see Note [Implicit and explicit type variable binders]
+-- For the CpsRn base monad, see Note [CpsRn monad]
 newtype TPRnM a =
   MkTPRnM (ReaderT (HsDocContext, OccSet) (WriterT HsTyPatRnBuilder CpsRn) a)
   deriving newtype (Functor, Applicative, Monad)
@@ -1164,6 +1168,8 @@ lookupTypeOccTPRnM rdr_name = liftRnFV $ do
   name <- lookupTypeOccRn rdr_name
   pure (name, unitFV name)
 
+-- | A variant of HsTyPatRn that uses difference lists for efficient concatenation.
+-- See Note [Implicit and explicit type variable binders]
 data HsTyPatRnBuilder =
   HsTPRnB {
     hstpb_nwcs :: [Name] -> [Name],
@@ -1204,7 +1210,8 @@ rn_lty_pat (L l hs_ty) = do
 rn_ty_pat_var :: LocatedN RdrName -> TPRnM (LocatedN Name)
 rn_ty_pat_var lrdr@(L l rdr) = do
   locals <- askLocals
-  if isRdrTyVar rdr && not (elemOccSet (occName rdr) locals)
+  if isRdrTyVar rdr
+    && not (elemOccSet (occName rdr) locals) -- See Note [Locally bound names in type patterns]
 
     then do -- binder
       name <- liftTPRnCps $ newPatName (LamMk True) lrdr
@@ -1215,6 +1222,10 @@ rn_ty_pat_var lrdr@(L l rdr) = do
       name <- lookupTypeOccTPRnM rdr
       pure (L l name)
 
+-- | Rename type patterns
+--
+-- For the difference between `rn_ty_pat` and `rnHsTyKi` see Note [CpsRn monad]
+-- and Note [Implicit and explicit type variable binders]
 rn_ty_pat :: HsType GhcPs -> TPRnM (HsType GhcRn)
 rn_ty_pat (HsTyVar an prom lrdr) = do
   name <- rn_ty_pat_var lrdr
@@ -1227,7 +1238,7 @@ rn_ty_pat (HsForAllTy an tele body) = liftTPRnRaw $ \ctxt locals thing_inside ->
       locals' = locals `extendOccSetList` map occName tele_names
 
     unTPRnRaw (rn_lty_pat body) ctxt locals' $ \(body', tpb) ->
-      delLocalNames tele_names $
+      delLocalNames tele_names $ -- locally bound names do not scope over the continuation
         thing_inside ((HsForAllTy an tele' body'), tpb)
 
 rn_ty_pat (HsQualTy an lctx body) = do
@@ -1322,13 +1333,18 @@ rn_ty_pat (HsSpliceTy _ splice) = do
       | otherwise                       = lhs_ty
 
 rn_ty_pat (HsBangTy an bang_src lty) = do
+  ctxt <- askDocContext
   lty'@(L _ ty') <- rn_lty_pat lty
-  liftRn $ addErr $ TcRnUnexpectedAnnotation ty' bang_src
+  liftRn $ addErr $
+    TcRnWithHsDocContext ctxt $
+    TcRnUnexpectedAnnotation ty' bang_src
   pure (HsBangTy an bang_src lty')
 
 rn_ty_pat ty at HsRecTy{} = do
   ctxt <- askDocContext
-  liftRn $ addErr $ TcRnIllegalRecordSyntax (Just ctxt) (Left ty)
+  liftRn $ addErr $
+    TcRnWithHsDocContext ctxt $
+    TcRnIllegalRecordSyntax (Left ty)
   pure (HsWildCardTy noExtField) -- trick to avoid `failWithTc`
 
 rn_ty_pat ty@(XHsType{}) = do
@@ -1341,3 +1357,44 @@ rn_ty_pat_arrow (HsLinearArrow (HsPct1 pct1 arr)) = pure (HsLinearArrow (HsPct1
 rn_ty_pat_arrow (HsLinearArrow (HsLolly arr)) = pure (HsLinearArrow (HsLolly arr))
 rn_ty_pat_arrow (HsExplicitMult pct p arr)
   = rn_lty_pat p <&> (\mult -> HsExplicitMult pct mult arr)
+
+
+{- Note [Locally bound names in type patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type patterns can bind local names using forall. Compare the following examples:
+  f (Proxy @(Either a b)) = ...
+  g (Proxy @(forall a . Either a b)) = ...
+
+In `f` both `a` and `b` are bound by the pattern and scope over the RHS of f.
+In `g` only `b` is bound by the pattern, whereas `a` is locally bound in the pattern
+and does not scope over the RHS of `g`.
+
+We track locally bound names in the `OccSet` in `TPRnM` monad, and use it to
+decide whether occurences of type variables are usages or bindings.
+
+The check is done in `rn_ty_pat_var`
+
+Note [Implicit and explicit type variable binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type patterns are renamed differently from ordinary types.
+  * Types are renamed by `rnHsType` where all type variable occurences are considered usages
+  * Type patterns are renamed by `rnHsTyPat` where some type variable occurences are usages
+    and other are bindings
+
+Here is an example:
+  {-# LANGUAGE ScopedTypeVariables #-}
+  f :: forall b. Proxy _ -> ...
+  f (Proxy @(x :: (a, b))) = ...
+
+In the (x :: (a,b)) type pattern
+  * `x` is a type variable explicitly bound by type pattern
+  * `a` is a type variable implicitly bound in a pattern signature
+  * `b` is a usage of type variable bound by the outer forall
+
+This classification is clear to us in `rnHsTyPat`, but it is also useful in later passes, such
+as `collectPatBinders` and `tcHsTyPat`, so we store it in the extension field of `HsTyPat`, namely
+`HsTyPatRn`.
+
+To collect lists of those variables efficiently we use `HsTyPatRnBuilder` which is exactly like
+`HsTyPatRn`, but uses difference lists.
+-}


=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -983,13 +983,9 @@ instance Diagnostic TcRnMessage where
                  HsSrcBang _ _ _                   -> "strictness"
             in text "Unexpected" <+> text err <+> text "annotation:" <+> ppr ty $$
                text err <+> text "annotation cannot appear nested inside a type"
-    TcRnIllegalRecordSyntax m_ctxt either_ty_ty
-      -> mkSimpleDecorated $ case m_ctxt of
-        Nothing ->
+    TcRnIllegalRecordSyntax either_ty_ty
+      -> mkSimpleDecorated $
            text "Record syntax is illegal here:" <+> either ppr ppr either_ty_ty
-        Just ctxt ->
-          text "Illegal record syntax" <+> either ppr ppr either_ty_ty
-          $$ inHsDocContext ctxt
 
     TcRnInvalidVisibleKindArgument arg ty
       -> mkSimpleDecorated $


=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -500,6 +500,8 @@ data TcRnMessage where
                  rename/should_fail/T2723
                  rename/should_compile/T3262
                  driver/werror
+                 rename/should_fail/T22478d
+                 typecheck/should_fail/TyAppPat_ScopedTyVarConflict
   -}
   TcRnShadowedName :: OccName -> ShadowedNameProvenance -> TcRnMessage
 
@@ -2201,6 +2203,7 @@ data TcRnMessage where
 
     Test cases: parser/should_fail/unpack_inside_type
                 typecheck/should_fail/T7210
+                rename/should_fail/T22478b
   -}
   TcRnUnexpectedAnnotation :: !(HsType GhcRn) -> !HsSrcBang -> TcRnMessage
 
@@ -2211,8 +2214,9 @@ data TcRnMessage where
 
     Test cases: rename/should_fail/T7943
                 rename/should_fail/T9077
+                rename/should_fail/T22478b
   -}
-  TcRnIllegalRecordSyntax :: Maybe HsDocContext -> Either (HsType GhcPs) (HsType GhcRn) -> TcRnMessage
+  TcRnIllegalRecordSyntax :: Either (HsType GhcPs) (HsType GhcRn) -> TcRnMessage
 
   {-| TcRnInvalidVisibleKindArgument is an error for a kind application on a
      target type that cannot accept it.
@@ -4011,7 +4015,9 @@ data TcRnMessage where
 
     Test cases:
       dsrun006, mdofail002, mdofail003, mod23, mod24, qq006, rnfail001,
-      rnfail004, SimpleFail6, T14114, T16110_Fail1, tcfail038, TH_spliceD1
+      rnfail004, SimpleFail6, T14114, T16110_Fail1, tcfail038, TH_spliceD1,
+      T22478b, TyAppPat_NonlinearMultiAppPat, TyAppPat_NonlinearMultiPat,
+      TyAppPat_NonlinearSinglePat,
   -}
   TcRnBindingNameConflict :: !RdrName -- ^ The conflicting name
                           -> !(NE.NonEmpty SrcSpan)


=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1147,7 +1147,7 @@ tc_hs_type _ ty@(HsBangTy _ bang _) _
 tc_hs_type _ ty@(HsRecTy {})      _
       -- Record types (which only show up temporarily in constructor
       -- signatures) should have been removed by now
-    = failWithTc $ TcRnIllegalRecordSyntax Nothing (Right ty)
+    = failWithTc $ TcRnIllegalRecordSyntax (Right ty)
 
 -- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSpliceType'.
 -- Here we get rid of it and add the finalizers to the global environment
@@ -4156,18 +4156,39 @@ tcHsPatSigType ctxt hole_mode
   ctxt_kind
   = tc_type_in_pat ctxt hole_mode hs_ty sig_wcs sig_ns ctxt_kind
 
+
+-- Type check type patterns. This is different from `tcHsPatSigType`
+-- in that we give special treatment to simple binders like
+-- `@a` or `@(a :: k)` allowing them to have polymorphic kinds (#18986)
+--
+-- See Note [Type patterns: binders and unifiers] in GHC.Hs.Type
 tcHsTyPat :: HsTyPat GhcRn               -- The type pattern
           -> Kind                        -- What kind is expected
           -> TcM ( [(Name, TcTyVar)]     -- Wildcards
                  , [(Name, TcTyVar)]     -- The new bit of type environment, binding
                                          -- the scoped type variables
                  , TcType)               -- The type
-tcHsTyPat hs_pat@(HsTP{hstp_ext = bndrs}) expected_kind
-  | Just bndr <- isTyPatBndr hs_pat -- See Note [Type patterns: binders and unifiers] in GHC.Hs.Type
-
-  , HsTPRn { hstp_nwcs = wcs, hstp_imp_tvs = imp_ns} <- bndrs
-  = do
-  traceTc "tcHsTyPat 1" (ppr expected_kind)
+tcHsTyPat hs_pat@(HsTP{hstp_ext = hstp_rn, hstp_body = hs_ty}) expected_kind
+  = case tyPatToBndr hs_pat of
+    Nothing   -> tc_unif_in_pat hs_ty wcs all_ns (TheKind expected_kind)
+    Just bndr -> tc_bndr_in_pat bndr  wcs imp_ns  expected_kind
+  where
+    all_ns = imp_ns ++ exp_ns
+    HsTPRn{hstp_nwcs = wcs, hstp_imp_tvs = imp_ns, hstp_exp_tvs = exp_ns} = hstp_rn
+    tc_unif_in_pat = tc_type_in_pat TypeAppCtxt HM_TyAppPat
+
+-- `tc_bndr_in_pat` is used in type patterns to handle the binders case.
+-- See Note [Type patterns: binders and unifiers] in GHC.Hs.Type
+tc_bndr_in_pat :: HsTyVarBndr flag GhcRn
+               -> [Name]  -- All named wildcards in type
+               -> [Name]  -- Implicit (but not explicit) binders in type
+               -> Kind    -- Expected kind
+               -> TcM ( [(Name, TcTyVar)]     -- Wildcards
+                      , [(Name, TcTyVar)]     -- The new bit of type environment, binding
+                                              -- the scoped type variables
+                      , TcType)               -- The type
+tc_bndr_in_pat bndr wcs imp_ns expected_kind = do
+  traceTc "tc_bndr_in_pat 1" (ppr expected_kind)
   case bndr of
     UserTyVar _ _ (L _ name) -> do
       tv <- newPatTyVar name expected_kind
@@ -4175,7 +4196,7 @@ tcHsTyPat hs_pat@(HsTP{hstp_ext = bndrs}) expected_kind
     KindedTyVar _ _ (L _ name) ki -> do
       tkv_prs <- mapM new_implicit_tv imp_ns
       wcs <- addTypeCtxt ki              $
-             solveEqualities "tcHsTyPat" $
+             solveEqualities "tc_bndr_in_pat" $
                -- See Note [Failure in local type signatures]
                -- and c.f #16033
              bindNamedWildCardBinders wcs $ \ wcs ->
@@ -4189,7 +4210,7 @@ tcHsTyPat hs_pat@(HsTP{hstp_ext = bndrs}) expected_kind
 
       tv <- newPatTyVar name expected_kind
 
-      traceTc "tcHsTyPat 2" $ vcat
+      traceTc "tc_bndr_in_pat 2" $ vcat
         [ text "expected_kind" <+> ppr expected_kind
         , text "wcs" <+> ppr wcs
         , text "(name,tv)" <+>  ppr (name,tv)
@@ -4203,13 +4224,10 @@ tcHsTyPat hs_pat@(HsTP{hstp_ext = bndrs}) expected_kind
              -- NB: tv's Name is fresh
            ; return (name, tv) }
 
-tcHsTyPat
-  (HsTP { hstp_ext  = HsTPRn wcs imp_ns exp_ns
-        , hstp_body = hs_ty })
-  ki
-  = tc_type_in_pat TypeAppCtxt HM_TyAppPat hs_ty wcs (imp_ns ++ exp_ns) (TheKind ki)
-
-
+-- * In type patterns `tc_type_in_pat` is used to handle the unifiers case.
+--   See Note [Type patterns: binders and unifiers] in GHC.Hs.Type
+--
+-- * In patterns `tc_type_in_pat` is used to check pattern signatures.
 tc_type_in_pat :: UserTypeCtxt
                -> HoleMode -- HM_Sig when in a SigPat, HM_TyAppPat when in a ConPat checking type applications.
                -> LHsType GhcRn          -- The type in pattern


=====================================
testsuite/tests/gadt/T18191.stderr
=====================================
@@ -16,13 +16,13 @@ T18191.hs:15:21: error: [GHC-71492]
     • In the definition of data constructor ‘MkZ1’
 
 T18191.hs:15:31: error: [GHC-89246]
-    Illegal record syntax {unZ1 :: (a, b)}
-    In the definition of data constructor ‘MkZ1’
+    • Record syntax is illegal here: {unZ1 :: (a, b)}
+    • In the definition of data constructor ‘MkZ1’
 
 T18191.hs:16:19: error: [GHC-71492]
     • GADT constructor type signature cannot contain nested ‘forall’s or contexts
     • In the definition of data constructor ‘MkZ2’
 
 T18191.hs:16:27: error: [GHC-89246]
-    Illegal record syntax {unZ1 :: (a, b)}
-    In the definition of data constructor ‘MkZ2’
+    • Record syntax is illegal here: {unZ1 :: (a, b)}
+    • In the definition of data constructor ‘MkZ2’


=====================================
testsuite/tests/rename/should_fail/T22478b.stderr
=====================================
@@ -6,15 +6,16 @@ T22478b.hs:14:14: error: [GHC-10498]
     • In an equation for ‘fOutOfOrder’
 
 T22478b.hs:16:10: error: [GHC-18932]
-    Unexpected strictness annotation: Int
-    strictness annotation cannot appear nested inside a type
+    • Unexpected strictness annotation: Int
+      strictness annotation cannot appear nested inside a type
+    • In a type argument in a pattern
 
 T22478b.hs:19:54: error: [GHC-76037]
     Not in scope: type variable ‘a’
 
 T22478b.hs:21:12: error: [GHC-89246]
-    Illegal record syntax {fld :: Int}
-    In a type argument in a pattern
+    • Record syntax is illegal here: {fld :: Int}
+    • In a type argument in a pattern
 
 T22478b.hs:23:21: error: [GHC-10498]
     • Conflicting definitions for ‘a’


=====================================
testsuite/tests/rename/should_fail/T7943.stderr
=====================================
@@ -1,4 +1,4 @@
 
 T7943.hs:4:21: error: [GHC-89246]
-    Illegal record syntax {bar :: String}
-    In the definition of data constructor ‘B’
+    • Record syntax is illegal here: {bar :: String}
+    • In the definition of data constructor ‘B’


=====================================
testsuite/tests/rename/should_fail/T9077.stderr
=====================================
@@ -1,4 +1,4 @@
 
 T9077.hs:3:12: error: [GHC-89246]
-    Illegal record syntax {}
-    In the type signature for ‘main’
+    • Record syntax is illegal here: {}
+    • In the type signature for ‘main’



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/94791a6126351f76240c7f76448bb22886f866ef

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/94791a6126351f76240c7f76448bb22886f866ef
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/20230628/6388332f/attachment-0001.html>


More information about the ghc-commits mailing list