Opened 2 years ago

Closed 19 months ago

Last modified 19 months ago

#14098 closed bug (fixed)

Incorrect pattern match warning on nested GADTs

Reported by: jmgrosen Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.2.1
Keywords: PatternMatchWarnings Cc: diatchki, RyanGlScott, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case: T11984, T14098
Blocked By: Blocking:
Related Tickets: #11984 Differential Rev(s): Phab:D4434
Wiki Page:

Description

{-# 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.

Change History (10)

comment:1 Changed 2 years ago 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.

comment:2 Changed 2 years ago by RyanGlScott

Cc: RyanGlScott added

comment:3 Changed 2 years ago 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:

{-# 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 mkOneConFull function. In particular, this line:

(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 DataCons) to their counterparts in a PmCon. But I have no idea how one would accomplish that...

comment:4 Changed 2 years ago by Iceland_jack

Cc: Iceland_jack added

comment:5 Changed 19 months ago 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:

f :: T f a -> App f a -> ()
f C (App TBool) = ...

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

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:

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.

comment:6 Changed 19 months ago by RyanGlScott

To hammer home the fact that guards are the culprit, note that this problem also erroneously generates a warning:

{-# Language GADTs #-}
{-# OPTIONS_GHC -Wall #-}

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)

f :: T f a -> App f a -> ()
f C (App x)
  | TBool <- x = ()

comment:7 Changed 19 months ago by RyanGlScott

Differential Rev(s): Phab:D4434
Status: newpatch

comment:8 Changed 19 months ago by Ben Gamari <ben@…>

In a2d03c6/ghc:

Fix the coverage checker's treatment of existential tyvars

Previously, the pattern-match coverage checker was far too
eager to freshen the names of existentially quantified type
variables, which led to incorrect sets of type constraints that
misled GHC into thinking that certain programs that involve nested
GADT pattern matches were non-exhaustive (when in fact they were).
Now, we generate extra equality constraints in the ConCon case of
the coverage algorithm to ensure that these fresh tyvars align
with existing existential tyvars. See
`Note [Coverage checking and existential tyvars]` for the full story.

Test Plan: make test TEST="T11984 T14098"

Reviewers: gkaracha, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie, carter

GHC Trac Issues: #11984, #14098

Differential Revision: https://phabricator.haskell.org/D4434

comment:9 Changed 19 months ago by bgamari

Milestone: 8.6.1
Resolution: fixed
Status: patchclosed

comment:10 Changed 19 months ago by bgamari

Test Case: T11984, T14098
Note: See TracTickets for help on using tickets.