#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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by jmgrosen): D'oh. Right after posting this, I found #11984, of which this looks like a duplicate, though this one is perhaps slightly simpler. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14098#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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

#14098: Incorrect pattern match warning on nested GADTs -------------------------------------+------------------------------------- Reporter: jmgrosen | Owner: (none) Type: bug | Status: patch 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): Phab:D4434 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D4434 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14098#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14098: Incorrect pattern match warning on nested GADTs -------------------------------------+------------------------------------- Reporter: jmgrosen | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.1 Resolution: fixed | 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): Phab:D4434 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * resolution: => fixed * milestone: => 8.6.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14098#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler