Opened 14 months ago
Last modified 11 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 14 months ago by
comment:2 Changed 14 months ago by
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 14 months ago by
Keywords: | PatternSynonyms PatternMatchWarnings added |
---|---|
Milestone: | 8.6.1 → 8.8.1 |
comment:4 Changed 11 months ago by
Summary: | Take {-# COMPLETE #-} pragma into consideration when using MonadFailDesugaring → 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...
comment:5 Changed 11 months ago by
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 11 months ago by
Milestone: | 8.8.1 → 8.10.1 |
---|
Bumping milestones of low-priority tickets.
Ah. This is because
isIrrefutableHsPat
, which determines is a pattern warrants aMonadFail
constraint when matched upon indo
-notation, treats pattern synonyms quite conservatively:Compare the treatment for plain old data constructors:
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 forPatSynCon
:compiler/hsSyn/HsPat.hs
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 takeCOMPLETE
sets into account. The code to look upCOMPLETE
sets, dsGetCompleteMatches, lives in theDsM
monad, whileisIrrefutableHsPat
is pure. Moreover,isIrrefutableHsPat
has call sites that are outside ofDsM
, so it's unclear to me if we could factor out the monadic parts ofdsGetCompleteMatches
.