Reject pattern synonyms with linear types (#18806)wip/T18806

8 files changed, 36 insertions, 5 deletions

diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 73ef9d9470..de04bedfe2 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -73,6 +73,9 @@ instance Diagnostic TcRnMessage where
       -> mkSimpleDecorated $
            hang (text "Illegal pattern synonym declaration for" <+> quotes (ppr rdrname))
               2 (text "Pattern synonym declarations are only valid at top level")
+    TcRnLinearPatSyn ty
+      -> mkSimpleDecorated $
+           hang (text "Pattern synonyms do not support linear fields (GHC #18806):") 2 (ppr ty)
     TcRnEmptyRecordUpdate
       -> mkSimpleDecorated $ text "Empty record update"
     TcRnIllegalFieldPunning fld
@@ -123,6 +126,8 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnIllegalPatSynDecl{}
       -> ErrorWithoutFlag
+    TcRnLinearPatSyn{}
+      -> ErrorWithoutFlag
     TcRnEmptyRecordUpdate
       -> ErrorWithoutFlag
     TcRnIllegalFieldPunning{}
@@ -168,6 +173,8 @@ instance Diagnostic TcRnMessage where
       -> [SuggestIncreaseSimplifierIterations]
     TcRnIllegalPatSynDecl{}
       -> noHints
+    TcRnLinearPatSyn{}
+      -> noHints
     TcRnEmptyRecordUpdate{}
       -> noHints
     TcRnIllegalFieldPunning{}
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 6d133bff61..a82ac7328f 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -231,6 +231,15 @@ data TcRnMessage where
   -}
   TcRnIllegalPatSynDecl :: !(LIdP GhcPs) -> TcRnMessage
 
+  {-| TcRnLinearPatSyn is an error that occurs whenever a pattern
+      synonym signature uses a field that is not unrestricted.
+
+      Example(s): None
+
+     Test cases: linear/should_fail/LinearPatSyn2
+  -}
+  TcRnLinearPatSyn :: !Type -> TcRnMessage
+
   {-| TcRnEmptyRecordUpdate is an error that occurs whenever
       a record is updated without specifying any field.
 
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index bc78e8b592..fa4cd8fecf 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -23,7 +23,7 @@ import GHC.Prelude
 import GHC.Hs
 import GHC.Tc.Gen.Pat
 import GHC.Core.Multiplicity
-import GHC.Core.Type ( tidyTyCoVarBinders, tidyTypes, tidyType )
+import GHC.Core.Type ( tidyTyCoVarBinders, tidyTypes, tidyType, isManyDataConTy )
 import GHC.Core.TyCo.Subst( extendTvSubstWithClone )
 import GHC.Tc.Errors.Types
 import GHC.Tc.Utils.Monad
@@ -389,6 +389,10 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
              univ_tvs   = binderVars univ_bndrs
              ex_tvs     = binderVars ex_bndrs
 
+         -- Pattern synonyms currently cannot be linear (#18806)
+       ; checkTc (all (isManyDataConTy . scaledMult) arg_tys) $
+           TcRnLinearPatSyn sig_body_ty
+
          -- Skolemise the quantified type variables. This is necessary
          -- in order to check the actual pattern type against the
          -- expected type. Even though the tyvars in the type are
@@ -513,8 +517,8 @@ Hence a special-purpose skolemiseTvBndrX here, similar to
 GHC.Tc.Utils.Instantiate.tcInstSkolTyVarsX except that the latter
 does cloning.
 
-[Pattern synonyms and higher rank types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Pattern synonyms and higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
   data T = MkT (forall a. a->a)
 
diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn.hs b/testsuite/tests/linear/should_fail/LinearPatSyn.hs
index 3e87bfc078..a874d320d0 100644
--- a/testsuite/tests/linear/should_fail/LinearPatSyn.hs
+++ b/testsuite/tests/linear/should_fail/LinearPatSyn.hs
@@ -7,7 +7,6 @@ module LinearPatSyn where
 -- seems to require changes to the desugarer. So currently pattern synonyms are
 -- disallowed in linear patterns.
 
-pattern P :: b %1 -> a %1 -> (a, b)
 pattern P y x = (x, y)
 
 s :: (a, b) %1 -> (b, a)
diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn.stderr b/testsuite/tests/linear/should_fail/LinearPatSyn.stderr
index f7c3aab406..95d18396aa 100644
--- a/testsuite/tests/linear/should_fail/LinearPatSyn.stderr
+++ b/testsuite/tests/linear/should_fail/LinearPatSyn.stderr
@@ -1,5 +1,5 @@
 
-LinearPatSyn.hs:14:4: error:
+LinearPatSyn.hs:13:4: error:
     • Couldn't match type ‘'Many’ with ‘'One’
         arising from a non-linear pattern
     • In the pattern: P y x
diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn2.hs b/testsuite/tests/linear/should_fail/LinearPatSyn2.hs
new file mode 100644
index 0000000000..ae1d35ce66
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearPatSyn2.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE PatternSynonyms, LinearTypes #-}
+module LinearPatSyn2 where
+
+-- Should be rejected, #18806
+pattern J :: x %1 -> Maybe x
+pattern J a = Just a
diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr b/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr
new file mode 100644
index 0000000000..1360983907
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr
@@ -0,0 +1,5 @@
+
+LinearPatSyn2.hs:6:9: error:
+    • Pattern synonyms do not support linear fields (GHC #18806):
+        x %1 -> Maybe x
+    • In the declaration for pattern synonym ‘J’
diff --git a/testsuite/tests/linear/should_fail/all.T b/testsuite/tests/linear/should_fail/all.T
index a831011cef..9f8ba14483 100644
--- a/testsuite/tests/linear/should_fail/all.T
+++ b/testsuite/tests/linear/should_fail/all.T
@@ -17,6 +17,7 @@ test('LinearSeq', normal, compile_fail, [''])
 test('LinearViewPattern', normal, compile_fail, [''])
 test('LinearConfusedDollar', normal, compile_fail, [''])
 test('LinearPatSyn', normal, compile_fail, [''])
+test('LinearPatSyn2', normal, compile_fail, [''])
 test('LinearRole', normal, compile_fail, [''])
 test('LinearGADTNewtype', normal, compile_fail, [''])
 test('LinearPartialSig', normal, compile_fail, [''])