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

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

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.

Solution

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.