Does not accept a simple impossible case

[spcfox]

Steps to Reproduce

data NatEq : Nat -> Nat -> Type where
  Z : NatEq Z Z
  S : NatEq n m -> NatEq (S n) (S m)

foo : NatEq 1 2 -> Void
foo _ impossible

Expected Behavior

Successful type checking

Observed Behavior

Error: foo _ is not a valid impossible case.

Main:6:1--6:17
 2 |   Z : NatEq Z Z
 3 |   S : NatEq n m -> NatEq (S n) (S m)
 4 | 
 5 | foo : NatEq 1 2 -> Void
 6 | foo _ impossible
     ^^^^^^^^^^^^^^^^

Details

This is not a bug, because we do not expect compiler to be able to infer that a case is impossible in all situations. However, I think this example is sufficiently trivial that it would be nice if the compiler could handle it.

For NatEq 0 1 it cannot find a matching constructor, but for NatEq 1 2 it does find one, and it does not check whether its arguments are inhabited.

[buzden]

My opinion is when, roughly speaking, compiler is able to %search Nat 2 1, then it should be able to prove impossibility of Nat 1 2

[dunhamsteve]

It seems like it could be exponential if we start recursing on these arguments, unless we've got some heuristics to help (e.g. return "don't know" if there are multiple candidates and maybe limit depth).

Given other issues we have with impossible, I suspect Agda may have a better approach by asking the user to expand the LHS and point out the empty bit with (). If we do drill down in Idris it does sort this case out:

foo : NatEq 1 2 -> Void
foo (S _) impossible

But doing that would be painful with something like NatEq 42 51 -> Void.

[gallais]

I suspect Agda may have a better approach by asking the user to expand the LHS and point out the empty bit with ().

💯

But doing that would be painful with something like NatEq 42 51 -> Void.!

Which is a good hint that one should prove a general theorem and deploy it rather than trying to insert more (costly) automation.