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

24 Sep 2017

      #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):

 I took a look at this recently. To debug this, I took the original program
 and gave everything some more easily recognizable names:

 {{{#!hs
 {-# Language GADTs #-}
 {-# OPTIONS_GHC -Wall #-}
 module Bug where

 data App f_App a_App where
   MkApp :: f_MkApp a_MkApp -> App f_MkApp (Maybe a_MkApp)

 data Ty a_Ty where
   TBool :: Ty Bool
   TInt  :: Ty Int

 data T f_T a_T where
   C :: T Ty (Maybe Bool)

 -- Warning
 foo :: T f_foo a_foo -> App f_foo a_foo -> ()
 foo C (MkApp TBool) = ()

 -- No warning
 goo :: T f_goo a_goo -> App f_goo a_goo -> ()
 goo C (MkApp x) = case x of
                     TBool -> ()
 }}}

 I then traced the results of the `ConVar` case in the patter-match checker
 to see exactly what sets of constraints were being checked for
 satisfiability. To my horror, the sets were different in `foo` and `goo`!
 In particular, when checking if `TInt` is reachable in `foo`, this set of
 constraints is checked:

 {{{
   ty_state pm_d1Pq_d1Pq :: (a_MkApp_a1NK[sk:2] :: *) ~# (Int :: *)
            pm_d1Ph_d1Ph :: (a_foo_a1NG[sk:2] :: *)
                            ~# (Maybe a_MkApp_d1Pi[sk:2] :: *)
            pm_d1Pc_d1Pc :: (f_foo_a1NF[sk:2] :: (* -> *)) ~# (Ty :: (* ->
 *))
            pm_d1Pd_d1Pd :: (a_foo_a1NG[sk:2] :: *) ~# (Maybe Bool :: *)
   sat_ty True
 }}}

 Here, `ty_state` is the set of constraints, and `sat_ty` is whether they
 are satisfiable. The fact that `sat_ty` is `True` means that the patter-
 match checker concluded that `TInt` is indeed reachable. Contrast this
 with checking if `TInt` is reachable in `goo`:

 {{{
   ty_state pm_d1Py_d1Py :: (a_MkApp_a1NW[sk:2] :: *) ~# (Int :: *)
            cobox_a1NU :: (f_goo_a1NR[sk:2] :: (* -> *)) ~# (Ty :: (* ->
 *))
            cobox_a1NV :: (a_goo_a1NS[sk:2] :: *) ~# (Maybe Bool :: *)
            cobox_a1NX :: (a_goo_a1NS[sk:2] :: *)
                          ~# (Maybe a_MkApp_a1NW[sk:2] :: *)
   sat_ty False
 }}}

 This time, `sat_ty` is `False`, so `TInt` is deemed as unreachable.
 However, these two sets of constraints look awfully similar! But compare
 these two constraints from `foo`'s `ty_state`:

 {{{
 (a_MkApp_a1NK[sk:2] :: *) ~# (Int :: *)
 (a_foo_a1NG[sk:2] :: *)   ~# (Maybe a_MkApp_d1Pi[sk:2] :: *)
 }}}

 With the analogous two constraints from `goo`'s `ty_state`:

 {{{
 (a_MkApp_a1NW[sk:2] :: *) ~# (Int :: *)
 (a_goo_a1NS[sk:2] :: *)   ~# (Maybe a_MkApp_a1NW[sk:2] :: *)
 }}}

 In `goo`'s `ty_state`, the type variable `a_MkApp_a1NW` is used in both
 equalities. But in `foo`'s `ty_state`, we have two separate type
 variables, `a_MkApp_a1NK` and `a_MkApp_d1Pi`! This difference alone is
 enough to account for the oracle's different answers.

 The reason this is happening is because `a_MkApp` is being freshened
 excessively in the
 [http://git.haskell.org/ghc.git/blob/d55961262be1b6bbacea0cd6864346f8822ee99b...
 mkOneConFull] function. In particular,
 [http://git.haskell.org/ghc.git/blob/d55961262be1b6bbacea0cd6864346f8822ee99b...
 this line]:

 {{{#!hs
 (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
 }}}

 That is, `a_MkApp` is an existentially quantified type variable (retrieved
 from the `MkApp` `DataCon`), so it will be cloned to some other name (in
 this case, `a_MkApp_d1Pi`). But a later call to `mkOneConFull` assumes
 that `a_MkApp` was mapped to `a_MkApp_a1NK`, causing the inconsistent
 `ty_state` (and thus this bug).

 In order to resolve this, we need to determine an intelligent way to map
 existentially quantified type variables (retrieved from `DataCon`s) to
 their counterparts in a `PmCon`. But I have no idea how one would
 accomplish that...

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