[Agda] Instance arguments and types who have a unique construction.

[Ulf Norell]

Instance search does check solutions for *definitional* equality. The
problem in your case is that `q` is only propositionally (provably) equal
to `z≤n`. I think it's a bit too much to ask of instance search that it
would look for proofs that two candidate solutions are equal.

Did you have a particular suggestion for what kind of smartness improvement
would make this work?

/ Ulf

On Thu, Jan 11, 2018 at 10:03 AM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> Currently, instance resolution tries all possible ways to construct an
> instance argument.
>
> It will look for arguments in the environment and it will use instance
> functions to create new ones. If there are multiple solutions, instance
> resolution will fail.
>
> example :
>
> Assuming we have defined "less than" as instance.
>
> if we have in the context, a variable q with type zero ≤ (suc zero) ,
> instance resolution will fail because there are two solutions, q and z≤n.
>
> But q is in fact z≤n.
>
>
> We can prove that there is only one possible construction of the type,
> thus any variables with the same type are the same.
>
> At the moment, I am trying to prune my context but it would be nice if
> instance resolution was a bit smarter.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180111/4ab2dd25/attachment.html>