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