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

[Apostolis Xekoukoulotakis]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180111/729a2c0c/attachment.html>