#11984: Pattern match incompleteness / inaccessibility discrepancy -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gkaracha): Replying to [comment:1 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 :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11984#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11984: Pattern match incompleteness / inaccessibility discrepancy -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14098 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11984#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11984: Pattern match incompleteness / inaccessibility discrepancy -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14098 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): Ryan, have you seen [[wiki:PatternMatchCheckImplementation]]? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11984#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11984: Pattern match incompleteness / inaccessibility discrepancy -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14098 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11984#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11984: Pattern match incompleteness / inaccessibility discrepancy -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14098 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11984#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11984: Pattern match incompleteness / inaccessibility discrepancy -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14098 | Differential Rev(s): Phab:D4434 Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11984#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11984: Pattern match incompleteness / inaccessibility discrepancy -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: | PatternMatchWarnings 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: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * testcase: => T11984 * resolution: => fixed * milestone: => 8.6.1 Old description:

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.

New description: Consider this module: {{{#!hs {-# 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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11984#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler