Re: [GHC] #15681: Take exhaustiveness checking into consideration when using MonadFailDesugaring (was: Take {-# COMPLETE #-} pragma into consideration when using MonadFailDesugaring)

18 Dec 2018

      #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