Opened 12 months ago

Last modified 9 months ago

#15681 new bug

Take exhaustiveness checking into consideration when using MonadFailDesugaring

Reported by: chshersh Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.6.1
Keywords: pattern-matching, monadfail, desugaring, PatternSynonyms, PatternMatchWarnings Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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
   |     ^^^^^^^^^^^^^^

Change History (6)

comment:1 Changed 12 months ago by RyanGlScott

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:

  • compiler/hsSyn/HsPat.hs

    diff --git a/compiler/hsSyn/HsPat.hs b/compiler/hsSyn/HsPat.hs
    index 6f65487..c23c479 100644
    a b import Var 
    5757import RdrName ( RdrName )
    5858import ConLike
    5959import DataCon
     60import PatSyn
    6061import TyCon
    6162import Outputable
    6263import Type
    isIrrefutableHsPat pat 
    691692           -- NB: tyConSingleDataCon_maybe, *not* isProductTyCon, because
    692693           -- the latter is false of existentials. See Trac #4439
    693694        && all go (hsConPatArgs details)
    694     go1 (ConPatOut{ pat_con = L _ (PatSynCon _pat) })
    695         = False -- Conservative
     695    go1 (ConPatOut{ pat_con = L _ (PatSynCon pat), pat_args = details })
     696        |  (_, _, _, _, _, res_ty) <- patSynSig pat
     697        ,  Just tc <- tyConAppTyCon_maybe res_ty
     698        =  isJust (tyConSingleDataCon_maybe tc)
     699        && all go (hsConPatArgs details)
     700        |  otherwise
     701        =  False -- Conservative
    696702
    697703    go1 (LitPat {})         = False
    698704    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.

comment:2 Changed 12 months ago by simonpj

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.

comment:3 Changed 12 months ago by RyanGlScott

Keywords: PatternSynonyms PatternMatchWarnings added
Milestone: 8.6.18.8.1

comment:4 Changed 9 months ago by RyanGlScott

Summary: Take {-# COMPLETE #-} pragma into consideration when using MonadFailDesugaringTake 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...

comment:5 Changed 9 months ago by simonpj

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!

comment:6 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.