Opened 17 months ago

Closed 15 months ago

Last modified 15 months ago

#15305 closed bug (fixed)

Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation

Reported by: jkoppel Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.4.3
Keywords: PatternMatchWarnings Cc: alanz, sh.najd@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case: pmcheck/should_compile/T15305
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5087
Wiki Page:

Description

In the following code, fun contains an exhaustive pattern match, but, when compiling with -Wall, ghc erroneously reports a non-exhaustive pattern match.

data (:+:) f g a = Inl !(f a) | Inr !(g a)

data A
data B

data Foo l where
  Foo :: Foo A

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1

This report came from https://stackoverflow.com/questions/16225281/gadts-failed-exhaustiveness-checking . Without strictness annotations, this is indeed a failed exhaustive check, due to bottom. I spoke to Richard Eisenberg at PLDI a few days ago, and he informed me that, if this warning did not disappear with strictness annotations, it was a bug. I added strictness annotations, and it did not disappear. I've tried all combinations of using strictness annotations and/or running with {-# LANGUAGE Strict #-}.

Attachments (1)

Main.hs (280 bytes) - added by jkoppel 17 months ago.

Download all attachments as: .zip

Change History (16)

Changed 17 months ago by jkoppel

Attachment: Main.hs added

comment:1 Changed 17 months ago by RyanGlScott

Keywords: PatternMatchWarnings added

comment:2 Changed 17 months ago by simonpj

Good point.

Pattern-match coverage checking sorely needs a champion: someone who is willing to take ownership of the code (which is in only one module!) and give it love and care.

There are a lot of open tickets: see this summary wiki page

comment:3 Changed 17 months ago by RyanGlScott

It's unclear to me what can even be done about this. The GADTs Meet Their Match paper is completely silent on the topic of bang patterns, so this seems like a theory bug, not an implementation one.

comment:4 Changed 16 months ago by goldfire

If this were fixed, then I believe that GHC could usefully use empty types as many of its "Trees That Grow" extension fields, make the extensions strict, and then remove many tiresome panics in redundant patterns. For example (simplified):

data HsImplicitBndrs pass
  = UsefulConstructor ...
  | XHsImplicitBndrs !(XXHsImplicitBndrs pass)

type instance XXHsImplicitBndrs (GhcPass _) = Void

Note the bang.

Currently, if we did this, we would still need to match against XHsImplicitBndrs every time. But with this patch fixed, we could avoid doing so.

comment:5 Changed 16 months ago by simonpj

Cc: alanz sh.najd@… added

comment:6 Changed 16 months ago by RyanGlScott

To be clear, this is another occurrence of this phenomenon, right?

{-# LANGUAGE EmptyCase #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where

data Abyss = MkAbyss !Abyss

stareIntoTheAbyss :: Abyss -> a
stareIntoTheAbyss a = case a of {}

(In that GHC warns that stareIntoTheAbyss is non-exhaustive, even though it shouldn't?)

Last edited 16 months ago by RyanGlScott (previous) (diff)

comment:7 Changed 16 months ago by RyanGlScott

I tried thinking of an (ad hoc) algorithm to check for this sort of thing. This is the closest I could get:

  1. In mkOneConFull (which generates pattern-matching information for each constructor), record the type and strictness of each constructor's fields.
  2. When checking if a match on that constructor is reachable, perform the following additional checks:
    1. Check if all fields are strict.
    2. Check if each field's type is uninhabitable.

If both (i) and (ii) are true, then deem the entire constructor to be unreachable.

I think this would work for the original program, but not the program in comment:6

data Abyss = MkAbyss !Abyss

stareIntoTheAbyss :: Abyss -> a
stareIntoTheAbyss a = case a of {}

Why? In order to check that a match on (MkAbyss _) is unreachable, we need to check:

  1. That the field of MkAbyss is strict. (This is the case.)
  2. That the type of the field of MkAbyss (Abyss) is uninhabitable.

But in order to check that Abyss in uninhabitable, we need to check the MkAbyss constructor again, which requires repeating this algorithm. Now we've entered an infinite loop!

comment:8 Changed 16 months ago by RyanGlScott

Milestone: 8.6.1Research needed

comment:9 Changed 16 months ago by simonpj

My strong instinct here is to go back to the paper. In rule [UConVar] and friends we split up 'x' into a union of constructors {K x1, K2 x2 x3, K3}. Each of those split constructors comes with an extended Delta, which describes the constraints in scope. If these constraints prove contradicatory we can drop the entire branch.

So for a strict constructor, say

data T a where
  MkT :: a -> !a -> T a

we want to add a constraint to Delta that says that the type of that second argument is non-void; that is, it contains at least one element that terminates. So maybe we need a constraint NonVoid( tau ).

In the OP, NonVoid( Bar A ) would be a contradiction.

In the implementation we have a simple "term oracle" that works alongside the type oracle that is implemented by the constraint solver. Maybe we could add the new constraint to the term oracle?

comment:10 in reply to:  9 Changed 16 months ago by RyanGlScott

I think this would work fine for simple, non-recursive examples like the original program, but I fail to see how this would work for recursive examples like the program in comment:7. If you have the constraint NonVoid(Abyss), how do you conclude that that is contradictory? Presumably, you'd need some sort of way to determine if there are any terminating inhabitants of Abyss. Unlike the InL example, where the type of its field alone (Foo B) is enough to conclude that it is uninhabitable, nothing about the type of MkAbyss's field (Abyss) suggests that it is uninhabitable, so you'd have to check if its field satisfies the constraint NonVoid(Abyss). But that brings us back to the infinite loop in comment:7.

In short, I just don't see how this is possible to do in a way that's complete.

comment:11 Changed 16 months ago by simonpj

I fail to see how this would work for recursive examples like the program in comment:7

Correct. Computing NonVoid( tau ) is an open-ended question. For some taus (lke Bar A) it's easy; for others we could be more ambitious. It's probably undecidable in general.

So we could start with something simple and become more ambitious later.

comment:12 Changed 15 months ago by RyanGlScott

Differential Rev(s): Phab:D5087
Status: newpatch

Implementing a naïve NonVoid(ty) solver ends up being pretty darn simple: just check if there is at least one inhabitation candidate for ty (as determined through inhabitationCandidates) such that its term and type constraints are satisfiable. That's sufficient to avoid warnings in the original program and in the program in comment:4. See Phab:D5087.

comment:13 Changed 15 months ago by Krzysztof Gogolewski <krz.gogolewski@…>

In 744b034d/ghc:

Take strict fields into account in coverage checking

Summary:
The current pattern-match coverage checker implements the
formalism presented in the //GADTs Meet Their Match// paper in a
fairly faithful matter. However, it was discovered recently that
there is a class of unreachable patterns that
//GADTs Meet Their Match// does not handle: unreachable code due to
strict argument types, as demonstrated in #15305. This patch
therefore goes off-script a little and implements an extension to
the formalism presented in the paper to handle this case.

Essentially, when determining if each constructor can be matched on,
GHC checks if its associated term and type constraints are
satisfiable. This patch introduces a new form of constraint,
`NonVoid(ty)`, and checks if each constructor's strict argument types
satisfy `NonVoid`. If any of them do not, then that constructor is
deemed uninhabitable, and thus cannot be matched on. For the full
story of how this works, see
`Note [Extensions to GADTs Meet Their Match]`.

Along the way, I did a little bit of much-needed refactoring. In
particular, several functions in `Check` were passing a triple of
`(ValAbs, ComplexEq, Bag EvVar)` around to represent a constructor
and its constraints. Now that we're adding yet another form of
constraint to the mix, I thought it appropriate to turn this into
a proper data type, which I call `InhabitationCandidate`.

Test Plan: make test TEST=T15305

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15305

Differential Revision: https://phabricator.haskell.org/D5087

comment:14 Changed 15 months ago by monoidal

Resolution: fixed
Status: patchclosed

comment:15 Changed 15 months ago by RyanGlScott

Milestone: Research needed8.8.1
Test Case: pmcheck/should_compile/T15305
Note: See TracTickets for help on using tickets.