[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 4 commits: Clarify the meaning of "exactly once" in LinearTypes

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Sun Oct 6 13:54:53 UTC 2024



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


Commits:
535a2117 by Daniel Díaz at 2024-10-06T09:51:46-04:00
Clarify the meaning of "exactly once" in LinearTypes

Solves documentaion issue #25084.

- - - - -
92f8939a by Krzysztof Gogolewski at 2024-10-06T09:52:22-04:00
Only allow (a => b) :: Constraint rather than CONSTRAINT rep

Fixes #25243

- - - - -
2173bce4 by Alan Zimmerman at 2024-10-06T09:54:42-04:00
EPA: Remove unused hsCaseAnnsRest

We never populate it, so remove it.

- - - - -
50d9fc5e by Teo Camarasu at 2024-10-06T09:54:42-04:00
Add changelog entries for !12479

- - - - -


12 changed files:

- compiler/GHC/Hs/Expr.hs
- compiler/GHC/Parser.y
- compiler/GHC/Tc/Gen/HsType.hs
- docs/users_guide/exts/linear_types.rst
- libraries/base/changelog.md
- libraries/template-haskell/changelog.md
- testsuite/tests/parser/should_compile/DumpSemis.stderr
- + testsuite/tests/quantified-constraints/T25243.hs
- + testsuite/tests/quantified-constraints/T25243.stderr
- testsuite/tests/quantified-constraints/all.T
- testsuite/tests/rename/should_fail/rnfail026.stderr
- utils/check-exact/ExactPrint.hs


Changes:

=====================================
compiler/GHC/Hs/Expr.hs
=====================================
@@ -202,11 +202,10 @@ type instance XUntypedBracket GhcTc = HsBracketTc
 data EpAnnHsCase = EpAnnHsCase
       { hsCaseAnnCase :: EpaLocation
       , hsCaseAnnOf   :: EpaLocation
-      , hsCaseAnnsRest :: [AddEpAnn]
       } deriving Data
 
 instance NoAnn EpAnnHsCase where
-  noAnn = EpAnnHsCase noAnn noAnn noAnn
+  noAnn = EpAnnHsCase noAnn noAnn
 
 data EpAnnUnboundVar = EpAnnUnboundVar
      { hsUnboundBackquotes :: (EpaLocation, EpaLocation)


=====================================
compiler/GHC/Parser.y
=====================================
@@ -3042,7 +3042,7 @@ aexp    :: { ECP }
                                              return $ ECP $
                                                $4 >>= \ $4 ->
                                                mkHsCasePV (comb3 $1 $3 $4) $2 $4
-                                                    (EpAnnHsCase (glAA $1) (glAA $3) []) }
+                                                    (EpAnnHsCase (glAA $1) (glAA $3)) }
         -- QualifiedDo.
         | DO  stmtlist               {% do
                                       hintQualifiedDo $1


=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -1154,14 +1154,17 @@ tcHsType mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
              -- Do not kind-generalise here!  See Note [Kind generalisation]
            ; return (mkForAllTys tv_bndrs ty') }
 
-tcHsType mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
+tcHsType mode t@(HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
   | null (unLoc ctxt)
   = tcLHsType mode rn_ty exp_kind
-    -- See Note [Body kind of a HsQualTy]
-  | Check kind <- exp_kind, isConstraintLikeKind kind
+    -- See Note [Body kind of a HsQualTy], point (BK1)
+  | Check kind <- exp_kind     -- Checking mode
+  , isConstraintLikeKind kind  -- CONSTRAINT rep
   = do { ctxt' <- tc_hs_context mode ctxt
-      ; ty'   <- tc_check_lhs_type mode rn_ty constraintKind
-      ; return (tcMkDFunPhiTy ctxt' ty') }
+         -- See Note [Body kind of a HsQualTy], point (BK2)
+       ; ty'   <- tc_check_lhs_type mode rn_ty constraintKind
+       ; let res_ty = tcMkDFunPhiTy ctxt' ty'
+       ; checkExpKind t res_ty constraintKind exp_kind }
 
   | otherwise
   = do { ctxt' <- tc_hs_context mode ctxt
@@ -1170,8 +1173,7 @@ tcHsType mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
                                 -- be TYPE r, for any r, hence newOpenTypeKind
       ; ty' <- tc_check_lhs_type mode rn_ty ek
       ; let res_ty = tcMkPhiTy ctxt' ty'
-      ; checkExpKind (unLoc rn_ty) res_ty
-                      liftedTypeKind exp_kind }
+      ; checkExpKind t res_ty liftedTypeKind exp_kind }
 
 --------- Lists, arrays, and tuples
 tcHsType mode rn_ty@(HsListTy _ elt_ty) exp_kind
@@ -2110,22 +2112,36 @@ However, consider
     instance Eq a => Eq [a] where ...
 or
     f :: (Eq a => Eq [a]) => blah
-Here both body-kind of the HsQualTy is Constraint rather than *.
+Here both body-kind and result kind of the HsQualTy is Constraint rather than *.
 Rather crudely we tell the difference by looking at exp_kind. It's
 very convenient to typecheck instance types like any other HsSigType.
 
-Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
-better to reject in checkValidType.  If we say that the body kind
-should be '*' we risk getting TWO error messages, one saying that Eq
-[a] doesn't have kind '*', and one saying that we need a Constraint to
-the left of the outer (=>).
-
-How do we figure out the right body kind?  Well, it's a bit of a
-kludge: I just look at the expected kind.  If it's Constraint, we
-must be in this instance situation context. It's a kludge because it
-wouldn't work if any unification was involved to compute that result
-kind -- but it isn't.  (The true way might be to use the 'mode'
-parameter, but that seemed like a sledgehammer to crack a nut.)
+(BK1) How do we figure out the right body kind?
+
+Well, it's a bit of a kludge: I just look at the expected kind, `exp_kind`.
+If we are in checking mode (`exp_kind` = `Check k`), and the pushed-in kind
+`k` is `CONSTRAINT rep`, then we check that the body type has kind `Constraint` too.
+
+This is a kludge because it wouldn't work if any unification was
+involved to compute that result kind -- but it isn't.
+
+Note that in the kludgy "figure out whether we are in a type or constraint"
+check, we only check if `k` is a `CONSTRAINT rep`, not `Constraint`.
+That turns out to give a better error message in T25243.
+
+(BK2)
+
+Note that, once we are in the constraint case, we check that the body has
+kind Constraint; see the call to tc_check_lhs_type. (In contrast, for
+types we check that the body has kind TYPE kappa for some fresh unification
+variable kappa.)
+Reason: we don't yet have support for constraints that are not lifted: it's
+not possible to declare a class returning a different type than CONSTRAINT LiftedRep.
+Evidence is always lifted, the fat arrow c => t requires c to be
+a lifted constraint. In a far future, if we add support for non-lifted
+constraints, we could allow c1 => c2 where
+c1 :: CONSTRAINT rep1, c2 :: CONSTRAINT rep2
+have arbitrary representations rep1 and rep2.
 
 Note [Inferring tuple kinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~


=====================================
docs/users_guide/exts/linear_types.rst
=====================================
@@ -28,8 +28,9 @@ once*, then its argument is consumed *exactly once*. Intuitively, it
 means that in every branch of the definition of ``f``, its argument
 ``x`` must be used exactly once. Which can be done by
 
-* Returning ``x`` unmodified
-* Passing ``x`` to a *linear* function
+* Returning ``x`` unmodified.
+* Passing ``x`` to a *linear* function and using the result exactly once
+  in the same fashion.
 * Pattern-matching on ``x`` and using each argument exactly once in the
   same fashion.
 * Calling it as a function and using the result exactly once in the same


=====================================
libraries/base/changelog.md
=====================================
@@ -34,6 +34,7 @@
       the context since it will be redundant. These functions are mostly useful
       for libraries that define exception-handling combinators like `catch` and
       `onException`, such as `base`, or the `exceptions` package.
+  * Move `Lift ByteArray` and `Lift Fixed` instances into `base` from `template-haskell`. See [CLC proposal #287](https://github.com/haskell/core-libraries-committee/issues/287).
 
 ## 4.20.0.0 May 2024
   * Shipped with GHC 9.10.1


=====================================
libraries/template-haskell/changelog.md
=====================================
@@ -4,6 +4,7 @@
 
   * Extend `Exp` with `ForallE`, `ForallVisE`, `ConstraintedE`,
     introduce functions `forallE`, `forallVisE`, `constraintedE` (GHC Proposal #281).
+  * `template-haskell` is no longer wired-in. All wired-in identifiers have been moved to `ghc-internal`.
 
 ## 2.22.1.0
 


=====================================
testsuite/tests/parser/should_compile/DumpSemis.stderr
=====================================
@@ -2170,8 +2170,7 @@
                 (HsCase
                  (EpAnnHsCase
                   (EpaSpan { DumpSemis.hs:37:3-6 })
-                  (EpaSpan { DumpSemis.hs:37:10-11 })
-                  [])
+                  (EpaSpan { DumpSemis.hs:37:10-11 }))
                  (L
                   (EpAnn
                    (EpaSpan { DumpSemis.hs:37:8 })


=====================================
testsuite/tests/quantified-constraints/T25243.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE DataKinds, QuantifiedConstraints, UndecidableInstances #-}
+module T25243 where
+
+import GHC.Exts
+import Data.Kind
+
+type T :: Constraint -> Constraint -> CONSTRAINT IntRep
+type T a b = a => b


=====================================
testsuite/tests/quantified-constraints/T25243.stderr
=====================================
@@ -0,0 +1,6 @@
+T25243.hs:8:14: error: [GHC-83865]
+    • Expected an IntRep constraint,
+      but ‘a => b’ is a lifted constraint
+    • In the type ‘a => b’
+      In the type declaration for ‘T’
+


=====================================
testsuite/tests/quantified-constraints/all.T
=====================================
@@ -45,3 +45,4 @@ test('T23143', normal, compile, [''])
 test('T23333', normal, compile, [''])
 test('T23323', normal, compile, [''])
 test('T22238', normal, compile, [''])
+test('T25243', normal, compile_fail, [''])


=====================================
testsuite/tests/rename/should_fail/rnfail026.stderr
=====================================
@@ -1,6 +1,6 @@
-
 rnfail026.hs:16:27: error: [GHC-83865]
-    • Expected kind ‘* -> *’, but ‘Set a’ has kind ‘*’
+    • Expected kind ‘* -> *’, but ‘Eq a => Set a’ has kind ‘*’
     • In the first argument of ‘Monad’, namely
         ‘(forall a. Eq a => Set a)’
       In the instance declaration for ‘Monad (forall a. Eq a => Set a)’
+


=====================================
utils/check-exact/ExactPrint.hs
=====================================
@@ -1211,7 +1211,6 @@ laiElseSemi k parent = fmap (\new -> parent { aiElseSemi = new })
 -- data EpAnnHsCase = EpAnnHsCase
 --       { hsCaseAnnCase :: EpaLocation
 --       , hsCaseAnnOf   :: EpaLocation
---       , hsCaseAnnsRest :: [AddEpAnn]
 --       } deriving Data
 
 lhsCaseAnnCase :: Lens EpAnnHsCase EpaLocation
@@ -1222,10 +1221,6 @@ lhsCaseAnnOf :: Lens EpAnnHsCase EpaLocation
 lhsCaseAnnOf k parent = fmap (\new -> parent { hsCaseAnnOf = new })
                                (k (hsCaseAnnOf parent))
 
-lhsCaseAnnsRest :: Lens EpAnnHsCase [AddEpAnn]
-lhsCaseAnnsRest k parent = fmap (\new -> parent { hsCaseAnnsRest = new })
-                                (k (hsCaseAnnsRest parent))
-
 -- ---------------------------------------------------------------------
 
 -- data HsRuleAnn
@@ -3161,11 +3156,8 @@ instance ExactPrint (HsExpr GhcPs) where
     an0 <- markLensKw an lhsCaseAnnCase AnnCase
     e' <- markAnnotated e
     an1 <- markLensKw an0 lhsCaseAnnOf AnnOf
-    an2 <- markEpAnnL an1 lhsCaseAnnsRest AnnOpenC
-    an3 <- markEpAnnAllL' an2 lhsCaseAnnsRest AnnSemi
     alts' <- setLayoutBoth $ markAnnotated alts
-    an4 <- markEpAnnL an3 lhsCaseAnnsRest AnnCloseC
-    return (HsCase an4 e' alts')
+    return (HsCase an1 e' alts')
 
   exact (HsIf an e1 e2 e3) = do
     an0 <- markLensKw an laiIf AnnIf
@@ -3635,11 +3627,8 @@ instance ExactPrint (HsCmd GhcPs) where
     an0 <- markLensKw an lhsCaseAnnCase AnnCase
     e' <- markAnnotated e
     an1 <- markLensKw an0 lhsCaseAnnOf AnnOf
-    an2 <- markEpAnnL an1 lhsCaseAnnsRest AnnOpenC
-    an3 <- markEpAnnAllL' an2 lhsCaseAnnsRest AnnSemi
     alts' <- markAnnotated alts
-    an4 <- markEpAnnL an3 lhsCaseAnnsRest AnnCloseC
-    return (HsCmdCase an4 e' alts')
+    return (HsCmdCase an1 e' alts')
 
   exact (HsCmdIf an a e1 e2 e3) = do
     an0 <- markLensKw an laiIf AnnIf



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/de75e423af3d3e64e4cec487ad6358f75ee5edc0...50d9fc5e73228228c5ca79fb615df38544688108

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/de75e423af3d3e64e4cec487ad6358f75ee5edc0...50d9fc5e73228228c5ca79fb615df38544688108
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/20241006/f2bee414/attachment-0001.html>


More information about the ghc-commits mailing list