Opened 11 days ago

Last modified 11 days ago

#13964 new bug

Pattern-match warnings for datatypes with COMPLETE sets break abstraction

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1-rc2
Keywords: PatternSynonyms, PatternMatchWarnings Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Here's a file:

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Bug (Boolean(F, TooGoodToBeTrue), catchAll) where

data Boolean = F | T
  deriving Eq

pattern TooGoodToBeTrue :: Boolean
pattern TooGoodToBeTrue <- ((== T) -> True)
  where
    TooGoodToBeTrue = T
{-# COMPLETE F, TooGoodToBeTrue #-}

catchAll :: Boolean -> Int
catchAll F               = 0
-- catchAll TooGoodToBeTrue = 1

If you compile this with -Wall, the warning will warn about T, not TooGoodToBeTrue (the other conlike in the COMPLETE set):

$ /opt/ghc/8.2.1/bin/ghc -fforce-recomp -Wall Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:15:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘catchAll’: Patterns not matched: T
   |
15 | catchAll F               = 0
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Perhaps this isn't so bad, since it's intra-module. But the problem persists even across modules:

module Foo where

import Bug

catchAll2 :: Boolean -> Int
catchAll2 F               = 0
-- catchAll2 TooGoodToBeTrue = 1
$ /opt/ghc/8.2.1/bin/ghc -fforce-recomp -c Bug.hs
$ /opt/ghc/8.2.1/bin/ghc -fforce-recomp -c -Wall Foo.hs

Foo.hs:6:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘catchAll2’: Patterns not matched: Bug.T
  |
6 | catchAll2 F               = 0
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This one is really bad, since it's warning about Bug.T, which should be hidden!

Change History (3)

comment:1 Changed 11 days ago by RyanGlScott

Version: 8.0.18.2.1-rc2

comment:2 Changed 11 days ago by mpickering

This is nothing unique to COMPLETE pragmas, the exhaustiveness checker already breaks abstraction in this way.

For example:

module T (D(A)) where

data D = A | B
module M where

import T

foo A = ()

warns with

M.hs:5:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘foo’: Patterns not matched: T.B
  |
5 | foo A = ()
  | 

and after all, to retain safety it has to. A function exported by T could mention B and then be used in M.

comment:3 in reply to:  2 Changed 11 days ago by RyanGlScott

Perhaps I'm fundamentally misunderstanding something about COMPLETE sets, but this doesn't feel like a very satisfying explanation. My intuition is that specifying a COMPLETE set for a data type is tantamount to overriding the pattern match exhaustiveness checker's behavior w.r.t. to that particular data type, and as such, I would any warnings that are emitted under the -Wincomplete-patterns label to be adjusted according to whatever COMPLETE sets are in scope. For example, in my original example, I would simply expect that in this warning:

Foo.hs:6:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘catchAll2’: Patterns not matched: Bug.T

It would warn about TooGoodToBeTrue, not Bug.T. That's all.

Replying to mpickering:

This is nothing unique to COMPLETE pragmas, the exhaustiveness checker already breaks abstraction in this way.

For example:

module T (D(A)) where

data D = A | B
module M where

import T

foo A = ()

warns with

M.hs:5:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘foo’: Patterns not matched: T.B
  |
5 | foo A = ()
  | 

That seems fine to me, since the user didn't specify {-# COMPLETE A #-} for the data type D. If she did, I wouldn't expect a warning for foo.

and after all, to retain safety it has to. A function exported by T could mention B and then be used in M.

I don't understand what you mean. A function exported from T surely doesn't have any effect on whether a function defined in M is exhaustive, right?

Note: See TracTickets for help on using tickets.