<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Nov 27, 2016 at 4:22 PM, András Kovács <span dir="ltr">&lt;<a href="mailto:kovacsahun@hotmail.com" target="_blank">kovacsahun@hotmail.com</a>&gt;</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&#39;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 &quot;u [ Nat ] = t&quot;, where &quot;u&quot; is a meta, &quot;[ Nat ]&quot; is a substitution with one entry which is the &quot;Nat&quot; type. Can we solve &quot;u&quot; as &quot;\_ -&gt; t&quot;? No Agda terms can branch on types in any way, so this seems correct at least on the first look, but I&#39;m not sure if this breaks something.</div></div></blockquote><div> </div><div>What if &quot;t = Nat&quot;? One could certainly imagine restrictions on &quot;t&quot; that would make it safe, but we don&#39;t do anything like that at the moment. I suspect constraints like that are not very common in practise.</div><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&#39;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&#39;s thesis).<br></div></div></blockquote><div><br></div><div>The occurs check is implemented in Agda.TypeChecking.MetaVars.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 &quot;U [x] = c (V [x, y])&quot; for metas &quot;U&quot; and &quot;V&quot; and constructor &quot;c&quot;, we can conclude that &quot;V&quot; cannot depend on &quot;y&quot; and solve it by &quot;V [x, _] := W [x]&quot; for a fresh meta &quot;W&quot;. This then lets us solve &quot;U [x] := c (W [x])&quot;.</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">https://github.com/agda/agda/blob/509d481/src/full/Agda/TypeChecking/MetaVars/Occurs.hs</a></div><div>[2] <a href="https://github.com/agda/agda/blob/509d481/src/full/Agda/TypeChecking/MetaVars.hs#L683">https://github.com/agda/agda/blob/509d481/src/full/Agda/TypeChecking/MetaVars.hs#L683</a></div></div></div></div>