Patterns in do-notation incorrectly considered inexhaustive

Summary

Consider a simple GADT indexed by a phantom type variable. Within do-notation blocks GHC incorrectly flags pattern matches, exhaustiveness of which depends on these phantom type variables, as inexhaustive.

Steps to reproduce

The following code does not compile:

{-# LANGUAGE GADTs #-}
module Test where

data Initial
data Final

data S a where
  Init :: S Initial
  Fin :: Int -> S Final

f :: Monad m => Int -> S Initial -> m (S Final)
f n Init = return $ Fin (n + 1)

correct :: Monad m => Int -> m Int
correct n = do
  final <- f n Init
  case final of
    Fin n' -> return n'

buggy :: Monad m => Int -> m Int
buggy n = do
  Fin n' <- f n Init
  return n'

While correct is considered fine, buggy does not compile with the following error:

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

I assume this is because GHC cannot convince itself that this pattern matching is exhaustive. However, in correct it can do so. Both these notations should be equivalent.

Expected behavior

Both correct and buggy should compile.

Environment

• GHC version used: 8.10.7

Optional:

• Operating System: Linux
• System Architecture: x86_64