Pattern match incompleteness / inaccessibility discrepancy

[goldfire]

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.

[simonpj]

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

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

[RyanGlScott]

See #14098 for a similar example.

[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.

[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.)

[bgamari]

Ryan, have you seen PatternMatchCheckImplementation?

[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

[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.

[RyanGlScott]

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

[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.

[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