[Git][ghc/ghc][master] 2 commits: Improve error messages coming from non-linear patterns

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Fri Mar 1 20:02:56 UTC 2024



Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
dec6d8d3 by Arnaud Spiwack at 2024-03-01T15:02:30-05:00
Improve error messages coming from non-linear patterns

This enriched the `CtOrigin` for non-linear patterns to include data
of the pattern that created the constraint (which can be quite useful
if it occurs nested in a pattern) as well as an explanation why the
pattern is non-restricted in (at least in some cases).

- - - - -
6612388e by Arnaud Spiwack at 2024-03-01T15:02:30-05:00
Adjust documentation of linear lets according to committee decision

- - - - -


13 changed files:

- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Types/Origin.hs
- docs/users_guide/exts/linear_types.rst
- testsuite/tests/linear/should_fail/Linear9.stderr
- testsuite/tests/linear/should_fail/LinearAsPat.stderr
- testsuite/tests/linear/should_fail/LinearLazyPat.stderr
- testsuite/tests/linear/should_fail/LinearLet6.stderr
- testsuite/tests/linear/should_fail/LinearLet7.stderr
- testsuite/tests/linear/should_fail/LinearPatSyn.stderr
- testsuite/tests/linear/should_fail/LinearViewPattern.stderr
- testsuite/tests/linear/should_fail/T20083.stderr


Changes:

=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -1175,7 +1175,7 @@ reportGroup mk_err ctxt items
 
 -- See Note [No deferring for multiplicity errors]
 nonDeferrableOrigin :: CtOrigin -> Bool
-nonDeferrableOrigin NonLinearPatternOrigin  = True
+nonDeferrableOrigin (NonLinearPatternOrigin {}) = True
 nonDeferrableOrigin (UsageEnvironmentOf {}) = True
 nonDeferrableOrigin (FRROrigin {})          = True
 nonDeferrableOrigin _                       = False


=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -804,7 +804,7 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
     manyIfPat bind@(L _ (PatBind{pat_lhs=(L _ (VarPat{}))}))
       = return bind
     manyIfPat (L loc pat@(PatBind {pat_mult=mult_ann, pat_lhs=lhs, pat_ext =(pat_ty,_)}))
-      = do { mult_co_wrap <- tcSubMult NonLinearPatternOrigin ManyTy (getTcMultAnn mult_ann)
+      = do { mult_co_wrap <- tcSubMult (NonLinearPatternOrigin GeneralisedPatternReason nlWildPatName) ManyTy (getTcMultAnn mult_ann)
            -- The wrapper checks for correct multiplicities.
            -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
            ; let lhs' = mkLHsWrapPat mult_co_wrap lhs pat_ty


=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -114,14 +114,14 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside
       | xopt LangExt.Strict dflags = xstrict lpat
       | otherwise = not_xstrict lpat
       where
-        xstrict (L _ (LazyPat _ _)) = checkManyPattern pat_ty
+        xstrict p@(L _ (LazyPat _ _)) = checkManyPattern LazyPatternReason p pat_ty
         xstrict (L _ (ParPat _ p)) = xstrict p
         xstrict _ = return WpHole
 
         not_xstrict (L _ (BangPat _ _)) = return WpHole
         not_xstrict (L _ (VarPat _ _)) = return WpHole
         not_xstrict (L _ (ParPat _ p)) = not_xstrict p
-        not_xstrict _ = checkManyPattern pat_ty
+        not_xstrict p = checkManyPattern LazyPatternReason p pat_ty
 
 -----------------
 tcMatchPats :: forall a.
@@ -467,8 +467,8 @@ tc_lpats tys penv pats
 
 --------------------
 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
-checkManyPattern :: Scaled a -> TcM HsWrapper
-checkManyPattern pat_ty = tcSubMult NonLinearPatternOrigin ManyTy (scaledMult pat_ty)
+checkManyPattern :: NonLinearPatternReason -> LPat GhcRn -> Scaled a -> TcM HsWrapper
+checkManyPattern reason pat pat_ty = tcSubMult (NonLinearPatternOrigin reason pat) ManyTy (scaledMult pat_ty)
 
 
 tc_forall_lpat :: TcTyVar -> Checker (LPat GhcRn) (LPat GhcTc)
@@ -582,7 +582,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
         ; return (BangPat x pat', res) }
 
   LazyPat x pat -> do
-        { mult_wrap <- checkManyPattern pat_ty
+        { mult_wrap <- checkManyPattern LazyPatternReason (noLocA ps_pat) pat_ty
             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
         ; (pat', (res, pat_ct))
                 <- tc_lpat pat_ty (makeLazy penv) pat $
@@ -600,14 +600,14 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
         ; return (mkHsWrapPat mult_wrap (LazyPat x pat') pat_ty, res) }
 
   WildPat _ -> do
-        { mult_wrap <- checkManyPattern pat_ty
+        { mult_wrap <- checkManyPattern OtherPatternReason (noLocA ps_pat) pat_ty
             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
         ; res <- thing_inside
         ; pat_ty <- expTypeToType (scaledThing pat_ty)
         ; return (mkHsWrapPat mult_wrap (WildPat pat_ty) pat_ty, res) }
 
   AsPat x (L nm_loc name) pat -> do
-        { mult_wrap <- checkManyPattern pat_ty
+        { mult_wrap <- checkManyPattern OtherPatternReason (noLocA ps_pat) pat_ty
             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
         ; (wrap, bndr_id) <- setSrcSpanA nm_loc (tcPatBndr penv name pat_ty)
         ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
@@ -624,7 +624,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
         ; return (mkHsWrapPat (wrap <.> mult_wrap) (AsPat x (L nm_loc bndr_id) pat') pat_ty, res) }
 
   ViewPat _ expr pat -> do
-        { mult_wrap <- checkManyPattern pat_ty
+        { mult_wrap <- checkManyPattern ViewPatternReason (noLocA ps_pat) pat_ty
          -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
          --
          -- It should be possible to have view patterns at linear (or otherwise
@@ -790,7 +790,7 @@ Fortunately that's what matchActualFunTy returns anyway.
 --
 -- When there is no negation, neg_lit_ty and lit_ty are the same
   NPat _ (L l over_lit) mb_neg eq -> do
-        { mult_wrap <- checkManyPattern pat_ty
+        { mult_wrap <- checkManyPattern OtherPatternReason (noLocA ps_pat) pat_ty
           -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
           --
           -- It may be possible to refine linear pattern so that they work in
@@ -843,7 +843,7 @@ AST is used for the subtraction operation.
 -- See Note [NPlusK patterns]
   NPlusKPat _ (L nm_loc name)
                (L loc lit) _ ge minus -> do
-        { mult_wrap <- checkManyPattern pat_ty
+        { mult_wrap <- checkManyPattern OtherPatternReason (noLocA ps_pat) pat_ty
             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
         ; let pat_exp_ty = scaledThing pat_ty
               orig = LiteralOrigin lit
@@ -1225,7 +1225,7 @@ tcPatSynPat (L con_span con_name) pat_syn pat_ty penv arg_pats thing_inside
 
         ; when (any isEqPred prov_theta) warnMonoLocalBinds
 
-        ; mult_wrap <- checkManyPattern pat_ty
+        ; mult_wrap <- checkManyPattern PatternSynonymReason nlWildPatName pat_ty
             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
 
         ; (univ_ty_args, ex_ty_args) <- splitConTyArgs con_like arg_pats


=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -22,7 +22,7 @@ module GHC.Tc.Types.Origin (
   isVisibleOrigin, toInvisibleOrigin,
   pprCtOrigin, isGivenOrigin, isWantedWantedFunDepOrigin,
   isWantedSuperclassOrigin,
-  ClsInstOrQC(..), NakedScFlag(..),
+  ClsInstOrQC(..), NakedScFlag(..), NonLinearPatternReason(..),
 
   TypedThing(..), TyVarBndrs(..),
 
@@ -621,7 +621,7 @@ data CtOrigin
       Module  -- ^ Module in which the instance was declared
       ClsInst -- ^ The declared typeclass instance
 
-  | NonLinearPatternOrigin
+  | NonLinearPatternOrigin NonLinearPatternReason (LPat GhcRn)
   | UsageEnvironmentOf Name
 
   | CycleBreakerOrigin
@@ -642,6 +642,12 @@ data CtOrigin
       Type   -- the instantiated type of the method
   | AmbiguityCheckOrigin UserTypeCtxt
 
+data NonLinearPatternReason
+  = LazyPatternReason
+  | GeneralisedPatternReason
+  | PatternSynonymReason
+  | ViewPatternReason
+  | OtherPatternReason
 
 -- | The number of superclass selections needed to get this Given.
 -- If @d :: C ty@   has @ScDepth=2@, then the evidence @d@ will look
@@ -881,6 +887,10 @@ pprCtOrigin (ScOrigin (IsQC orig) nkd)
          , whenPprDebug (braces (text "sc-origin:" <> ppr nkd))
          , pprCtOrigin orig ]
 
+pprCtOrigin (NonLinearPatternOrigin reason pat)
+  = hang (ctoHerald <+> text "a non-linear pattern" <+> quotes (ppr pat))
+       2 (pprNonLinearPatternReason reason)
+
 pprCtOrigin simple_origin
   = ctoHerald <+> pprCtO simple_origin
 
@@ -921,7 +931,6 @@ pprCtO PatCheckOrigin        = text "a pattern-match completeness check"
 pprCtO ListOrigin            = text "an overloaded list"
 pprCtO IfThenElseOrigin      = text "an if-then-else expression"
 pprCtO StaticOrigin          = text "a static form"
-pprCtO NonLinearPatternOrigin = text "a non-linear pattern"
 pprCtO (UsageEnvironmentOf x) = hsep [text "multiplicity of", quotes (ppr x)]
 pprCtO BracketOrigin         = text "a quotation bracket"
 
@@ -949,7 +958,14 @@ pprCtO (WantedSuperclassOrigin {})  = text "a superclass constraint"
 pprCtO (InstanceSigOrigin {})       = text "a type signature in an instance"
 pprCtO (AmbiguityCheckOrigin {})    = text "a type ambiguity check"
 pprCtO (ImpedanceMatching {})       = text "combining required constraints"
-
+pprCtO (NonLinearPatternOrigin _ pat) = hsep [text "a non-linear pattern" <+> quotes (ppr pat)]
+
+pprNonLinearPatternReason :: HasCallStack => NonLinearPatternReason -> SDoc
+pprNonLinearPatternReason LazyPatternReason = parens (text "non-variable lazy pattern aren't linear")
+pprNonLinearPatternReason GeneralisedPatternReason = parens (text "non-variable pattern bindings that have been generalised aren't linear")
+pprNonLinearPatternReason PatternSynonymReason = parens (text "pattern synonyms aren't linear")
+pprNonLinearPatternReason ViewPatternReason = parens (text "view patterns aren't linear")
+pprNonLinearPatternReason OtherPatternReason = empty
 
 {- *********************************************************************
 *                                                                      *


=====================================
docs/users_guide/exts/linear_types.rst
=====================================
@@ -119,7 +119,7 @@ multiplicity if:
 - The binding is a pattern binding (including a simple variable)
   ``p=e`` (you can't write ``let %1 f x = u``, instead write ``let %1
   f = \x -> u``)
-- Either ``p`` is of the form ``!p'`` or ``p`` is a variable. In
+- Either ``p`` is strict (see infra) or ``p`` is a variable. In
   particular neither ``x at y`` nor ``(x)`` are covered by “is a
   variable”
 
@@ -136,13 +136,79 @@ as follows:
 - In all other cases, including function bindings ``let f x1...xn = rhs``,
   the multiplicity is inferred from the term.
 
-When ``-XMonoLocalBinds`` is on, the following also holds:
+When ``-XMonoLocalBinds`` is off, the following also holds:
 
 - Multiplicity-annotated non-variable pattern-bindings (such as
   ``let %1 !(x,y) = rhs``) are never generalised.
 - Non-variable pattern bindings which are inferred as polymorphic or
   qualified are inferred as having multiplicity ``Many``.
 
+Strict patterns
+~~~~~~~~~~~~~~~
+
+GHC considers that non-variable lazy patterns consume the scrutinee
+with multiplicity ``Many``. In practice, a pattern is strict (hence
+can be linear) if (otherwise the pattern is lazy):
+
+- The pattern is a case alternative and isn't annotated with a ``~``
+- The pattern is a let-binding, and is annotated with a ``!``
+- The pattern is a let-binding, :extension:`Strict` is on, and isn't
+  annotated with a ``~``
+- The pattern is nested inside a strict pattern
+
+Here are some examples of the impact on linear typing:
+
+Without ``-XStrict``::
+
+   -- good
+   let %1 x = u in …
+
+   -- good
+   let %1 !x = u in …
+
+   -- bad
+   let %1 (x, y) = u in …
+
+   -- good
+   let %Many (x, y) = u in …
+
+   -- good
+   let %1 !(x, y) = u in …
+
+   -- good
+   let %1 (!(x, y)) = u in …
+
+   -- inferred unrestricted
+   let (x, y) = u in …
+
+   -- can be inferred linear
+   case u of (x, y) -> …
+
+   -- inferred unrestricted
+   case u of ~(x, y) -> …
+
+With ``-XStrict``::
+   -- good
+   let %1 x = u in …
+
+   -- good
+   let %1 !x = u in …
+
+   -- good
+   let %1 (x, y) = u in …
+
+   -- bad
+   let %1 ~(x, y) = u in …
+
+   -- good
+   let %Many ~(x, y) = u in …
+
+   -- can be inferred linear
+   let (x, y) = u in …
+
+   -- inferred unrestricted
+   let ~(x, y) = u in …
+
 Data types
 ----------
 By default, all fields in algebraic data types are linear (even if


=====================================
testsuite/tests/linear/should_fail/Linear9.stderr
=====================================
@@ -1,7 +1,7 @@
 
 Linear9.hs:9:17: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘_’
     • In the pattern: _
       In the pattern: (a, _)
       In an equation for ‘incorrectFst’: incorrectFst (a, _) = a
@@ -21,14 +21,14 @@ Linear9.hs:15:20: error: [GHC-18872]
 
 Linear9.hs:18:21: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘_’
     • In the pattern: _
       In the pattern: (a, _)
       In the pattern: ((a, _), _)
 
 Linear9.hs:18:24: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘_’
     • In the pattern: _
       In the pattern: ((a, _), _)
       In an equation for ‘incorrectFstFst’:
@@ -36,7 +36,7 @@ Linear9.hs:18:24: error: [GHC-18872]
 
 Linear9.hs:25:25: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘_’
     • In the pattern: _
       In the pattern: Foo a _
       In an equation for ‘incorrectTestFst’:


=====================================
testsuite/tests/linear/should_fail/LinearAsPat.stderr
=====================================
@@ -1,5 +1,5 @@
 
 LinearAsPat.hs:6:12: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘x at True’
     • In an equation for ‘shouldFail’: shouldFail x at True = x


=====================================
testsuite/tests/linear/should_fail/LinearLazyPat.stderr
=====================================
@@ -1,6 +1,7 @@
 
 LinearLazyPat.hs:5:3: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘~(x, y)’
+          (non-variable lazy pattern aren't linear)
     • In the pattern: ~(x, y)
       In an equation for ‘f’: f ~(x, y) = (y, x)


=====================================
testsuite/tests/linear/should_fail/LinearLet6.stderr
=====================================
@@ -15,7 +15,8 @@ LinearLet6.hs:10:3: error: [GHC-18872]
 
 LinearLet6.hs:15:14: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘Just y’
+          (non-variable lazy pattern aren't linear)
     • In a pattern binding: (Just y) = x
       In the expression: let %1 (Just y) = x in y
       In an equation for ‘h’: h x = let %1 (Just y) = x in y


=====================================
testsuite/tests/linear/should_fail/LinearLet7.stderr
=====================================
@@ -8,6 +8,7 @@ LinearLet7.hs:6:14: error: [GHC-18872]
 
 LinearLet7.hs:6:14: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘_’
+          (non-variable pattern bindings that have been generalised aren't linear)
     • In the expression: let %1 g = \ y -> ... in g x
       In an equation for ‘f’: f x = let %1 g = ... in g x


=====================================
testsuite/tests/linear/should_fail/LinearPatSyn.stderr
=====================================
@@ -1,6 +1,7 @@
 
 LinearPatSyn.hs:13:4: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘_’
+          (pattern synonyms aren't linear)
     • In the pattern: P y x
       In an equation for ‘s’: s (P y x) = (y, x)


=====================================
testsuite/tests/linear/should_fail/LinearViewPattern.stderr
=====================================
@@ -1,6 +1,7 @@
 
 LinearViewPattern.hs:11:4: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘not -> True’
+          (view patterns aren't linear)
     • In the pattern: not -> True
       In an equation for ‘f’: f (not -> True) = True


=====================================
testsuite/tests/linear/should_fail/T20083.stderr
=====================================
@@ -13,6 +13,6 @@ T20083.hs:6:6: error: [GHC-25897]
 
 T20083.hs:9:5: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
-        arising from a non-linear pattern
+        arising from a non-linear pattern ‘_’
     • In the pattern: _
       In an equation for ‘ap2’: ap2 _ = ()



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/bbdb6286854dca442ab2b6aeebc734cfb7e0bd9a...6612388e0e360bd4f6eaddee3f632deed8616a5e

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/bbdb6286854dca442ab2b6aeebc734cfb7e0bd9a...6612388e0e360bd4f6eaddee3f632deed8616a5e
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/20240301/53e5bdf1/attachment-0001.html>


More information about the ghc-commits mailing list