[Agda] Questions about unification

[Ulf Norell]

On Sun, Nov 27, 2016 at 4:22 PM, András Kovács <kovacsahun at hotmail.com>
wrote:

> 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.
>

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.

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).
>

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 "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])".

/ Ulf

[1]
https://github.com/agda/agda/blob/509d481/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
[2]
https://github.com/agda/agda/blob/509d481/src/full/Agda/TypeChecking/MetaVars.hs#L683
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161128/db31fa06/attachment.html