[Agda] Ill-typed with construction

[Ulf Norell]

The problem in the example is that the expression you abstract over (fst p)
appears
in the type of another (non-variable) expression (snd p). The fix is to
also abstract
over the second expression:

good-with : (p : Σ A B) → H (fst p) (snd p)
good-with p with fst p | snd p
...            | x | y = {!!}

/ Ulf

On Tue, Nov 8, 2016 at 11:24 PM, Jacques Carette <carette at mcmaster.ca>
wrote:

> The page https://agda.readthedocs.io/en/latest/language/with-abstract
> ion.html is extremely informative (thanks!), but the subsection
> https://agda.readthedocs.io/en/latest/language/with-abstract
> ion.html#ill-typed-with-abstractions is a bit problematic in that it
> leaves off the most important part: how to fix it!
>
> 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.
>
> 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.
>
> Jacques
>
> [1] last line of https://github.com/copumpkin/c
> ategories/blob/master/Categories/NaturalIsomorphism.agda for those who
> are curious.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161109/9c1c7cb7/attachment.html