Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation
In the following code, fun
contains an exhaustive pattern match, but, when compiling with -Wall, ghc erroneously reports a non-exhaustive pattern match.
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
This report came from https://stackoverflow.com/questions/16225281/gadts-failed-exhaustiveness-checking . Without strictness annotations, this is indeed a failed exhaustive check, due to bottom. I spoke to Richard Eisenberg at PLDI a few days ago, and he informed me that, if this warning did not disappear with strictness annotations, it was a bug. I added strictness annotations, and it did not disappear. I've tried all combinations of using strictness annotations and/or running with {-# LANGUAGE Strict #-}
.
Trac metadata
Trac field | Value |
---|---|
Version | 8.4.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |