MonadFail exhaustivity checking does not take into account type information

The following example is the program from #15681 (comment 165436). In this program, the do block continues to (incorrectly) infer a MonadFail constraint (even after 572fbc44).

{-# 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 ()

Fixing this seems quite difficult at the moment. See e.g. this comment by Simon Peyton Jones:

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!

Note that the logic implemented in 572fbc44 to handle matching on a pattern synonym which is the sole member of a COMPLETE pragma does not take into consideration COMPLETE pragmas with a result TyCon, for the same reason: type information is not always available.

Another tricky example is to do with long-distance information (slightly contrived example, but it generalises to more meaningful programs):

{-# LANGUAGE GADTs #-}
module Bug2 where

data S = S1 | S2

f :: Monad m => S -> m ()
f s =
  case s of
    S1 -> pure ()
    _ -> do
      S2 <- s
      pure ()

This similarly infers a MonadFail constraint which the user might not want.