<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">That got me a little further, thanks.
But, of course, my situation has an expression that appears in the
type of another variable expression. [Why did this work pre-2.5
? Were there bugs here?]<br>
<br>
Jacques<br>
<br>
On 2016-11-09 01:17 , Ulf Norell wrote:<br>
</div>
<blockquote
cite="mid:CAJjNqYGRKto3CRq8MtH8Y-49EjHX6GOzO1VRc8YBG1zR=wEVyQ@mail.gmail.com"
type="cite">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<div dir="ltr">The problem in the example is that the expression
you abstract over (fst p) appears
<div>in the type of another (non-variable) expression (snd p).
The fix is to also abstract</div>
<div>over the second expression:</div>
<div><br>
</div>
<div>
<div>good-with : (p : Σ A B) → H (fst p) (snd p)</div>
<div>good-with p with fst p | snd p</div>
<div>... | x | y = {!!}</div>
</div>
<div><br>
</div>
<div>/ Ulf</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Tue, Nov 8, 2016 at 11:24 PM,
Jacques Carette <span dir="ltr"><<a moz-do-not-send="true"
href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">The page <a
moz-do-not-send="true"
href="https://agda.readthedocs.io/en/latest/language/with-abstraction.html"
rel="noreferrer" target="_blank">https://agda.readthedocs.io/en<wbr>/latest/language/with-abstract<wbr>ion.html</a>
is extremely informative (thanks!), but the subsection <a
moz-do-not-send="true"
href="https://agda.readthedocs.io/en/latest/language/with-abstraction.html#ill-typed-with-abstractions"
rel="noreferrer" target="_blank">https://agda.readthedocs.io/en<wbr>/latest/language/with-abstract<wbr>ion.html#ill-typed-with-<wbr>abstractions</a>
is a bit problematic in that it leaves off the most
important part: how to fix it!<br>
<br>
This is motivated by a real breakage (still the categories
library). Try as I might, I simply cannot hand-write the
correct "with" incantation to fix the one that used to work
pre-2.5, and now is broken [1]. The example is very much
like the one in the documentation linked to above, just
"more so" in that there are many more type-level
dependencies.<br>
<br>
If someone could hand-write the correct helper function that
fixes the documentation, hopefully that would be a big
enough hint that I can figure this out myself.<br>
<br>
Jacques<br>
<br>
[1] last line of <a moz-do-not-send="true"
href="https://github.com/copumpkin/categories/blob/master/Categories/NaturalIsomorphism.agda"
rel="noreferrer" target="_blank">https://github.com/copumpkin/c<wbr>ategories/blob/master/Categori<wbr>es/NaturalIsomorphism.agda</a>
for those who are curious.<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a moz-do-not-send="true"
href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a moz-do-not-send="true"
href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote>
</div>
<br>
</div>
</blockquote>
<p><br>
</p>
</body>
</html>