<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><br></div><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">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).</div><div><br></div><div>Thanks</div><div>András Kovács</div><div><br></div><div><b><br></b></div></div>