[Agda] what is happening here?

[Roman]

Hi Thorsten,

I think you're confused by the fact that Agda eagerly binds implicits.
If I tweak your definitions a bit

    record isMonoid {A : Set}(e : A)(_•_ : A → A → A) : Set where
      field
        <...>
        assoc : ⊤ -> {x y z : A} → (x • y) • z ≡ x • (y • z)

    assoc+ : ⊤ -> {l m n : ℕ} → (l + m) + n ≡ l + (m + n)

    +isMonoid : isMonoid zero _+_
    +isMonoid = record {
      lneutr = lneutr+ ;
      rneutr = rneutr+ ;
      assoc = assoc+ }

then Agda happily accepts the code.

The reason for that is that Agda elaborates your original example

    assoc = assoc+

to

    assoc {x} {y} {z} = assoc+ {_} {_} {_}

and then Agda is unable to solve the wildcard metavariables.

In my code above I introduce an explicit argument before the implicit
ones, which prevents Agda from binding implicits eagerly, which makes
the whole thing work as you'd expect.

2020-03-09 18:22 GMT+03:00, Nils Anders Danielsson <nad at cse.gu.se>:
> On 2020-03-08 22:48, Thorsten Altenkirch wrote:
>> Ok, but shouldn’t it always work if there is a trivial solution, i.e.
>> the goal matches given exactly (i.e. upto alpha conversion)?
>
> I don't think we should solve meta-variables unless there is a most
> general solution. This criterion ensures that if a reader of the code
> finds one way to solve the meta-variables, and the meta-variables are
> solved by Agda, then the solution found by the reader matches the one
> found by Agda (in the case of a non-unique most general solution the
> reader's solution might be more specific). I want it to be possible to
> read code without knowing the details of the unification algorithm.
>
> --
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>