MonadFail desugaring doesn't use GADT exhaustiveness
The mechanism for deciding whether a monad pattern patch is "failable" and requires MonadFail
does not take GADTs into account. In contrast, the warning for regular non-exhaustive pattern matching does consider GADTs.
For example:
{-# LANGUAGE GADTs #-}
module Match where
import Data.Functor.Identity (Identity)
data Value a where
IntValue :: Int -> Value Int
StringValue :: String -> Value String
getInt :: Value Int -> Int
getInt (IntValue x) = x
getIntM :: Value Int -> Identity Int
getIntM v = do
IntValue x <- pure v
return x
With -Wall
, GHC doesn't complain about getInt
being non-exhaustive. However, it doesn't seem to apply the same logic to getIntM
's pattern match:
Match.hs:15:5: error:
• No instance for (Control.Monad.Fail.MonadFail Identity)
arising from a do statement
with the failable pattern ‘IntValue x’
• In a stmt of a 'do' block: IntValue x <- pure v
In the expression:
do IntValue x <- pure v
return x
In an equation for ‘getIntM’:
getIntM v
= do IntValue x <- pure v
return x
|
15 | IntValue x <- pure v
| ^^^^^^^^^^^^^^^^^^^^
It would be helpful if the same logic could be used to prove that this match is not failable and not require a MonadFail
instance.