[GHC] #14098: Incorrect pattern match warning on nested GADTs

[GHC]

#14098: Incorrect pattern match warning on nested GADTs
-------------------------------------+-------------------------------------
        Reporter:  jmgrosen          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  error/warning at compile-time      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11984            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 OK. I now have a better understand of what is going wrong. It all has to
 do with coercion patterns. In source syntax, we have:

 {{{#!hs
 f :: T f a -> App f a -> ()
 f C (App TBool) = ...
 }}}

 When desugared to Core, this turns into (roughly):

 {{{#!hs
 f :: T f a -> App f a -> ()
 f @f @a (C co1 co2) (App @a1 co3 (TBool |> co1)) = ()
 }}}

 Where `a1` is an existentially quantified type variable bound by `App`.
 When checking for pattern-match coverage, it turns out we desugar the
 coercion pattern `TBool |> co1` into a guard! So the clause ends up
 looking something like:

 {{{#!hs
 f C (App pmvar123)
   | TBool <- pmvar123 |> co1
   = ()
 }}}

 Note that the type of `pmvar123` is `f a1`—this will be important later.

 Now, we proceed with coverage-checking the guard as usual. When we come to
 the ConVar case for `App`, we end up creating a fresh variable `a2` to
 represent its existentially quantified type variable, as described in the
 GADTs Meet Their Match paper.

 However, when we check the guard, it's going to use `a1` instead of `a2`,
 since that's the type variable mentioned in the type of `pmvar123`, not
 `a2`! As a result, we generate some equality constraints mentioning `a1`
 and some mentioning `a2`, but they end up being disjoint in the end (that
 is, we never generate an `a1 ~ a2`), so GHC believes the overall
 constraint set is satisfiable.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14098#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler