[GHC] #9951: OverloadedLists breaks exhaustiveness check
#9951: OverloadedLists breaks exhaustiveness check -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE OverloadedLists #-} module Bug where f :: [a] -> () f x = case x of [] -> () (_:_) -> () }}} GHC reports: {{{ bug.hs:6:7: Warning: Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: [] }}} This is reproducible with 7.8 and 7.10rc1. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9951> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9951: OverloadedLists breaks exhaustiveness check -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by MartinF): I note patterns using OverloadedLists desugar to view patterns - from that wiki page:
{{{#!haskell f [] = ... g [x,y,z] = ... }}}
will be treated as
{{{#!haskell f (toList -> []) = ... g (toList -> [x,y,z]) = ... }}}
So I'd guess this has the same underlying cause as the known problem with exhaustiveness checking of view patterns - see #5762. For instance, this: {{{ $ ghci -Wall -XOverloadedLists GHCi, ... Prelude> let f [] = (); f (_:_) = () <interactive>:2:5: Warning: Pattern match(es) are non-exhaustive In an equation for `f': Patterns not matched: [] }}} and its one-step-desugared equivalent: {{{ $ ghci -Wall -XViewPatterns GHCi, ... Prelude> :module +GHC.Exts Prelude GHC.Exts> let f (fromList -> []) = (); f (fromList -> _:_) = () <interactive>:3:5: Warning: Pattern match(es) are non-exhaustive In an equation for `f': Patterns not matched: _ }}} ... both produce spurious exhaustiveness warnings. Slightly different ones, though. How curious. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9951#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9951: OverloadedLists breaks exhaustiveness check -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by Feuerbach): Thanks Martin, that desugaring explains everything. I didn't know it was so simple. The cause of the difference you point is that the cons pattern, `_:_`, is not overloaded. The question then becomes, should there be some way to write the non- overloaded empty list constructor even when OverloadedLists is on? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9951#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9951: OverloadedLists breaks exhaustiveness check -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by thomie): Also reported as #10393. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9951#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9951: OverloadedLists breaks exhaustiveness check -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): -------------------------------------+------------------------------------- Comment (by George Karachalias <george.karachalias@…>): In [changeset:"8a506104d5b5b71d5640afc69c992e0af40f2213/ghc" 8a506104/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="8a506104d5b5b71d5640afc69c992e0af40f2213" Major Overhaul of Pattern Match Checking (Fixes #595) This patch adresses several problems concerned with exhaustiveness and redundancy checking of pattern matching. The list of improvements includes: * Making the check type-aware (handles GADTs, Type Families, DataKinds, etc.). This fixes #4139, #3927, #8970 and other related tickets. * Making the check laziness-aware. Cases that are overlapped but affect evaluation are issued now with "Patterns have inaccessible right hand side". Additionally, "Patterns are overlapped" is now replaced by "Patterns are redundant". * Improved messages for literals. This addresses tickets #5724, #2204, etc. * Improved reasoning concerning cases where simple and overloaded patterns are matched (See #322). * Substantially improved reasoning for pattern guards. Addresses #3078. * OverloadedLists extension does not break exhaustiveness checking anymore (addresses #9951). Note that in general this cannot be handled but if we know that an argument has type '[a]', we treat it as a list since, the instance of 'IsList' gives the identity for both 'fromList' and 'toList'. If the type is not clear or is not the list type, then the check cannot do much still. I am a bit concerned about OverlappingInstances though, since one may override the '[a]' instance with e.g. an '[Int]' instance that is not the identity. * Improved reasoning for nested pattern matching (partial solution). Now we propagate type and (some) term constraints deeper when checking, so we can detect more inconsistencies. For example, this is needed for #4139. I am still not satisfied with several things but I would like to address at least the following before the next release: Term constraints are too many and not printed for non-exhaustive matches (with the exception of literals). This sometimes results in two identical (in appearance) uncovered warnings. Unless we actually show their difference, I would like to have a single warning. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9951#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9951: OverloadedLists breaks exhaustiveness check -------------------------------------+------------------------------------- Reporter: Feuerbach | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: duplicate | 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => PatternMatchWarnings -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9951#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC