<div dir="ltr"><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="font-size:12.8px">What if "t = Nat"?</span></blockquote><div><br></div><div>So in this case "u" is solvable both as "\x -> x" and "\_ -> Nat", right, which is no good? I think I get it.</div><div><span style="font-size:12.8px"><br></span></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="font-size:12.8px">The occurs check is implemented in Agda.TypeChecking.MetaVars.</span><wbr style="font-size:12.8px"><span style="font-size:12.8px">Occurs [1], and is called before solving a meta in Agda</span></blockquote><div><br></div><div>I did not meant the usual occurs check or the pruning on the right hand side. I meant that we have meta "u" with type "Delta -> A", and we have "u [ sigma ] = t" to be solved, and in this case what if "u" occurs in its own "A [ sigma ]" type? In the link I sent, around the end of the slides, Pientka talks about this kind of occurs check, and concludes that "u" cannot occur in its own return type if we have an ordered metacontext where solutions for a meta can only depend on metas declared to the left. This is the kind of occurs check I couldn't find in the Agda sources, but I also don't think Agda has ordered metacontexts. Does this mean that self-type occurrence is not possible either with unordered metacxt as well? </div></div><div class="gmail_extra"><br><div class="gmail_quote">2016-11-28 7:10 GMT+01:00 Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote"><span class="">On Sun, Nov 27, 2016 at 4:22 PM, András Kovács <span dir="ltr"><<a href="mailto:kovacsahun@hotmail.com" target="_blank">kovacsahun@hotmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">I'm learning about pattern unification, and I have a couple of questions.<div><br></div><div>First, in Agda, are types irrelevant for the purpose of unification, and if not, why? I mean the following: suppose we have "u [ Nat ] = t", where "u" is a meta, "[ Nat ]" is a substitution with one entry which is the "Nat" type. Can we solve "u" as "\_ -> t"? No Agda terms can branch on types in any way, so this seems correct at least on the first look, but I'm not sure if this breaks something.</div></div></blockquote><div> </div></span><div>What if "t = Nat"? One could certainly imagine restrictions on "t" that would make it safe, but we don't do anything like that at the moment. I suspect constraints like that are not very common in practise.</div><span class=""><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Second, does Agda do occurs check for the type of the meta to be solved? I couldn't find it (as of now) in the sources. Pientka writes <a href="http://wips.cs.umn.edu/slides/pientka.pdf" target="_blank">here</a> that ordered metacontexts make occurs checks for types unnecessary. As far as I saw in the sources Agda has no ordered contexts (and no reshuffling of contexts like in ch. 4 of Adam Gundry's thesis).<br></div></div></blockquote><div><br></div></span><div>The occurs check is implemented in Agda.TypeChecking.MetaVars.<wbr>Occurs [1], and is called before solving a meta in Agda.TypeChecking.MetaVars [2]. It also does pruning; removing impossible variable dependencies from metas in the right hand side. For instance given a constraint "U [x] = c (V [x, y])" for metas "U" and "V" and constructor "c", we can conclude that "V" cannot depend on "y" and solve it by "V [x, _] := W [x]" for a fresh meta "W". This then lets us solve "U [x] := c (W [x])".</div><div><br></div><div>/ Ulf</div><div><br></div><div>[1] <a href="https://github.com/agda/agda/blob/509d481/src/full/Agda/TypeChecking/MetaVars/Occurs.hs" target="_blank">https://github.com/agda/<wbr>agda/blob/509d481/src/full/<wbr>Agda/TypeChecking/MetaVars/<wbr>Occurs.hs</a></div><div>[2] <a href="https://github.com/agda/agda/blob/509d481/src/full/Agda/TypeChecking/MetaVars.hs#L683" target="_blank">https://github.com/agda/<wbr>agda/blob/509d481/src/full/<wbr>Agda/TypeChecking/MetaVars.hs#<wbr>L683</a></div></div></div></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>