<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">There is already a problem in your example. If split is allowed in this case, then you will obtain
</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">G {zero} (c {n}) = ?</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">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.</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:james.smith.69781@gmail.com">James Smith</a><br>
<b>Sent: </b>Tuesday, August 10, 2021 8:05 PM<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>
<b>Subject: </b>[Agda] Why disallow case splits that involve impossible unification</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal">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:<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">...<span style="font-family:"Courier New"">→ c {Δ</span><span style="font-family:"Cambria Math",serif">₁</span><span style="font-family:"Courier New"">} {Δ</span><span style="font-family:"Cambria Math",serif">₂</span><span style="font-family:"Courier New"">}
(Δ</span><span style="font-family:"Cambria Math",serif">₁</span><span style="font-family:"Courier New""> ++ Δ</span><span style="font-family:"Cambria Math",serif">₂</span><span style="font-family:"Courier New"">)</span> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">prefer:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Courier New"">...→ c {Δ</span><span style="font-family:"Cambria Math",serif">₁</span><span style="font-family:"Courier New"">} {Δ</span><span style="font-family:"Cambria Math",serif">₂</span><span style="font-family:"Courier New"">}
{Δ} (Appending Δ</span><span style="font-family:"Cambria Math",serif">₁</span><span style="font-family:"Courier New""> Δ</span><span style="font-family:"Cambria Math",serif">₂</span><span style="font-family:"Courier New""> Δ)</span><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>
<span style="font-family:"Courier New"">open import Data.Nat<br>
<br>
postulate f : </span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""> →
</span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""><br>
<br>
data Ex : </span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""> → Set where<br>
c : {n : </span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New"">} → Ex (f n)<br>
<br>
g : </span><span style="font-family:"Cambria Math",serif">∀</span><span style="font-family:"Courier New""> {A} → Ex A →
</span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""><br>
g {zero} ex = { }0<br>
g {suc A} ex = { }1</span><o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Case-split on ex gives the "I'm not sure..." with the unifier stuck on <span style="font-family:"Courier New"">f n
</span><span style="font-family:"Cambria Math",serif">≟</span><span style="font-family:"Courier New""> zero
</span><span style="font-family:"Arial",sans-serif">or</span><span style="font-family:"Courier New""> f n
</span><span style="font-family:"Cambria Math",serif">≟</span><span style="font-family:"Courier New""> suc A</span><span style="font-family:"Cambria Math",serif">₁</span><span style="font-family:"Courier New"">. </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><br>
What goes wrong if I were allowed to split on ex to get <span style="font-family:"Courier New"">
(c {n})</span>? <span style="font-family:"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. </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-family:"Arial",sans-serif">If the split were allowed instead, I could even imagine somehow getting to use
</span><span style="font-family:"Courier New"">f n ≡ ... </span><span style="font-family:"Arial",sans-serif">on the right</span> , something akin to a
<span style="font-family:"Courier New"">with_in_</span>.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>