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

[Ulf Norell]

The more fundamental problem here is that it does actually matter which
solution we
pick when they aren't definitionally equal, even in the case when they are
provable equal.
It might well be the case that picking `q` is the right choice and picking
`z≤s` is wrong and
doing so would result in a type error further down in the code.

/ Ulf

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

> I do not know.
>
> From a use case point of view, I would like to provide a proof that all
> construction of a type are equal.
>
> "∀ x y → (a : x ≤ y) → (b : x ≤ y) → a ≡ b" , and then use this proof to
> merge all solutions into one.
>
> Is this possible today ?
>
>
> On Thu, Jan 11, 2018 at 11:20 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
>
>> 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/56157934/attachment.html>