Failable match on a seemingly irrefutable GADT pattern

Question

Continuing my crusade against MonadFail being a constraint in my monad, I'm now faced with the following:

data Thing :: Bool -> Type where
  TrueThing :: Thing 'True
  FalseThing :: Thing 'False

myFunc :: Monad m => m ()
myFunc = do
  TrueThing <- return TrueThing
  return ()

Which won't compile because, you guessed it:

• Could not deduce (MonadFail m)
    arising from a do statement
    with the failable pattern ‘TrueThing’

Indeed, if I read whatever¹ documentation I could find on the subject, it's not quite clear how the matching should work on a GADT. I would obviously have thought this case fell under the “matches unconditionally” umbrella. But I'll concede it doesn't qualify as a “single constructor data type”². Even though avoiding that sort of ambiguity was the point of using a GADT in the first place.

Sure ~lazyPattern works, but that's just band-aid. I've desugared the match:

myFunc' :: Monad m => m ()
myFunc' = let f :: _
              f TrueThing = return ()
          in return TrueThing >>= f

And now, while the error message isn't that explicit (Couldn't match expected type ‘p’ with actual type ‘m0 ()), the type wildcard is more telling:

• Found type wildcard ‘_’ standing for ‘Thing a -> p’

…and guides me towards a “solution”:

myFunc' :: forall m. Monad m => m ()
myFunc' = let f :: Thing 'True -> m ()
              f TrueThing = return ()
          in return TrueThing >>= f

Well, that works. Can I sugar it back? f doesn't occur in the initial expression, but there are two spots I can annotate with a type: the monadic expression and the pattern. I've tried both separately as well as together, and it's all “could not deduce MonadFail”.

I suppose my expectations were too high, but I'd like to understand why. Is it some type inference limitation? A GADT one? Am I not using the right machinery in the first place? How could this pattern fail at all?

---

(1) It's hard to find an authority on the subject. The GHC manual mentions MonadFail, but links to the HaskellPrime wiki, which seems to be an older revision of the same page on the Haskell wiki

(2) Replacing Bool with () works too. But that's too much simplification with regard to my actual problem.

Answer 1

This is probably not going to be a fully satisfactory answer, but I'd like to share my findings anyway.

I started from a case where pattern matching failure is indeed possible, modifying your GADT to add another constructor for 'True. Then I added a MonadFail context just to make ti compile, and see later on where it was used.

{-# LANGUAGE GADTs , DataKinds, KindSignatures #-}
{-# OPTIONS -Wall #-}

import Data.Kind
import Control.Monad.Fail

data Thing :: Bool -> Type where
  TrueThing :: Thing 'True
  FalseThing :: Thing 'False
  TrueThing2 :: Thing 'True

myFunc :: (Monad m, MonadFail m) => m ()
myFunc = do
  TrueThing <- return TrueThing
  return ()

The above code results in the following Core:

myFunc
  = \ (@ (m_a1mR :: * -> *))
      _ [Occ=Dead]
      ($dMonadFail_a1mU :: MonadFail m_a1mR) ->
      let {
        $dMonad1_a1nj :: Monad m_a1mR
        [LclId]
        $dMonad1_a1nj
          = Control.Monad.Fail.$p1MonadFail @ m_a1mR $dMonadFail_a1mU } in
      >>=
        @ m_a1mR
        $dMonad1_a1nj
        @ (Thing 'True)
        @ ()
        (return
           @ m_a1mR $dMonad1_a1nj @ (Thing 'True) GADTmonad.$WTrueThing)
        (\ (ds_d1ol :: Thing 'True) ->
           case ds_d1ol of {
             TrueThing co_a1n5 ->
               return @ m_a1mR $dMonad1_a1nj @ () GHC.Tuple.();
             TrueThing2 ipv_s1ph ->
               Control.Monad.Fail.fail
                 @ m_a1mR
                 $dMonadFail_a1mU
                 @ ()
                 (GHC.CString.unpackCString#
                    "Pattern match failure in do expression at GADTmonad.hs:15:3-11"#)
           })

Above, we can see that:

• The Monad dictionary which is being passed to myFunc is discarded! Instead the dictionary is recovered from the MonadFail dictionary (which includes the Monad one). I have no idea about why GHC prefers that one.
• The MonadFail dictionary is used to handle the TrueThing2 case in the very last match. This was expected.

Now, if we remove the TrueThing2 constructor, we get the following Core:

myFunc
  = \ (@ (m_a1mJ :: * -> *))
      _ [Occ=Dead]
      ($dMonadFail_a1mM :: MonadFail m_a1mJ) ->
      let {
        $dMonad1_a1nb :: Monad m_a1mJ
        [LclId]
        $dMonad1_a1nb
          = Control.Monad.Fail.$p1MonadFail @ m_a1mJ $dMonadFail_a1mM } in
      >>=
        @ m_a1mJ
        $dMonad1_a1nb
        @ (Thing 'True)
        @ ()
        (return
           @ m_a1mJ $dMonad1_a1nb @ (Thing 'True) GADTmonad.$WTrueThing)
        (\ (ds_d1od :: Thing 'True) ->
           case ds_d1od of { TrueThing co_a1mX ->
           return @ m_a1mJ $dMonad1_a1nb @ () GHC.Tuple.()
           })

Now the TrueThing2 case disappeared, and that removed the use of the fail function from MonadFail.

However, for some reason, the Monad dictionary is still being obtained through the MonadFail dictionary, even if that could now be avoided.

My guess is that this is a current limitation of GHC. In principle it could desugar, generate Core, and then observe that MonadFail is not needed. However, I think type checking is performed before such steps happen, and at that point GHC prepares for the worst case, where MonadFail could still be needed later on. I don't know how much work should be added to make it smarter during type checking and avoid requiring MonadFail unless it is really needed.