[Agda] Why disallow case splits that involve impossible unification

[Jason Hu]

There is already a problem in your example. If split is allowed in this case, then you will obtain

G {zero} (c {n}) = ?

For some n. However, that is the same as solving f n = zero for a postulated `f`. This is what the system tells you: it cannot solve f n = zero.


From: James Smith<mailto:james.smith.69781 at gmail.com>
Sent: Tuesday, August 10, 2021 8:05 PM
To: agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>
Subject: [Agda] Why disallow case splits that involve impossible unification

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/20210811/47c89b2d/attachment.html>