Opened 13 years ago

Closed 5 months ago

#595 closed task (fixed)

Overhaul GHC's overlapping/non-exhaustive pattern checking

Reported by: simonmar Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler Version: None
Keywords: warnings Cc: lelf, marcot@…, ryani.spam@…, benjross@…, carter.schonwald@…, the.dead.shall.rise@…, jkarni@…, michael.b.bassett@…, cheecheeo@…, george.karachalias@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case: N/A
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonmar)

GHC has a module in the desugarer (Check) which checks whether patterns are overlapping and/or exhaustive, to support the flags -fwarn-overlapping-patterns and -fwarn-non-exhaustive-patterns. The code is old and crufty, and has several outstanding bugs. A rewrite is needed.

Change History (29)

comment:1 Changed 10 years ago by simonmar

  • Component changed from None to Compiler
  • Description modified (diff)

comment:2 Changed 10 years ago by simonmar

  • Architecture set to Unknown
  • difficulty set to Difficult (1 week)
  • Operating System set to Unknown

comment:3 Changed 10 years ago by igloo

  • Keywords warnings added
  • Milestone set to _|_
  • Test Case set to N/A

comment:4 Changed 9 years ago by simonmar

Related tickets: #29, #322, #851, #1307

comment:5 Changed 8 years ago by simonpj

And #2006

comment:6 Changed 8 years ago by simonpj

And #2204

comment:7 Changed 8 years ago by simonmar

And #366.

Someone could fix this and bag 8 tickets in one go :-)

comment:8 Changed 8 years ago by simonmar

  • Architecture changed from Unknown to Unknown/Multiple

comment:9 Changed 8 years ago by simonmar

  • Operating System changed from Unknown to Unknown/Multiple

comment:10 Changed 7 years ago by simonpj

Also look at #3078: pattern guards.

comment:11 Changed 7 years ago by simonmar

  • difficulty changed from Difficult (1 week) to Difficult (2-5 days)

comment:12 Changed 6 years ago by igloo

  • Type of failure set to Incorrect warning at compile-time

comment:13 Changed 6 years ago by marcotmarcot

  • Owner set to marcotmarcot

I'm studying the source code related to the bug, and I have read the pointed paper. I'm describing my progress in this page.

comment:14 Changed 6 years ago by simonpj

Excellent! Please also consult http://www.cs.cmu.edu/~neelk/pattern-popl09.pdf

Also do not forget about view patterns

Simon

comment:15 Changed 6 years ago by marcotmarcot

Hi.

I won't work with this task, because I've not found the relevance. Issue #322 doens't seem to be fixable, and issue #2204 and #1307 are only about improving the error message.

Greetings.

comment:16 Changed 6 years ago by marcotmarcot

  • Owner marcotmarcot deleted

comment:17 Changed 6 years ago by marcotmarcot

  • Cc marcot@… added

comment:18 Changed 6 years ago by ryani

  • Cc ryani.spam@… added

comment:19 Changed 4 years ago by bross279

  • Cc benjross@… added

Is anyone working on this? This project interests me for GSoC, and I was wondering who I could talk to to find more information on this project.

comment:20 Changed 4 years ago by simonpj

No, no one is working on it, as far as I know, and I would love someone to pay attention to it. There are a bunch of related tickets: at least #595, #5728, #3927, #5724, #5762, #4139. It has the great merit of being a nicely-separable task, one that doesn't interact with the rest of GHC.

There is a good literature to guide you:

However these papers focus entirely on a "block" of pattern matching, for example, a function defined by pattern matching. Many of the tickets go further:

  • Consider
    f xs@(y:ys) = .....case xs of { (y:ys) -> ... }
    
    The inner pattern match should not complain about a missing nil case. You may think this is a silly program, but it's less silly when record updates are concerned.
  • Matches that involve GADTs. Here things are a bit more complicated, and involve figuring out what branches are inaccessible because of type constraints. It's not that hard, but generating good warnings goes beyond what the literature covers.

I don't want to supervise this, but would would be happy to offer advice and guidance about GHC aspects, if someone else would lead.

comment:21 Changed 3 years ago by carter

  • Cc carter.schonwald@… added

comment:22 Changed 3 years ago by refold

  • Cc the.dead.shall.rise@… added

comment:23 Changed 2 years ago by jkarni

  • Cc jkarni@… added

comment:24 Changed 2 years ago by mbassett

  • Cc michael.b.bassett@… added

comment:25 Changed 8 months ago by cheecheeo

  • Cc cheecheeo@… added

comment:26 Changed 7 months ago by lelf

  • Cc lelf added

comment:27 Changed 6 months ago by gkaracha

  • Cc george.karachalias@… added

comment:28 Changed 6 months ago by George Karachalias <george.karachalias@…>

In 8a506104/ghc:

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.

comment:29 Changed 5 months ago by adamgundry

  • Milestone changed from to 8.0.1
  • Resolution changed from None to fixed
  • Status changed from new to closed

Great work @gkaracha!

Note: See TracTickets for help on using tickets.