Linked Questions

Popular Questions

GADT's failed exhaustiveness checking

Asked by At

Consider the following code:

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1

Even though fun is an exhaustive match, when compiling with -Wall, GHC complains about a missing case. However, if I add another constructor:

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A
  Baz :: Foo B

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl Baz) = 2

Then GHC correctly detects that fun is total.

I am using code similar to this in my work, and would like GHC to raise warnings if I have missed cases, and not raise warnings if I don't. Why is GHC complaining on the first program, and how can I get the first sample to compile without warnings without adding spurious constructors or cases?

Related Questions