[Agda] Why unification fail?

[Guillaume Allais]

Hi Serge,

The issue comes from the fact that this case forces Agda to consider
a problem of the form `f x =? c y` where `f` is a function and `c` a
constructor. For Agda to be able to solve this type of problem, it
would have to somehow invert `f`. Needless to say this is impossible
in the general case.

The typical solution to this kind of issue is to abstract over `f x`
at the same time as you are computing the indexed value which will
mention it. This way the unification problem is `fx =? c y` where `fx`
is a variable (the name you gave to the value `f x` corresponds to).
This vastly simpler unification problem can be easily solved by Agda.
And indeed the following works fine:

=======================================
  ⪾ : ℕ → 𝕃′ → 𝕃′
  ⪾ i l with ŋ l | compare i (ŋ l)
  ... | ŋl | less m k = {!   !}
  ... | ŋl | equal m = l
  ... | ŋl | greater m k = suc k ∷ l
=======================================

If you need Agda to remember the connection between the intermediate
result `ŋl` and the function call `ŋ l`, you can use the inspect idiom.
I have written a bit of doc for it two weeks ago:

https://github.com/agda/agda-stdlib/blob/8594b26dd817ffbf9024310521c9e79d9f199603/README/Inspect.agda

Cheers,
--
gallais



On 06/03/2019 19:22, Serge Leblanc wrote:
> Hi every,
> 
> Would anyone please tell me why the unification fails in the following
> example and what I do to succeed?
> 
> Thank you for your help.
> 
> Saluton ĉiun,
> 
> Ĉu iu bonvolus indiki al mi la kialon pro la unuiĝo fiaskas en la sekva
> ekzemplo kaj kion mi faru por sukcesi? 
> 
> Sinceran dankon pro via helpo.
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>