[Agda] Help with stuck unification/intrinsic typing in general

[Daniel Lee]

Hi all,

I'm super new to Agda and the Agda community. Hopefully this is the right
place to ask something like this, but please call me out if it isn't.


I'm working on an Agda development for a QTT formalization. I'm trying to
use an intrinsically typed representation for terms, but run into
unification issues when trying to define substitution.

Substitution:
[image: Screen Shot 2020-09-30 at 8.34.38 PM.png]

Error message:
[image: Screen Shot 2020-09-30 at 8.34.50 PM.png]

Application def:
[image: Screen Shot 2020-09-30 at 8.35.05 PM.png]

I'm sort of at a loss for how to get around this. Is the issue because of
the functions in the return type?

More broadly, it seems like intrinsic typing is the Agda way of doing
things, and gives a lot for free. And it works really well in the STLC
example given in the PLFA textbook. But for a more complicated type system
like this, I'm starting to think it might be easier to use extrinsic
typing? I've also had to rely on the REWRITE pragma which I just learned
isn't allowed in --safe due to potential non-convergence.
Does someone maybe have experience with this and could speak to pros/cons
of using intrinsic vs extrinsic typing here?

Thanks,
Daniel
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200930/b81e1ca9/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2020-09-30 at 8.34.38 PM.png
Type: image/png
Size: 9933 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200930/b81e1ca9/attachment.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2020-09-30 at 8.34.50 PM.png
Type: image/png
Size: 24441 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200930/b81e1ca9/attachment-0001.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2020-09-30 at 8.35.05 PM.png
Type: image/png
Size: 8827 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200930/b81e1ca9/attachment-0002.png>