diff options
| -rw-r--r-- | compiler/GHC/HsToCore/Errors/Ppr.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Errors.hs | 31 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 2 | ||||
| -rw-r--r-- | docs/users_guide/exts/defer_type_errors.rst | 5 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/LinearPolyType.stderr | 4 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/T20083.hs | 9 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/T20083.stderr | 18 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/all.T | 1 |
8 files changed, 67 insertions, 5 deletions
diff --git a/compiler/GHC/HsToCore/Errors/Ppr.hs b/compiler/GHC/HsToCore/Errors/Ppr.hs index c5f3aca1ec..eba5c12e74 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 a504fd44ea..dc95a6a81d 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 b60be4557d..6f2a871709 100644 --- a/docs/users_guide/exts/defer_type_errors.rst +++ b/docs/users_guide/exts/defer_type_errors.rst @@ -125,3 +125,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 bf0f392192..89363cba85 100644 --- a/testsuite/tests/linear/should_fail/all.T +++ b/testsuite/tests/linear/should_fail/all.T @@ -38,3 +38,4 @@ test('LinearTHFail3', 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']) |