[Agda] what is happening here?

[Nils Anders Danielsson]

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