Add a warning for GADT match + NoMonoLocalBinds (#20485)wip/T20485

Previously, it was an error to pattern match on a GADT
without GADTs or TypeFamilies.
This is now allowed. Instead, we check the flag MonoLocalBinds;
if it is not enabled, we issue a warning, controlled by -Wgadt-mono-local-binds.

Also fixes #20485: pattern synonyms are now checked too.

12 files changed, 109 insertions, 14 deletions

diff --git a/compiler/GHC/Driver/Flags.hs b/compiler/GHC/Driver/Flags.hs
index 192b983887..02b42b1dcd 100644
--- a/compiler/GHC/Driver/Flags.hs
+++ b/compiler/GHC/Driver/Flags.hs
@@ -538,6 +538,7 @@ data WarningFlag =
    | Opt_WarnRedundantStrictnessFlags     -- Since 9.4
    | Opt_WarnForallIdentifier             -- Since 9.4
    | Opt_WarnUnicodeBidirectionalFormatCharacters -- Since 9.0.2
+   | Opt_WarnGADTMonoLocalBinds           -- Since 9.4
    deriving (Eq, Ord, Show, Enum)
 
 -- | Return the names of a WarningFlag
@@ -639,6 +640,7 @@ warnFlagNames wflag = case wflag of
   Opt_WarnMissingExportedPatternSynonymSignatures -> "missing-exported-pattern-synonym-signatures" :| []
   Opt_WarnForallIdentifier                        -> "forall-identifier" :| []
   Opt_WarnUnicodeBidirectionalFormatCharacters    -> "unicode-bidirectional-format-characters" :| []
+  Opt_WarnGADTMonoLocalBinds                      -> "gadt-mono-local-binds" :| []
 
 -- -----------------------------------------------------------------------------
 -- Standard sets of warning options
@@ -731,7 +733,8 @@ standardWarnings -- see Note [Documenting warning flags]
         Opt_WarnNonCanonicalMonoidInstances,
         Opt_WarnOperatorWhitespaceExtConflict,
         Opt_WarnForallIdentifier,
-        Opt_WarnUnicodeBidirectionalFormatCharacters
+        Opt_WarnUnicodeBidirectionalFormatCharacters,
+        Opt_WarnGADTMonoLocalBinds
       ]
 
 -- | Things you get with -W
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 5f4479939a..92149c96f4 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -3219,7 +3219,8 @@ wWarningFlagsDeps = mconcat [
   warnSpec    Opt_WarnImplicitLift,
   warnSpec    Opt_WarnMissingExportedPatternSynonymSignatures,
   warnSpec    Opt_WarnForallIdentifier,
-  warnSpec    Opt_WarnUnicodeBidirectionalFormatCharacters
+  warnSpec    Opt_WarnUnicodeBidirectionalFormatCharacters,
+  warnSpec    Opt_WarnGADTMonoLocalBinds
  ]
 
 -- | These @-\<blah\>@ flags can all be reversed with @-no-\<blah\>@
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index b5a0dbb284..5353280438 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -522,6 +522,10 @@ instance Diagnostic TcRnMessage where
             fsep [ text "The use of" <+> quotes (ppr rdr_name)
                                      <+> text "as an identifier",
                    text "will become an error in a future GHC release." ]
+    TcRnGADTMonoLocalBinds
+      -> mkSimpleDecorated $
+            fsep [ text "Pattern matching on GADTs without MonoLocalBinds"
+                 , text "is fragile." ]
 
   diagnosticReason = \case
     TcRnUnknownMessage m
@@ -740,6 +744,8 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnForallIdentifier {}
       -> WarningWithFlag Opt_WarnForallIdentifier
+    TcRnGADTMonoLocalBinds {}
+      -> WarningWithFlag Opt_WarnGADTMonoLocalBinds
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -952,6 +958,8 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnForallIdentifier {}
       -> [SuggestRenameForall]
+    TcRnGADTMonoLocalBinds {}
+      -> [suggestAnyExtension [LangExt.GADTs, LangExt.TypeFamilies]]
 
 deriveInstanceErrReasonHints :: Class
                              -> UsingGeneralizedNewtypeDeriving
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 98e2479e52..accd611e68 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -1423,6 +1423,15 @@ data TcRnMessage where
   -}
   TcRnForallIdentifier :: RdrName -> TcRnMessage
 
+  {-| TcRnGADTMonoLocalBinds is a warning controlled by -Wgadt-mono-local-binds
+      that occurs when pattern matching on a GADT when -XMonoLocalBinds is off.
+
+      Example(s): None
+
+      Test cases: T20485, T20485a
+  -}
+  TcRnGADTMonoLocalBinds :: TcRnMessage
+
 -- | Which parts of a record field are affected by a particular error or warning.
 data RecordFieldPart
   = RecordFieldConstructor !Name
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index a235c43236..00b2e053f8 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -868,6 +868,19 @@ tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside
                                              pat_ty arg_pats thing_inside
         }
 
+-- Warn when pattern matching on a GADT or a pattern synonym
+-- when MonoLocalBinds is off.
+warnMonoLocalBinds :: TcM ()
+warnMonoLocalBinds
+  = do { mono_local_binds <- xoptM LangExt.MonoLocalBinds
+       ; unless mono_local_binds $
+           addDiagnostic TcRnGADTMonoLocalBinds
+           -- We used to require the GADTs or TypeFamilies extension
+           -- to pattern match on a GADT (#2905, #7156)
+           --
+           -- In #20485 this was made into a warning.
+       }
+
 tcDataConPat :: PatEnv -> LocatedN Name -> DataCon
              -> Scaled ExpSigmaType        -- Type of the pattern
              -> HsConPatDetails GhcRn -> TcM a
@@ -940,21 +953,12 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
         { let theta'     = substTheta tenv (eqSpecPreds eq_spec ++ theta)
                            -- order is *important* as we generate the list of
                            -- dictionary binders from theta'
-              no_equalities = null eq_spec && not (any isEqPred theta)
               skol_info = PatSkol (RealDataCon data_con) mc
               mc = case pe_ctxt penv of
                      LamPat mc -> mc
                      LetPat {} -> PatBindRhs
 
-        ; gadts_on    <- xoptM LangExt.GADTs
-        ; families_on <- xoptM LangExt.TypeFamilies
-        ; checkTc (no_equalities || gadts_on || families_on)
-                  (TcRnUnknownMessage $ mkPlainError noHints $
-                   text "A pattern match on a GADT requires the" <+>
-                   text "GADTs or TypeFamilies language extension")
-                  -- #2905 decided that a *pattern-match* of a GADT
-                  -- should require the GADT language flag.
-                  -- Re TypeFamilies see also #7156
+        ; when (not (null eq_spec) || any isEqPred theta) warnMonoLocalBinds
 
         ; given <- newEvVars theta'
         ; (ev_binds, (arg_pats', res))
@@ -999,6 +1003,8 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
               prov_theta' = substTheta tenv prov_theta
               req_theta'  = substTheta tenv req_theta
 
+        ; when (any isEqPred prov_theta) warnMonoLocalBinds
+
         ; mult_wrap <- checkManyPattern pat_ty
             -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
 
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index baabbbdc37..6ddeb66e41 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -57,6 +57,7 @@ To reverse ``-Werror``, which makes all warnings into errors, use ``-Wwarn``.
         * :ghc-flag:`-Wambiguous-fields`
         * :ghc-flag:`-Wunicode-bidirectional-format-characters`
         * :ghc-flag:`-Wforall-identifier`
+        * :ghc-flag:`-Wgadt-mono-local-binds`
 
 The following flags are simple ways to select standard "packages" of warnings:
 
@@ -2203,6 +2204,8 @@ of ``-W(no-)*``.
     :type: dynamic
     :category:
 
+    :since: 9.0.2
+
     Explicit unicode bidirectional formatting characters can cause source code
     to be rendered misleadingly in many viewers. We warn if any such character
     is present in the source.
@@ -2212,8 +2215,31 @@ of ``-W(no-)*``.
     category of the `Unicode Bidirectional Character Type Listing
     <https://www.unicode.org/reports/tr9/#Bidirectional_Character_Types>`_
 
-    :since: 9.0.2
+.. ghc-flag:: -Wgadt-mono-local-binds
+    :shortdesc: warn when pattern matching on a GADT without MonoLocalBinds
+    :type: dynamic
+    :reverse: -Wno-gadt-mono-local-binds
+
+    :since: 9.4.1
+
+    This warning is triggered on pattern matching involving GADTs,
+    if :extension:`MonoLocalBinds` is disabled.
+    Type inference can be fragile in this case.
+
+    See the `OutsideIn(X) <https://www.microsoft.com/en-us/research/publication/outsideinx-modular-type-inference-with-local-assumptions/>`__
+    paper (section 4.2) and :ref:`mono-local-binds` for more details.
+
+    To resolve this warning, you can enable :extension:`MonoLocalBinds`
+    or an extension implying it (:extension:`GADTs` or
+    :extension:`TypeFamilies`).
+
+    The warning is also triggered when matching on GADT-like
+    pattern synonyms (i.e. pattern synonyms containing equalities in provided
+    constraints).
 
+    In previous versions of GHC (9.2 and below), it was an error
+    to pattern match on a GADT if neither :extension:`GADTs`
+    nor :extension:`TypeFamilies` were enabled.
 
 If you're feeling really paranoid, the :ghc-flag:`-dcore-lint` option is a good choice.
 It turns on heavyweight intra-pass sanity-checking within GHC. (It checks GHC's
diff --git a/testsuite/tests/gadt/T20485.hs b/testsuite/tests/gadt/T20485.hs
new file mode 100644
index 0000000000..5fb115df6e
--- /dev/null
+++ b/testsuite/tests/gadt/T20485.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE PatternSynonyms #-}
+module T20485 where
+
+import Data.Type.Equality
+
+f :: a :~: b -> a -> b
+f Refl x = x
+
+pattern ReflPat = Refl
+
+g :: a :~: b -> a -> b
+g ReflPat x = x
diff --git a/testsuite/tests/gadt/T20485.stderr b/testsuite/tests/gadt/T20485.stderr
new file mode 100644
index 0000000000..e140b58ad3
--- /dev/null
+++ b/testsuite/tests/gadt/T20485.stderr
@@ -0,0 +1,15 @@
+
+T20485.hs:7:3: warning: [-Wgadt-mono-local-binds (in -Wdefault)]
+    Pattern matching on GADTs without MonoLocalBinds is fragile.
+    Suggested fix:
+      Enable any of the following extensions: GADTs, TypeFamilies
+
+T20485.hs:9:19: warning: [-Wgadt-mono-local-binds (in -Wdefault)]
+    Pattern matching on GADTs without MonoLocalBinds is fragile.
+    Suggested fix:
+      Enable any of the following extensions: GADTs, TypeFamilies
+
+T20485.hs:12:3: warning: [-Wgadt-mono-local-binds (in -Wdefault)]
+    Pattern matching on GADTs without MonoLocalBinds is fragile.
+    Suggested fix:
+      Enable any of the following extensions: GADTs, TypeFamilies
diff --git a/testsuite/tests/gadt/T20485a.hs b/testsuite/tests/gadt/T20485a.hs
new file mode 100644
index 0000000000..fa8c1ee969
--- /dev/null
+++ b/testsuite/tests/gadt/T20485a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE PatternSynonyms, MonoLocalBinds #-}
+module T20485a where
+
+import Data.Type.Equality
+
+f :: a :~: b -> a -> b
+f Refl x = x
+
+pattern ReflPat = Refl
+
+g :: a :~: b -> a -> b
+g ReflPat x = x
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index 9179a40288..3152f3561b 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -122,3 +122,5 @@ test('T16427', normal, compile_fail, [''])
 test('T18191', normal, compile_fail, [''])
 test('T20278', normal, compile, [''])
 test('SynDataRec', normal, compile, [''])
+test('T20485', normal, compile, [''])
+test('T20485a', normal, compile, [''])
diff --git a/testsuite/tests/patsyn/should_compile/T10997.hs b/testsuite/tests/patsyn/should_compile/T10997.hs
index 69a7940a5f..49278a2a33 100644
--- a/testsuite/tests/patsyn/should_compile/T10997.hs
+++ b/testsuite/tests/patsyn/should_compile/T10997.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -Wno-gadt-mono-local-binds #-}
 module T10997 where
 
 import T10997a
diff --git a/testsuite/tests/typecheck/should_run/Typeable1.hs b/testsuite/tests/typecheck/should_run/Typeable1.hs
index 02a7ebb98b..9a38c85927 100644
--- a/testsuite/tests/typecheck/should_run/Typeable1.hs
+++ b/testsuite/tests/typecheck/should_run/Typeable1.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE PolyKinds, GADTs #-}
 
 import Type.Reflection
 import Data.Kind