[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 5 commits: Add role annotations to SNat, SSymbol and SChar

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Sat Jun 10 09:57:31 UTC 2023



Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC


Commits:
4639100b by Matthew Pickering at 2023-06-09T18:50:43-04:00
Add role annotations to SNat, SSymbol and SChar

Ticket #23454 explained it was possible to implement unsafeCoerce
because SNat was lacking a role annotation.

As these are supposed to be singleton types but backed by an efficient
representation the correct annotation is nominal to ensure these kinds
of coerces are forbidden.

These annotations were missed from https://github.com/haskell/core-libraries-committee/issues/85
which was implemented in 532de36870ed9e880d5f146a478453701e9db25d.

CLC Proposal: https://github.com/haskell/core-libraries-committee/issues/170

Fixes #23454

- - - - -
9c0dcff7 by Matthew Pickering at 2023-06-09T18:51:19-04:00
Remove non-existant bytearray-ops.txt.pp file from ghc.cabal.in

This broke the sdist generation.

Fixes #23489

- - - - -
273ff0c7 by David Binder at 2023-06-09T18:52:00-04:00
Regression test T13438 is no longer marked as "expect_broken" in the testsuite driver.

- - - - -
460c9efb by Andrei Borzenkov at 2023-06-10T05:57:20-04:00
Fix -Wterm-variable-capture scope (#23434)

-Wterm-variable-capture wasn't accordant with type variable
scoping in associated types, in type classes. For example,
this code produced the warning:
  k = 12

  class C k a where
    type AT a :: k -> Type

I solved this issue by reusing machinery of newTyVarNameRn function
that is accordand with associated types: it does lookup for each free type
variable when we are in the type class context. And in this patch I
use result of this work to make sure that -Wterm-variable-capture warns
only on implicitly quantified type variables.

- - - - -
229b60d3 by Jorge Mendes at 2023-06-10T05:57:23-04:00
Remove redundant case statement in rts/js/mem.js.
- - - - -


23 changed files:

- compiler/GHC/Rename/HsType.hs
- compiler/ghc.cabal.in
- libraries/base/GHC/TypeLits.hs
- libraries/base/GHC/TypeNats.hs
- libraries/base/changelog.md
- + libraries/base/tests/T23454.hs
- + libraries/base/tests/T23454.stderr
- libraries/base/tests/all.T
- rts/js/mem.js
- testsuite/tests/ghci/scripts/T9181.stdout
- testsuite/tests/overloadedrecflds/ghci/T13438.script
- testsuite/tests/overloadedrecflds/ghci/T13438.stdout
- testsuite/tests/overloadedrecflds/ghci/all.T
- testsuite/tests/rename/should_compile/T22513a.stderr
- testsuite/tests/rename/should_compile/T22513b.stderr
- testsuite/tests/rename/should_compile/T22513c.stderr
- testsuite/tests/rename/should_compile/T22513d.stderr
- testsuite/tests/rename/should_compile/T22513e.stderr
- testsuite/tests/rename/should_compile/T22513f.stderr
- testsuite/tests/rename/should_compile/T22513g.stderr
- testsuite/tests/rename/should_compile/T22513h.stderr
- + testsuite/tests/rename/should_compile/T23434.hs
- testsuite/tests/rename/should_compile/all.T


Changes:

=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -386,7 +386,6 @@ rnImplicitTvOccs :: Maybe assoc
                  -> RnM (a, FreeVars)
 rnImplicitTvOccs mb_assoc implicit_vs_with_dups thing_inside
   = do { let implicit_vs = nubN implicit_vs_with_dups
-       ; mapM_ warn_term_var_capture implicit_vs
 
        ; traceRn "rnImplicitTvOccs" $
          vcat [ ppr implicit_vs_with_dups, ppr implicit_vs ]
@@ -395,7 +394,7 @@ rnImplicitTvOccs mb_assoc implicit_vs_with_dups thing_inside
          -- See Note [Source locations for implicitly bound type variables].
        ; loc <- getSrcSpanM
        ; let loc' = noAnnSrcSpan loc
-       ; vars <- mapM (newTyVarNameRn mb_assoc . L loc' . unLoc) implicit_vs
+       ; vars <- mapM (newTyVarNameRnImplicit mb_assoc . L loc' . unLoc) implicit_vs
 
        ; bindLocalNamesFV vars $
          thing_inside vars }
@@ -1136,6 +1135,7 @@ bindHsOuterTyVarBndrs doc mb_cls implicit_vars outer_bndrs thing_inside =
         thing_inside $ HsOuterExplicit { hso_xexplicit = noExtField
                                        , hso_bndrs     = exp_bndrs' }
 
+-- See Note [Term variable capture and implicit quantification]
 warn_term_var_capture :: LocatedN RdrName -> RnM ()
 warn_term_var_capture lVar = do
     gbl_env <- getGlobalRdrEnv
@@ -1242,15 +1242,68 @@ rnHsBndrVis :: HsBndrVis GhcPs -> HsBndrVis GhcRn
 rnHsBndrVis HsBndrRequired = HsBndrRequired
 rnHsBndrVis (HsBndrInvisible at) = HsBndrInvisible at
 
-newTyVarNameRn :: Maybe a -- associated class
-               -> LocatedN RdrName -> RnM Name
-newTyVarNameRn mb_assoc lrdr@(L _ rdr)
+newTyVarNameRn, newTyVarNameRnImplicit
+  :: Maybe a -- associated class
+  -> LocatedN RdrName -> RnM Name
+newTyVarNameRn         mb_assoc = new_tv_name_rn mb_assoc newLocalBndrRn
+newTyVarNameRnImplicit mb_assoc = new_tv_name_rn mb_assoc $ \lrdr ->
+  do { warn_term_var_capture lrdr
+     ; newLocalBndrRn lrdr }
+
+new_tv_name_rn :: Maybe a -- associated class
+               -> (LocatedN RdrName -> RnM Name) -- how to create a new name
+               -> (LocatedN RdrName -> RnM Name)
+new_tv_name_rn Nothing  cont lrdr = cont lrdr
+new_tv_name_rn (Just _) cont lrdr@(L _ rdr)
   = do { rdr_env <- getLocalRdrEnv
-       ; case (mb_assoc, lookupLocalRdrEnv rdr_env rdr) of
-           (Just _, Just n) -> return n
-              -- Use the same Name as the parent class decl
+       ; case lookupLocalRdrEnv rdr_env rdr of
+           Just n -> return n -- Use the same Name as the parent class decl
+           _      -> cont lrdr }
+
+{- Note [Term variable capture and implicit quantification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-Wterm-variable-capture is a warning introduced in GHC Proposal #281 "Visible forall in types of terms",
+Section 7.3: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst#73implicit-quantification
+
+Its purpose is to notify users when implicit quantification occurs that would
+stop working under RequiredTypeArguments (a future GHC extension). Example:
+
+   a = 42
+   id :: a -> a
+
+As it stands, the `a` in the signature `id :: a -> a` is considered free and
+leads to implicit quantification, as if the user wrote `id :: forall a. a -> a`.
+Under RequiredTypeArguments it will capture the term-level variable `a` (bound by `a = 42`),
+leading to a type error.
+
+`warn_term_var_capture` detects this by demoting the namespace of the
+implicitly quantified type variable (`TvName` becomes `VarName`) and looking it up
+in the environment. But when do we call `warn_term_var_capture`? It's tempting
+to do so at the start of `rnImplicitTvOccs`, as soon as we know our implicit
+variables:
+
+  rnImplicitTvOccs mb_assoc implicit_vs_with_dups thing_inside
+    = do { let implicit_vs = nubN implicit_vs_with_dups
+         ; mapM_ warn_term_var_capture implicit_vs
+         ... }
+
+This approach generates false positives (#23434) because it misses a corner
+case: class variables in associated types. Consider the following example:
+
+  k = 12
+  class C k a where
+    type AT a :: k -> Type
+
+If we look at the signature for `AT` in isolation, the `k` looks like a free
+variable, so it's passed to `rnImplicitTvOccs`. And if we passed it to
+`warn_term_var_capture`, we would find the `k` bound by `k = 12` and report a warning.
+But we don't want that: `k` is actually bound in the declaration header of the
+parent class.
+
+The solution is to check if it's a class variable (this is done in `new_tv_name_rn`)
+before we check for term variable capture.
+-}
 
-           _                -> newLocalBndrRn lrdr }
 {-
 *********************************************************
 *                                                       *


=====================================
compiler/ghc.cabal.in
=====================================
@@ -25,7 +25,6 @@ Build-Type: Custom
 
 extra-source-files:
     GHC/Builtin/primops.txt.pp
-    GHC/Builtin/bytearray-ops.txt.pp
     Unique.h
     CodeGen.Platform.h
     -- Shared with rts via hard-link at configure time. This is safer


=====================================
libraries/base/GHC/TypeLits.hs
=====================================
@@ -15,6 +15,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RoleAnnotations #-}
 
 {-|
 GHC's @DataKinds@ language extension lifts data constructors, natural
@@ -340,6 +341,7 @@ withSomeSNat n k
 --
 -- @since 4.18.0.0
 newtype SSymbol (s :: Symbol) = UnsafeSSymbol String
+type role SSymbol nominal
 
 -- | A explicitly bidirectional pattern synonym relating an 'SSymbol' to a
 -- 'KnownSymbol' constraint.
@@ -442,6 +444,7 @@ withSomeSSymbol s k = k (UnsafeSSymbol s)
 --
 -- @since 4.18.0.0
 newtype SChar (s :: Char) = UnsafeSChar Char
+type role SChar nominal
 
 -- | A explicitly bidirectional pattern synonym relating an 'SChar' to a
 -- 'KnownChar' constraint.


=====================================
libraries/base/GHC/TypeNats.hs
=====================================
@@ -16,6 +16,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RoleAnnotations #-}
 
 {-| This module is an internal GHC module.  It declares the constants used
 in the implementation of type-level natural numbers.  The programmer interface
@@ -344,6 +345,7 @@ cmpNat x y = case compare (natVal x) (natVal y) of
 --
 -- @since 4.18.0.0
 newtype SNat (n :: Nat) = UnsafeSNat Natural
+type role SNat nominal
 
 -- | A explicitly bidirectional pattern synonym relating an 'SNat' to a
 -- 'KnownNat' constraint.


=====================================
libraries/base/changelog.md
=====================================
@@ -32,6 +32,7 @@
   * Make `(&)` representation polymorphic in the return type ([CLC proposal #158](https://github.com/haskell/core-libraries-committee/issues/158))
   * Implement `GHC.IORef.atomicSwapIORef` via a new dedicated primop `atomicSwapMutVar#` ([CLC proposal #139](https://github.com/haskell/core-libraries-committee/issues/139))
   * Change codebuffers to use an unboxed implementation, while providing a compatibility layer using pattern synonyms. ([CLC proposal #134](https://github.com/haskell/core-libraries-committee/issues/134))
+  * Add nominal role annotations to SNat/SSymbol/SChar ([CLC proposal #170](https://github.com/haskell/core-libraries-committee/issues/170))
 
 ## 4.18.0.0 *March 2023*
   * Shipped with GHC 9.6.1


=====================================
libraries/base/tests/T23454.hs
=====================================
@@ -0,0 +1,27 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T23454 where
+
+import Data.Coerce (coerce)
+import Data.Kind (Type)
+import Data.Type.Equality
+import GHC.TypeNats
+
+bogus :: forall a b . KnownNat a => a :~: b
+bogus = case testEquality (SNat @a) (coerce (SNat @a) :: SNat b) of
+          Just r  -> r
+          Nothing -> error "bug fixed"
+
+type G :: Nat -> Type -> Type -> Type
+type family G n s t where
+  G 0 s _ = s
+  G _ _ t = t
+
+newtype N n s t = MkN { unN :: G n s t }
+
+oops :: forall b s t . N 0 s t -> N b s t
+oops x = gcastWith (bogus @0 @b) x
+
+unsafeCoerce :: s -> t
+unsafeCoerce x = unN (oops @1 (MkN x))


=====================================
libraries/base/tests/T23454.stderr
=====================================
@@ -0,0 +1,21 @@
+
+T23454.hs:12:38: error: [GHC-25897]
+    • Couldn't match type ‘a’ with ‘b’ arising from a use of ‘coerce’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          bogus :: forall (a :: Nat) (b :: Nat). KnownNat a => a :~: b
+        at T23454.hs:11:1-43
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          bogus :: forall (a :: Nat) (b :: Nat). KnownNat a => a :~: b
+        at T23454.hs:11:1-43
+    • In the second argument of ‘testEquality’, namely
+        ‘(coerce (SNat @a) :: SNat b)’
+      In the expression:
+        testEquality (SNat @a) (coerce (SNat @a) :: SNat b)
+      In the expression:
+        case testEquality (SNat @a) (coerce (SNat @a) :: SNat b) of
+          Just r -> r
+          Nothing -> error "bug fixed"
+    • Relevant bindings include
+        bogus :: a :~: b (bound at T23454.hs:12:1)


=====================================
libraries/base/tests/all.T
=====================================
@@ -300,3 +300,4 @@ test('listThreads1', normal, compile_and_run, [''])
 test('inits1tails1', normal, compile_and_run, [''])
 test('CLC149', normal, compile, [''])
 test('AtomicSwapIORef', normal, compile_and_run, [''])
+test('T23454', normal, compile_fail, [''])


=====================================
rts/js/mem.js
=====================================
@@ -747,9 +747,6 @@ function h$setField(o,n,v) {
     case 45:
         o.d2.d45 = v;
         return;
-    case 45:
-        o.d2.d45 = v;
-        return;
     case 46:
         o.d2.d46 = v;
         return;


=====================================
testsuite/tests/ghci/scripts/T9181.stdout
=====================================
@@ -18,12 +18,12 @@ type GHC.TypeLits.NatToChar :: GHC.Num.Natural.Natural -> Char
 type family GHC.TypeLits.NatToChar a
 pattern GHC.TypeLits.SChar
   :: () => GHC.TypeLits.KnownChar c => GHC.TypeLits.SChar c
-type role GHC.TypeLits.SChar phantom
+type role GHC.TypeLits.SChar nominal
 type GHC.TypeLits.SChar :: Char -> *
 newtype GHC.TypeLits.SChar s = GHC.TypeLits.UnsafeSChar Char
 pattern GHC.TypeLits.SSymbol
   :: () => GHC.TypeLits.KnownSymbol s => GHC.TypeLits.SSymbol s
-type role GHC.TypeLits.SSymbol phantom
+type role GHC.TypeLits.SSymbol nominal
 type GHC.TypeLits.SSymbol :: GHC.Types.Symbol -> *
 newtype GHC.TypeLits.SSymbol s = GHC.TypeLits.UnsafeSSymbol String
 type GHC.TypeLits.SomeChar :: *
@@ -166,7 +166,7 @@ data Data.Type.Ord.OrderingI a b where
                        Data.Type.Ord.OrderingI a b
 pattern GHC.TypeNats.SNat
   :: () => GHC.TypeNats.KnownNat n => GHC.TypeNats.SNat n
-type role GHC.TypeNats.SNat phantom
+type role GHC.TypeNats.SNat nominal
 type GHC.TypeNats.SNat :: GHC.TypeNats.Nat -> *
 newtype GHC.TypeNats.SNat n
   = GHC.TypeNats.UnsafeSNat GHC.Num.Natural.Natural


=====================================
testsuite/tests/overloadedrecflds/ghci/T13438.script
=====================================
@@ -1,5 +1,3 @@
 :l T13438.hs
 :browse! T13438
 :browse T13438
-:ctags
-:!cat tags


=====================================
testsuite/tests/overloadedrecflds/ghci/T13438.stdout
=====================================
@@ -5,6 +5,3 @@ MkT :: Int -> T
 foo :: T -> Int
 type T :: *
 data T = MkT {foo :: Int}
-foo	T13438.hs	3;"	v	file:
-MkT	T13438.hs	3;"	d
-T	T13438.hs	3;"	t


=====================================
testsuite/tests/overloadedrecflds/ghci/all.T
=====================================
@@ -1,6 +1,6 @@
 test('duplicaterecfldsghci01', combined_output, ghci_script, ['duplicaterecfldsghci01.script'])
 test('overloadedlabelsghci01', combined_output, ghci_script, ['overloadedlabelsghci01.script'])
-test('T13438', [expect_broken(13438), combined_output], ghci_script, ['T13438.script'])
+test('T13438', combined_output, ghci_script, ['T13438.script'])
 test('GHCiDRF', [extra_files(['GHCiDRF.hs']), combined_output], ghci_script, ['GHCiDRF.script'])
 test('T19322', combined_output, ghci_script, ['T19322.script'])
 test('T19314', combined_output, ghci_script, ['T19314.script'])


=====================================
testsuite/tests/rename/should_compile/T22513a.stderr
=====================================
@@ -1,6 +1,7 @@
-T22513a.hs:5:6: warning: [GHC-54201] [-Wterm-variable-capture]
+
+T22513a.hs:5:1: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘a’ is implicitly quantified,
     even though another variable of the same name is in scope:
-        ‘a’ defined at T22513a.hs:3:1
+      ‘a’ defined at T22513a.hs:3:1
     This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
-    Suggested fix: Consider renaming the type variable.
\ No newline at end of file
+    Suggested fix: Consider renaming the type variable.


=====================================
testsuite/tests/rename/should_compile/T22513b.stderr
=====================================
@@ -1,4 +1,5 @@
-T22513b.hs:5:6: warning: [GHC-54201] [-Wterm-variable-capture]
+
+T22513b.hs:5:1: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘id’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513b.hs:3:17-18


=====================================
testsuite/tests/rename/should_compile/T22513c.stderr
=====================================
@@ -1,4 +1,5 @@
-T22513c.hs:6:10: warning: [GHC-54201] [-Wterm-variable-capture]
+
+T22513c.hs:6:5: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘a’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘a’ defined at T22513c.hs:4:3


=====================================
testsuite/tests/rename/should_compile/T22513d.stderr
=====================================
@@ -1,7 +1,8 @@
-T22513d.hs:3:28: warning: [GHC-54201] [-Wterm-variable-capture]
+
+T22513d.hs:3:4: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘id’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513d.hs:1:8-14
            (and originally defined in ‘GHC.Base’)
     This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
-    Suggested fix: Consider renaming the type variable.
\ No newline at end of file
+    Suggested fix: Consider renaming the type variable.


=====================================
testsuite/tests/rename/should_compile/T22513e.stderr
=====================================
@@ -1,7 +1,8 @@
-T22513e.hs:3:14: warning: [GHC-54201] [-Wterm-variable-capture]
+
+T22513e.hs:3:1: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘id’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513e.hs:1:8-14
            (and originally defined in ‘GHC.Base’)
     This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
-    Suggested fix: Consider renaming the type variable.
\ No newline at end of file
+    Suggested fix: Consider renaming the type variable.


=====================================
testsuite/tests/rename/should_compile/T22513f.stderr
=====================================
@@ -1,7 +1,8 @@
-T22513f.hs:5:25: warning: [GHC-54201] [-Wterm-variable-capture]
+
+T22513f.hs:5:1: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘id’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513f.hs:1:8-14
            (and originally defined in ‘GHC.Base’)
     This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
-    Suggested fix: Consider renaming the type variable.
\ No newline at end of file
+    Suggested fix: Consider renaming the type variable.


=====================================
testsuite/tests/rename/should_compile/T22513g.stderr
=====================================
@@ -1,7 +1,8 @@
-T22513g.hs:5:15: warning: [GHC-54201] [-Wterm-variable-capture]
+
+T22513g.hs:5:1: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘head’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘head’ imported from ‘Prelude’ at T22513g.hs:2:8-14
              (and originally defined in ‘GHC.List’)
     This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
-    Suggested fix: Consider renaming the type variable.
\ No newline at end of file
+    Suggested fix: Consider renaming the type variable.


=====================================
testsuite/tests/rename/should_compile/T22513h.stderr
=====================================
@@ -1,7 +1,8 @@
-T22513h.hs:6:19: warning: [GHC-54201] [-Wterm-variable-capture]
+
+T22513h.hs:6:10: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘id’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513h.hs:1:8-14
            (and originally defined in ‘GHC.Base’)
     This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
-    Suggested fix: Consider renaming the type variable.
\ No newline at end of file
+    Suggested fix: Consider renaming the type variable.


=====================================
testsuite/tests/rename/should_compile/T23434.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wterm-variable-capture #-}
+module T23434 where
+
+import GHC.Types (Type)
+
+k = 12
+
+class C k a where
+  type AT a :: k -> Type


=====================================
testsuite/tests/rename/should_compile/all.T
=====================================
@@ -211,3 +211,4 @@ test('GHCIImplicitImportNullaryRecordWildcard', combined_output, ghci_script, ['
 test('T22122', [expect_broken(22122), extra_files(['T22122_aux.hs'])], multimod_compile, ['T22122', '-v0'])
 test('T23240', [req_th, extra_files(['T23240_aux.hs'])], multimod_compile, ['T23240', '-v0'])
 test('T23318', normal, compile, ['-Wduplicate-exports'])
+test('T23434', normal, compile, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7204d3f8c305e4569df9e3421fa2bff1ec8805b1...229b60d30c7a6dbafb9afc970d511c8c02191d78

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7204d3f8c305e4569df9e3421fa2bff1ec8805b1...229b60d30c7a6dbafb9afc970d511c8c02191d78
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/20230610/38965c35/attachment-0001.html>


More information about the ghc-commits mailing list