Getting rid of "non-exhaustive patten matches" while limiting GADT with family types

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 generic 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 to add 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 the GHC that f is shared? Also, this is a GHC bug or just a known limitation; or is there really a very good reason why there is no way to see that the pattern matching in f complete?

Answer 1

This is annoying, yes. The GHC has the assumption that types (and classes) of the open type are completely baked in their algorithms everywhere; however, you are writing a type family parameterized by a private type. This tension explains the misunderstanding between you and the GHC. I think there is some thought on how to handle private classes and families, but this is a complex area.

In the meantime, you can avoid the openness of type families to convince integrity checking.

 {-# 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 match the pattern to everything as the last condition of the case.

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

This will summarize the case in the argument.

There is also a Neal Mitchell library that checks non-exhaustive patterns to prevent runtime crashes due to inappropriate patterns.