Opened 4 years ago

Closed 2 years ago

#10746 closed bug (fixed)

No non-exhaustive pattern match warning given for empty case analysis

Reported by: bgamari Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 7.10.2
Keywords: PatternMatchWarnings Cc: edsko, gkaracha
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #7669, #11806 Differential Rev(s): Phab:D2105
Wiki Page:

Description

I would expect GHC to warn of a non-exhaustive pattern match at compile-time when faced with this,

{-# LANGUAGE EmptyCase #-}
module Test where

test :: Bool -> Int
test a = case a of

Yet it happily accepts this without complaint. If one attempts to evaluate, e.g., test True the expected "Non-exhaustive patterns in case" error is thrown at runtime.

Change History (29)

comment:1 Changed 4 years ago by thomie

Resolution: duplicate
Status: newclosed

comment:2 Changed 4 years ago by bgamari

Resolution: duplicate
Status: closednew

To be clear, the problem here is that we *are* in fact missing cases in the example cited above as the case is scrutinizing a value of non-empty type. In the case of #7669 the compiler was complaining about missing cases despite the fact that the user cannot provide any more cases (as we are matching against an empty type).

Last edited 4 years ago by bgamari (previous) (diff)

comment:3 Changed 4 years ago by bgamari

Resolution: duplicate
Status: newclosed

Ahh, in the interest of aiding the bug sweep (see ticket:7669#comment:8) I'll leave this as a duplicate.

comment:4 Changed 4 years ago by rwbarton

It's a duplicate of ticket:7669#comment:3, not the original bug report in #7669.

comment:5 Changed 3 years ago by rwbarton

Resolution: duplicate
Status: closednew

This was closed through a chain of duplicates leading to #595, but the new pattern exhaustiveness checker in 8.0 still exhibits the issue described in this ticket.

comment:6 Changed 3 years ago by simonpj

Keywords: PatternMatchWarnings added

comment:7 Changed 3 years ago by dfeuer

comment:8 Changed 3 years ago by dfeuer

Cc: gkaracha added

simonpj indicated in the duplicate #11806 that gkaracha is in charge of some of this.

comment:9 Changed 3 years ago by dfeuer

I don't actually understand most of this code, but it *looks* like the problem is probably in the checkMatches' function in compiler/deSugar/Check.hs. Specifically, there's a guard

 | null matches = return ([], [], [])

that looks fishy. I don't have things set up properly to build GHC at the moment, but my guess is that simply removing this clause and going straight to the otherwise will fix the bug.

comment:10 Changed 3 years ago by erikd

Yep, removing that (and the | otherwise pattern guard seems to fix it. At @deuer 's suggestion I'm going to stick this fix (with a test case) up on Phabricator.

comment:11 Changed 3 years ago by erikd

Hmm, wit this fix, building base fails due to:

absurd :: Void -> a
absurd a = case a of {}

which triggers:

libraries/base/Data/Void.hs:66:12: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: _

comment:12 in reply to:  11 Changed 3 years ago by dfeuer

Replying to erikd:

Hmm, wit this fix, building base fails due to:

absurd :: Void -> a
absurd a = case a of {}

which triggers:

libraries/base/Data/Void.hs:66:12: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: _

Argh! That seems surprising. I'd have expected mkInitialUncovered to have produced an empty list there.

comment:13 Changed 3 years ago by simonpj

The discussion in #11806 is worth reading

comment:14 Changed 3 years ago by dfeuer

If I understand it correctly, empty case *always* forces its scrutinee, and thus should be considered complete if that is guaranteed to diverge. I don't really understand gkaracha's argument to the contrary, but he knows much more about this than I do, so I could be missing some key point.

comment:15 Changed 3 years ago by gkaracha

I guess my wording was not clear in #11806 after all, I will try to elaborate here in more detail. :-)

Current state

Indeed the guard in checkMatches' is responsible for the current behaviour on empty case expressions:

| null matches = return ([], [], [])

By default, the new checker would issue a non-exhaustive warning for empty cases, which is correct. Yet, there has been a request (#7669) to not issue a warning in these cases. Hence, Simon changed this with commit 9162d159a62d19d4b371b7348eb1b524001fddcd. I have added the above guard in the new implementation to keep the same behaviour (even though I strongly disagree with it) and by removing it we get the default behaviour, which #11806 & #10746 request.

Laziness

Replying to dfeuer:

Replying to erikd:

Hmm, wit this fix, building base fails due to:

absurd :: Void -> a
absurd a = case a of {}

which triggers:

libraries/base/Data/Void.hs:66:12: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: _

Argh! That seems surprising. I'd have expected mkInitialUncovered to have produced an empty list there.

This is the right behaviour! The call (absurd undefined) :: Int will crash, not because of evaluating undefined but because the match is non-exhaustive, try it out and see! About mkInitialUncovered, it should not produce an empty list: If you check our paper (https://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf, paragraph Initialisation, Section 4.2), you will see that U_0 is not empty, independently of the argument types.

Replying to dfeuer:

If I understand it correctly, empty case *always* forces its scrutinee, and thus should be considered complete if that is guaranteed to diverge. I don't really understand gkaracha's argument to the contrary, but he knows much more about this than I do, so I could be missing some key point.

This is probably the key point that is not clear. The part case x of does not force x, the patterns that appear after do that. This means that, for example, case x of { y -> ... } does not force x.

Type Inhabitation

All the related tickets give me the impression that it is expected for f to be non-exhaustive and g to be exhaustive, which is not in accordance with Haskell's operational semantics.

f :: Int -> a
f x = case x of {}

g :: Void -> a
g x = case x of {}

Unless you force x in another way, both case x of {} are equally non-exhaustive. In OCaml for example this is different, and this is precisely why the OCaml community identifies the pattern match checking as a type inhabitation problem http://www.math.nagoya-u.ac.jp/~garrigue/papers/gadtspm.pdf, in contrast to what we do.

Nevertheless, there are ways in Haskell to force arguments explicitly (e.g. via seq) which means that it becomes an inhabitation problem for us as well (like for g' below) in some cases.

g' :: Void -> a
g' x = x `seq` case x of {}

Indeed, this kind of reasoning we lack at the moment. I can imagine that if the strictness analysis phase came before our checking we would be able to use this information and improve our reasoning for cases like g', by checking type inhabitation, where possible.

Conclusion

Personally, I am really happy that the guard from checkMatches' is finally removed, and I surely vote for non-exhaustive warnings in empty case expressions, including function absurd above which is non-exhaustive. I'd be happy to see how we can make g' issue no warnings, but this, I think, is a quite different problem.

Sorry for the long post, I just hope things are more clear now :-)

comment:16 in reply to:  15 Changed 3 years ago by dfeuer

Replying to gkaracha:

Replying to dfeuer: All the related tickets give me the impression that it is expected for f to be non-exhaustive and g to be exhaustive, which is not in accordance with Haskell's operational semantics.

f :: Int -> a
f x = case x of {}

g :: Void -> a
g x = case x of {}

Unless you force x in another way, both case x of {} are equally non-exhaustive.

It seems your argument may be valid, but your premise is false! Using GHCi 7.10.3,

Prelude> :set -XEmptyCase -XEmptyDataDecls 
Prelude> data Void
Prelude> let absurd :: Void -> a; absurd x = case x of
Prelude> absurd (error "Really?")
*** Exception: Really?

As you can see, the scrutinee is forced, producing the desired exception, not a pattern match failure. This is explained in the note on "Empty case alternatives" in compiler/deSugar/Match.hs:

The list of EquationInfo can be empty, arising from

case x of {} or \case {}

In that situation we desugar to

case x of { _ -> error "pattern match failure" }

The desugarer isn't certain whether there really should be no alternatives, so it adds a default case, as it always does. A later pass may remove it if it's inaccessible. (See also Note [Empty case alternatives] in CoreSyn.)

We do not desugar simply to

error "empty case"

or some such, because x might be bound to (error "hello"), in which case we want to see that "hello" exception, not (error "empty case").

Note that in the above text,

case x of { _ -> error "pattern match failure" }

represents a Core case expression, not a Haskell case expression, so it always forces its scrutinee, regardless of what patterns it may or may not contain.

comment:17 Changed 3 years ago by dfeuer

To summarize, empty case is desugared specially. It therefore needs a special case for coverage checking, but not the trivial one we currently have. I suspect the right thing is probably to avoid including _|_ in mkInitialUncovered when checking an empty case, whatever that involves. You may need to do something else if you want to catch an overlapping trivial pattern in since cases, but even if you miss that it's no big deal.

comment:18 Changed 3 years ago by nomeata

Looks like the confusion was due to the lack of a proper specification of the EmptyCase extension, in particular about the operational semantics of it. Maybe someone feels like extending https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/syntax-extns.html#empty-case with a sentence or two on that?

comment:19 Changed 3 years ago by gkaracha

Replying to dfeuer:

Prelude> :set -XEmptyCase -XEmptyDataDecls
Prelude> data Void
Prelude> let absurd :: Void -> a; absurd x = case x of
Prelude> absurd (error "Really?")
*** Exception: Really?

Wow! I was indeed not familiar with this unintuitive design choice, you are right.

Replying to dfeuer:

To summarize, empty case is desugared specially. It therefore needs a special case for coverage checking, but not the trivial one we currently have. I suspect the right thing is probably to avoid including _|_ in mkInitialUncovered when checking an empty case, whatever that involves. You may need to do something else if you want to catch an overlapping trivial pattern in since cases, but even if you miss that it's no big deal.

Overlap checking is not affected by this I think. Since this eager evaluation happens only in the EmptyCase case, there are no patterns to be considered redundant. Nevertheless, the case needs special treatment. The best fix I can think about this is a function

areInhabited :: [Id] -> TcM [ValVec]

which unfolds everything to WHNF if possible (recursively, I guess, if there are strict fields) and checks for satisfiability (approximately, of course, since this may not terminate). Then, checkMatches' could be adjusted:

checkMatches' :: [Id] -> [LMatch Id (LHsExpr Id)] -> DsM PmResult
checkMatches' vars matches
  | null matches = areInhabited vars >>= \us -> return ([],us,[])
  | otherwise    = ...

Does this sound reasonable? I'd like to think this through first, but I could write such a fix.

comment:20 Changed 3 years ago by dfeuer

I don't think you need to go that far to satisfy many people, although maybe I'm missing something. We mostly want you to inspect all constructors of the relevant datatype that have not obviously been eliminated previously and check that their result types are apart from the type of the scrutinee. The reason for the perhaps-counterintuitive design choice is that a lazy empty case would be quite useless--you'd always be better off with an error call than such a beast! Strict empty case, on the other hand, will be quite useful once this bug is squashed.

comment:21 Changed 3 years ago by dfeuer

Oh, I see what you mean about recursively checking strict fields to some limit. That would be very nice, yes, but it's not urgent because there's a good way to work around it:

data SId a = SId !a

--With recursive checking
foo :: SId Void -> a
foo bad = case bad of

--Without recursive checking
foo (SId bad) = absurd bad

What I don't understand is what you mean about unfolding something to WHNF. If the goal is to try to determine the actual WHNF of the scrutinee, that sounds like overkill to me, unless you're doing that in other cases already.

comment:22 in reply to:  21 Changed 3 years ago by gkaracha

Replying to dfeuer:

What I don't understand is what you mean about unfolding something to WHNF. If the goal is to try to determine the actual WHNF of the scrutinee, that sounds like overkill to me, unless you're doing that in other cases already.

Ah, no, I think we mean the same thing. Maybe my wording was not clear. :-) For example, for Fin, we need to unfold the x to FZ and FS y to check whether the match is exhaustive or not.

data Fin n where
  FZ ::          Fin (Succ n)
  FS :: Fin n -> Fin (Succ n)

f :: Fin Zero -> a
f x = case x of {}

For what is worth, I have a small patch that does exactly this, expanding patterns of type T tys (only type constructor applications) to all possible patterns (one layer unfolding only) and behaves as expected for Void, Fin and other GADTs I have tried it on. I'll put it on Phab later today :-)

comment:23 Changed 3 years ago by dfeuer

Excellent! I think one layer only is probably a good goal for right this minute. More extensive checking would likely involve more research and design decisions. Thanks a lot for working on this.

comment:24 Changed 3 years ago by dfeuer

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

comment:25 Changed 3 years ago by simonpj

This all seems a bit more complicated than it need be. My guiding light is that it should all be very similar to case x of { C y -> blah }. For this we enumerate all the data constructors other than C y as non-matching (modulo inaccessible GADT constructors).

We can do the same here. The only real difference is that we don't have a data constructor C to start from. Instead we start from the type of x :: tyx.

So it looks simple:

  • Normalise x's type, to get it to the form T ty1 .. tyn. (I don't understand the "bounded" bit.) For this, we must reduce type families, but NOT newtypes. For pattern matching purposes, newtypes behave just like data types. So use FamInstEnv.normaliseType.
  • If T has no data constructors, we are done. For example, empty data types, which don't produce an error message here.
  • If none of T's data constructors are GADTs, then just produce an error of form
    Blah.hs:4:1: warning: [-Wincomplete-patterns]
        Pattern match(es) are non-exhaustive
        In a case alternative: Patterns not matched: _ :: Bool
    
    Here I've added the ":: Bool" part so the reader understands the type of the pattern. No need to enumerate True and False.
  • If some of T's data constructor are GADTs, then enumerate them all and recurse.

comment:26 in reply to:  25 Changed 3 years ago by gkaracha

Replying to simonpj:

  • Normalise x's type, to get it to the form T ty1 .. tyn. (I don't understand the "bounded" bit.) For this, we must reduce type families, but NOT newtypes. For pattern matching purposes, newtypes behave just like data types. So use FamInstEnv.normaliseType.

This sounds wrong to me. Newtypes and data types do not behave the same when it comes to pattern matching. From Newtype Wiki Page:

data    Foo1 = Foo1 Int
newtype Foo3 = Foo3 Int
 
y1 = case undefined of
       Foo1 _ -> 1      -- undefined
 
y3 = case undefined of
       Foo3 _ -> 1      -- 1

which is verified by my GHCi (7.10). Additionally, by bounded I mean that when we have a family

type family F (a :: *) :: *
type instance F a = F a

we do not want to keep rewriting forever. Hence, I would bound normalization with a fixed number of maximum iterations. If we exceed that, we (playing on the safe side) assume that the type is inhabited and issue a warning.

The rest you mentioned I agree with, but I missed a bit:

  • If some of T's data constructor are GADTs, then enumerate them all and recurse.

What do you mean by recurse in this case? Does EmptyCase imply deep evaluation (is it really strict pattern matching) or just in WHNF? Because I thought that it means the latter.

comment:27 Changed 3 years ago by dfeuer

I don't know about the other stuff, but I think I disagree on the bounded bit. In that situation, I would expect the compiler to go into an infinite loop (unless it has pity on us in that particular case and happens to detect the loop, which is not the pattern checker's problem in any case). If I tell the type checker to go into an infinite loop and heat up my computer, it's really okay if it does that. Again, I can always write

foo :: F Int -> a
foo !_ = error "Unreachable, but that's not provable within Haskell."

if I want to impose an ad hoc postulate about program behavior. Empty case is for what GHC *can* prove. The case of terminally stuck closed type families (ones that no additional information could possibly reduce) is a bit weird; I think for now at least you should probably treat them the same as stuck open type families and assume them inhabited.

comment:28 Changed 2 years ago by Ben Gamari <ben@…>

In b103532/ghc:

Exhaustiveness check for EmptyCase (Trac #10746)

Empty case expressions have strict semantics so the problem boils down
to inhabitation checking for the type of the scrutinee. 3 main functions
added:

- pmTopNormaliseType_maybe for the normalisation of the scrutinee type

- inhabitationCandidates for generating the possible patterns of the
  appropriate type

- checkEmptyCase' to filter out the candidates that give rise to
  unsatisfiable constraints.

See Note [Checking EmptyCase Expressions] in Check
and Note [Type normalisation for EmptyCase] in FamInstEnv

Test Plan: validate

Reviewers: simonpj, goldfire, dfeuer, austin, bgamari

Reviewed By: bgamari

Subscribers: mpickering, thomie

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

GHC Trac Issues: #10746

comment:29 Changed 2 years ago by bgamari

Milestone: 8.2.1
Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.