Don't allow orphan COMPLETE pragmas (#13349)

We might support them properly in the future, but for now it's simpler
to disallow them.

Test Plan: validate

Reviewers: mpickering, austin, bgamari, simonpj

Reviewed By: mpickering, simonpj

Subscribers: simonpj, thomie

Differential Revision: https://phabricator.haskell.org/D3243

7 files changed, 64 insertions, 6 deletions

diff --git a/compiler/rename/RnBinds.hs b/compiler/rename/RnBinds.hs
index f8b3347ca5..705befd1bb 100644
--- a/compiler/rename/RnBinds.hs
+++ b/compiler/rename/RnBinds.hs
@@ -952,10 +952,44 @@ renameSig ctxt sig@(SCCFunSig st v s)
 
 -- COMPLETE Sigs can refer to imported IDs which is why we use
 -- lookupLocatedOccRn rather than lookupSigOccRn
-renameSig _ctxt (CompleteMatchSig s (L l bf) mty)
+renameSig _ctxt sig@(CompleteMatchSig s (L l bf) mty)
   = do new_bf <- traverse lookupLocatedOccRn bf
        new_mty  <- traverse lookupLocatedOccRn mty
+
+       this_mod <- fmap tcg_mod getGblEnv
+       unless (any (nameIsLocalOrFrom this_mod . unLoc) new_bf) $ do
+         -- Why 'any'? See Note [Orphan COMPLETE pragmas]
+         addErrCtxt (text "In" <+> ppr sig) $ failWithTc orphanError
+
        return (CompleteMatchSig s (L l new_bf) new_mty, emptyFVs)
+  where
+    orphanError :: SDoc
+    orphanError =
+      text "Orphan COMPLETE pragmas not supported" $$
+      text "A COMPLETE pragma must mention at least one data constructor" $$
+      text "or pattern synonym defined in the same module."
+
+{-
+Note [Orphan COMPLETE pragmas]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We define a COMPLETE pragma to be a non-orphan if it includes at least
+one conlike defined in the current module. Why is this sufficient?
+Well if you have a pattern match
+
+  case expr of
+    P1 -> ...
+    P2 -> ...
+    P3 -> ...
+
+any COMPLETE pragma which mentions a conlike other than P1, P2 or P3
+will not be of any use in verifying that the pattern match is
+exhaustive. So as we have certainly read the interface files that
+define P1, P2 and P3, we will have loaded all non-orphan COMPLETE
+pragmas that could be relevant to this pattern match.
+
+For now we simply disallow orphan COMPLETE pragmas, as the added
+complexity of supporting them properly doesn't seem worthwhile.
+-}
 
 ppr_sig_bndrs :: [Located RdrName] -> SDoc
 ppr_sig_bndrs bs = quotes (pprWithCommas ppr bs)
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 205e12a549..3e6e50cb2e 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -13128,11 +13128,14 @@ and ``RightChoice`` is total. ::
 definition matches on all the constructors specified in the pragma then the
 compiler will produce no warning.
 
-``COMPLETE`` pragmas can contain any data constructors or pattern synonyms
-which are in scope. Once defined, they are automatically imported and exported
-from modules. ``COMPLETE`` pragmas should be thought of as asserting a universal
-truth about a set of patterns and as a result, should not be used to silence
-context specific incomplete match warnings.
+``COMPLETE`` pragmas can contain any data constructors or pattern
+synonyms which are in scope, but must mention at least one data
+constructor or pattern synonym defined in the same module.
+``COMPLETE`` pragmas may only appear at the top level of a module.
+Once defined, they are automatically imported and exported from
+modules. ``COMPLETE`` pragmas should be thought of as asserting a
+universal truth about a set of patterns and as a result, should not be
+used to silence context specific incomplete match warnings.
 
 When specifing a ``COMPLETE`` pragma, the result types of all patterns must
 be consistent with each other. This is a sanity check as it would be impossible
diff --git a/testsuite/tests/patsyn/should_compile/T13349b.hs b/testsuite/tests/patsyn/should_compile/T13349b.hs
new file mode 100644
index 0000000000..9d77d5667f
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13349b.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module T13349b where
+
+pattern Nada = Nothing
+
+-- Not orphan because it mentions the locally-defined Nada.
+{-# COMPLETE Just, Nada #-}
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index a5066eaa09..87de2f00bb 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -63,3 +63,4 @@ test('T12615', normal, compile, [''])
 test('T12698', normal, compile, [''])
 test('T12746', normal, multi_compile, ['T12746', [('T12746A.hs', '-c')],'-v0'])
 test('T12968', normal, compile, [''])
+test('T13349b', normal, compile, [''])
diff --git a/testsuite/tests/patsyn/should_fail/T13349.hs b/testsuite/tests/patsyn/should_fail/T13349.hs
new file mode 100644
index 0000000000..45bdc23ace
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T13349.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module T13349 where
+
+{-# COMPLETE False #-}
diff --git a/testsuite/tests/patsyn/should_fail/T13349.stderr b/testsuite/tests/patsyn/should_fail/T13349.stderr
new file mode 100644
index 0000000000..5bf91cbaa4
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T13349.stderr
@@ -0,0 +1,6 @@
+
+T13349.hs:5:1: error:
+    • Orphan COMPLETE pragmas not supported
+      A COMPLETE pragma must mention at least one data constructor
+      or pattern synonym defined in the same module.
+    • In {-# COMPLETE False #-}
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 50a3eea6c1..f674a8b258 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -34,3 +34,4 @@ test('T11667', normal, compile_fail, [''])
 test('T12165', normal, compile_fail, [''])
 test('T12819', normal, compile_fail, [''])
 test('UnliftedPSBind', normal, compile_fail, [''])
+test('T13349', normal, compile_fail, [''])