[Agda] Questions about unification

[András Kovács]

I'm learning about pattern unification, and I have a couple of questions.

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.

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 here
<http://wips.cs.umn.edu/slides/pientka.pdf> 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).

Thanks
András Kovács
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161127/df0ec365/attachment.html