[Git][ghc/ghc][wip/int-index/decl-invis-binders] 4 commits: Revert reification of type variable binders

Vladislav Zavialov (@int-index) gitlab at gitlab.haskell.org
Tue Jan 24 21:03:51 UTC 2023



Vladislav Zavialov pushed to branch wip/int-index/decl-invis-binders at Glasgow Haskell Compiler / GHC


Commits:
d328bb8e by Vladislav Zavialov at 2023-01-24T23:17:06+03:00
Revert reification of type variable binders

- - - - -
a23ae5bb by Vladislav Zavialov at 2023-01-24T23:44:20+03:00
Add documentation to TyVarBndr flag

- - - - -
62d23df8 by Vladislav Zavialov at 2023-01-24T23:50:13+03:00
Move GhcDiagnosticCode "PsErrUnexpectedTypeAppInDecl"

- - - - -
4e57030e by Vladislav Zavialov at 2023-01-24T23:54:35+03:00
Add more tests

- - - - -


18 changed files:

- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Types/Error/Codes.hs
- libraries/template-haskell/Language/Haskell/TH/Syntax.hs
- libraries/template-haskell/changelog.md
- testsuite/tests/th/T11463.stdout
- testsuite/tests/th/T12045TH2.stderr
- testsuite/tests/th/T12646.stderr
- testsuite/tests/th/T17296.stderr
- testsuite/tests/th/T8884.stderr
- testsuite/tests/th/T8953.stderr
- testsuite/tests/th/T9692.stderr
- testsuite/tests/th/TH_reifyDecl1.stderr
- testsuite/tests/typecheck/should_compile/T22560d.hs
- testsuite/tests/typecheck/should_compile/T22560d.script
- testsuite/tests/typecheck/should_compile/T22560d.stdout
- + testsuite/tests/typecheck/should_fail/T22560_fail_c.hs
- + testsuite/tests/typecheck/should_fail/T22560_fail_c.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
compiler/GHC/Tc/Gen/Splice.hs
=====================================
@@ -2641,15 +2641,40 @@ instance ReifyFlag Specificity TH.Specificity where
 instance ReifyFlag TyConBndrVis (Maybe TH.BndrVis) where
     reifyFlag AnonTCB              = Just TH.BndrReq
     reifyFlag (NamedTCB Required)  = Just TH.BndrReq
-    reifyFlag (NamedTCB Specified) = Just TH.BndrInvis
-    reifyFlag (NamedTCB Inferred)  = Nothing    -- inferred variables can not be bound
+    reifyFlag (NamedTCB (Invisible _)) =
+      Nothing -- See Note [Reifying invisible type variable binders] and #22828.
 
+-- Currently does not return invisible type variable binders (@k-binders).
+-- See Note [Reifying invisible type variable binders] and #22828.
 reifyTyConBinders :: TyCon -> TcM [TH.TyVarBndr TH.BndrVis]
 reifyTyConBinders tc = fmap (mapMaybe get_bndr) (reifyTyVarBndrs (tyConBinders tc))
   where
     get_bndr :: TH.TyVarBndr (Maybe flag) -> Maybe (TH.TyVarBndr flag)
     get_bndr = sequenceA
 
+{- Note [Reifying invisible type variable binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In reifyFlag for TyConBndrVis, we have the following clause:
+
+    reifyFlag (NamedTCB (Invisible _)) = Nothing
+
+This means that reifyTyConBinders doesn't reify invisible type variables as
+ at k-binders. However, it is possible (and not hard) to change this.
+Just replace the above clause with:
+
+    reifyFlag (NamedTCB Specified) = Just TH.BndrInvis
+    reifyFlag (NamedTCB Inferred)  = Nothing    -- Inferred variables can not be bound
+
+There are two reasons we opt not to do that for now.
+  1. It would be a (sometimes silent) breaking change affecting th-abstraction,
+     aeson, and other libraries that assume that reified binders are visible.
+  2. It would create an asymmetry with visible kind applications, which are
+     not reified either.
+
+This decision is not set in stone. If a use case for reifying invisible type
+variable binders presents itself, we can reconsider. See #22828.
+-}
+
 reifyTyVars :: [TyVar] -> TcM [TH.TyVarBndr ()]
 reifyTyVars = reifyTyVarBndrs . map mk_bndr
   where


=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -253,7 +253,6 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "PsErrAtInPatPos"                               = 08382
   GhcDiagnosticCode "PsErrParseErrorOnInput"                        = 66418
   GhcDiagnosticCode "PsErrMalformedDecl"                            = 85316
-  GhcDiagnosticCode "PsErrUnexpectedTypeAppInDecl"                  = 45054   -- Historical
   GhcDiagnosticCode "PsErrNotADataCon"                              = 25742
   GhcDiagnosticCode "PsErrInferredTypeVarNotAllowed"                = 57342
   GhcDiagnosticCode "PsErrIllegalTraditionalRecordSyntax"           = 65719
@@ -609,6 +608,7 @@ type family GhcDiagnosticCode c = n | n -> c where
   -- no longer reports. These are collected below.
 
   GhcDiagnosticCode "Example outdated error"                        = 00000
+  GhcDiagnosticCode "PsErrUnexpectedTypeAppInDecl"                  = 45054
 
 {- *********************************************************************
 *                                                                      *


=====================================
libraries/template-haskell/Language/Haskell/TH/Syntax.hs
=====================================
@@ -2805,6 +2805,12 @@ data Specificity = SpecifiedSpec          -- ^ @a@
                  | InferredSpec           -- ^ @{a}@
       deriving( Show, Eq, Ord, Data, Generic )
 
+-- | The @flag@ type parameter is instantiated to one of the following types:
+--
+--   * 'Specificity' (examples: 'ForallC', 'ForallT')
+--   * 'BndrVis' (examples: 'DataD', 'ClassD', etc.)
+--   * '()', a catch-all type for other forms of binders, including 'ForallVisT', 'DataInstD', 'RuleP', and 'TyVarSig'
+--
 data TyVarBndr flag = PlainTV  Name flag      -- ^ @a@
                     | KindedTV Name flag Kind -- ^ @(a :: k)@
       deriving( Show, Eq, Ord, Data, Generic, Functor, Foldable, Traversable )


=====================================
libraries/template-haskell/changelog.md
=====================================
@@ -9,9 +9,6 @@
     to any data type with a `DefaultBndrFlag` instance, including `()`,
     `Specificity`, and `BndrVis`.
 
-  * Reified type declarations now contain invisible binders
-    for non-inferred type variables.
-
 ## 2.20.0.0
 
   * The `Ppr.pprInfixT` function has gained a `Precedence` argument. 


=====================================
testsuite/tests/th/T11463.stdout
=====================================
@@ -1,3 +1,2 @@
-data Main.Proxy1 @(k_0 :: *) (a_1 :: Main.Id1 k_0) = Main.Proxy1
-data Main.Proxy2 @(k_0 :: *) (a_1 :: Main.Id2 (*) k_0)
-    = Main.Proxy2
+data Main.Proxy1 (a_0 :: Main.Id1 k_1) = Main.Proxy1
+data Main.Proxy2 (a_0 :: Main.Id2 (*) k_1) = Main.Proxy2


=====================================
testsuite/tests/th/T12045TH2.stderr
=====================================
@@ -1,5 +1,5 @@
-type family T12045TH2.Foo @(k_0 :: *) (a_1 :: k_0) :: * where
+type family T12045TH2.Foo (a_0 :: k_1) :: * where
     forall (a_2 :: *). T12045TH2.Foo (a_2 :: *) = GHC.Types.Bool
-type family T12045TH2.Baz @(k_0 :: *) (a_1 :: k_0) :: *
+type family T12045TH2.Baz (a_0 :: k_1) :: *
 type instance forall (a_0 :: * ->
                              * -> *). T12045TH2.Baz (a_0 :: * -> * -> *) = GHC.Types.Char


=====================================
testsuite/tests/th/T12646.stderr
=====================================
@@ -1,4 +1,4 @@
-type family T12646.F @(k_0 :: *) (a_1 :: k_0) :: * where
+type family T12646.F (a_0 :: k_1) :: * where
     forall (a_2 :: * -> *). T12646.F (a_2 :: * -> *) = GHC.Types.Int
     forall (k_3 :: *)
            (a_4 :: k_3). T12646.F (a_4 :: k_3) = GHC.Types.Char


=====================================
testsuite/tests/th/T17296.stderr
=====================================
@@ -2,14 +2,14 @@ data family T17296.Foo1 :: * -> *
 data instance forall (a_0 :: *). T17296.Foo1 (GHC.Maybe.Maybe a_0)
 data instance T17296.Foo1 GHC.Types.Bool = T17296.Foo1Bool
 
-data family T17296.Foo2 @(k_0 :: *) :: k_0 -> *
+data family T17296.Foo2 :: k_0 -> *
 data instance T17296.Foo2 :: (GHC.Types.Char -> GHC.Types.Char) ->
                              *
 data instance T17296.Foo2 :: GHC.Types.Char -> *
 data instance forall (a_1 :: *). T17296.Foo2 (GHC.Maybe.Maybe a_1 :: *)
 data instance T17296.Foo2 GHC.Types.Bool = T17296.Foo2Bool
 
-data family T17296.Foo3 @(k_0 :: *) :: k_0
+data family T17296.Foo3 :: k_0
 data instance T17296.Foo3 :: GHC.Types.Char -> *
 data instance T17296.Foo3 :: (GHC.Types.Char -> GHC.Types.Char) ->
                              *


=====================================
testsuite/tests/th/T8884.stderr
=====================================
@@ -1,5 +1,5 @@
 type family T8884.Foo (a_0 :: k_1) = (r_2 :: k_1) | r_2 -> k_1 a_0 where
     forall (k_3 :: *) (x_4 :: k_3). T8884.Foo (x_4 :: k_3) = x_4
-type family T8884.Baz @(k_0 :: *) (a_1 :: k_0) = (r_2 :: k_0) | r_2 -> k_0 a_1
+type family T8884.Baz (a_0 :: k_1) = (r_2 :: k_1) | r_2 -> k_1 a_0
 type instance forall (k_0 :: *)
                      (x_1 :: k_0). T8884.Baz (x_1 :: k_0) = x_1


=====================================
testsuite/tests/th/T8953.stderr
=====================================
@@ -1,21 +1,21 @@
-type family T8953.Poly @(k_0 :: *) (a_1 :: k_0) :: *
+type family T8953.Poly (a_0 :: k_1) :: *
 type instance forall (k_2 :: *)
                      (x_3 :: GHC.Maybe.Maybe k_2). T8953.Poly (x_3 :: GHC.Maybe.Maybe k_2) = GHC.Types.Double
 type instance forall (x_4 :: GHC.Types.Bool). T8953.Poly (x_4 :: GHC.Types.Bool) = GHC.Types.Int
-type family T8953.Silly @(k_0 :: *) :: k_0 -> *
+type family T8953.Silly :: k_0 -> *
 type instance T8953.Silly = (Data.Proxy.Proxy :: (* -> *) -> *)
 type instance T8953.Silly = (Data.Proxy.Proxy :: * -> *)
 T8953.a :: Data.Proxy.Proxy (Data.Proxy.Proxy :: * -> *)
 T8953.b :: Data.Proxy.Proxy (Data.Proxy.Proxy :: (* -> *) -> *)
 type T8953.StarProxy (a_0 :: *) = Data.Proxy.Proxy a_0
-class T8953.PC @(k_0 :: *) (a_1 :: k_0)
+class T8953.PC (a_0 :: k_1)
 instance T8953.PC (Data.Proxy.Proxy :: (k_2 -> *) -> *)
 instance T8953.PC (a_3 :: *)
-type family T8953.F @(k_0 :: *) (a_1 :: *) :: k_0
+type family T8953.F (a_0 :: *) :: k_1
 type instance T8953.F GHC.Types.Char = T8953.G (T8953.T1 :: * ->
                                                             (* -> *) -> *)
                                                GHC.Types.Bool
-type family T8953.G @(k_0 :: *) (a_1 :: k_0) :: k_0
+type family T8953.G (a_0 :: k_1) :: k_1
 type instance forall (k1_2 :: *)
                      (k2_3 :: *). T8953.G (T8953.T1 :: k1_2 ->
                                                        k2_3 -> *) = (T8953.T2 :: k1_2 -> k2_3 -> *)


=====================================
testsuite/tests/th/T9692.stderr
=====================================
@@ -1,3 +1,3 @@
-data family T9692.F @(k_0 :: *) (a_1 :: k_2) (b_3 :: k_0) :: *
+data family T9692.F (a_0 :: k_1) (b_2 :: k_3) :: *
 data instance forall (x_4 :: *). T9692.F GHC.Types.Int (x_4 :: *)
     = T9692.FInt x_4


=====================================
testsuite/tests/th/TH_reifyDecl1.stderr
=====================================
@@ -37,7 +37,7 @@ data family TH_reifyDecl1.DF1 (a_0 :: *) :: *
 data family TH_reifyDecl1.DF2 (a_0 :: *) :: *
 data instance TH_reifyDecl1.DF2 GHC.Types.Bool
     = TH_reifyDecl1.DBool
-data family TH_reifyDecl1.DF3 @(k_0 :: *) (a_1 :: k_0) :: *
+data family TH_reifyDecl1.DF3 (a_0 :: k_1) :: *
 data instance forall (b_2 :: * ->
                              *). TH_reifyDecl1.DF3 (b_2 :: * -> *)
     = TH_reifyDecl1.DF3Char


=====================================
testsuite/tests/typecheck/should_compile/T22560d.hs
=====================================
@@ -23,4 +23,10 @@ class C @k (a :: k) where
 
 -- type F :: forall k. k -> k
 type family F @k (a :: k) :: k where
-  F a = a
\ No newline at end of file
+  F a = a
+
+-- type U :: forall {k} (a :: k). Type
+type U @a = Int
+
+-- type Z :: forall k -> forall (a :: k). Type
+type Z k @(a :: k) = Proxy a
\ No newline at end of file


=====================================
testsuite/tests/typecheck/should_compile/T22560d.script
=====================================
@@ -5,4 +5,6 @@
 :kind N
 :kind S
 :kind C
-:kind F
\ No newline at end of file
+:kind F
+:kind U
+:kind Z
\ No newline at end of file


=====================================
testsuite/tests/typecheck/should_compile/T22560d.stdout
=====================================
@@ -4,3 +4,5 @@ N :: forall k. k -> Type
 S :: forall k. k -> Type
 C :: forall k. k -> Constraint
 F :: forall k. k -> k
+U :: forall {k} (a :: k). Type
+Z :: forall k -> forall (a :: k). Type


=====================================
testsuite/tests/typecheck/should_fail/T22560_fail_c.hs
=====================================
@@ -0,0 +1,3 @@
+module T22560_fail_c where
+
+data Dup @k @k (a :: k)
\ No newline at end of file


=====================================
testsuite/tests/typecheck/should_fail/T22560_fail_c.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T22560_fail_c.hs:3:11: error:
+    Conflicting definitions for ‘k’
+    Bound at: T22560_fail_c.hs:3:11
+              T22560_fail_c.hs:3:14


=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -670,4 +670,5 @@ test('T20666', normal, compile_fail, [''])
 test('T20666a', normal, compile_fail, [''])
 test('T22560_fail_a', normal, compile_fail, [''])
 test('T22560_fail_b', normal, compile_fail, [''])
+test('T22560_fail_c', normal, compile_fail, [''])
 test('T22560_fail_ext', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9b2f2bfb6d2f3fbfa4c9728598bb3d64a051fef9...4e57030e1623d4b5712a28ec1b73359663233cce

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9b2f2bfb6d2f3fbfa4c9728598bb3d64a051fef9...4e57030e1623d4b5712a28ec1b73359663233cce
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/20230124/418fffea/attachment-0001.html>


More information about the ghc-commits mailing list