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