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