[Agda] Ill-typed with construction

[Jacques Carette]

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?]

Jacques

On 2016-11-09 01:17 , Ulf Norell wrote:
> 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 
> <mailto:carette at mcmaster.ca>> wrote:
>
>     The page
>     https://agda.readthedocs.io/en/latest/language/with-abstraction.html
>     <https://agda.readthedocs.io/en/latest/language/with-abstraction.html>
>     is extremely informative (thanks!), but the subsection
>     https://agda.readthedocs.io/en/latest/language/with-abstraction.html#ill-typed-with-abstractions
>     <https://agda.readthedocs.io/en/latest/language/with-abstraction.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/categories/blob/master/Categories/NaturalIsomorphism.agda
>     <https://github.com/copumpkin/categories/blob/master/Categories/NaturalIsomorphism.agda>
>     for those who are curious.
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161109/d3ea847d/attachment.html