<div dir="ltr">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. <br><br>I found <a href="https://doisinkidney.com/posts/2018-09-20-agda-tips.html">https://doisinkidney.com/posts/2018-09-20-agda-tips.html</a> 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:<div><br></div><div>...<font face="monospace">→ c {Δ₁} {Δ₂} (Δ₁ ++ Δ₂)</font> </div><div><br></div><div>prefer:</div><div><br></div><div><font face="monospace">...→ c {Δ₁} {Δ₂} {Δ} (Appending Δ₁ Δ₂ Δ)</font><br><br>I also found this passage from Ulf Norell's thesis (<a href="http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf">http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf</a> 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."<br><br>Small example:<br><br><font face="monospace">open import Data.Nat<br><br>postulate f : ℕ → ℕ<br><br>data Ex : ℕ → Set where<br>  c : {n : ℕ} → Ex (f n)<br><br>g : ∀ {A} → Ex A → ℕ<br>g {zero} ex = { }0<br>g {suc A} ex = { }1</font><div><br></div><div>Case-split on ex gives the "I'm not sure..." with the unifier stuck on <font face="monospace">f n ≟ zero </font><font face="arial, sans-serif">or</font><font face="monospace"> f n ≟ suc A₁. </font></div><div><br>What goes wrong if I were allowed to split on ex to get <font face="monospace">(c {n})</font>? <font face="arial, sans-serif"> 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. </font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">If the split were allowed instead, I could even imagine somehow getting to use </font><font face="monospace">f n ≡ ... </font><font face="arial, sans-serif">on the right</font> , something akin to a <font face="monospace">with_in_</font>.</div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif"><br></font><div><br></div></div></div></div>