Take exhaustiveness checking into consideration when using MonadFailDesugaring

Consider the following code:

import Data.List.NonEmpty (NonEmpty (..))

foo :: Monad m => m (NonEmpty a) -> m a
foo m = do
    (x :| _) <- m
    pure x

It works completely fine on GHC 8.6.1 and doesn't require MonadFail constraint because NonEmpty has only single constructor so there're no other cases in pattern-matching. Howewer, if I rewrite this code using -XPatternSynonyms with {-# COMPLETE #-} pragma, it doesn't work anymore.

{-# LANGUAGE PatternSynonyms #-}

import Data.List.NonEmpty (NonEmpty (..))

newtype Foo a = Foo (NonEmpty a)

pattern (:||) :: a -> [a] -> Foo a
pattern x :|| xs <- Foo (x :| xs)
{-# COMPLETE (:||) #-}

foo :: Monad m => m (Foo a) -> m a
foo m = do
    (x :|| _) <- m
    pure x

And I see the following error:

    • Could not deduce (Control.Monad.Fail.MonadFail m)
        arising from a do statement
        with the failable pattern ‘(x :|| _)’
      from the context: MonadFoo m
        bound by the type signature for:
                   foo :: forall (m :: * -> *) a. MonadFoo m => m (Foo a) -> m a
        at /Users/fenx/haskell/sandbox/Fail.hs:13:1-37
      Possible fix:
        add (Control.Monad.Fail.MonadFail m) to the context of
          the type signature for:
            foo :: forall (m :: * -> *) a. MonadFoo m => m (Foo a) -> m a
    • In a stmt of a 'do' block: (x :|| _) <- m
      In the expression:
        do (x :|| _) <- m
           pure x
      In an equation for ‘foo’:
          foo m
            = do (x :|| _) <- m
                 pure x
   |
15 |     (x :|| _) <- m
   |     ^^^^^^^^^^^^^^

Trac metadata

Trac field	Value
Version	8.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import labels

Ah. This is because isIrrefutableHsPat, which determines is a pattern warrants a MonadFail constraint when matched upon in do-notation, treats pattern synonyms quite conservatively:

isIrrefutableHsPat pat
  = go pat
  where
    go (L _ pat) = go1 pat
    ...
    go1 (ConPatOut{ pat_con = L _ (PatSynCon _pat) })
        = False -- Conservative
    ...

Compare the treatment for plain old data constructors:

    go1 (ConPatOut{ pat_con = L _ (RealDataCon con), pat_args = details })
        =  isJust (tyConSingleDataCon_maybe (dataConTyCon con))
        && all go (hsConPatArgs details)

This essentially says that a plain old data-constructor pattern match is irrefutable if its corresponding data type is inhabited by only one constructor.

Could we do the same for pattern synonyms? We certainly could adapt the code for the RealDataCon case and reuse it for PatSynCon:

diff --git a/compiler/hsSyn/HsPat.hs b/compiler/hsSyn/HsPat.hs
index 6f65487..c23c479 100644
--- a/compiler/hsSyn/HsPat.hs
+++ b/compiler/hsSyn/HsPat.hs
@@ -57,6 +57,7 @@ import Var
 import RdrName ( RdrName )
 import ConLike
 import DataCon
+import PatSyn
 import TyCon
 import Outputable
 import Type
@@ -691,8 +692,13 @@ isIrrefutableHsPat pat
            -- NB: tyConSingleDataCon_maybe, *not* isProductTyCon, because
            -- the latter is false of existentials. See Trac #4439
         && all go (hsConPatArgs details)
-    go1 (ConPatOut{ pat_con = L _ (PatSynCon _pat) })
-        = False -- Conservative
+    go1 (ConPatOut{ pat_con = L _ (PatSynCon pat), pat_args = details })
+        |  (_, _, _, _, _, res_ty) <- patSynSig pat
+        ,  Just tc <- tyConAppTyCon_maybe res_ty
+        =  isJust (tyConSingleDataCon_maybe tc)
+        && all go (hsConPatArgs details)
+        |  otherwise
+        =  False -- Conservative
 
     go1 (LitPat {})         = False
     go1 (NPat {})           = False

While this fixes the particular example in this ticket, it's a bit dodgy. That's because it's determining if a pattern synonym is irrefutable by consulting the plain old data constructors that correspond to the type constructor that heads its return type. This is a bit of an impedance mismatch since exhaustiveness checking for pattern synonyms can only ever really be done in the context of one or more user-defined COMPLETE sets.

It's not clear to me if isIrrefutableHsPat could be changed to take COMPLETE sets into account. The code to look up COMPLETE sets, dsGetCompleteMatches, lives in the DsM monad, while isIrrefutableHsPat is pure. Moreover, isIrrefutableHsPat has call sites that are outside of DsM, so it's unclear to me if we could factor out the monadic parts of dsGetCompleteMatches.

That's because it's determining if a pattern synonym is irrefutable by consulting the plain old data constructors that correspond to the type constructor that heads its return type

Yes, that is pretty dodgy! Eg I think it would give the wrong answer for

pattern P a = (Just a, True)

The outer constructor is (,), but that doesn't mean that P x is irrefutable.

Naively, one might think that the simple thing do to is to behave as if the type synonym was expanded at the use site. But that breaks the abstraction that is part of the purpose of having a pattern synonym. And in fact, in separate compilation, GHC does not record the original definition directly; it just exports teh builder and matcher functions for the pattern synonym.

The right thing must surely be to use the COMPLETE sets, somehow.

changed milestone to %8.8.1

changed title from Take {-# COMPLETE # pragma-} into consideration when using MonadFailDesugaring to Take exhaustiveness checking into consideration when using MonadFailDesugaring

Actually, it turns out this problem affects more than just pattern synonyms. It also affects GADTs, too, as the following //should// compile, but doesn't:

{-# LANGUAGE GADTs #-}
module Bug where

data T a where
  TInt  :: T Int
  TBool :: T Bool

f :: Monad m => m (T Int) -> m ()
f t = do
  TInt <- t
  pure ()

$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:10:3: error:
    • Could not deduce (Control.Monad.Fail.MonadFail m)
        arising from a do statement
        with the failable pattern ‘TInt’
      from the context: Monad m
        bound by the type signature for:
                   f :: forall (m :: * -> *). Monad m => m (T Int) -> m ()
        at Bug.hs:8:1-33
      Possible fix:
        add (Control.Monad.Fail.MonadFail m) to the context of
          the type signature for:
            f :: forall (m :: * -> *). Monad m => m (T Int) -> m ()
    • In a stmt of a 'do' block: TInt <- t
      In the expression:
        do TInt <- t
           pure ()
      In an equation for ‘f’:
          f t
            = do TInt <- t
                 pure ()
   |
10 |   TInt <- t
   |   ^^^^^^^^^

Again, the culprit is the fact that we're trying to determine whether a function needs a MonadFail constraint all the way back in the renamer/typechecker, well before the pattern-match coverage checker runs. It feels like there ought to be a way to only emit MonadFail constraints if the coverage checker deems a do-pattern match to be non-exhaustive, although I don't know how to do that...

The real problem here is that we are trying to infer whether any of the patterns can fail -- if so, generate a MonadFail constraint, but not if not. But pattern-match-coverage is a tricky thing, as the examples demonstrate. And making the generation of a constraint depend on how another set of constraints is solved is pretty thin ice.

I wish it were possible to specify unambiguously whether you want Applicative or Monad or MonadFail. Something like do{Monad} or do{Applicative} or do{MonadFail}. That would be a lot clearer!

changed milestone to %8.10.1

Bumping milestones of low-priority tickets.

marked #16470 (closed) as a duplicate of this issue

mentioned in issue #16470 (closed)

Also worth mentioning is that with rebindable syntax in play, GHC want's the MonadFail constraint even for non-GADT data types. This causes basement-0.0.10 to fail to build with the GHC 8.8 alpha release:

> cabal unpack basement-0.0.10
> cabal build -w ghc-8.8.0.20190424
...
[49 of 84] Compiling Basement.Block.Base ( Basement/Block/Base.hs, /home/amartin/Development/basement-0.0.10/dist-newstyle/build/x86_64-linux/ghc-8.8.0.20190424/basement-0.0.10/build/Basement/Block/Base.o )

Basement/Block/Base.hs:398:9: error:
    Not in scope: ‘fail’
    Perhaps you meant ‘Data.List.tail’ (imported from Data.List)
    |
398 |         arr@(Block arrBa) <- makeTrampoline
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Basement/Block/Base.hs:481:9: error:
    Not in scope: ‘fail’
    Perhaps you meant ‘Data.List.tail’ (imported from Data.List)
    |
481 |         b@(Block ba) <- unsafeFreeze pinnedMb
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Notice that RebindableSyntax is enabled in the default-extensions section in the cabal file, and the data type Block is a plain old ADT.

@andrewthad, I think it's fairer to categorize that as a separate issue due to RebindableSyntax's involvement. See #16618 (closed)/#16628 (closed).

added Pnormal label

So, going all the way back to the Haskell 1.4 report, it had this special definition with regard to determining how the do-syntax should be desugared:

Failure-free patterns are defined as follows:

• All irrefutable patterns are failure-free.
• If C is the only constructor in its type, then C p_1 ... p_n is failure-free when each of the p_i is failure-free.
• If pattern p is failure-free, then the pattern v @ p is failure-free.

Even before pattern synonyms, to modernise this, we would need to add cases for at least view patterns and bang patterns, but those are almost surely going to be analogous to the case for @-patterns:

• If pattern p is failure-free, then the view-pattern v -> p is as well.
• If pattern p is failure-free, then the bang-pattern !p is as well.

Now, how should COMPLETE pragmas fit into this? How about the following:

• If there exists a COMPLETE pragma specifying C as the sole member of a complete set, then C p_1 ... p_n is failure-free when each of the p_i is failure-free.

Can anyone think of a reason this isn't sufficient or might result in problems?

I should mention, I did think of one thing this approach doesn't take care of. There may be cases where one is pattern matching against a GADT for which there is but a single constructor for each indexed type, e.g.

data Example a where
  C :: Example Char
  I :: Example Int
  B :: Example Bool

Then one might wish, when matching a pattern C at type Example Char, to consider C the sole constructor which could have produced such a result, and thus not be failable. That's fair and would seem to warrant using the exhaustiveness checker. I'm uncertain as to whether we'd really want to introduce that level of complication in determining how syntax merely desugars though. In general in the presence of type families occurring in indices, it seems to be quite complicated, even perhaps undecidable, to tell that there is at most one constructor that can produce a result at a given index. Having the desugaring, and thus the type of do-expressions depend on that seems potentially frustrating, but then, if someone is running into this type of scenario, perhaps having the compiler generate dead occurrences of 'fail' is frustrating as well.

mentioned in issue #17501 (closed)

I opened another issue without searching issues first.

This bug trumps an ability of using PatternSynonyms as an abstraction & compatibility mechanism. If I change a constructor name and introduce compatibility pattern some code will stop from compiling, even if I specify COMPLETE.

And thinking of GADTs, I actually wrote code in Cabal which does

(IODataBinary foo, bar) <- doStuff IODataModeBinary

I then refactored it away to just be

(foo, bar) <- doStuff2 IODataModeBinary

as I realized that wrapping in GADT weren't strictly necessary. But surely an error would confused me if I weren't writing IO code, which happens to be MonadFail.

---

data IOData mode where
  IODataBinary :: ByteString -> IOData ByteString
  ...

data IODataMode mode where
  IODataModeBinary :: IODataMode ByteString
  ...

doStuff  :: IODataMode mode -> IO (IOData mode)
doStuff2 :: IODataMode mode -> IO mode

And another addition: with GADTs, adding lazy pattern won't work as a workaround because

    • An existential or GADT data constructor cannot be used
        inside a lazy (~) pattern

that forces to rewrite the code to use explicit eliminator :/

added pattern match warnings label

@Ericson2314 and I have been looking at the possibilities in this space, and we've come up with a bunch of options for what might be reasonable approaches to the problem posed by the examples here. We agree with #15681 (comment 165441) that it’s premature to spend tons of effort so GHC can better guess what you want, before opening up a way to tell it explicitly. Moreover, it’s dubious whether do-syntax and desugaring in general ought to depend on typechecking and other complicated analyses. We aim to teach beginners the desugaring, after all, rather than leave it a spooky black box. Anything which makes syntactic desugaring depend on type analysis also potentially introduces a strange sort of fixed-point, where the code being typechecked may depend on the result of that typechecking, which we obviously want to avoid.

1. Do {-# COMPLETE #-} accumulation in a previous pass before type checking.

   Perhaps could be done in the renamer? Or could be its own pass? (The way in which this data is accumulated right now is broken down by type constructor and not indexed on the data constructors, so we’d probably want to accumulate separately a Set of data constructors that are to be regarded as complete on their own.)

   This doesn’t work for the GADT case though. It would be interesting to allow specifying GADT indices in {-# COMPLETE #-} annotations (for regular constructors too) to state the user’s intent, but this doesn’t solve the problem as we still need the typing information in the bind to know which complete-set to use; once again, do desugaring is type-driven when we wanted to avoid that.

2. Annotate do blocks.

   Basically @simonpj’s comment in #15681 (comment 165441) . This is a bit coarse-grained however. While a Monad do won’t use any fail desugaring, a MonadFail do need not use fail on every bind. We would fall back on the current heuristics in that case. Probably fine in practice though.

3. Annotate individual binds.

   This is the highest-effort solution, but the most “powerful”. Individual binds are annotated with whether the pattern is fallible or not, and then the coverage check can check the assumption later, with far more information to make the call than the heuristic had. This is also good for ApplicativeDo too, when the programmer wants guarantees / explicit control over which binds can erased and applicative statements used downstream instead. This is done by adding a third option in addition to fallible and infallible for the bind: “merely applicative”. Care should be taken here though, given that this is supposed to be syntactic sugar: if the annotations end up being too long, it defeats the purpose of having the syntax at all. By that valuation, it’s likely to be less useful for MonadFail than ApplicativeDo, and so perhaps a good idea that’s just out of scope for this ticket.

4. Allow disabling fail desugar altogether, e.g. with a language extension.

   Who in this thread actually wants to use MonadFail's errors vs. their own structured errors? Our guess is that many “serious” applications will want to use structured errors, rather than Text, let alone String. Put another way, If we didn’t have MonadFail and the fail desugaring, would we want to add it today?

   This is a blunt fix, but perhaps involves less churn than the other options. There are a few decisions such as whether list comprehensions should be affected (probably not), and when to warn on incomplete bind patterns (Extension + -fwarn-incomplete-patterns tor maybe + -fwarn-incomplete-uni-patterns seems appropriate, but perhaps the warning should be implied by the extension), but that’s about it. The refactor seems slightly more involved as our initial investigation indicates that perhaps the coverage checker or other part of later pipeline stage is second-guessing the earlier decisions on whether to fail, but this shouldn’t be too hard to fix.

   [The specific symptom is we put noSyntaxExpr for fail on all patterns, as done for infallible patterns, and then we got weird unsafeCoerces of the string “noSyntaxExpr” rather than a PatternMatchFail exception as expected. So our noSyntaxExpr “fail” implementation was being used anyways.]

   Lastly, -XMonadZeroDesugaring might also be another middle ground that satisfies some need, though not helping with the examples in this thread.

5. Find a way to unfold pattern synonyms before doing the current check for failability as-is (or make the check do this unfolding perhaps).

   If the problem is actually just that pattern synonyms are being regarded as incomplete when they shouldn’t be, perhaps the solution should just be to ensure they’re unfolded more aggressively, rather than providing the user with more ways to annotate them as complete.

   It is true that patterns synonyms are not macros, due to some difference in behavior with bottoms. Is that important here? It’s not immediately clear.

mentioned in merge request !2306 (merged)

changed milestone to %9.0.1

https://github.com/ghc-proposals/ghc-proposals/pull/319 is a proposal for option 4 in Cale's previous comment.

Just ran into this. I really like option 4, as it keeps the syntactic sugar of do straightforward and unsurprising.

I kind of assumed the weird pattern match fail thing in do-blocks had gone away when fail was removed from Monad, but apparently not.

@AshleyYakeley That was exactly my experience when I first read that changelog! https://github.com/ghc-proposals/ghc-proposals/pull/319 is option 4, so take a look.

The pattern match coverage checker would detect the match as complete, but also runs on the typechecked AST, just before desugaring. It seems weird to inform type inference by non-trivial reasoning of the pattern match checker. That would mean that the pattern match checker is suddenly responsible for whether or not a runtime-relevant dictionary is generated. I'll remove the pattern match warnings label.

removed pattern match warnings label

@sgraf812 is that supposed to be a criticism of the status quo or one of the alternatives?

It is impossible for type checking to depend on the exhaustiveness checker, with a single pass of each. The choices for the current semantics are type check twice, and exhaustiveness check twice, and GHC chooses the latter in the heuristic that is currently run prior to type checking.

What I like about option 4 in conjunction with https://github.com/ghc-proposals/ghc-proposals/pull/351 (that's -XNoFallibleDo + -XNoSugaredIncompleteness) is while it is complex whether a program is accepted: the type checker and then exhaustiveness checker needs to accept it, both the dynamic and static semantics of the accepted program are utterly predictable if it is accepted: there's no implicitly-and-conditionally-emitted MonadFail constraint, _ -> fail match arm, or _ -> throw $ PatternMatchFailure .. match arm.

@sgraf812 is that supposed to be a criticism of the status quo or one of the alternatives?

It was intended as neither, or maybe as an impossible alternative (as you also pointed out) and as a consequence, I removed the pattern match warnings label. My attention was drawn to this issue precisely because it was labelled as such and I was doing a sweep. So I removed the label.

changed milestone to %9.2.1

This will not be fixed in time for %9.2.1

changed milestone to %⊥

This issue is affecting me now.

I'm working around #21369 (closed) by providing a pattern synonym:

-- old:
data Entity recrd = 
    Entity { entityKey :: Key record, entityVal :: record }

-- new:
data Entity record =
    Entity' (Key record) record

pattern Entity :: Key rec -> rec -> Entity rec
pattern Entity { entityKey,  entityVal } = Entity' entityKey entityVal

{-# COMPLETE Entity #-}

This works everywhere except in pattern matches out of a do block. This means that replacing a record with an equivalent pattern synonym is a breaking change, instead of a much smaller change.

It's not a huge issue, but it is blocking a potential feature release behind figuring out some other breaking changes.

As Ryan says above

Ah. This is because isIrrefutableHsPat, which determines is a pattern warrants a MonadFail constraint when matched upon in do-notation, treats pattern synonyms quite conservatively

This seems a pity if the programmer is supplying a COMPLETE pragma for the new pattern synonym, with a single constructor in it. Ideally we'd spot this, and add a boolean flag to the PatSyn data type to permanently record that this pattern synonym is irrefutable. (Would need to be serialised into interface files etc of course.)

Currently the typechecker looks at COMPLETE pragmas after finishing with pattern synonyms (in GHC.Tc.Gen.Bind.tcCompleteSigs), but typechecking a pattern synonym could surely sneak a peek at the COMPLETE pragmas.

This would all be a bit ad-hoc (recording just irrefutability in a pattern synonym) but I can see the force of the motivations above.

I can advise, if anyone wants to have a go.

I'd be interested in attempting this. Sounds relatively straight forward:

• Add a Bool to a pattern synonym representation type, intially False
• If the pattern appears in a COMPLETE pragma, mark it as True
• When desugaring MonadFail, check the PatSyn field. If it's COMPLETE, then do not emit a MonadFail constraint

If this overall design would be accepted then I can try to implement soon.

Thanks!

That sounds about right, yes. Thanks!

added PatternSynonyms label

This would all be a bit ad-hoc (recording just irrefutability in a pattern synonym) but I can see the force of the motivations above.

I do believe there are non ad-hoc solutions to this also :).

If someone has a burst of creativity to find a good surface syntax for https://github.com/ghc-proposals/ghc-proposals/discussions/423, I think I can write a proposal for that, and resurrect https://github.com/ghc-proposals/ghc-proposals/pull/351 and https://github.com/ghc-proposals/ghc-proposals/pull/319 in a way that addresses prior feedback and has a nice unified design across all 3 proposals.

(Maybe even write a "modern completeness" mega proposal analogous to https://github.com/ghc-proposals/ghc-proposals/pull/448)

mentioned in merge request !8013 (closed)

mentioned in merge request !8228 (closed)

mentioned in issue #22004 (closed)

marked this issue as related to #22004 (closed)

marked #22004 (closed) as a duplicate of this issue

marked #23458 (closed) as a duplicate of this issue

marked this issue as related to #23458 (closed)

I've got a fix in the works for pattern synonyms with COMPLETE pragmas that I'll be presenting at the GHC contributor workshop next week. cc-ing @trac-parsonsmatt who had a WIP MR (!8013 (closed)).

Wonderful, thank you! I haven't had time to put any effort towards that MR, so happy to close in favor of your solution

MR is !10565 (closed).

mentioned in merge request !10565 (closed)

I don't understand the technical issues involved, and this may not be relevant anymore, but: I use pattern synonyms within a large monorepo primarily in order to preserve an interface after a refactoring, in order to make code review easier and so on. I wouldn't be interested in workarounds that involved twiddling things at the usage sites, or altering fail behavior, etc.

In that universe I would just simply give up and not use pattern synonyms, make the rote alterations in 20 places.

I encountered this with QuickCheck and a COMPLETE pattern;

-- | SEE: http://stackoverflow.com/questions/33325370/why-cant-i-pattern-match-against-a-ratio-in-haskell
pattern (:%) :: forall a. a -> a -> Ratio a
pattern n :% d <- (\x -> (numerator x, denominator x) -> (n, d))
{-# COMPLETE (:%) #-}

    • No instance for (MonadFail Gen)
        arising from a do statement
        with the failable pattern ‘(Normal (n :% d))’
    • In a stmt of a 'do' block: (Normal (n :% d)) <- arbitrary

Until this is fixed, a workaround is to split it into two steps. Here's what I did when I encountered the above problem to get around it;

-        (Normal (n :% d)) <- arbitrary
+        normal <- arbitrary
+        let (Normal (n :% d)) = normal

For the example of this issue, the change working around the problem would be;

import Data.List.NonEmpty (NonEmpty (..))

foo :: Monad m => m (NonEmpty a) -> m a
foo m = do
-   (x :| _) <- m
+   xs <- m
+   let (x :| _) = xs
    pure x

I just ran into this dealing with the whole Solo -> MkSolo mess. Yikes!

Similarly, just hit this when introducing an error-checking smart constructor. https://github.com/IntersectMBO/lsm-tree/pull/141#pullrequestreview-1960891837

No strong opinion on which solution, just that there be one

I've updated !10565 (closed) (which fixes the issues involving pattern synonyms and COMPLETE pragmas described in this ticket), and hope to land it soon.

mentioned in commit 6afdc244

closed with commit 572fbc44

mentioned in issue #25085

mentioned in commit 572fbc44