Phantom type makes pattern matching irrefutable, but that seemingly does not work inside do notation

Question

Please look at the code. I believe using phantom type makes the pattern matching irrefutable so there is no need in MonadFail instance.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wincomplete-uni-patterns #-}

data Type = I | S

data T t where
    TI :: Int -> T 'I
    TS :: String -> T 'S

ti :: T 'I
ti = TI 42

test :: Monad m => m Int 
test = do
    (TI v) <- return ti
    return v

But I am getting this error:

    • Could not deduce (MonadFail m)
        arising from a do statement
        with the failable pattern ‘(TI v)’

What's wrong with this approach?

I checked this with ghc 9.0.2 and 8.10.4.

By the way, matching it in let does not produce any warning even in the presence of -Wincomplete-uni-patterns option.

Answer 1

There's nothing wrong with your approach; it should work as you expect it to. It's a known bug in GHC that it currently doesn't: MonadFail exhaustivity checking does not take into account type information (#25085)

Until they fix it, you can work around it by writing ~(TI v) <- return ti instead of (TI v) <- return ti.