Incorrect pattern match warning on nested GADTs
{-# Language GADTs #-}
data App f a where
App :: f a -> App f (Maybe a)
data Ty a where
TBool :: Ty Bool
TInt :: Ty Int
data T f a where
C :: T Ty (Maybe Bool)
-- Warning
f :: T f a -> App f a -> ()
f C (App TBool) = ()
-- No warning
g :: T f a -> App f a -> ()
g C (App x) = case x of
TBool -> ()
When compiling, with -Wincomplete-patterns
:
Foo.hs:15:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘f’: Patterns not matched: C (App TInt)
|
15 | f C (App TBool) = ()
| ^^^^^^^^^^^^^^^^^^^^
I'm sorry for such a complicated example, but I wasn't able to reduce it any further than this.
The gist of the problem is that this code gives a pattern matching non-exhaustiveness warning when matching a nested pattern, when pulling out a value then matching on it produces no warning (correctly). It also seems to have to do with using a type constructor (Maybe
) within the constructor definition of App
, as changing it to
data App f a where
App :: f a -> App f a
...
data T f a where
C :: T Ty Bool
does not give a warning, even when App
is modified further to force it to be a proper GADT.
This might be a known limitation of the checker, but given that it works fine when the nesting is removed, I would think it would be more of a bug.
Thanks to Iavor for helping me minimize the test case.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | diatchki |
Operating system | |
Architecture |