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?
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