Opened 3 years ago

Closed 19 months ago

#11984 closed bug (fixed)

Pattern match incompleteness / inaccessibility discrepancy

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.1
Keywords: PatternMatchWarnings Cc: gkaracha, RyanGlScott, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: T11984
Blocked By: Blocking:
Related Tickets: #14098 Differential Rev(s): Phab:D4434
Wiki Page:

Description (last modified by bgamari)

Consider this module:

{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}

module Bug where

data family Sing (a :: k)

data Schema = Sch [Bool]

data instance Sing (x :: Schema) where
  SSch :: Sing x -> Sing ('Sch x)

data instance Sing (x :: [k]) where
  SNil :: Sing '[]
  SCons :: Sing a -> Sing b -> Sing (a ': b)

data G a where
  GCons :: G ('Sch (a ': b))

eval :: G s -> Sing s -> ()
eval GCons s =
        case s of
          -- SSch SNil -> undefined
          SSch (SCons _ _) -> undefined

Upon seeing this, GHC says

Bug.hs:21:9: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: (SSch SNil)

So I uncomment the second-to-last line, inducing GHC to say

Bug.hs:22:16: error:
    • Couldn't match type ‘a : b’ with ‘'[]’
      Inaccessible code in
        a pattern with constructor: SNil :: forall k. Sing '[],
        in a case alternative
    • In the pattern: SNil
      In the pattern: SSch SNil
      In a case alternative: SSch SNil -> undefined

Thankfully, this pattern is much rarer than it once was, but it's a bit sad that it's still possible.

Change History (14)

comment:1 Changed 3 years ago by simonpj

Cc: gkaracha added
Keywords: PatternMatchWarnings added

This looks like a plain bug (in the exhaustiveness checker) to me. George?

comment:2 in reply to:  1 Changed 3 years ago by gkaracha

Replying to simonpj:

This looks like a plain bug (in the exhaustiveness checker) to me. George?

Ah, yes, indeed. The checker by design keeps the exhaustiveness and the redundancy checker synced, as well as both of them with the type checker. This is definitely a bug (or omission when we propagate type constraints for nested matches' checking?) of the implementation only. I will look into it :-)

comment:3 Changed 2 years ago by RyanGlScott

Cc: RyanGlScott added

See #14098 for a similar example.

comment:4 Changed 2 years ago by simonpj

George, any progress?

Everyone: George is now doing many other things. Would anyone like to step up to looking after the patterm-match overlap checker? It's a thing of some beauty but needs love.

comment:5 Changed 2 years ago by RyanGlScott

I often find myself working in Check and Match, and I'd certainly like to address some of these pattern match coverage check-oriented tickets some day. But I often find myself handicapped by my unfamiliarity with the structure of the code in that part of GHC, so I think that in order to productively maintain it, I'd need someone to give a tour of that section of the codebase, highlighting what each thing does. (I've read "GADTs meet their match", but that doesn't really come with a field guide as to how each concept translates to actual GHC code.)

comment:6 Changed 2 years ago by bgamari

Ryan, have you seen PatternMatchCheckImplementation?

comment:7 Changed 2 years ago by RyanGlScott

In case you're reading this ticket and looking for a workaround, you can add an extra case to make it compile without warnings:

{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}

module Bug where

data family Sing (a :: k)

data Schema = Sch [Bool]

data instance Sing (x :: Schema) where
  SSch :: Sing x -> Sing ('Sch x)

data instance Sing (x :: [k]) where
  SNil :: Sing '[]
  SCons :: Sing a -> Sing b -> Sing (a ': b)

data G a where
  GCons :: G ('Sch (a ': b))

eval :: G s -> Sing s -> ()
eval GCons s =
        case s of
          SSch y -> case y of
                      SCons _ _ -> undefined

comment:8 Changed 2 years ago by simonpj

I'd need someone to give a tour of that section of the codebase, highlighting what each thing does

I volunteer to do this. Yell when you'd like a Skype call.

comment:9 Changed 2 years ago by RyanGlScott

See https://ghc.haskell.org/trac/ghc/ticket/14098#comment:3 for a diagnosis of the issue occurring here.

comment:10 Changed 2 years ago by Iceland_jack

Cc: Iceland_jack added

comment:11 Changed 19 months ago by RyanGlScott

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

comment:12 Changed 19 months ago by simonpj

Thanks Ryan. You've nailed the problem.

I think your fix will work. And your long Note is great.

But the particular solution smells wrong.

I think the real bug is in the "ConCon" case of pmcheckHd, which looks like this

pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_args = args1})) ps guards
          (va@(PmCon {pm_con_con = c2, pm_con_args = args2})) (ValVec vva delta)
  | c1 /= c2  =
    return (usimple [ValVec (va:vva) delta])
  | otherwise = kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
                <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta)

Notice that it totally ignores the existential pm_con_tvs of the two arguments. If the two aren't identical we'll get failure in precisely the way you diagnosed.

I think your fix arranges that they are always identical. But even if we adopt your approach, we should add an ASSERT (with explanation) on the "ConCon" case.

More fundamentally, how can we be sure that the assertion holds? I'm not sure. An alternative (and more solid) approach would be to fix the bug in ConCon. How? Well, looking back at the paper, if we have

pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_tvs = tvs1, pm_con_args = args1})) ps guards
          (va@(PmCon {pm_con_con = c2, pm_con_tvs = tvs2, pm_con_args = args2})) (ValVec vva delta)

then we want to add equalities to Delta that say tvs1 = tvs2. And that should be dead easy to do.

If a corresponding pair tv1 and tv2 are already equal, no need to geneate the equality.

Now the mkOneCOnFull fix turns into mere optimisation, one that makes it more likely that the equalities will hold.

Does that makes sense?

I'd be content with the ASSERT; that's the shortest path to a fix. But at least refer to this comment if so.

comment:13 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:14 Changed 19 months ago by bgamari

Description: modified (diff)
Milestone: 8.6.1
Resolution: fixed
Status: patchclosed
Test Case: T11984
Note: See TracTickets for help on using tickets.