Opened 6 years ago

Closed 14 months ago

Last modified 10 months ago

#4139 closed bug (duplicate)

Spurious non-exhaustive pattern match warnings are given using GADTs

Reported by: blarsen Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.4.1
Keywords: GADTs, warnings, pattern matching Cc: eir@…, hackage.haskell.org@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #3927 Differential Rev(s):
Wiki Page:

Description

When using slightly complicated GADTs, GHC gives me erroneous non-exhaustive pattern match warnings. I have attached an example. I have observed this behavior in the four versions of ghc that I tried (6.10.4, and 6.12.{1,2,3}).

Attachments (2)

GADTNonExhaustive.hs (1.4 KB) - added by blarsen 6 years ago.
A simple evaluator that demonstrates spurious non-exhaustive pattern match warnings
GADTbug.hs (369 bytes) - added by goldfire 5 years ago.
produces warning about non-exhaustive pattern match in GADT

Download all attachments as: .zip

Change History (12)

Changed 6 years ago by blarsen

A simple evaluator that demonstrates spurious non-exhaustive pattern match warnings

comment:1 Changed 6 years ago by igloo

  • Milestone set to 6.14.1
  • Owner set to simonpj

Thanks for the report.

See also #3927.

comment:2 follow-up: Changed 6 years ago by simonpj

  • Resolution set to invalid
  • Status changed from new to closed

Now I look at your example, I see that your claim isn't true! Consider

evalFst (Const (undefined :: Const (Int,Int))

That will hit the allegedly impossible alternative.

So in this case GHC is quite right. (The pattern match warnings are not all correct, but this one is, I think.)

Simon

comment:3 in reply to: ↑ 2 Changed 6 years ago by blarsen

Replying to simonpj:

Now I look at your example, I see that your claim isn't true! Consider

evalFst (Const (undefined :: Const (Int,Int))

That will hit the allegedly impossible alternative.

So in this case GHC is quite right. (The pattern match warnings are not all correct, but this one is, I think.)

Simon

Indeed! I had forgotten about undefined / bottom values.

Brad

comment:4 Changed 5 years ago by goldfire

  • Cc eir@… added
  • Owner simonpj deleted
  • Resolution invalid deleted
  • Status changed from closed to new
  • Type of failure changed from None/Unknown to Incorrect warning at compile-time
  • Version changed from 6.12.3 to 7.4.1

I have a case with the same bug description as above, but when I include the pattern suggested by the warning statement, I get a compiler error indicating unreachable code. I have attached my code.

Changed 5 years ago by goldfire

produces warning about non-exhaustive pattern match in GADT

comment:5 Changed 5 years ago by simonpj

  • difficulty set to Unknown

Good example. It has the same cause as #3927. Sorry no imminent cure. Needs someone to pay proper attention to it.

comment:6 Changed 4 years ago by goldfire

comment:7 Changed 4 years ago by liyang

  • Cc hackage.haskell.org@… added

comment:8 Changed 2 years ago by ezyang

  • Milestone 7.0.1 deleted

comment:9 Changed 14 months ago by thomie

  • Resolution set to duplicate
  • Status changed from new to closed

Because the existence of duplicate tickets makes doing a BugSweep of the bug tracker more cumbersome, I'm closing these tickets as duplicate. Don't worry, they're still listed on PatternMatchCheck, and will hopefully all be addressed by the work on #595 ("Overhaul GHC's overlapping/non-exhaustive pattern checking").

comment:10 Changed 10 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.
Note: See TracTickets for help on using tickets.