Pattern alternative binding empty type does not cause redundant alternative warning

[lovely-error]

So, lean has coverage checking in pattern-matching, e.g. this code...

def v : Option Bool -> Bool
| .none => false
-- | .some _ => true

...does not get accepted and missing case is reported. Good!

Lets now consider a slightly different definition:

def v' : Option Empty -> Bool
| .none => false

This one is considered correct by lean, no errors about missing cases are reported.
However, if I add another pattern to this definition...

def v' : Option Empty -> Bool
| .none => false
| .some _ => true -- offending pattern

...it still gets accepted without a warning. The redundant pattern is not reported as such!

This means that matches on empty types are redundant, but the helpful warning does not appear.

It would be helpful if it would, if possible.

[nomeata]

Thanks for your report. I believe the current behavior is correct: for Option Empty, there cannot be a value of the form .some x (what should x be?), so the pattern is inaccessible and thus redundant.

Note that Empty is not like C's void and unlike Haskell we don't have lazy values.

If you are unsure about this I suggest you bring this up on the community Zulip.

[lovely-error]

Thanks for your report. I believe the current behavior is correct: for Option Empty, there cannot be a value of the form .some x (what should x be?), so the pattern is inaccessible and thus redundant.

This is what I was saying!

The following is considered a hard error in lean: third case is considered redundant

def c : Bool -> Unit
| true => ()
| false => ()
| _ => ()

In this code, however, I can add or remove last pattern at will.

def v' : Option Empty -> Bool
| .none => false
| .some _ => true -- this should be reported as hard error

Did I actually fail to convey this? 👀

[nomeata]

Ah, yes, I think I misunderstood your issue indeed. Sorry! I think you are right that there is something unexpecting about leans behavior here.

I guess the current implementation has its reasons. After all, it's ok to bind x to Empty, e.g. as a direct parameters and then use by contradiction. And maybe the pattern match checked doesn't look into such nested types when they are not actually matched. Or maybe it's just too expensive to check every pattern for empty types in the pattern.

But I agree that it's reasonable to expect that an alternative that can be omitted is warned about, and we can keep this issue for it.

[nomeata]

I took the library of tweaking the issue description and title a bit. Thanks for your report!

[david-christiansen]

I agree that this is confusing.

There is a fundamental issue here. In general, we cannot decide whether a pattern is redundant - I can define a type whose constructor is a witness of the truth of the Collatz conjecture, for instance. This means that checking pattern coverage is, at the end of the day, an approximation.

When the user omits a pattern for a given constructor, our task is to try to prove that this constructor was impossible. Here, we want an under-approximation - it's OK to make a user write a proof that a case was impossible, but we can't accept Lean missing a case that actually is possible. The elaboration to eliminators checks our work here.

When a user does write a pattern for a constructor, we want an over-approximation. It'd be terrible to prevent the use of a constructor that's actually possible, but it's not the end of the world to allow a provably superfluous but otherwise type-correct constructor that the user then must write a manual proof about.

I'd characterize this issue as Lean not preventing you from manually writing a proof that it could otherwise build automatically, but the UI certainly doesn't make it clear that this is what's going on.

We're in the realm of two undecidable analyses meeting in a gray area. It's good for them to agree often, especially in simply-typed cases like this one, but perfection is unachievable.

[nomeata]

Right! But why unachievable?

In the example above lean is perfectly happy if you omit the case, so it is able to determine that the case wasn't needed! So, superficially, why can't it use whatever logic is at work to warn the user about it?

My (blind) guess is that when the user omits a clause lean tries harder to prove that this is ok (maybe using by contradiction), and maybe that's possibly expensive, and so we don't do it in classes that are present, and only a cheaper check for redundancy is used to trigger the warning.

[david-christiansen]

Right! But why unachievable?

Perfection is unachievable here, but we could absolutely give better errors/warnings/lints for this particular situation, as well as many related ones. No question about that!

[nomeata]

Sorry, what I meant was: perfection of recognizing unreachable branches is of course unachievable. But showing a warning exactly about those branches that you could omit without lean complaining is certainly achievable, isn't it?

[digama0]

I think there are good reasons to preserve the current lean behavior. If you have a macro that generates

def foo : Option $type -> Nat
  | none => 0
  | some x => 1

it should not suddenly become a type error if we substitute $type to be Empty. The user is allowed to write pattern matches containing pattern variables which can be (but are not currently) pattern matched further. In fact, this can be undesirable, since pattern matching an expression further makes the intermediate results no longer available as equations (although for an example like this where one of the variables is trivially empty this is probably not as relevant).

That said, it would be reasonable to have a linter that points out when a given pattern can safely be removed because it is refutable by lean, although it may be expensive.

[nomeata]

Interesting, “redundant alternative” is actually an error, not a warning (which could be turned off for generated code) as I expected. I guess warnings and linters are not that difficult.

Anyways, even if there is something that can be improved here, it's probably not pressing. We can keep the issue to refer to should this come up again

[mik-jozef]

I'd like to point out this can also arise without an empty type, if certain branches are known by Lean to be impossible:

inductive T (n: Nat)
| a (_: n = 3)
| b (_: n = 4)

def T.foo (t: T 3): True :=
  match t with
  | a _ => trivial -- accepted

def T.fooUnnecessary (t: T 3): True :=
  match t with
  | a _ => trivial
  | b _ => trivial -- accepted, but redundant

At least in my experience, it has happened in practice that such a warning would have saved me time as a user, because I did not always realize Lean could automatically handle an impossible branch for me.