Disable -fdefer-type-errors for linear types (#20083)wip/T20083

8 files changed, 67 insertions, 5 deletions

diff --git a/compiler/GHC/HsToCore/Errors/Ppr.hs b/compiler/GHC/HsToCore/Errors/Ppr.hs
index c8bda5562b..0c440c4936 100644
--- a/compiler/GHC/HsToCore/Errors/Ppr.hs
+++ b/compiler/GHC/HsToCore/Errors/Ppr.hs
@@ -88,7 +88,7 @@ instance Diagnostic DsMessage where
       -> mkSimpleDecorated $
           text "Ignoring useless SPECIALISE pragma for NOINLINE function:" <+> quotes (ppr poly_id)
     DsMultiplicityCoercionsNotSupported
-      -> mkSimpleDecorated $ text "Multiplicity coercions are currently not supported (see GHC #19517)"
+      -> mkSimpleDecorated $ text "GHC bug #19517: GHC currently does not support programs using GADTs or type families to witness equality of multiplicities"
     DsOrphanRule rule
       -> mkSimpleDecorated $ text "Orphan rule:" <+> ppr rule
     DsRuleLhsTooComplicated orig_lhs lhs2
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 766b88408d..bc2adbb298 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -926,10 +926,18 @@ suppressGroup mk_err ctxt cts
       ; traceTc "Suppressing errors for" (ppr cts)
       ; mapM_ (addDeferredBinding ctxt err) cts }
 
+-- See Note [No deferring for multiplicity errors]
+nonDeferrableOrigin :: CtOrigin -> Bool
+nonDeferrableOrigin NonLinearPatternOrigin = True
+nonDeferrableOrigin (UsageEnvironmentOf _) = True
+nonDeferrableOrigin _                      = False
+
 maybeReportError :: ReportErrCtxt -> Ct -> Report -> TcM ()
 maybeReportError ctxt ct report
   = unless (cec_suppress ctxt) $ -- Some worse error has occurred, so suppress this diagnostic
-    do let reason = cec_defer_type_errors ctxt
+    do let reason | nonDeferrableOrigin (ctOrigin ct) = ErrorWithoutFlag
+                  | otherwise                         = cec_defer_type_errors ctxt
+                  -- See Note [No deferring for multiplicity errors]
        msg <- mkErrorReport reason ctxt (ctLocEnv (ctLoc ct)) report
        reportDiagnostic msg
 
@@ -1087,6 +1095,27 @@ is perhaps a bit *over*-consistent!
 
 With #10283, you can now opt out of deferred type error warnings.
 
+Note [No deferring for multiplicity errors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As explained in Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify,
+linear types do not support casts and any nontrivial coercion will raise
+an error during desugaring.
+
+This means that even if we defer a multiplicity mismatch during typechecking,
+the desugarer will refuse to compile anyway. Worse: the error raised
+by the desugarer would shadow the type mismatch warnings (#20083).
+As a solution, we refuse to defer submultiplicity constraints. Test: T20083.
+
+To determine whether a constraint arose from a submultiplicity check, we
+look at the CtOrigin. All calls to tcSubMult use one of two origins,
+UsageEnvironmentOf and NonLinearPatternOrigin. Those origins are not
+used outside of linear types.
+
+In the future, we should compile 'WpMultCoercion' to a runtime error with
+-fdefer-type-errors, but the current implementation does not always
+place the wrapper in the right place and the resulting program can fail Lint.
+This plan is tracked in #20083.
+
 Note [Deferred errors for coercion holes]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we need to defer a type error where the destination for the evidence
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 4b12595f72..7b8920f555 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -792,7 +792,7 @@ solved to check whether they are trivial or not. Plus there is precedent for
 type errors during desuraging (such as the representation polymorphism
 restriction). An alternative would be to have a kind of constraint which can
 only produce trivial evidence, then this check would happen in the constraint
-solver.
+solver (#18756).
 -}
 
 tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
diff --git a/docs/users_guide/exts/defer_type_errors.rst b/docs/users_guide/exts/defer_type_errors.rst
index 1c644c5eda..818287bfdc 100644
--- a/docs/users_guide/exts/defer_type_errors.rst
+++ b/docs/users_guide/exts/defer_type_errors.rst
@@ -126,3 +126,8 @@ In a few cases, equality constraints cannot be deferred.  Specifically:
 - Kind errors in a ``default`` declaration.  e.g. ::
 
     default( Double, Int Int )
+
+- Errors involving linear types (c.f. :ghc-ticket:`20083`). e.g. ::
+
+    f :: a %1 -> a
+    f _  = ()
diff --git a/testsuite/tests/linear/should_fail/LinearPolyType.stderr b/testsuite/tests/linear/should_fail/LinearPolyType.stderr
index c2d8b7d452..22d8013aed 100644
--- a/testsuite/tests/linear/should_fail/LinearPolyType.stderr
+++ b/testsuite/tests/linear/should_fail/LinearPolyType.stderr
@@ -1,6 +1,6 @@
 
 LinearPolyType.hs:15:1: error:
-    Multiplicity coercions are currently not supported (see GHC #19517)
+    GHC bug #19517: GHC currently does not support programs using GADTs or type families to witness equality of multiplicities
 
 LinearPolyType.hs:15:1: error:
-    Multiplicity coercions are currently not supported (see GHC #19517)
+    GHC bug #19517: GHC currently does not support programs using GADTs or type families to witness equality of multiplicities
diff --git a/testsuite/tests/linear/should_fail/T20083.hs b/testsuite/tests/linear/should_fail/T20083.hs
new file mode 100644
index 0000000000..21a0ca98b4
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/T20083.hs
@@ -0,0 +1,9 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+
+module T20083 where
+
+ap :: (a -> b) -> a %m -> b
+ap f x = f x
+
+ap2 :: a %1-> ()
+ap2 _ = ()
diff --git a/testsuite/tests/linear/should_fail/T20083.stderr b/testsuite/tests/linear/should_fail/T20083.stderr
new file mode 100644
index 0000000000..5799d7c86d
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/T20083.stderr
@@ -0,0 +1,18 @@
+
+T20083.hs:6:6: error:
+    • Couldn't match type ‘m’ with ‘'Many’
+        arising from multiplicity of ‘x’
+      ‘m’ is a rigid type variable bound by
+        the type signature for:
+          ap :: forall a b (m :: GHC.Types.Multiplicity).
+                (a -> b) -> a %m -> b
+        at T20083.hs:5:1-27
+    • In an equation for ‘ap’: ap f x = f x
+    • Relevant bindings include
+        ap :: (a -> b) -> a %m -> b (bound at T20083.hs:6:1)
+
+T20083.hs:9:5: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from a non-linear pattern
+    • In the pattern: _
+      In an equation for ‘ap2’: ap2 _ = ()
diff --git a/testsuite/tests/linear/should_fail/all.T b/testsuite/tests/linear/should_fail/all.T
index a831011cef..b5e14ca07f 100644
--- a/testsuite/tests/linear/should_fail/all.T
+++ b/testsuite/tests/linear/should_fail/all.T
@@ -35,3 +35,4 @@ test('LinearTHFail', normal, compile_fail, [''])
 test('T18888', normal, compile_fail, [''])
 test('T18888_datakinds', normal, compile_fail, [''])
 test('T19120', normal, compile_fail, [''])
+test('T20083', normal, compile_fail, ['-XLinearTypes'])