GHC does not warn about redundant patterns

Given the 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 (closed)) 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?

mentioned in issue #9182

changed weight to 5

added Tbug Trac import error messages labels

changed title from GHC does not warn about redundant equations to GHC does not warn about redundant patterns

changed the description

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?

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

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 (closed) makes it hard to tell what GHC thinks about this.

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

With dependently-typed features it is more useful (see Trac #2431 (closed)). 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.

changed the description

changed the description

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.

removed error messages label

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.

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?

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.

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

Yes, I think we can close this :-)

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

mentioned in issue #11806 (closed)

added error messages label

added Pnormal label

added pattern match warnings label