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.

In any case, I'm not experienced enough with type-level programming (GADTS and DataKinds) to offer up any kind of answer, but I'm curious what your actual intention is behind this code. Particularly as, by the Monad laws, having x <- return y in a do block is redundant, as you can simply remove that line replace any x that occurs later in the block with y. — Robin Zigmond
@RobinZigmond Presumably return y is a simplification of some other expression that is known to have type m (Thing 'True). — amalloy
Since using an irrefutable pattern won't warn you when the pattern isn't actually safe (for example if you add another valid constructor later), in my opinion your best bet is to bind a dummy variable (so x <- foo), then pattern match using case ... of ..., perhaps in a let binding . This will at least warn you when you add a constructor if you enable -Wincomplete-patterns. There appears to be an open issue about it (and a related example with pattern synonyms) — Mor A.

chi chi · Accepted Answer · 2020-01-02T22:36:51

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.

Failable match on a seemingly irrefutable GADT pattern

1 Answers