GHC Warning: Non-exhaustive Pattern Match for List Despite Explicit Match on Empty List

changed the description

Here's a more self-contained reproducer (just save it to a file and runhaskell it):

{-# LANGUAGE OverloadedLists, RebindableSyntax #-}
{-# OPTIONS -Wincomplete-patterns #-}

import Prelude (Bool(..), IO, print)
import GHC.Exts (IsList(fromListN, toList))

null :: [a] -> Bool
null [] = True
null (_:_) = False

main :: IO ()
main = print (null [])

OverloadedLists turns null's definition into basically this:

null (toList -> []) = True
null (_:_) = False

Now the warning seems a bit more reasonable. Consider this modified program:

{-# LANGUAGE OverloadedLists, RebindableSyntax #-}
{-# OPTIONS -Wincomplete-patterns #-}

import Prelude (Bool(..), IO, print)
import GHC.Exts (IsList(fromListN))

toList :: [a] -> [()]
toList _ = ():[]

null :: [a] -> Bool
null [] = True
null (_:_) = False

main :: IO ()
main = print (null [])

It really will crash with a Non-exhaustive patterns in function null error.

OverloadedLists turns null's definition into basically this:

null (toList -> []) = True
null (_:_) = False

That's surprising to me. Shouldn't it desugar into:

null x = case toList x of
  [] -> True
  (_:_) -> False

(I haven't read the spec though)

added Pnormal Tbug pattern match warnings labels and removed needs triage label

added documentation label

If it had been

data Wombat = K Wombat Wombat | ...

instance IsLit Wombat where
  type Item Wombat = Int
  toList w = ...<maybe big>...

nullWombat :: Wombat -> Bool
null [] = True
null (K x y) = ...

we would not be surprised at a pattern match warning, because null turns into

null w = case toList @Wombat w of
           [] -> True
           _  -> case x of
                   K x y -> ...
                   _ -> error "not covered"

Not having such a warning would require GHC to figure out that the [] restul from toList deals will all constructors of w other than K.

But here we are in the very special case of toList called at type [a], where it is the identity function.

It seems plausible that the pattern match checker might have built-in knowledge of this, and treat toList @[type] x just the same way it treats x. Yes, that's ad-hoc, but everything the pattern match checker is on a best-efforts basis.

@sgraf812 ?

This is unrelated to whether or not we want to look through the definition of toList. We would detect both

null (toList -> []) = True
null (toList -> (_:_)) = False

null [] = True
null (_:_) = False

as complete. The former is the desugaring under -XOverloadedLists, the latter is the vanilla desugaring. It is only with -XRebindableSyntax that we get the weird desugaring

null (toList -> []) = True
null (_:_) = False

as discovered by #25257 (comment 583185).

Why are we expanding [] differently to (_:_)? That's the bug here. If we fix it, we won't see any warnings, I believe (try removing -XRebindableSyntax in the reproducer to test).

Ah, the problem is that [] is desugared as a ListPat while (_:_) is a ConPat. In the absence of -XRebindableSyntax, we have a special code path in Pmc.Desugar.desugarPat, but that is deactivated in case of -XRebindableSyntax.

Perhaps instead of deactivating that code path completely, we could see whether the expansion is the vanilla GHC.Exts.toList which amounts to inlining it.

Why are we expanding [] differently to (_:_)?

Because [] is built-in syntax, expanded by OverloadedLists (as is [a,b,c]), while _:_ is just a regular old data constructor, like Just x which has no relationship with OverloadedLists.

I don't see how deactivating code paths can help with that.

mentioned in commit 4b8dbe28

mentioned in merge request !13261 (closed)

The fix is in !13261 (closed).

mentioned in issue #25264 (closed)

mentioned in commit 077028f3

mentioned in commit 7377be17

It looks like this is actually a regression. In GHC 8.4.4, the false positive warning doesn't happen, but you do still get the warning on my modified one where it really is incomplete.

mentioned in commit 60dca249

mentioned in commit 6d4a2a04

closed with commit 7fd9e5e2

mentioned in commit 7fd9e5e2

Fixed by 7fd9e5e2.

GHC Warning: Non-exhaustive Pattern Match for List Despite Explicit Match on Empty List

Summary

Steps to reproduce

Expected behavior

Environment

Child items ...

Activity