Pattern synonyms in do notation require MonadFail although one-clause pattern match does not emit warnings

Summary

GHC reports a pattern synonym as failable and requires a MonadFail m instance when used in do-notation, but does not emit incomplete patterns warning when used in a single-clause pattern matching.

Steps to reproduce

Consider the following code:

{-# OPTIONS_GHC -Wall -Werror #-}
{-# LANGUAGE  PatternSynonyms
            , GADTs
            , TypeApplications
            , RankNTypes
            , ScopedTypeVariables 
            , ViewPatterns
#-}

-- GADT of possible types
data Type a where
  TInt :: Type Int

class ToType a where
  toType :: Type a

instance ToType Int where
  toType = TInt

instance Show (Type a) where
  show TInt = "TInt"

-- type of expressions
data Expr a where
  EInt :: Expr Int

-- existential adding info of ToType dictionary
data SomeExpr where
  Expr :: ToType a => Expr a -> SomeExpr

-- explicit use of dictionary
typeof :: forall a. ToType a => Expr a -> Type a
typeof _ = toType @a

{-# COMPLETE (:::) #-}
pattern (:::) :: () => ToType a => Expr a -> Type a -> SomeExpr
pattern expr ::: tt <- Expr expr@(typeof -> tt)
  where expr ::: _  = Expr expr

test :: Monad m => m String
test = do
  _e ::: t <- pure $ Expr EInt
  case t of
    TInt -> pure "TInt"

main :: IO ()
main = do
  case Expr EInt of
    _ ::: t -> print t
  test >>= putStrLn

The following error is produced:

Main.hs:42:3: error:
    • Could not deduce (MonadFail m)
        arising from a do statement
        with the failable pattern ‘_e ::: t’
      from the context: Monad m
        bound by the type signature for:
                   test :: forall (m :: * -> *). Monad m => m String
        at Main.hs:40:1-29
      Possible fix:
        add (MonadFail m) to the context of
          the type signature for:
            test :: forall (m :: * -> *). Monad m => m String
    • In a stmt of a 'do' block: _e ::: t <- pure $ Expr EInt
      In the expression:
        do _e ::: t <- pure $ Expr EInt
           case t of { TInt -> pure "TInt" }
      In an equation for ‘test’:
          test
            = do _e ::: t <- pure $ Expr EInt
                 case t of { TInt -> pure "TInt" }
   |
42 |   _e ::: t <- pure $ Expr EInt
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Expected behavior

Compiles correctly and prints "TInt" twice.

Environment

• GHC version used: tried 8.10.{6,7}

Optional:

• Operating System & architecture: Any (tried both on Mac and in online repl)