[Agda] Why disallow case splits that involve impossible unification

[James Smith]

This is probably a dumb beginner question. Out of curiosity, I'm trying to
understand the "why" of the "I'm not sure if there should be a case for the
constructor" error.

I found https://doisinkidney.com/posts/2018-09-20-agda-tips.html and "How
to Keep Your Neighbors In Order" which give the "what" of the end-user
solution, which seems to be to express desired relations purely in datatype
constructions/proofs rather than use functions. For example, instead of:

...→ c {Δ₁} {Δ₂} (Δ₁ ++ Δ₂)

prefer:

...→ c {Δ₁} {Δ₂} {Δ} (Appending Δ₁ Δ₂ Δ)

I also found this passage from Ulf Norell's thesis (
http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf p.33–35) which I think
is referring to this same issue: "If A = suc n 􏰂 suc m then the leqZero
constructor cannot be used to construct an element of A, so splitting only
generates a single new context where x has been instantiated with an
application of leqSuc. If, on the other hand, A = f n 􏰂 m for some defined
function f we cannot tell which constructors are legal and so splitting
along x is not possible." ... "In some cases it might be possible to tell,
but rather than resorting to complicated heuristics we chose the simpler
approach of refusing to split."

Small example:

open import Data.Nat

postulate f : ℕ → ℕ

data Ex : ℕ → Set where
  c : {n : ℕ} → Ex (f n)

g : ∀ {A} → Ex A → ℕ
g {zero} ex = { }0
g {suc A} ex = { }1

Case-split on ex gives the "I'm not sure..." with the unifier stuck on f n
≟ zero or f n ≟ suc A₁.

What goes wrong if I were allowed to split on ex to get (c {n})?  I can see
that I might be forced to write code to handle some impossible cases, e.g.
if f was equivalent to suc, I could be forced to either extrinsically prove
the zero case is impossible, or write some useless code.

If the split were allowed instead, I could even imagine somehow getting to
use f n ≡ ... on the right , something akin to a with_in_.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210810/c9e40395/attachment.html>