Allow as-patterns in unidirectional patttern synonyms

This patch implements GHC Proposal #94, described here
   https://github.com/ghc-proposals/ghc-proposals/pull/94

The effect is simply to lift a totally-undocumented restriction to
unidirecional pattern synonyms, namely that they can't have as-patterns
or n+k patterns.

The fix is easy: just remove the checks.

I also took the opportunity to improve the manual entry for
the semantics of pattern matching for pattern synonyms.

5 files changed, 20 insertions, 71 deletions

diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 1e2d85e323..9c8880e7ce 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -72,7 +72,6 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
                        psb_def = lpat, psb_dir = dir }
   = addPatSynCtxt lname $
     do { traceTc "tcInferPatSynDecl {" $ ppr name
-       ; tcCheckPatSynPat lpat
 
        ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
        ; (tclvl, wanted, ((lpat', args), pat_ty))
@@ -250,8 +249,6 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
          vcat [ ppr implicit_tvs, ppr explicit_univ_tvs, ppr req_theta
               , ppr explicit_ex_tvs, ppr prov_theta, ppr sig_body_ty ]
 
-       ; tcCheckPatSynPat lpat
-
        ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
                                  Right stuff  -> return stuff
                                  Left missing -> wrongNumberOfParmsErr name decl_arity missing
@@ -1032,68 +1029,6 @@ Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
 want to avoid difficult to decipher core lint errors!
  -}
 
-tcCheckPatSynPat :: LPat GhcRn -> TcM ()
-tcCheckPatSynPat = go
-  where
-    go :: LPat GhcRn -> TcM ()
-    go = addLocM go1
-
-    go1 :: Pat GhcRn -> TcM ()
-    -- See Note [Bad patterns]
-    go1 p@(AsPat _ _)         = asPatInPatSynErr p
-    go1 p@NPlusKPat{}         = nPlusKPatInPatSynErr p
-
-    go1   (ConPatIn _ info)   = mapM_ go (hsConPatArgs info)
-    go1   VarPat{}            = return ()
-    go1   WildPat{}           = return ()
-    go1   (LazyPat pat)       = go pat
-    go1   (ParPat pat)        = go pat
-    go1   (BangPat pat)       = go pat
-    go1   (PArrPat pats _)    = mapM_ go pats
-    go1   (ListPat pats _ _)  = mapM_ go pats
-    go1   (TuplePat pats _ _) = mapM_ go pats
-    go1   (SumPat pat _ _ _)  = go pat
-    go1   LitPat{}            = return ()
-    go1   NPat{}              = return ()
-    go1   (SigPatIn pat _)    = go pat
-    go1   (ViewPat _ pat _)   = go pat
-    go1   (SplicePat splice)
-      | HsSpliced mod_finalizers (HsSplicedPat pat) <- splice
-                              = do addModFinalizersWithLclEnv mod_finalizers
-                                   go1 pat
-      | otherwise             = panic "non-pattern from spliced thing"
-    go1   ConPatOut{}         = panic "ConPatOut in output of renamer"
-    go1   SigPatOut{}         = panic "SigPatOut in output of renamer"
-    go1   CoPat{}             = panic "CoPat in output of renamer"
-
-asPatInPatSynErr :: (SourceTextX p, OutputableBndrId p) => Pat p -> TcM a
-asPatInPatSynErr pat
-  = failWithTc $
-    hang (text "Pattern synonym definition cannot contain as-patterns (@):")
-       2 (ppr pat)
-
-nPlusKPatInPatSynErr :: (SourceTextX p, OutputableBndrId p) => Pat p -> TcM a
-nPlusKPatInPatSynErr pat
-  = failWithTc $
-    hang (text "Pattern synonym definition cannot contain n+k-pattern:")
-       2 (ppr pat)
-
-{- Note [Bad patterns]
-~~~~~~~~~~~~~~~~~~~~~~
-We don't currently allow as-patterns or n+k patterns in a pattern synonym.
-Reason: consider
-  pattern P x y = x@(Just y)
-
-What would
-  f (P Nothing False) = e
-mean?  Presumably something like
-  f Nothing@(Just False) = e
-But as-patterns don't allow a pattern before the @ sign!  Perhaps they
-should -- with p1@p2 meaning match both p1 and p2 -- but they don't
-currently.  Hence bannning them in pattern synonyms.  Actually lifting
-the restriction would be simple and well-defined.  See Trac #9793.
--}
-
 
 nonBidirectionalErr :: Outputable name => name -> TcM a
 nonBidirectionalErr name = failWithTc $
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 49c6ed4709..1717cbb0b2 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -5586,6 +5586,24 @@ Matching of pattern synonyms
 
 A pattern synonym occurrence in a pattern is evaluated by first matching
 against the pattern synonym itself, and then on the argument patterns.
+
+More precisely, the semantics of pattern matching is given in
+`Section 3.17 of the Haskell 2010 report <https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.17>`__.   To the informal semantics in Section 3.17.2 we add this extra rule:
+
+* If the pattern is a constructor pattern ``(P p1 ... pn)``, where ``P`` is
+  a pattern synonym defined by ``P x1 ... xn = p`` or ``P x1 ... xn <- p``, then:
+
+  (a) Match the value ``v`` against ``p``. If this match fails or diverges,
+      so does the whole (pattern synonym) match.   Otherwise the match
+      against ``p`` must bind the variables ``x1 ... xn``; let them be bound to values ``v1 ... vn``.
+
+  (b) Match ``v1`` against ``p1``, ``v2`` against ``p2`` and so on.
+      If any of these matches fail or diverge, so does the whole match.
+
+  (c) If all the matches against the ``pi`` succeed, the match succeeds,
+      binding the variables bound by the ``pi`` . (The ``xi`` are not
+      bound; they remain local to the pattern synonym declaration.)
+
 For example, in the following program, ``f`` and ``f'`` are equivalent: ::
 
     pattern Pair x y <- [x, y]
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 0f4c608169..d3a0a9b771 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -1,7 +1,7 @@
 test('mono', normal, compile_fail, [''])
 test('unidir', normal, compile_fail, [''])
 test('local', normal, compile_fail, [''])
-test('as-pattern', normal, compile_fail, [''])
+test('as-pattern', normal, compile, [''])
 test('T9161-1', normal, compile_fail, [''])
 test('T9161-2', normal, compile_fail, [''])
 test('T9705-1', normal, compile_fail, [''])
diff --git a/testsuite/tests/patsyn/should_fail/as-pattern.hs b/testsuite/tests/patsyn/should_fail/as-pattern.hs
index 2794bed16a..f3ec9c9029 100644
--- a/testsuite/tests/patsyn/should_fail/as-pattern.hs
+++ b/testsuite/tests/patsyn/should_fail/as-pattern.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE PatternSynonyms #-}
 module ShouldFail where
 
+-- This is now ok (following GHC proposal #94)
 pattern P x y <- x@(Just y)
diff --git a/testsuite/tests/patsyn/should_fail/as-pattern.stderr b/testsuite/tests/patsyn/should_fail/as-pattern.stderr
deleted file mode 100644
index 61df61742e..0000000000
--- a/testsuite/tests/patsyn/should_fail/as-pattern.stderr
+++ /dev/null
@@ -1,5 +0,0 @@
-
-as-pattern.hs:4:18: error:
-    • Pattern synonym definition cannot contain as-patterns (@):
-        x@(Just y)
-    • In the declaration for pattern synonym ‘P’