Opened 4 years ago

Closed 4 years ago

#11390 closed bug (invalid)

GHC does not warn about redundant patterns

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.1
Keywords: warnings, PatternMatchWarnings Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by rwbarton)

Given the Phab:D1535 effort in GHC 8.0 I was curious how an example from Richard's post What are type families? would fare:

% ghci -Wall -XTypeFamilies -ignore-dot-ghci
GHCi, version 8.1.20160105: http://www.haskell.org/ghc/ :? for help
Prelude> :set +m
Prelude> type family F1 a where
Prelude| F1 Int = Bool
Prelude|
Prelude> let
Prelude| sillyId :: F1 Char -> F1 Char
Prelude| sillyId x = x
Prelude|
Prelude>

This seems to fly, even though as the blog post noted, ”[...] sillyId can’t ever be called on a value.” Isn't the clause redundant and should be defined using EmptyCase (#2431) as sillyId = \case? It seems GHC doesn't care that the pattern match in the equation absurd2 _ = ... is redundant either:

data Void
absurd1 :: Void -> a
absurd1 = \case
absurd2 :: Void -> a
absurd2 _ = undefined

Is this intended or known behaviour?

Change History (15)

comment:1 Changed 4 years ago by Iceland_jack

Summary: GHC does not warn about redundant equationsGHC does not warn about redundant patterns

comment:2 Changed 4 years ago by Iceland_jack

Description: modified (diff)

comment:3 Changed 4 years ago by rwbarton

Empty data declarations are Haskell 2010, so it doesn't seem reasonable to give a warning that suggests something outside the Haskell 2010 language. If EmptyCase is already on, though, it could make sense to issue a warning in your second example.

I don't understand your first example. Isn't the clause sillyId x = case x of {} just as "redundant" as the clause sillyId x = x was in the first place?

comment:4 Changed 4 years ago by Iceland_jack

I thought case x of {} indicated to the compiler that the clause is empty (Empty case alternative)

comment:5 Changed 4 years ago by rwbarton

I would say that case x of {} is just a case expression with no alternatives. It is, itself, still an ordinary expression. So both versions look like sillyId x = <expr> and should be equivalent as far as redundancy of the outer pattern match, the one done by sillyId, is concerned. Since you cannot write a definition with 0 equations, this "redundancy" is unavoidable. (Unless you use LambdaCase and EmptyCase, I guess.)

Are you suggesting treating case x of {} as some kind of special form?

Also, I'm not sure a "stuck" type family application is really empty in the same sense as an empty data type. But #10746 makes it hard to tell what GHC thinks about this.

comment:6 Changed 4 years ago by Iceland_jack

I thought that was what the documentation for EmptyCase is alluding to:

With dependently-typed features it is more useful (see Trac #2431). For example, consider these two candidate definitions of absurd:

data a :==: b where
  Refl :: a :==: a

absurd :: True :~: False -> a
absurd x = error "absurd"    -- (A)
absurd x = case x of {}      -- (B)

We much prefer (B). Why? Because GHC can figure out that (True :~: False) is an empty type. So (B) has no partiality and GHC should be able to compile with -Wincomplete-patterns. (Though the pattern match checking is not yet clever enough to do that.) On the other hand (A) looks dangerous, and GHC doesn’t check to make sure that, in fact, the function can never get called.

I wasn't sure whether the "Though the pattern match checking is not yet clever enough to do that." statement had changed in 8, I'll edit the code to enable LambdaCase as well.

comment:7 Changed 4 years ago by Iceland_jack

Description: modified (diff)

comment:8 Changed 4 years ago by rwbarton

Description: modified (diff)

The manual there is talking about partiality, or completeness of pattern matches, not redundancy. (B) is complete because the pattern match in absurd is complete, and the pattern match in the case is also complete. But the pattern match in absurd is "redundant", regardless of what happens on the right-hand side of the equation.

comment:9 Changed 4 years ago by simonpj

Keywords: PatternMatchWarnings added

comment:10 Changed 4 years ago by gkaracha

Actually nothing is redundant in the above examples. As we discuss in the paper (section about laziness), (sillyId undefined) will give you the right hand-side so the clause:

sillyId x = x

is not redundant at all. Of course, this is not the case for:

sillyId2 :: F1 Char -> F1 Char
sillyId2 (!x) = x

because it is strict in the argument, so no WHNF can have the type F1 Char. But even in this case, the clause is not actually redundant, it just has an inaccessible RHS (remember this is not Agda). Pattern matching is not just used for discrimination in Haskell but also for evaluation, which I see as a side effect. Hence, the clause may have an inaccessible RHS, but by removing it the expression is not evaluated and you change the semantics of sillyId2.

comment:11 Changed 4 years ago by rwbarton

Good point. If the return type was a type with values, the clause would really not be redundant!

sillyFun :: F1 Char -> String
sillyFun x = "hi"

Surely it doesn't make sense for redundancy of a pattern match to depend on what sort of thing is on the right hand side?

comment:12 Changed 4 years ago by goldfire

I agree with George (gkaracha). sillyId x = x can't be called on a value, but Haskell isn't call-by-value. I will use Void instead of F1 Char, because the type family bit isn't the interesting part here.

silly1 :: Void -> Void
silly1 x = x

silly2 :: Void -> Void
silly2 x = error "urk"

silly1 undefined and silly2 undefined have different runtime behavior; the pattern is not redundant.

comment:13 Changed 4 years ago by rwbarton

In that case, GHC's behavior is correct and we can close this ticket, right?

comment:14 Changed 4 years ago by gkaracha

Yes, I think we can close this :-)

comment:15 Changed 4 years ago by gkaracha

Resolution: invalid
Status: newclosed
Note: See TracTickets for help on using tickets.