[Agda] Wildcards

[Guillaume Brunerie]

2012/3/25 Nils Anders Danielsson <nad at chalmers.se>:
> On 2012-03-25 19:33, Guillaume Brunerie wrote:
>>
>> My impression is that if you try to unify the types of [assoc] and
>> [big-assoc], you automatically find the three arguments of [assoc], so
>> I do not understand why the wildcards are not sufficient.
>
>
> You can ask Agda to display unsolved constraints (using a menu entry or
> C-c C-=). In your case:
>
>  [112] ((_89 p q r s ∘ _90 p q r s) ∘ _91 p q r s) = ((p ∘ q) ∘ (r ∘ s)) :
> .x ≡ .u
>  [112] (_89 p q r s ∘ (_90 p q r s ∘ _91 p q r s)) = (p ∘ (q ∘ (r ∘ s))) :
> .x ≡ .u
>  _92 := λ {.A} {.x} {.y} {.z} {.t} {.u} p q r s →
>    assoc (_89 p q r s) (_90 p q r s) (_91 p q r s) [blocked by problem 112]

But why Agda does not solve the constraints automatically?

It seems to me that Agda could try to simplify the first constraint to
(_89 p q r s ∘ _90 p q r s) = (p ∘ q)
_91 p q r s = (r ∘ s)

and then to
_89 p q r s = p
_90 p q r s = q
_91 p q r s = (r ∘ s)

which solves the first constraint, and then notice that the second is
also satisfied.

Is there a reason Agda does not do this?


Guillaume