Opened 8 years ago

Closed 2 years ago

Last modified 2 years ago

#3927 closed bug (duplicate)

Incomplete/overlapped pattern warnings + GADTs = inadequate

Reported by: simonpj Owned by: simonpj
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 6.12.1
Keywords: Cc: pumpkingod@…, ppremont@…, conal@…, sjoerd@…, nathanhowell@…, eir@…, ghartshaw@…, jeroen.weijers@…, wren@…, hackage.haskell.org@…, george.karachalias@…, gergo@…, ulf.norell@…, victor@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #4139 Differential Rev(s):
Wiki Page:

Description

Consider these defintions

data T a where
  T1 :: T Int
  T2 :: T Bool

-- f1 should be exhaustive
f1 :: T a -> T a -> Bool
f1 T1 T1 = True
f1 T2 T2 = False

-- f2 is exhaustive too, even more obviously
f2 :: T a -> T a -> Bool
f2 T1 (T1 :: T Int) = True
f2 T2 (T2 :: T Bool) = False

-- f3's first equation is unreachable
f3 :: T a -> T a -> Bool
f3 T2 T1 = False
f3 _  _  = True 

With HEAD (GHC 6.13) we get

G1.hs:11:1:
    Warning: Pattern match(es) are non-exhaustive
             In the definition of `f1':
                 Patterns not matched:
                     T1 T2
                     T2 T1

This is wrong.

  • f1 should behave like f2, and be accepted without warning.
  • f3 has an inaccessible branch that is not reported.

The type checker accepts just the right programs, but the rather simple-minded approach to overlap warnings isn't doing the right thing.

Note to self: the reason is that tcPat does not insert a coercion on the second arg to narrow the type, because there's no type reason to do so. So for f1 we get

f1 a (x:T a) (y:T a)
  = case x of { T1 (cox:a~Int) ->
      case y of { T1 (coy:a~Int) -> ... }

In the inner case it's not obvious that T2 is inaccessible. If we refined eagerly we might get

f1 a (x:T a) (y:T a)
  = case x of { T1 (cox:a~Int) ->
      case (y |> T cox) of { T1 (coy:Int~Int) -> ... }

and now the scrutinee of the inner case has type (T Int) and the T2 constructor obviously can't occur.

Fix this with the new inference engine.

Attachments (1)

test.hs (2.0 KB) - added by merijn 3 years ago.
Test case exhibiting wrong exhaustiveness checks that SPJ asked me to attach.

Download all attachments as: .zip

Change History (45)

comment:1 Changed 8 years ago by igloo

Milestone: 6.14.1
Priority: normalhigh

comment:2 Changed 7 years ago by igloo

Owner: set to simonpj

See #4139 for a tricker case of the same problem.

Simon, I'm assigning the ticket to you as I think you're working on the inference engine at the moment.

Incidentally, in 6.13.20100617 this fails with:

    Pattern signature must exactly match: T a
    In the pattern: T1 :: T Int
    In the definition of `f2': f2 T1 (T1 :: T Int) = True

comment:4 Changed 7 years ago by igloo

Blocked By: 4232 added

comment:5 Changed 7 years ago by pumpkin

Cc: pumpkingod@… added

Mostly just adding myself to the CC list here, but I figured I'd attach the test code that made me interested in this ticket in the first place, in case you wanted a more tangible example of why some people might want this.

{-# OPTIONS_GHC -Wall #-}
{-# Language GADTs #-}

data Nz = Nz
newtype Ns n = Ns n

data Fin n where
  Fz :: Fin (Ns n)
  Fs :: Fin n -> Fin (Ns n)
  
data Vec n a where
  Nil  :: Vec Nz a
  Cons :: a -> Vec n a -> Vec (Ns n) a

-- This works nicely!
test :: Fin Nz -> a
test _ = undefined
-- test Fz = undefined -- Rightfully rejected by GHC
-- test (Fs n) = undefined -- Rightfully rejected by GHC

-- Here, "knowledge" acquired by patern matching on one parameter refines the type of the other, and in the Nil case,
-- refines the second parameter to Fin Nz, which contains nothing and thus I cannot provide a meaningful pattern.
index :: Vec n a -> Fin n -> a
index Nil Fz = error "GHC shouldn't even let me write this combination of patterns, but the coverage checker tells me my pattern is non-exhaustive if I don't write it"
index Nil (Fs _) = error "Ditto"
index (Cons x _) Fz = x
index (Cons _ xs) (Fs n) = index xs n

comment:6 Changed 7 years ago by igloo

Blocked By: 4232 removed

comment:6 Changed 7 years ago by simonpj

Pumpkin, GHC is quite correct in its warnings about your code. If you put in the "error" lines in your code above, then GHC correctly warns that those branches are inaccessible:

T3927b.hs:26:11:
    Inaccessible code in
      a pattern with constructor `Fz', in an equation for `index'
    Couldn't match type `Nz' with `Ns n'
    In the pattern: Fz
    In an equation for `index':
        index Nil Fz
          = error
              "GHC shouldn't even let me write this combination of ..."

If you comment out both those lines you get the non-exhaustive warning:

T3927b.hs:28:1:
    Warning: Pattern match(es) are non-exhaustive
             In an equation for `index': Patterns not matched: Nil _

And that is right too! For example consider the call:

index Nil (undefined :: Fin Nz)

If you don't have an equation for Nil the pattern match indeed is not exhaustive. So you need an equation

index Nil _ = error "index called with Nil argument"

However, my original bug report remains valid

Simon

comment:7 Changed 7 years ago by pumpkin

I understand that you can provide bottoms for Fin Nz, but the issue is that in the code I submitted, the pattern match itself is badly typed. The warning alludes to it, but the fact remains that for my index function, Nil and Fz or Fs cannot "coexist" within a pattern and have consistent types. I see that the warning spots that, but I'd expect it to be an error instead of a warning, a bit like the test function above, since the constructors in the pattern are impossible to type correctly.

Just to clarify, I'm advocating that

index :: Vec n a -> Fin n -> a
index Nil Fz = error "GHC shouldn't even let me write this combination of patterns, but the coverage checker tells me my pattern is non-exhaustive if I don't write it"
index Nil (Fs _) = error "Ditto"
index (Cons x _) Fz = x
index (Cons _ xs) (Fs n) = index xs n

be rejected, and

index :: Vec n a -> Fin n -> a
index Nil _ = error "damn!"
index (Cons x _) Fz = x
index (Cons _ xs) (Fs n) = index xs n

be accepted (that is, for a Nil in the Vec position, the only valid pattern for the Fin should be _ or a variable).

comment:8 Changed 7 years ago by simonpj

Ok so you are saying that GHC is giving correct messages, but you'd like to see the warning become an error.

I don't think we'll do this:

  • Technically dead GADT case alternatives are not ill-typed. (Just look at any GADT paper.)
  • More pragmatically, GHC can spot some dead code, but not all dead code. Eg
     f x y | x > y  = ...
           | x <= y = ....
           | otherwise = ...dead code...
    
    Even thinking only of type equalities, the solver cannot guarantee to find all unsatisfiable contexts. So it'd be tricky to pin down exactly which programs were errors (and hence would not even compile) and which were only warnings (and hence would run).

All in all, I think it's best as it is. That said, the original bug report of this ticket still stands.

comment:9 Changed 7 years ago by pumpkin

Oh! I see the difference now!

Matching on a GADT constructor introduces a type equality context on the matched variables, but doesn't refine them explicitly, as far as I can tell.

To test this, in addition to the

test :: Fin Nz -> a
test _ = undefined
-- test Fz = undefined -- Rightfully rejected by GHC
-- test (Fs n) = undefined -- Rightfully rejected by GHC

example above, I wrote the following:

test' :: (n ~ Nz) => Fin n -> a
test' Fz = undefined
test' (Fs n) = undefined

It seems like roughly the same thing as test, but GHC happily accepts the Fz and Fs constructors. I see now that that is what matching on Nil does in my original index function, so that is why the seemingly incompatible Fin constructors are accepted!

Anyway, I promise I'll shut up about this now! It had just misunderstood how GADT matching actually refined the types. I'm putting this up here for the benefit of anyone else who might be interested and have the same confusion (a couple of people in the Haskell IRC channel expressed interest in my example). Sorry for the noise :)

comment:10 Changed 7 years ago by Saizan

Replying to simonpj:

Pumpkin, GHC is quite correct in its warnings about your code. If you put in the "error" lines in your code above, then GHC correctly warns that those branches are inaccessible:

T3927b.hs:26:11:
    Inaccessible code in
      a pattern with constructor `Fz', in an equation for `index'
    Couldn't match type `Nz' with `Ns n'
    In the pattern: Fz
    In an equation for `index':
        index Nil Fz
          = error
              "GHC shouldn't even let me write this combination of ..."

but with the latest GHC HEAD that's an error not just a warning (ghci refuses to load the module, at least), so it actually implements what pumpkin is advocating in comment #7

comment:11 Changed 7 years ago by simonpj

Ha ha, how true! Well, I could revert it to a warning, but its somethign of a moot point anyway, and I'm inclined to leave it as it is.

S

comment:12 Changed 7 years ago by simonpj

Milestone: 7.0.17.2.1

There is still improvement to be had here, and I want to get to it, but it's not critical for 7.0.

Simon

comment:13 Changed 7 years ago by patrick_premont

Cc: ppremont@… added

comment:14 Changed 7 years ago by conal

Cc: conal@… added

Here is another example of this problem, which arose in the blog post Fixing lists. This example doesn't appear to be handled correctly in ghc 7.0.1 either. Moreover, I don't think SPJ's "quite correct" remark above (to pumpkin) applies in this case.

{-# LANGUAGE GADTs, KindSignatures, EmptyDataDecls #-}
{-# OPTIONS_GHC -Wall #-}

module Test where

data Z
data S n

infixr 5 :<
data Vec :: * -> * -> * where
  ZVec :: Vec Z a
  (:<) :: a -> Vec n a -> Vec (S n) a

applyV :: Vec n (a -> b) -> Vec n a -> Vec n b
ZVec      `applyV` ZVec      = ZVec
(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)

-- GHC 6.12.3 gives me a warning (with -Wall)

--     Warning: Pattern match(es) are non-exhaustive
--              In the definition of `<*>':
--                  Patterns not matched:
--                      ZVec (_ :< _)
--                      (_ :< _) ZVec

-- Adding the following cases silences the compiler.

-- ZVec `applyV` (_ :< _) = undefined
-- (_ :< _) `applyV` ZVec = undefined

-- However, benmachine found that GHC 7.0.1 balks at these definitions as ill-typed,
-- but also warns of non-exhaustive patterns when the lines are removed.

comment:15 Changed 7 years ago by simonpj

Yes, this is another example of f1 above. And since GHC now rejects inacccessible case branches, you can't even put in the missing cases. Well you can say

_ `applyV` _ = undefined

to suppress the warning.

I wish this was easier to fix. The difficulty is that the type inference engine (which has a sophisticated constraint solver) only sees one equation at a time, and hence can't check exhaustiveness). But the overlap checker (which sees all the equations at once) does not have a sophisticated solver.

Obviously this is fixable with enough work. But annoyingly it needs real work. For example the desugarer could collect constraints, and call the solver to make the check.

To be honest I keep putting this off because it doesn't seem that important, and there are always more important things to do. So keep adding examples to this ticket if you come across them, and adding yourself to the cc list. The more complaints the more likely I am to put off other things to do this one!

comment:16 Changed 7 years ago by sjoerd_visscher

So keep adding examples to this ticket if you come across them, and adding yourself to the cc list.

In the data-category package I constantly run into this. See for example https://github.com/sjoerdvisscher/data-category/blob/master/Data/Category/Boolean.hs

comment:17 Changed 7 years ago by sjoerd_visscher

Cc: sjoerd@… added

comment:18 Changed 7 years ago by sjoerd_visscher

comment:19 Changed 6 years ago by simonpj

difficulty: Unknown
Milestone: 7.4.17.6.1

Punting to 7.6; sorry.

comment:20 Changed 6 years ago by nathanhowell

Cc: nathanhowell@… added

comment:21 Changed 6 years ago by goldfire

Cc: eir@… added

comment:22 Changed 6 years ago by goldfire

comment:23 Changed 5 years ago by ghartshaw

Cc: ghartshaw@… added

comment:24 Changed 5 years ago by jweijers

Cc: jeroen.weijers@… added

comment:25 Changed 5 years ago by igloo

Milestone: 7.6.17.6.2

comment:26 Changed 5 years ago by simonpj

See also #7294

comment:27 Changed 5 years ago by igloo

Milestone: 7.6.27.8.1

comment:28 Changed 5 years ago by WrenThornton

Cc: wren@… added

comment:29 Changed 5 years ago by mcandre

Bump, please fix.

comment:30 Changed 5 years ago by liyang

Cc: hackage.haskell.org@… added

comment:31 Changed 4 years ago by cactus

I was asked about the following program failing to compile. Do you think this is also caused by the same underlying problem?

{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}
{-# LANGUAGE GADTs, TypeFamilies #-}

type family F a
type instance F a = ()

data Foo a where
    FooA :: Foo ()
    FooB :: Foo Int

f :: a -> Foo (F a) -> ()
f _ FooA = ()

The error/warning is, of course:

gadt-incomplete.hs:12:1: Warning:
    Pattern match(es) are non-exhaustive
    In an equation for `f': Patterns not matched: _ FooB

comment:32 Changed 4 years ago by cactus

Cc: gergo@… added

comment:33 Changed 4 years ago by simonpj

Yes, I think it's the same thing, though this time you have do some type-family rewrites too, to see that the patterns are exhaustive.

Simon

comment:34 Changed 4 years ago by thoughtpolice

Milestone: 7.8.37.10.1

Bumping priority down (these tickets haven't been closely followed or fixed in 7.4), and moving out to 7.10 and out of 7.8.3.

comment:35 Changed 4 years ago by thoughtpolice

Priority: highnormal

Actually dropping priority. :)

comment:36 Changed 4 years ago by ulfn

Cc: ulf.norell@… added

Changed 3 years ago by merijn

Attachment: test.hs added

Test case exhibiting wrong exhaustiveness checks that SPJ asked me to attach.

comment:37 Changed 3 years ago by vlopez

Cc: victor@… added

comment:38 Changed 3 years ago by vlopez

Instead of fixing the exhaustiveness checker, we could have some way to tell the compiler that a particular branch in a case expression (or function definition) is inaccessible.

A possible syntax for this would be an "empty guard" (a vertical bar immediately followed by a semicolon).

data T a where
  T1 :: T Int
  T2 :: T Bool

f1 :: T a -> T a -> Bool
f1 T1 T1 = True
f1 T2 T2 = False
f1 T1 T2 |; -- absurd branch
f1 T2 T1 |; -- another absurd branch

f2 :: T a -> T a -> Bool
f2 a b = case (a,b) of
    (T1, T1) -> True
    (T2, T2) -> False
    (T1, T2) |;
    (T2, T1) |;
  • In GHC 7.8.3, it results in an immediate parser error at the ;, so it shouldn't conflict with other features.
  • It works well with the indentation heuristics in emacs haskell-mode (and hopefully with other editors too).

comment:39 Changed 3 years ago by nh2

I'm having the same problem, -Wall reporting Patterns not matched: Step _ (End _) for some code but if I put that match in, I get Inaccessible code in a pattern with constructor.

comment:40 Changed 3 years ago by simonpj

Cc: george.karachalias@… added

Happily, George K is working on this: see PatternMatchCheck

Last edited 3 years ago by simonpj (previous) (diff)

comment:41 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:42 Changed 2 years ago by thomie

Resolution: duplicate
Status: newclosed

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:43 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:44 Changed 2 years 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.