#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation -------------------------------------+------------------------------------- Reporter: jkoppel | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In the following code, `fun` contains an exhaustive pattern match, but, when compiling with -Wall, ghc erroneously reports a non-exhaustive pattern match. {{{#!hs 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 #-}`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15305 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler