Getting rid of "non-exhaustive patten matches" warning when restricting GADTs with type families

Question

Given the following program:

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B
type family IsA (foo :: Foo) :: Bool

type instance IsA A = True
type instance IsA B = False

data Bar (foo :: Foo) where
    BarA :: (IsA foo ~ True) => Int -> Bar foo
    BarB :: (IsA foo ~ False) => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x

I get this warning from GHC 7.4.2 when using -fwarn-incomplete-patterns for the total function f defined above:

Warning: Pattern match(es) are non-exhaustive
         In a case alternative: Patterns not matched: BarB _

Of course, it makes no sense to even try adding a match for BarB:

Couldn't match type `'False' with `'True'
Inaccessible code in
  a pattern with constructor
    BarB :: forall (foo :: Foo). IsA foo ~ 'False => String -> Bar foo,
  in a case alternative
In the pattern: BarB _
In a case alternative: BarB _ -> undefined
In the expression:
  case bar of {
    BarA x -> x
    BarB _ -> undefined }

Is there a way to convince GHC that f is total? Also, is this a bug of GHC, or just a known limitation; or is there actually a very good reason why there's no way to see that the pattern match in f is complete?

Answer 1

It's annoying, yes. GHC has the assumption that type families (and classes) are open baked deeply into its algorithms all over the place; however, you're writing a type family parameterized by a closed kind. This tension explains the misunderstanding between you and GHC. I think there has been some thought about how to handle closed type classes and families, but it's a tricky area.

In the meantime, you can avoid the openness of type families to convince the totality checker.

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B

data Bar (foo :: Foo) where
    BarA :: Int    -> Bar A -- or BarA :: foo ~ A => Int    -> Bar foo
    BarB :: String -> Bar B -- or BarB :: foo ~ B => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x
-- or f (BarA x) = x

Answer 2

You can always use _ to pattern match to anything as the last condition of the case.

So _ -> undefined instead of BarB _ -> undefined.

This will make case total in its argument.

There is also a library by Neil Mitchell which checks for non exhaustive patterns to prevent runtime failures due to non matching patterns.