[GHC] #15681: Take {-# COMPLETE #-} pragma into consideration when using MonadFailDesugaring
#15681: Take {-# COMPLETE #-} pragma into consideration when using MonadFailDesugaring -------------------------------------+------------------------------------- Reporter: chshersh | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Keywords: pattern- | Operating System: Unknown/Multiple matching,monadfail,desugaring | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following code: {{{#!hs 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. {{{#!hs {-# 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 | ^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15681 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15681: Take {-# COMPLETE #-} pragma into consideration when using MonadFailDesugaring -------------------------------------+------------------------------------- Reporter: chshersh | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: pattern- | matching,monadfail,desugaring Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Ah. This is because `isIrrefutableHsPat`, which determines is a pattern warrants a `MonadFail` constraint when matched upon in `do`-notation, [http://git.haskell.org/ghc.git/blob/1d7b61f97f9ec3780a1b7b5bf95a880d56224f4f... treats pattern synonyms quite conservatively]: {{{#!hs isIrrefutableHsPat pat = go pat where go (L _ pat) = go1 pat ... go1 (ConPatOut{ pat_con = L _ (PatSynCon _pat) }) = False -- Conservative ... }}} Compare the [http://git.haskell.org/ghc.git/blob/1d7b61f97f9ec3780a1b7b5bf95a880d56224f4f... treatment] for plain old data constructors: {{{#!hs 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 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, [http://git.haskell.org/ghc.git/blob/d00c308633fe7d216d31a1087e00e63532d87d6d... 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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15681#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15681: Take {-# COMPLETE #-} pragma into consideration when using MonadFailDesugaring -------------------------------------+------------------------------------- Reporter: chshersh | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: pattern- | matching,monadfail,desugaring Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15681#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15681: Take {-# COMPLETE #-} pragma into consideration when using MonadFailDesugaring -------------------------------------+------------------------------------- Reporter: chshersh | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: pattern- | matching,monadfail,desugaring,PatternSynonyms,PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: pattern-matching,monadfail,desugaring => pattern- matching,monadfail,desugaring,PatternSynonyms,PatternMatchWarnings * milestone: 8.6.1 => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15681#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15681: Take exhaustiveness checking into consideration when using MonadFailDesugaring -------------------------------------+------------------------------------- Reporter: chshersh | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: pattern- | matching,monadfail,desugaring,PatternSynonyms,PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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: {{{#!hs {-# 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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15681#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15681: Take exhaustiveness checking into consideration when using MonadFailDesugaring -------------------------------------+------------------------------------- Reporter: chshersh | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: pattern- | matching,monadfail,desugaring,PatternSynonyms,PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15681#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC